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 N' = multMagma(# the carrier of N,the multF of N #) as strict normal Subgroup of G by Lm7;
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 H' = multMagma(# the carrier of H,the multF of H #) as strict Subgroup of G ./. N by Lm16;
A1:
( the carrier of H' c= the carrier of (G ./. N) & the multF of H' = the multF of (G ./. N) || the carrier of H' )
by GROUP_2:def 5;
( the carrier of (G ./. N) = the carrier of (G ./. N') & the multF of (G ./. N) = the multF of (G ./. N') )
by Def14, Def15;
then reconsider H' = H' as strict Subgroup of G ./. N' 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 N' = (nat_hom N') " the carrier of H'
by Def23;
assume
not H = (1). (G ./. N)
; contradiction
then
not the carrier of H = {(1_ (G ./. N))}
by Def8;
then consider h being set 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:37;
then A5:
(nat_hom N') " {h} c= the
carrier of
N'
by A2, RELAT_1:178;
A6:
rng (nat_hom N') =
the
carrier of
(Image (nat_hom N'))
by GROUP_6:53
.=
the
carrier of
(G ./. N')
by GROUP_6:57
;
the
carrier of
H' c= the
carrier of
(G ./. N')
by GROUP_2:def 5;
then consider x being
set such that A7:
x in dom (nat_hom N')
and A8:
(nat_hom N') . x = h
by A4, A6, FUNCT_1:def 5;
(nat_hom N') . x in {h}
by A8, TARSKI:def 1;
then
x in (nat_hom N') " {h}
by A7, FUNCT_1:def 13;
then A9:
x in N'
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
by A7;
x * N' = h
by A8, GROUP_6:def 9;
hence
contradiction
by A10, A9, GROUP_2:136;
verum end;