let G be Group; :: thesis: for N1, N2 being strict normal Subgroup of G ex M being strict Subgroup of G st the carrier of M = N1 * N2

let N1, N2 be strict normal Subgroup of G; :: thesis: ex M being strict Subgroup of G st the carrier of M = N1 * N2

A1: 1_ G in N1 * N2

x * y in N1 * N2

x " in N1 * N2

let N1, N2 be strict normal Subgroup of G; :: thesis: ex M being strict Subgroup of G st the carrier of M = N1 * N2

A1: 1_ G in N1 * N2

proof

A3:
for x, y being Element of G st x in N1 * N2 & y in N1 * N2 holds
A2:
( 1_ G in N1 & 1_ G in N2 )
by GROUP_2:46;

(1_ G) * (1_ G) = 1_ G by GROUP_1:def 4;

hence 1_ G in N1 * N2 by A2, Th6; :: thesis: verum

end;(1_ G) * (1_ G) = 1_ G by GROUP_1:def 4;

hence 1_ G in N1 * N2 by A2, Th6; :: thesis: verum

x * y in N1 * N2

proof

for x being Element of G st x in N1 * N2 holds
let x, y be Element of G; :: thesis: ( x in N1 * N2 & y in N1 * N2 implies x * y in N1 * N2 )

assume that

A4: x in N1 * N2 and

A5: y in N1 * N2 ; :: thesis: x * y in N1 * N2

consider a, b being Element of G such that

A6: ( x = a * b & a in N1 & b in N2 ) by A4, Th6;

consider c, d being Element of G such that

A7: ( y = c * d & c in N1 & d in N2 ) by A5, Th6;

A8: x * y = ((a * b) * c) * d by A6, A7, GROUP_1:def 3

.= (a * (b * c)) * d by GROUP_1:def 3 ;

b * c in N2 * N1 by A6, A7, Th6;

then b * c in N1 * N2 by GROUP_3:125;

then consider b9, c9 being Element of G such that

A9: ( b * c = b9 * c9 & b9 in N1 & c9 in N2 ) by Th6;

A10: x * y = ((a * b9) * c9) * d by A8, A9, GROUP_1:def 3

.= (a * b9) * (c9 * d) by GROUP_1:def 3 ;

A11: a * b9 in N1 by A6, A9, GROUP_2:50;

c9 * d in N2 by A7, A9, GROUP_2:50;

hence x * y in N1 * N2 by A10, A11, Th6; :: thesis: verum

end;assume that

A4: x in N1 * N2 and

A5: y in N1 * N2 ; :: thesis: x * y in N1 * N2

consider a, b being Element of G such that

A6: ( x = a * b & a in N1 & b in N2 ) by A4, Th6;

consider c, d being Element of G such that

A7: ( y = c * d & c in N1 & d in N2 ) by A5, Th6;

A8: x * y = ((a * b) * c) * d by A6, A7, GROUP_1:def 3

.= (a * (b * c)) * d by GROUP_1:def 3 ;

b * c in N2 * N1 by A6, A7, Th6;

then b * c in N1 * N2 by GROUP_3:125;

then consider b9, c9 being Element of G such that

A9: ( b * c = b9 * c9 & b9 in N1 & c9 in N2 ) by Th6;

A10: x * y = ((a * b9) * c9) * d by A8, A9, GROUP_1:def 3

.= (a * b9) * (c9 * d) by GROUP_1:def 3 ;

A11: a * b9 in N1 by A6, A9, GROUP_2:50;

c9 * d in N2 by A7, A9, GROUP_2:50;

hence x * y in N1 * N2 by A10, A11, Th6; :: thesis: verum

x " in N1 * N2

proof

hence
ex M being strict Subgroup of G st the carrier of M = N1 * N2
by A1, A3, GROUP_2:52; :: thesis: verum
let x be Element of G; :: thesis: ( x in N1 * N2 implies x " in N1 * N2 )

assume x in N1 * N2 ; :: thesis: x " in N1 * N2

then consider a, b being Element of G such that

A12: ( x = a * b & a in N1 & b in N2 ) by Th6;

A13: x " = (b ") * (a ") by A12, GROUP_1:17;

( b " in N2 & a " in N1 ) by A12, GROUP_2:51;

then x " in N2 * N1 by A13, Th6;

hence x " in N1 * N2 by GROUP_3:125; :: thesis: verum

end;assume x in N1 * N2 ; :: thesis: x " in N1 * N2

then consider a, b being Element of G such that

A12: ( x = a * b & a in N1 & b in N2 ) by Th6;

A13: x " = (b ") * (a ") by A12, GROUP_1:17;

( b " in N2 & a " in N1 ) by A12, GROUP_2:51;

then x " in N2 * N1 by A13, Th6;

hence x " in N1 * N2 by GROUP_3:125; :: thesis: verum