let G be Group; :: thesis: for H, N being normal Subgroup of G ex M being strict normal Subgroup of G st the carrier of M = N ~ H

let H, N be normal Subgroup of G; :: thesis: ex M being strict normal Subgroup of G st the carrier of M = N ~ H

consider M being strict Subgroup of G such that

A1: the carrier of M = N ~ H by Th71;

for x being Element of G holds x * M c= M * x

hence ex M being strict normal Subgroup of G st the carrier of M = N ~ H by A1; :: thesis: verum

let H, N be normal Subgroup of G; :: thesis: ex M being strict normal Subgroup of G st the carrier of M = N ~ H

consider M being strict Subgroup of G such that

A1: the carrier of M = N ~ H by Th71;

for x being Element of G holds x * M c= M * x

proof

then
M is normal Subgroup of G
by GROUP_3:118;
let x be Element of G; :: thesis: x * M c= M * x

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in x * M or y in M * x )

assume A2: y in x * M ; :: thesis: y in M * x

then reconsider y = y as Element of G ;

consider z being Element of G such that

A3: ( y = x * z & z in M ) by A2, GROUP_2:103;

z in the carrier of M by A3, STRUCT_0:def 5;

then consider z9 being Element of G such that

A4: ( z9 in z * N & z9 in H ) by Th3, A1, Th51;

(x * z9) * (x ") in H by A4, Th4;

then A5: (x * z9) * (x ") in carr H by STRUCT_0:def 5;

A6: (x * z9) * (x ") in (x * (z * N)) * (x ") by A4, GROUP_8:15;

(x * (z * N)) * (x ") = x * ((z * N) * (x ")) by GROUP_2:33

.= x * (z * (N * (x "))) by GROUP_2:33

.= x * (z * ((x ") * N)) by GROUP_3:117

.= x * ((z * (x ")) * N) by GROUP_2:32

.= (x * (z * (x "))) * N by GROUP_2:32

.= ((x * z) * (x ")) * N by GROUP_1:def 3 ;

then ((x * z) * (x ")) * N meets carr H by A5, A6, XBOOLE_0:3;

then (x * z) * (x ") in N ~ H ;

then A7: (x * z) * (x ") in M by A1, STRUCT_0:def 5;

((x * z) * (x ")) * x = y by A3, GROUP_3:1;

hence y in M * x by A7, GROUP_2:104; :: thesis: verum

end;let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in x * M or y in M * x )

assume A2: y in x * M ; :: thesis: y in M * x

then reconsider y = y as Element of G ;

consider z being Element of G such that

A3: ( y = x * z & z in M ) by A2, GROUP_2:103;

z in the carrier of M by A3, STRUCT_0:def 5;

then consider z9 being Element of G such that

A4: ( z9 in z * N & z9 in H ) by Th3, A1, Th51;

(x * z9) * (x ") in H by A4, Th4;

then A5: (x * z9) * (x ") in carr H by STRUCT_0:def 5;

A6: (x * z9) * (x ") in (x * (z * N)) * (x ") by A4, GROUP_8:15;

(x * (z * N)) * (x ") = x * ((z * N) * (x ")) by GROUP_2:33

.= x * (z * (N * (x "))) by GROUP_2:33

.= x * (z * ((x ") * N)) by GROUP_3:117

.= x * ((z * (x ")) * N) by GROUP_2:32

.= (x * (z * (x "))) * N by GROUP_2:32

.= ((x * z) * (x ")) * N by GROUP_1:def 3 ;

then ((x * z) * (x ")) * N meets carr H by A5, A6, XBOOLE_0:3;

then (x * z) * (x ") in N ~ H ;

then A7: (x * z) * (x ") in M by A1, STRUCT_0:def 5;

((x * z) * (x ")) * x = y by A3, GROUP_3:1;

hence y in M * x by A7, GROUP_2:104; :: thesis: verum

hence ex M being strict normal Subgroup of G st the carrier of M = N ~ H by A1; :: thesis: verum