let G be Group; 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; [.(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 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;
( 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.]
;
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;
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 ;
TARSKI:def 3 ( not x in commutators ((N1 "\/" N2),N3) or x in [.N1,N3.] * [.N2,N3.] )
assume
x in commutators (
(N1 "\/" N2),
N3)
;
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;
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 A17, GROUP_2:55; verum