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