let O be set ; for G being strict GroupWithOperators of O
for N being strict normal StableSubgroup of G
for H being strict StableSubgroup of G ./. N st the carrier of N = (nat_hom N) " the carrier of H holds
H = (1). (G ./. N)
let G be strict GroupWithOperators of O; for N being strict normal StableSubgroup of G
for H being strict StableSubgroup of G ./. N st the carrier of N = (nat_hom N) " the carrier of H holds
H = (1). (G ./. N)
let N be strict normal StableSubgroup of G; for H being strict StableSubgroup of G ./. N st the carrier of N = (nat_hom N) " the carrier of H holds
H = (1). (G ./. N)
reconsider N9 = multMagma(# the carrier of N, the multF of N #) as strict normal Subgroup of G by Lm6;
let H be strict StableSubgroup of G ./. N; ( the carrier of N = (nat_hom N) " the carrier of H implies H = (1). (G ./. N) )
reconsider H9 = multMagma(# the carrier of H, the multF of H #) as strict Subgroup of G ./. N by Lm15;
A1:
( the carrier of H9 c= the carrier of (G ./. N) & the multF of H9 = the multF of (G ./. N) || the carrier of H9 )
by GROUP_2:def 5;
( the carrier of (G ./. N) = the carrier of (G ./. N9) & the multF of (G ./. N) = the multF of (G ./. N9) )
by Def14, Def15;
then reconsider H9 = H9 as strict Subgroup of G ./. N9 by A1, GROUP_2:def 5;
assume
the carrier of N = (nat_hom N) " the carrier of H
; H = (1). (G ./. N)
then A2:
the carrier of N9 = (nat_hom N9) " the carrier of H9
by Def20;
assume
not H = (1). (G ./. N)
; contradiction
then
not the carrier of H = {(1_ (G ./. N))}
by Def8;
then consider h being object such that
A3:
( ( h in the carrier of H & not h in {(1_ (G ./. N))} ) or ( h in {(1_ (G ./. N))} & not h in the carrier of H ) )
by TARSKI:2;
per cases
( ( h in the carrier of H & not h in {(1_ (G ./. N))} ) or ( not h in the carrier of H & h in {(1_ (G ./. N))} ) )
by A3;
suppose A4:
(
h in the
carrier of
H & not
h in {(1_ (G ./. N))} )
;
contradictionthen
{h} c= the
carrier of
H
by ZFMISC_1:31;
then A5:
(nat_hom N9) " {h} c= the
carrier of
N9
by A2, RELAT_1:143;
A6:
rng (nat_hom N9) =
the
carrier of
(Image (nat_hom N9))
by GROUP_6:44
.=
the
carrier of
(G ./. N9)
by GROUP_6:48
;
the
carrier of
H9 c= the
carrier of
(G ./. N9)
by GROUP_2:def 5;
then consider x being
object such that A7:
x in dom (nat_hom N9)
and A8:
(nat_hom N9) . x = h
by A4, A6, FUNCT_1:def 3;
(nat_hom N9) . x in {h}
by A8, TARSKI:def 1;
then
x in (nat_hom N9) " {h}
by A7, FUNCT_1:def 7;
then A9:
x in N9
by A5, STRUCT_0:def 5;
h <> 1_ (G ./. N)
by A4, TARSKI:def 1;
then A10:
h <> carr N
by Th43;
reconsider x =
x as
Element of
G by A7;
x * N9 = h
by A8, GROUP_6:def 8;
hence
contradiction
by A10, A9, GROUP_2:113;
verum end;