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;

commutators ((N1 "\/" N2),N3) c= [.N1,N3.] * [.N2,N3.]

then [.(N1 "\/" N2),N3.] is Subgroup of [.N1,N3.] "\/" [.N2,N3.] by GROUP_4:50;

hence [.(N1 "\/" N2),N3.] = [.N1,N3.] "\/" [.N2,N3.] by A17, GROUP_2:55; :: thesis: verum

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.]

then A17:
[.N1,N3.] "\/" [.N2,N3.] is Subgroup of [.(N1 "\/" N2),N3.]
by GROUP_2:58;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 A3, Th56;

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 A6, Th61;

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 A7, Th61;

A14: len (F1 ^ F2) = (len I1) + (len I2) by A8, A11, FINSEQ_1:22

.= 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 A9, A12, XBOOLE_1:13;

N1 is Subgroup of N1 "\/" N2 by GROUP_4:60;

then commutators (N1,N3) c= commutators ((N1 "\/" N2),N3) by A3, Th56;

then (commutators (N1,N3)) \/ (commutators (N2,N3)) c= commutators ((N1 "\/" N2),N3) by A4, XBOOLE_1:8;

then A16: rng (F1 ^ F2) c= commutators ((N1 "\/" N2),N3) by A15;

Product ((F1 ^ F2) |^ (I1 ^ I2)) = Product ((F1 |^ I1) ^ (F2 |^ I2)) by A8, A11, GROUP_4:19

.= a by A5, A10, A13, GROUP_4:5 ;

hence a in [.(N1 "\/" N2),N3.] by A16, A14, Th61; :: thesis: verum

end;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 A3, Th56;

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 A6, Th61;

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 A7, Th61;

A14: len (F1 ^ F2) = (len I1) + (len I2) by A8, A11, FINSEQ_1:22

.= 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 A9, A12, XBOOLE_1:13;

N1 is Subgroup of N1 "\/" N2 by GROUP_4:60;

then commutators (N1,N3) c= commutators ((N1 "\/" N2),N3) by A3, Th56;

then (commutators (N1,N3)) \/ (commutators (N2,N3)) c= commutators ((N1 "\/" N2),N3) by A4, XBOOLE_1:8;

then A16: rng (F1 ^ F2) c= commutators ((N1 "\/" N2),N3) by A15;

Product ((F1 ^ F2) |^ (I1 ^ I2)) = Product ((F1 |^ I1) ^ (F2 |^ I2)) by A8, A11, GROUP_4:19

.= a by A5, A10, A13, GROUP_4:5 ;

hence a in [.(N1 "\/" N2),N3.] by A16, A14, Th61; :: thesis: verum

commutators ((N1 "\/" N2),N3) c= [.N1,N3.] * [.N2,N3.]

proof

then
gr (commutators ((N1 "\/" N2),N3)) is Subgroup of gr ([.N1,N3.] * [.N2,N3.])
by GROUP_4:32;
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 A19, Th7;

[.c,b.] in [.N1,N3.] by A20, A22, Th65;

then [.c,b.] |^ d in [.N1,N3.] |^ d by GROUP_3:58;

then A24: [.c,b.] |^ d in [.N1,N3.] by A1, GROUP_3:def 13;

( 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 A24, Th4; :: thesis: verum

end;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 A19, Th7;

[.c,b.] in [.N1,N3.] by A20, A22, Th65;

then [.c,b.] |^ d in [.N1,N3.] |^ d by GROUP_3:58;

then A24: [.c,b.] |^ d in [.N1,N3.] by A1, GROUP_3:def 13;

( 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 A24, Th4; :: thesis: verum

then [.(N1 "\/" N2),N3.] is Subgroup of [.N1,N3.] "\/" [.N2,N3.] by GROUP_4:50;

hence [.(N1 "\/" N2),N3.] = [.N1,N3.] "\/" [.N2,N3.] by A17, GROUP_2:55; :: thesis: verum