reconsider K1 = Aut G as set ;
reconsider K2 = InnAut G as Subset of K1 by Th13;
for q being set st q in [:K2,K2:] holds
(AutComp G) . q in K2
then
AutComp G is Presv of K1,K2
by REALSET1:def 4;
then reconsider op = (AutComp G) || (InnAut G) as BinOp of (InnAut G) by REALSET1:6;
set IG = multMagma(# (InnAut G),op #);
A6:
for f, g, h being Element of multMagma(# (InnAut G),op #) holds (f * g) * h = f * (g * h)
ex e being Element of multMagma(# (InnAut G),op #) st
for h being Element of multMagma(# (InnAut G),op #) holds
( h * e = h & e * h = h & ex g being Element of multMagma(# (InnAut G),op #) st
( h * g = e & g * h = e ) )
proof
reconsider e =
id the
carrier of
G as
Element of
multMagma(#
(InnAut G),
op #)
by Th15;
take
e
;
for h being Element of multMagma(# (InnAut G),op #) holds
( h * e = h & e * h = h & ex g being Element of multMagma(# (InnAut G),op #) st
( h * g = e & g * h = e ) )
let h be
Element of
multMagma(#
(InnAut G),
op #);
( h * e = h & e * h = h & ex g being Element of multMagma(# (InnAut G),op #) st
( h * g = e & g * h = e ) )
consider A being
Element of
InnAut G such that A8:
A = h
;
h * e =
A * (id the carrier of G)
by A4, A8
.=
A
by FUNCT_2:17
;
hence
h * e = h
by A8;
( e * h = h & ex g being Element of multMagma(# (InnAut G),op #) st
( h * g = e & g * h = e ) )
e * h =
(id the carrier of G) * A
by A4, A8
.=
A
by FUNCT_2:17
;
hence
e * h = h
by A8;
ex g being Element of multMagma(# (InnAut G),op #) st
( h * g = e & g * h = e )
reconsider g =
A " as
Element of
multMagma(#
(InnAut G),
op #)
by Th16;
take
g
;
( h * g = e & g * h = e )
reconsider A =
A as
Element of
Aut G by Th12;
reconsider A =
A as
Homomorphism of
G,
G by Def1;
A9:
A is
one-to-one
by Def1;
A is
onto
by Def1;
then A10:
rng A = the
carrier of
G
;
thus h * g =
A * (A ")
by A4, A8
.=
e
by A9, A10, FUNCT_2:29
;
g * h = e
thus g * h =
(A ") * A
by A4, A8
.=
e
by A9, A10, FUNCT_2:29
;
verum
end;
then reconsider IG = multMagma(# (InnAut G),op #) as Group by A6, GROUP_1:def 2, GROUP_1:def 3;
the carrier of IG c= the carrier of (AutGroup G)
by Th13;
then reconsider IG = IG as strict Subgroup of AutGroup G by GROUP_2:def 5;
for f, k being Element of (AutGroup G) st k is Element of IG holds
k |^ f in IG
proof
let f,
k be
Element of
(AutGroup G);
( k is Element of IG implies k |^ f in IG )
consider f1 being
Element of
Aut G such that A11:
f1 = f
;
assume
k is
Element of
IG
;
k |^ f in IG
then consider g being
Element of
InnAut G such that A12:
g = k
;
reconsider D =
g as
Element of
Aut G by Th12;
g is
Element of
Aut G
by Th12;
then consider g1 being
Element of
Aut G such that A13:
g1 = g
;
g1 is
Element of
Funcs ( the
carrier of
G, the
carrier of
G)
by FUNCT_2:8;
then consider a being
Element of
G such that A14:
for
x being
Element of
G holds
g1 . x = x |^ a
by A13, Def4;
((f1 ") * g1) * f1 is
Element of
InnAut G
proof
f1 is
Homomorphism of
G,
G
by Def1;
then A15:
f1 is
one-to-one
by Def1;
A16:
rng f1 =
dom f1
by Lm3
.=
the
carrier of
G
by Lm3
;
then
f1 " is
Function of the
carrier of
G, the
carrier of
G
by A15, FUNCT_2:25;
then
(f1 ") * g1 is
Function of the
carrier of
G, the
carrier of
G
by FUNCT_2:13;
then
((f1 ") * g1) * f1 is
Function of the
carrier of
G, the
carrier of
G
by FUNCT_2:13;
then A17:
((f1 ") * g1) * f1 is
Element of
Funcs ( the
carrier of
G, the
carrier of
G)
by FUNCT_2:8;
f1 " is
Element of
Aut G
by Th6;
then
f1 " is
Homomorphism of
G,
G
by Def1;
then consider A being
Homomorphism of
G,
G such that A18:
A = f1 "
;
A19:
A * f1 = id the
carrier of
G
by A15, A16, A18, FUNCT_2:29;
hence
((f1 ") * g1) * f1 is
Element of
InnAut G
by A17, Def4;
verum
end;
then A20:
((f1 ") * g) * f1 in InnAut G
by A13;
reconsider C =
f1 " as
Element of
Aut G by Th6;
consider q being
set such that A21:
q = ((f ") * k) * f
;
f1 " = f "
by A11, Th10;
then
C * D = (f ") * k
by A12, Def2;
then
q in carr IG
by A11, A20, A21, Def2;
hence
k |^ f in IG
by A21, STRUCT_0:def 5;
verum
end;
then reconsider IG = IG as strict normal Subgroup of AutGroup G by Lm1;
take
IG
; the carrier of IG = InnAut G
thus
the carrier of IG = InnAut G
; verum