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

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

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

now :: thesis: for a being Element of G holds [.N1,N2.] |^ a is Subgroup of [.N1,N2.]

hence
[.N1,N2.] is normal Subgroup of G
by GROUP_3:122; :: thesis: verumlet a be Element of G; :: thesis: [.N1,N2.] |^ a is Subgroup of [.N1,N2.]

end;now :: thesis: for b being Element of G st b in [.N1,N2.] |^ a holds

b in [.N1,N2.]

hence
[.N1,N2.] |^ a is Subgroup of [.N1,N2.]
by GROUP_2:58; :: thesis: verumb in [.N1,N2.]

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

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

then consider c being Element of G such that

A1: b = c |^ a and

A2: c in [.N1,N2.] by GROUP_3:58;

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

A3: len F = len I and

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

A5: c = Product (F |^ I) by A2, GROUP_4:28;

A6: len (F |^ a) = len F by Def1;

A7: rng (F |^ a) c= commutators ((carr N1),(carr N2))

.= Product ((F |^ a) |^ I) by Th15 ;

hence b in [.N1,N2.] by A3, A6, A7, GROUP_4:28; :: thesis: verum

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

then consider c being Element of G such that

A1: b = c |^ a and

A2: c in [.N1,N2.] by GROUP_3:58;

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

A3: len F = len I and

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

A5: c = Product (F |^ I) by A2, GROUP_4:28;

A6: len (F |^ a) = len F by Def1;

A7: rng (F |^ a) c= commutators ((carr N1),(carr N2))

proof

b =
Product ((F |^ I) |^ a)
by A1, A5, Th14
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng (F |^ a) or x in commutators ((carr N1),(carr N2)) )

assume x in rng (F |^ a) ; :: thesis: x in commutators ((carr N1),(carr N2))

then consider y being object such that

A8: y in dom (F |^ a) and

A9: (F |^ a) . y = x by FUNCT_1:def 3;

reconsider y = y as Element of NAT by A8;

A10: y in dom F by A6, A8, FINSEQ_3:29;

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

y in dom F by A6, A8, FINSEQ_3:29;

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

then consider d, e being Element of G such that

A12: F . y = [.d,e.] and

A13: d in carr N1 and

A14: e in carr N2 by A4, Th47;

d in N1 by A13, STRUCT_0:def 5;

then d |^ a in N1 |^ a by GROUP_3:58;

then d |^ a in N1 by GROUP_3:def 13;

then A15: d |^ a in carr N1 by STRUCT_0:def 5;

e in N2 by A14, STRUCT_0:def 5;

then e |^ a in N2 |^ a by GROUP_3:58;

then e |^ a in N2 by GROUP_3:def 13;

then A16: e |^ a in carr N2 by STRUCT_0:def 5;

x = (F /. y) |^ a by A9, A10, Def1;

then x = [.(d |^ a),(e |^ a).] by A12, A11, Th23;

hence x in commutators ((carr N1),(carr N2)) by A15, A16; :: thesis: verum

end;assume x in rng (F |^ a) ; :: thesis: x in commutators ((carr N1),(carr N2))

then consider y being object such that

A8: y in dom (F |^ a) and

A9: (F |^ a) . y = x by FUNCT_1:def 3;

reconsider y = y as Element of NAT by A8;

A10: y in dom F by A6, A8, FINSEQ_3:29;

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

y in dom F by A6, A8, FINSEQ_3:29;

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

then consider d, e being Element of G such that

A12: F . y = [.d,e.] and

A13: d in carr N1 and

A14: e in carr N2 by A4, Th47;

d in N1 by A13, STRUCT_0:def 5;

then d |^ a in N1 |^ a by GROUP_3:58;

then d |^ a in N1 by GROUP_3:def 13;

then A15: d |^ a in carr N1 by STRUCT_0:def 5;

e in N2 by A14, STRUCT_0:def 5;

then e |^ a in N2 |^ a by GROUP_3:58;

then e |^ a in N2 by GROUP_3:def 13;

then A16: e |^ a in carr N2 by STRUCT_0:def 5;

x = (F /. y) |^ a by A9, A10, Def1;

then x = [.(d |^ a),(e |^ a).] by A12, A11, Th23;

hence x in commutators ((carr N1),(carr N2)) by A15, A16; :: thesis: verum

.= Product ((F |^ a) |^ I) by Th15 ;

hence b in [.N1,N2.] by A3, A6, A7, GROUP_4:28; :: thesis: verum