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.]
now :: thesis: for a being Element of G st a in [.N1,N2.] holds
a 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 H1( 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 = H1(k) from A5: dom F = Seg (len F) by FINSEQ_1:def 3;
A6: rng F1 c= commutators (N2,N1)
proof
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 ;
then A9: F /. y = F . y by PARTFUN1:def 6;
y in dom F by ;
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 ;
x = (F /. y) " by A4, A7, A8;
then x = [.c,b.] by ;
hence x in commutators (N2,N1) by ; :: thesis: verum
end;
A12: len (F |^ I) = len F by GROUP_4:def 3;
then A13: dom (F |^ I) = Seg (len F) by FINSEQ_1:def 3;
deffunc H2( 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 = H2(k) from set J = F1 |^ I1;
A16: dom F1 = dom F by ;
A17: dom I1 = dom F by ;
A18: now :: thesis: for k being Nat st k in dom (F |^ I) holds
(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 ;
A21: ( (F1 |^ I1) . k = (F1 /. k) |^ (@ (I1 /. k)) & F1 /. k = F1 . k ) by ;
A22: I1 . k = @ (- (@ (I /. k))) by A15, A5, A17, A13, A19;
( F1 . k = (F /. k) " & I1 . k = I1 /. k ) by ;
then (F1 |^ I1) . k = (((F /. k) ") |^ (@ (I /. k))) " by
.= (((F /. k) |^ (@ (I /. k))) ") " by GROUP_1:37
.= (F /. k) |^ (@ (I /. k)) ;
hence (F |^ I) . k = (F1 |^ I1) . k by ; :: thesis: verum
end;
len (F1 |^ I1) = len F by ;
then F1 |^ I1 = F |^ I by ;
hence a in [.N2,N1.] by A2, A3, A14, A6, Th61; :: thesis: verum
end;
hence [.N1,N2.] is Subgroup of [.N2,N1.] by GROUP_2:58; :: thesis: verum