let G be Group; 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; 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
let x be
Element of
G;
x * M c= M * xlet y be
object ;
TARSKI:def 3 ( not y in x * M or y in M * x )
assume A2:
y in x * M
;
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;
verum
end;
then
M is normal Subgroup of G
by GROUP_3:118;
hence
ex M being strict normal Subgroup of G st the carrier of M = N ~ H
by A1; verum