let G be Group; :: thesis: for N1, N2 being normal Subgroup of G holds [.N1,N2.] is Subgroup of [.N2,N1.]

let N1, N2 be normal Subgroup of G; :: thesis: [.N1,N2.] is Subgroup of [.N2,N1.]

let N1, N2 be normal Subgroup of G; :: thesis: [.N1,N2.] is Subgroup of [.N2,N1.]

now :: thesis: for a being Element of G st a in [.N1,N2.] holds

a in [.N2,N1.]

hence
[.N1,N2.] is Subgroup of [.N2,N1.]
by GROUP_2:58; :: thesis: veruma in [.N2,N1.]

let a be Element of G; :: thesis: ( a in [.N1,N2.] implies a in [.N2,N1.] )

assume a in [.N1,N2.] ; :: thesis: a in [.N2,N1.]

then consider F being FinSequence of the carrier of G, I being FinSequence of INT such that

len F = len I and

A1: rng F c= commutators (N1,N2) and

A2: a = Product (F |^ I) by Th61;

deffunc H_{1}( Nat) -> Element of the carrier of G = (F /. $1) " ;

consider F1 being FinSequence of the carrier of G such that

A3: len F1 = len F and

A4: for k being Nat st k in dom F1 holds

F1 . k = H_{1}(k)
from FINSEQ_2:sch 1();

A5: dom F = Seg (len F) by FINSEQ_1:def 3;

A6: rng F1 c= commutators (N2,N1)

then A13: dom (F |^ I) = Seg (len F) by FINSEQ_1:def 3;

deffunc H_{2}( Nat) -> Element of INT = @ (- (@ (I /. $1)));

consider I1 being FinSequence of INT such that

A14: len I1 = len F and

A15: for k being Nat st k in dom I1 holds

I1 . k = H_{2}(k)
from FINSEQ_2:sch 1();

set J = F1 |^ I1;

A16: dom F1 = dom F by A3, FINSEQ_3:29;

A17: dom I1 = dom F by A14, FINSEQ_3:29;

then F1 |^ I1 = F |^ I by A12, A18, FINSEQ_2:9;

hence a in [.N2,N1.] by A2, A3, A14, A6, Th61; :: thesis: verum

end;assume a in [.N1,N2.] ; :: thesis: a in [.N2,N1.]

then consider F being FinSequence of the carrier of G, I being FinSequence of INT such that

len F = len I and

A1: rng F c= commutators (N1,N2) and

A2: a = Product (F |^ I) by Th61;

deffunc H

consider F1 being FinSequence of the carrier of G such that

A3: len F1 = len F and

A4: for k being Nat st k in dom F1 holds

F1 . k = H

A5: dom F = Seg (len F) by FINSEQ_1:def 3;

A6: rng F1 c= commutators (N2,N1)

proof

A12:
len (F |^ I) = len F
by GROUP_4:def 3;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng F1 or x in commutators (N2,N1) )

assume x in rng F1 ; :: thesis: x in commutators (N2,N1)

then consider y being object such that

A7: y in dom F1 and

A8: F1 . y = x by FUNCT_1:def 3;

reconsider y = y as Element of NAT by A7;

y in dom F by A3, A7, FINSEQ_3:29;

then A9: F /. y = F . y by PARTFUN1:def 6;

y in dom F by A3, A7, FINSEQ_3:29;

then F . y in rng F by FUNCT_1:def 3;

then consider b, c being Element of G such that

A10: F . y = [.b,c.] and

A11: ( b in N1 & c in N2 ) by A1, Th52;

x = (F /. y) " by A4, A7, A8;

then x = [.c,b.] by A10, A9, Th22;

hence x in commutators (N2,N1) by A11, Th52; :: thesis: verum

end;assume x in rng F1 ; :: thesis: x in commutators (N2,N1)

then consider y being object such that

A7: y in dom F1 and

A8: F1 . y = x by FUNCT_1:def 3;

reconsider y = y as Element of NAT by A7;

y in dom F by A3, A7, FINSEQ_3:29;

then A9: F /. y = F . y by PARTFUN1:def 6;

y in dom F by A3, A7, FINSEQ_3:29;

then F . y in rng F by FUNCT_1:def 3;

then consider b, c being Element of G such that

A10: F . y = [.b,c.] and

A11: ( b in N1 & c in N2 ) by A1, Th52;

x = (F /. y) " by A4, A7, A8;

then x = [.c,b.] by A10, A9, Th22;

hence x in commutators (N2,N1) by A11, Th52; :: thesis: verum

then A13: dom (F |^ I) = Seg (len F) by FINSEQ_1:def 3;

deffunc H

consider I1 being FinSequence of INT such that

A14: len I1 = len F and

A15: for k being Nat st k in dom I1 holds

I1 . k = H

set J = F1 |^ I1;

A16: dom F1 = dom F by A3, FINSEQ_3:29;

A17: dom I1 = dom F by A14, FINSEQ_3:29;

A18: now :: thesis: for k being Nat st k in dom (F |^ I) holds

(F |^ I) . k = (F1 |^ I1) . k

len (F1 |^ I1) = len F
by A3, GROUP_4:def 3;(F |^ I) . k = (F1 |^ I1) . k

let k be Nat; :: thesis: ( k in dom (F |^ I) implies (F |^ I) . k = (F1 |^ I1) . k )

assume A19: k in dom (F |^ I) ; :: thesis: (F |^ I) . k = (F1 |^ I1) . k

then A20: k in dom F by A13, FINSEQ_1:def 3;

A21: ( (F1 |^ I1) . k = (F1 /. k) |^ (@ (I1 /. k)) & F1 /. k = F1 . k ) by A5, A16, A13, A19, GROUP_4:def 3, PARTFUN1:def 6;

A22: I1 . k = @ (- (@ (I /. k))) by A15, A5, A17, A13, A19;

( F1 . k = (F /. k) " & I1 . k = I1 /. k ) by A4, A5, A16, A17, A13, A19, PARTFUN1:def 6;

then (F1 |^ I1) . k = (((F /. k) ") |^ (@ (I /. k))) " by A21, A22, GROUP_1:36

.= (((F /. k) |^ (@ (I /. k))) ") " by GROUP_1:37

.= (F /. k) |^ (@ (I /. k)) ;

hence (F |^ I) . k = (F1 |^ I1) . k by A20, GROUP_4:def 3; :: thesis: verum

end;assume A19: k in dom (F |^ I) ; :: thesis: (F |^ I) . k = (F1 |^ I1) . k

then A20: k in dom F by A13, FINSEQ_1:def 3;

A21: ( (F1 |^ I1) . k = (F1 /. k) |^ (@ (I1 /. k)) & F1 /. k = F1 . k ) by A5, A16, A13, A19, GROUP_4:def 3, PARTFUN1:def 6;

A22: I1 . k = @ (- (@ (I /. k))) by A15, A5, A17, A13, A19;

( F1 . k = (F /. k) " & I1 . k = I1 /. k ) by A4, A5, A16, A17, A13, A19, PARTFUN1:def 6;

then (F1 |^ I1) . k = (((F /. k) ") |^ (@ (I /. k))) " by A21, A22, GROUP_1:36

.= (((F /. k) |^ (@ (I /. k))) ") " by GROUP_1:37

.= (F /. k) |^ (@ (I /. k)) ;

hence (F |^ I) . k = (F1 |^ I1) . k by A20, GROUP_4:def 3; :: thesis: verum

then F1 |^ I1 = F |^ I by A12, A18, FINSEQ_2:9;

hence a in [.N2,N1.] by A2, A3, A14, A6, Th61; :: thesis: verum