let G be strict Group; :: thesis:
deffunc H1( Element of G) -> Element of InnAut G = Conjugate (\$1 ");
consider f being Function of the carrier of G,() such that
A1: for a being Element of G holds f . a = H1(a) from reconsider f = f as Function of the carrier of G, the carrier of () by Def5;
now :: thesis: for a, b being Element of G holds f . (a * b) = (f . a) * (f . b)
let a, b be Element of G; :: thesis: f . (a * b) = (f . a) * (f . b)
A2: f . (a * b) = Conjugate ((a * b) ") by A1
.= Conjugate ((b ") * (a ")) by GROUP_1:17
.= (Conjugate (a ")) * (Conjugate (b ")) by Th21 ;
now :: thesis: for A, B being Element of () st A = f . a & B = f . b holds
f . (a * b) = (f . a) * (f . b)
let A, B be Element of (); :: thesis: ( A = f . a & B = f . b implies f . (a * b) = (f . a) * (f . b) )
assume A3: ( A = f . a & B = f . b ) ; :: thesis: f . (a * b) = (f . a) * (f . b)
then ( A = Conjugate (a ") & B = Conjugate (b ") ) by A1;
hence f . (a * b) = (f . a) * (f . b) by A2, A3, Th18; :: thesis: verum
end;
hence f . (a * b) = (f . a) * (f . b) ; :: thesis: verum
end;
then reconsider f1 = f as Homomorphism of G,() by GROUP_6:def 6;
A4: Ker f1 = center G
proof
set C = { a where a is Element of G : for b being Element of G holds a * b = b * a } ;
set KER = the carrier of (Ker f1);
A5: the carrier of (Ker f1) = { a where a is Element of G : f1 . a = 1_ () } by GROUP_6:def 9;
A6: the carrier of (Ker f1) c= { a where a is Element of G : for b being Element of G holds a * b = b * a }
proof
let q be object ; :: according to TARSKI:def 3 :: thesis: ( not q in the carrier of (Ker f1) or q in { a where a is Element of G : for b being Element of G holds a * b = b * a } )
assume A7: q in the carrier of (Ker f1) ; :: thesis: q in { a where a is Element of G : for b being Element of G holds a * b = b * a }
1_ () = id the carrier of G by Th19;
then consider x being Element of G such that
A8: q = x and
A9: f1 . x = id the carrier of G by A5, A7;
A10: for b being Element of G holds (Conjugate (x ")) . b = b
proof
let b be Element of G; :: thesis: (Conjugate (x ")) . b = b
(id the carrier of G) . b = b ;
hence (Conjugate (x ")) . b = b by A1, A9; :: thesis: verum
end;
A11: for b being Element of G holds b |^ (x ") = b
proof
let b be Element of G; :: thesis: b |^ (x ") = b
(Conjugate (x ")) . b = b |^ (x ") by Def6;
hence b |^ (x ") = b by A10; :: thesis: verum
end;
for b being Element of G holds x * b = b * x
proof
let b be Element of G; :: thesis: x * b = b * x
b |^ (x ") = (x * b) * (x ") ;
then ((x * b) * (x ")) * x = b * x by A11;
then (x * b) * ((x ") * x) = b * x by GROUP_1:def 3;
then (x * b) * (1_ G) = b * x by GROUP_1:def 5;
hence x * b = b * x by GROUP_1:def 4; :: thesis: verum
end;
hence q in { a where a is Element of G : for b being Element of G holds a * b = b * a } by A8; :: thesis: verum
end;
{ a where a is Element of G : for b being Element of G holds a * b = b * a } c= the carrier of (Ker f1)
proof
let q be object ; :: according to TARSKI:def 3 :: thesis: ( not q in { a where a is Element of G : for b being Element of G holds a * b = b * a } or q in the carrier of (Ker f1) )
assume q in { a where a is Element of G : for b being Element of G holds a * b = b * a } ; :: thesis: q in the carrier of (Ker f1)
then consider x being Element of G such that
A12: x = q and
A13: for b being Element of G holds x * b = b * x ;
consider g being Function of the carrier of G, the carrier of G such that
A14: g = Conjugate (x ") ;
A15: for b being Element of G holds b = (Conjugate (x ")) . b
proof
let b be Element of G; :: thesis: b = (Conjugate (x ")) . b
(x * b) * (x ") = (b * x) * (x ") by A13;
then (x * b) * (x ") = b * (x * (x ")) by GROUP_1:def 3;
then (x * b) * (x ") = b * (1_ G) by GROUP_1:def 5;
then b = b |^ (x ") by GROUP_1:def 4;
hence b = (Conjugate (x ")) . b by Def6; :: thesis: verum
end;
for b being Element of G holds (id the carrier of G) . b = g . b by ;
then g = id the carrier of G ;
then Conjugate (x ") = 1_ () by ;
then f1 . x = 1_ () by A1;
hence q in the carrier of (Ker f1) by ; :: thesis: verum
end;
then the carrier of (Ker f1) = { a where a is Element of G : for b being Element of G holds a * b = b * a } by ;
hence Ker f1 = center G by GROUP_5:def 10; :: thesis: verum
end;
A16: the carrier of () = InnAut G by Def5;
for q being object st q in the carrier of () holds
ex q1 being object st
( q1 in the carrier of G & q = f1 . q1 )
proof
let q be object ; :: thesis: ( q in the carrier of () implies ex q1 being object st
( q1 in the carrier of G & q = f1 . q1 ) )

assume A17: q in the carrier of () ; :: thesis: ex q1 being object st
( q1 in the carrier of G & q = f1 . q1 )

then A18: q is Element of InnAut G by Def5;
then consider y1 being Function of the carrier of G, the carrier of G such that
A19: y1 = q ;
y1 is Element of Funcs ( the carrier of G, the carrier of G) by FUNCT_2:9;
then consider b being Element of G such that
A20: for a being Element of G holds y1 . a = a |^ b by ;
take q1 = b " ; :: thesis: ( q1 in the carrier of G & q = f1 . q1 )
thus q1 in the carrier of G ; :: thesis: q = f1 . q1
f1 . q1 = Conjugate ((b ") ") by A1
.= Conjugate b ;
hence q = f1 . q1 by ; :: thesis: verum
end;
then rng f1 = the carrier of () by FUNCT_2:10;
then f1 is onto ;
then InnAutGroup G = Image f1 by GROUP_6:57;
hence InnAutGroup G,G ./. () are_isomorphic by ; :: thesis: verum