let G be strict Group; :: thesis: InnAutGroup G,G ./. (center G) are_isomorphic
A1: the carrier of (InnAutGroup G) = InnAut G by Def5;
deffunc H₁( Element of G) -> Element of InnAut G = Conjugate ($1 " );
consider f being Function of the carrier of G,(InnAut G) such that
A2: for a being Element of G holds f . a = H₁(a) from FUNCT_2:sch 4();
reconsider f = f as Function of the carrier of G,the carrier of (InnAutGroup G) by A1;

now

let a, b be Element of G; :: thesis: f . (a * b) = (f . a) * (f . b)
A3: f . (a * b) = Conjugate ((a * b) " ) by A2
.= Conjugate ((b " ) * (a " )) by GROUP_1:25
.= (Conjugate (a " )) * (Conjugate (b " )) by Th23 ;

now

let A, B be Element of (InnAutGroup G); :: thesis: ( A = f . a & B = f . b implies f . (a * b) = (f . a) * (f . b) )
assume A4: ( A = f . a & B = f . b ) ; :: thesis: f . (a * b) = (f . a) * (f . b)
then ( A = Conjugate (a " ) & B = Conjugate (b " ) ) by A2;
hence f . (a * b) = (f . a) * (f . b) by A3, A4, Th20; :: thesis: verum

end;

hence f . (a * b) = (f . a) * (f . b) ; :: thesis: verum

end;

then reconsider f1 = f as Homomorphism of G,(InnAutGroup G) by GROUP_6:def 7;
A5: Ker f1 = center G

proof

set KER = the carrier of (Ker f1);
set C = { a where a is Element of G : for b being Element of G holds a * b = b * a } ;
A6: the carrier of (Ker f1) = { a where a is Element of G : f1 . a = 1_ (InnAutGroup G) } by GROUP_6:def 10;
A7: 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 set ; :: 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 A8: 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_ (InnAutGroup G) = id the carrier of G by Th21;
then consider x being Element of G such that
A9: ( q = x & f1 . x = id the carrier of G ) by A6, A8;
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 by FUNCT_1:35;
hence (Conjugate (x " )) . b = b by A2, 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 4;
then (x * b) * (1_ G) = b * x by GROUP_1:def 6;
hence x * b = b * x by GROUP_1:def 5; :: 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 A9; :: 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 set ; :: 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 & ( for b being Element of G holds x * b = b * x ) ) ;
A13: 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 A12;
then (x * b) * (x " ) = b * (x * (x " )) by GROUP_1:def 4;
then (x * b) * (x " ) = b * (1_ G) by GROUP_1:def 6;
then b = (x * b) * (x " ) by GROUP_1:def 5;
then b = b |^ (x " ) ;
hence b = (Conjugate (x " )) . b by Def6; :: thesis: verum

end;

consider g being Function of the carrier of G,the carrier of G such that
A14: g = Conjugate (x " ) ;
for b being Element of G holds (id the carrier of G) . b = g . b

proof

let b be Element of G; :: thesis: (id the carrier of G) . b = g . b
( b = g . b & b = (id the carrier of G) . b ) by A13, A14, FUNCT_1:35;
hence (id the carrier of G) . b = g . b ; :: thesis: verum

end;

then g = id the carrier of G by FUNCT_2:113;
then Conjugate (x " ) = 1_ (InnAutGroup G) by A14, Th21;
then f1 . x = 1_ (InnAutGroup G) by A2;
hence q in the carrier of (Ker f1) by A6, A12; :: 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 A7, XBOOLE_0:def 10;
hence Ker f1 = center G by GROUP_5:def 10; :: thesis: verum

end;

f1 is onto

proof

for q being set st q in the carrier of (InnAutGroup G) holds
ex q1 being set st
( q1 in the carrier of G & q = f1 . q1 )

proof

let q be set ; :: thesis: ( q in the carrier of (InnAutGroup G) implies ex q1 being set st
( q1 in the carrier of G & q = f1 . q1 ) )
assume A15: q in the carrier of (InnAutGroup G) ; :: thesis: ex q1 being set st
( q1 in the carrier of G & q = f1 . q1 )
then A16: q is Element of InnAut G by Def5;
then consider y1 being Function of the carrier of G,the carrier of G such that
A17: y1 = q ;
y1 is Element of Funcs the carrier of G,the carrier of G by FUNCT_2:12;
then consider b being Element of G such that
A18: for a being Element of G holds y1 . a = a |^ b by A1, A15, A17, Def4;
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 A2
.= Conjugate b ;
hence q = f1 . q1 by A16, A17, A18, Def6; :: thesis: verum

end;

then rng f1 = the carrier of (InnAutGroup G) by FUNCT_2:16;
hence f1 is onto by FUNCT_2:def 3; :: thesis: verum

end;

then InnAutGroup G = Image f1 by GROUP_6:67;
hence InnAutGroup G,G ./. (center G) are_isomorphic by A5, GROUP_6:90; :: thesis: verum