let G be strict Group; :: thesis: for f being Element of InnAut G holds f is Element of Aut G

let f be Element of InnAut G; :: thesis: f is Element of Aut G

A1: f is Element of Funcs ( the carrier of G, the carrier of G) by FUNCT_2:9;

A3: f is one-to-one

ex q1 being object st

( q1 in dom f & q = f . q1 )

then rng f = the carrier of G by XBOOLE_0:def 10;

then f is onto ;

hence f is Element of Aut G by A3, Def1; :: thesis: verum

let f be Element of InnAut G; :: thesis: f is Element of Aut G

A1: f is Element of Funcs ( the carrier of G, the carrier of G) by FUNCT_2:9;

now :: thesis: for x, y being Element of G holds f . (x * y) = (f . x) * (f . y)

then reconsider f = f as Homomorphism of G,G by GROUP_6:def 6;let x, y be Element of G; :: thesis: f . (x * y) = (f . x) * (f . y)

consider a being Element of G such that

A2: for x being Element of G holds f . x = x |^ a by A1, Def4;

thus f . (x * y) = (x * y) |^ a by A2

.= (((a ") * x) * y) * a by GROUP_1:def 3

.= ((a ") * x) * (y * a) by GROUP_1:def 3

.= (((a ") * x) * (1_ G)) * (y * a) by GROUP_1:def 4

.= (((a ") * x) * (a * (a "))) * (y * a) by GROUP_1:def 5

.= ((((a ") * x) * a) * (a ")) * (y * a) by GROUP_1:def 3

.= (((((a ") * x) * a) * (a ")) * y) * a by GROUP_1:def 3

.= ((((a ") * x) * a) * ((a ") * y)) * a by GROUP_1:def 3

.= (x |^ a) * (y |^ a) by GROUP_1:def 3

.= (f . x) * (y |^ a) by A2

.= (f . x) * (f . y) by A2 ; :: thesis: verum

end;consider a being Element of G such that

A2: for x being Element of G holds f . x = x |^ a by A1, Def4;

thus f . (x * y) = (x * y) |^ a by A2

.= (((a ") * x) * y) * a by GROUP_1:def 3

.= ((a ") * x) * (y * a) by GROUP_1:def 3

.= (((a ") * x) * (1_ G)) * (y * a) by GROUP_1:def 4

.= (((a ") * x) * (a * (a "))) * (y * a) by GROUP_1:def 5

.= ((((a ") * x) * a) * (a ")) * (y * a) by GROUP_1:def 3

.= (((((a ") * x) * a) * (a ")) * y) * a by GROUP_1:def 3

.= ((((a ") * x) * a) * ((a ") * y)) * a by GROUP_1:def 3

.= (x |^ a) * (y |^ a) by GROUP_1:def 3

.= (f . x) * (y |^ a) by A2

.= (f . x) * (f . y) by A2 ; :: thesis: verum

A3: f is one-to-one

proof

for q being object st q in the carrier of G holds
let q, q1 be object ; :: according to FUNCT_1:def 4 :: thesis: ( not q in dom f or not q1 in dom f or not f . q = f . q1 or q = q1 )

assume that

A4: ( q in dom f & q1 in dom f ) and

A5: f . q = f . q1 ; :: thesis: q = q1

consider x, y being Element of G such that

A6: ( x = q & y = q1 ) by A4;

consider a being Element of G such that

A7: for x being Element of G holds f . x = x |^ a by A1, Def4;

f . x = y |^ a by A7, A5, A6;

then x |^ a = y |^ a by A7;

then a * ((a ") * (x * a)) = a * (((a ") * y) * a) by GROUP_1:def 3;

then (a * (a ")) * (x * a) = a * (((a ") * y) * a) by GROUP_1:def 3;

then (a * (a ")) * (x * a) = a * ((a ") * (y * a)) by GROUP_1:def 3;

then (a * (a ")) * (x * a) = (a * (a ")) * (y * a) by GROUP_1:def 3;

then (1_ G) * (x * a) = (a * (a ")) * (y * a) by GROUP_1:def 5;

then (1_ G) * (x * a) = (1_ G) * (y * a) by GROUP_1:def 5;

then x * a = (1_ G) * (y * a) by GROUP_1:def 4;

then (x * a) * (a ") = (y * a) * (a ") by GROUP_1:def 4;

then x * (a * (a ")) = (y * a) * (a ") by GROUP_1:def 3;

then x * (a * (a ")) = y * (a * (a ")) by GROUP_1:def 3;

then x * (1_ G) = y * (a * (a ")) by GROUP_1:def 5;

then x * (1_ G) = y * (1_ G) by GROUP_1:def 5;

then x = y * (1_ G) by GROUP_1:def 4;

hence q = q1 by A6, GROUP_1:def 4; :: thesis: verum

end;assume that

A4: ( q in dom f & q1 in dom f ) and

A5: f . q = f . q1 ; :: thesis: q = q1

consider x, y being Element of G such that

A6: ( x = q & y = q1 ) by A4;

consider a being Element of G such that

A7: for x being Element of G holds f . x = x |^ a by A1, Def4;

f . x = y |^ a by A7, A5, A6;

then x |^ a = y |^ a by A7;

then a * ((a ") * (x * a)) = a * (((a ") * y) * a) by GROUP_1:def 3;

then (a * (a ")) * (x * a) = a * (((a ") * y) * a) by GROUP_1:def 3;

then (a * (a ")) * (x * a) = a * ((a ") * (y * a)) by GROUP_1:def 3;

then (a * (a ")) * (x * a) = (a * (a ")) * (y * a) by GROUP_1:def 3;

then (1_ G) * (x * a) = (a * (a ")) * (y * a) by GROUP_1:def 5;

then (1_ G) * (x * a) = (1_ G) * (y * a) by GROUP_1:def 5;

then x * a = (1_ G) * (y * a) by GROUP_1:def 4;

then (x * a) * (a ") = (y * a) * (a ") by GROUP_1:def 4;

then x * (a * (a ")) = (y * a) * (a ") by GROUP_1:def 3;

then x * (a * (a ")) = y * (a * (a ")) by GROUP_1:def 3;

then x * (1_ G) = y * (a * (a ")) by GROUP_1:def 5;

then x * (1_ G) = y * (1_ G) by GROUP_1:def 5;

then x = y * (1_ G) by GROUP_1:def 4;

hence q = q1 by A6, GROUP_1:def 4; :: thesis: verum

ex q1 being object st

( q1 in dom f & q = f . q1 )

proof

then
the carrier of G c= rng f
by FUNCT_1:9;
let q be object ; :: thesis: ( q in the carrier of G implies ex q1 being object st

( q1 in dom f & q = f . q1 ) )

assume q in the carrier of G ; :: thesis: ex q1 being object st

( q1 in dom f & q = f . q1 )

then consider y being Element of G such that

A8: y = q ;

consider a being Element of G such that

A9: for x being Element of G holds f . x = x |^ a by A1, Def4;

take q1 = (a * y) * (a "); :: thesis: ( q1 in dom f & q = f . q1 )

ex f1 being Function st

( f = f1 & dom f1 = the carrier of G & rng f1 c= the carrier of G ) by A1, FUNCT_2:def 2;

hence q1 in dom f ; :: thesis: q = f . q1

y = (1_ G) * y by GROUP_1:def 4

.= ((1_ G) * y) * (1_ G) by GROUP_1:def 4

.= (((a ") * a) * y) * (1_ G) by GROUP_1:def 5

.= (((a ") * a) * y) * ((a ") * a) by GROUP_1:def 5

.= ((((a ") * a) * y) * (a ")) * a by GROUP_1:def 3

.= (((a ") * a) * (y * (a "))) * a by GROUP_1:def 3

.= ((a ") * (a * (y * (a ")))) * a by GROUP_1:def 3

.= q1 |^ a by GROUP_1:def 3

.= f . q1 by A9 ;

hence q = f . q1 by A8; :: thesis: verum

end;( q1 in dom f & q = f . q1 ) )

assume q in the carrier of G ; :: thesis: ex q1 being object st

( q1 in dom f & q = f . q1 )

then consider y being Element of G such that

A8: y = q ;

consider a being Element of G such that

A9: for x being Element of G holds f . x = x |^ a by A1, Def4;

take q1 = (a * y) * (a "); :: thesis: ( q1 in dom f & q = f . q1 )

ex f1 being Function st

( f = f1 & dom f1 = the carrier of G & rng f1 c= the carrier of G ) by A1, FUNCT_2:def 2;

hence q1 in dom f ; :: thesis: q = f . q1

y = (1_ G) * y by GROUP_1:def 4

.= ((1_ G) * y) * (1_ G) by GROUP_1:def 4

.= (((a ") * a) * y) * (1_ G) by GROUP_1:def 5

.= (((a ") * a) * y) * ((a ") * a) by GROUP_1:def 5

.= ((((a ") * a) * y) * (a ")) * a by GROUP_1:def 3

.= (((a ") * a) * (y * (a "))) * a by GROUP_1:def 3

.= ((a ") * (a * (y * (a ")))) * a by GROUP_1:def 3

.= q1 |^ a by GROUP_1:def 3

.= f . q1 by A9 ;

hence q = f . q1 by A8; :: thesis: verum

then rng f = the carrier of G by XBOOLE_0:def 10;

then f is onto ;

hence f is Element of Aut G by A3, Def1; :: thesis: verum