let G be Group; :: thesis: for N1, N2, N3 being strict normal Subgroup of G holds [.(N1 "\/" N2),N3.] = [.N1,N3.] "\/" [.N2,N3.]
let N1, N2, N3 be strict normal Subgroup of G; :: thesis: [.(N1 "\/" N2),N3.] = [.N1,N3.] "\/" [.N2,N3.]
A1: [.N1,N3.] is normal Subgroup of G by Th68;
A2: [.N2,N3.] is normal Subgroup of G by Th68;
now :: thesis: for a being Element of G st a in [.N1,N3.] "\/" [.N2,N3.] holds
a in [.(N1 "\/" N2),N3.]
let a be Element of G; :: thesis: ( a in [.N1,N3.] "\/" [.N2,N3.] implies a in [.(N1 "\/" N2),N3.] )
A3: N3 is Subgroup of N3 by GROUP_2:54;
N2 is Subgroup of N1 "\/" N2 by GROUP_4:60;
then A4: commutators (N2,N3) c= commutators ((N1 "\/" N2),N3) by ;
assume a in [.N1,N3.] "\/" [.N2,N3.] ; :: thesis: a in [.(N1 "\/" N2),N3.]
then consider b, c being Element of G such that
A5: a = b * c and
A6: b in [.N1,N3.] and
A7: c in [.N2,N3.] by A1, A2, Th7;
consider F1 being FinSequence of the carrier of G, I1 being FinSequence of INT such that
A8: len F1 = len I1 and
A9: rng F1 c= commutators (N1,N3) and
A10: b = Product (F1 |^ I1) by ;
consider F2 being FinSequence of the carrier of G, I2 being FinSequence of INT such that
A11: len F2 = len I2 and
A12: rng F2 c= commutators (N2,N3) and
A13: c = Product (F2 |^ I2) by ;
A14: len (F1 ^ F2) = (len I1) + (len I2) by
.= len (I1 ^ I2) by FINSEQ_1:22 ;
rng (F1 ^ F2) = (rng F1) \/ (rng F2) by FINSEQ_1:31;
then A15: rng (F1 ^ F2) c= (commutators (N1,N3)) \/ (commutators (N2,N3)) by ;
N1 is Subgroup of N1 "\/" N2 by GROUP_4:60;
then commutators (N1,N3) c= commutators ((N1 "\/" N2),N3) by ;
then (commutators (N1,N3)) \/ (commutators (N2,N3)) c= commutators ((N1 "\/" N2),N3) by ;
then A16: rng (F1 ^ F2) c= commutators ((N1 "\/" N2),N3) by A15;
Product ((F1 ^ F2) |^ (I1 ^ I2)) = Product ((F1 |^ I1) ^ (F2 |^ I2)) by
.= a by ;
hence a in [.(N1 "\/" N2),N3.] by ; :: thesis: verum
end;
then A17: [.N1,N3.] "\/" [.N2,N3.] is Subgroup of [.(N1 "\/" N2),N3.] by GROUP_2:58;
commutators ((N1 "\/" N2),N3) c= [.N1,N3.] * [.N2,N3.]
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in commutators ((N1 "\/" N2),N3) or x in [.N1,N3.] * [.N2,N3.] )
assume x in commutators ((N1 "\/" N2),N3) ; :: thesis: x in [.N1,N3.] * [.N2,N3.]
then consider a, b being Element of G such that
A18: x = [.a,b.] and
A19: a in N1 "\/" N2 and
A20: b in N3 by Th52;
consider c, d being Element of G such that
A21: a = c * d and
A22: c in N1 and
A23: d in N2 by ;
[.c,b.] in [.N1,N3.] by ;
then [.c,b.] |^ d in [.N1,N3.] |^ d by GROUP_3:58;
then A24: [.c,b.] |^ d in [.N1,N3.] by ;
( x = ([.c,b.] |^ d) * [.d,b.] & [.d,b.] in [.N2,N3.] ) by A18, A20, A21, A23, Th25, Th65;
hence x in [.N1,N3.] * [.N2,N3.] by ; :: thesis: verum
end;
then gr (commutators ((N1 "\/" N2),N3)) is Subgroup of gr ([.N1,N3.] * [.N2,N3.]) by GROUP_4:32;
then [.(N1 "\/" N2),N3.] is Subgroup of [.N1,N3.] "\/" [.N2,N3.] by GROUP_4:50;
hence [.(N1 "\/" N2),N3.] = [.N1,N3.] "\/" [.N2,N3.] by ; :: thesis: verum