let G be non trivial Group; for H being strict Subgroup of G
for phi being Automorphism of G st H is maximal holds
Image (phi | H) is maximal
let H be strict Subgroup of G; for phi being Automorphism of G st H is maximal holds
Image (phi | H) is maximal
let phi be Automorphism of G; ( H is maximal implies Image (phi | H) is maximal )
assume A1:
H is maximal
; Image (phi | H) is maximal
A2:
Image (phi | H) is proper Subgroup of G
by A1, Th23;
set UG = the carrier of G;
set UH = the carrier of H;
for K being strict Subgroup of G st Image (phi | H) <> K & Image (phi | H) is Subgroup of K holds
K = multMagma(# the carrier of G, the multF of G #)
proof
let K be
strict Subgroup of
G;
( Image (phi | H) <> K & Image (phi | H) is Subgroup of K implies K = multMagma(# the carrier of G, the multF of G #) )
assume B1:
Image (phi | H) <> K
;
( not Image (phi | H) is Subgroup of K or K = multMagma(# the carrier of G, the multF of G #) )
assume B2:
Image (phi | H) is
Subgroup of
K
;
K = multMagma(# the carrier of G, the multF of G #)
then consider psi being
Automorphism of
G such that B3:
psi = phi "
and B4:
H is
Subgroup of
Image (psi | K)
by Th18;
set UK = the
carrier of
K;
reconsider K =
K as non
trivial strict Subgroup of
G by A2, B1, B2, Th12;
not the
carrier of
K \ the
carrier of
(Image (phi | H)) is
empty
by B1, B2, Def1, Th11;
then consider k being
object such that B6:
k in the
carrier of
K \ the
carrier of
(Image (phi | H))
by XBOOLE_0:def 1;
reconsider k =
k as
Element of
K by B6;
set L =
Image (psi | K);
B8:
psi . k in Image (psi | K)
B9:
multMagma(# the
carrier of
H, the
multF of
H #)
<> Image (psi | K)
proof
set UPH = the
carrier of
(Image (phi | H));
C1:
(
phi is
one-to-one &
phi is
onto & the
carrier of
(Image (phi | H)) is non
empty Subset of the
carrier of
G &
phi is
Function of the
carrier of
G, the
carrier of
G )
by GROUP_2:def 5;
C2:
(
k in G & not
k in Image (phi | H) )
by B6, XBOOLE_0:def 5, GROUP_2:41;
consider phi2 being
Automorphism of
G such that C3:
phi2 = psi "
and C4:
Image (psi | (Image (phi2 | H))) = multMagma(# the
carrier of
H, the
multF of
H #)
by Th17;
C5:
phi2 = phi
by C3, B3, FUNCT_1:43;
set UPH = the
carrier of
(Image (phi | H));
psi .: the
carrier of
(Image (phi | H)) =
the
carrier of
(psi .: (Image (phi | H)))
by GRSOLV_1:8
.=
the
carrier of
(Image (psi | (Image (phi | H))))
by GRSOLV_1:def 3
;
hence
multMagma(# the
carrier of
H, the
multF of
H #)
<> Image (psi | K)
by B8, C1, C2, C4, C5, Th5;
verum
end;
B10:
Image (phi | (Image (psi | K))) = multMagma(# the
carrier of
G, the
multF of
G #)
Image (phi | (Image (psi | K))) = K
hence
K = multMagma(# the
carrier of
G, the
multF of
G #)
by B10;
verum
end;
hence
Image (phi | H) is maximal
by A2, Def1, GROUP_4:def 6; verum