let G be strict Group; :: thesis: InnAutGroup G,G ./. (center G) are_isomorphic

deffunc H_{1}( Element of G) -> Element of InnAut G = Conjugate ($1 ");

consider f being Function of the carrier of G,(InnAut G) such that

A1: for a being Element of G holds f . a = H_{1}(a)
from FUNCT_2:sch 4();

reconsider f = f as Function of the carrier of G, the carrier of (InnAutGroup G) by Def5;

A4: Ker f1 = center G

for q being object st q in the carrier of (InnAutGroup G) holds

ex q1 being object st

( q1 in the carrier of G & q = f1 . q1 )

then f1 is onto ;

then InnAutGroup G = Image f1 by GROUP_6:57;

hence InnAutGroup G,G ./. (center G) are_isomorphic by A4, GROUP_6:78; :: thesis: verum

deffunc H

consider f being Function of the carrier of G,(InnAut G) such that

A1: for a being Element of G holds f . a = H

reconsider f = f as Function of the carrier of G, the carrier of (InnAutGroup G) by Def5;

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

then reconsider f1 = f as Homomorphism of G,(InnAutGroup G) by GROUP_6:def 6;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 ;

end;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 (InnAutGroup G) st A = f . a & B = f . b holds

f . (a * b) = (f . a) * (f . b)

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

let A, B be Element of (InnAutGroup G); :: 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;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

A4: Ker f1 = center G

proof

A16:
the carrier of (InnAutGroup G) = InnAut G
by Def5;
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_ (InnAutGroup G) } 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 }

hence Ker f1 = center G by GROUP_5:def 10; :: thesis: verum

end;set KER = the carrier of (Ker f1);

A5: the carrier of (Ker f1) = { a where a is Element of G : f1 . a = 1_ (InnAutGroup G) } 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

{ a where a is Element of G : for b being Element of G holds a * b = b * a } c= the carrier of (Ker f1)
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_ (InnAutGroup G) = 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

end;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_ (InnAutGroup G) = 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

A11:
for b being Element of G holds b |^ (x ") = b
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;(id the carrier of G) . b = b ;

hence (Conjugate (x ")) . b = b by A1, A9; :: thesis: verum

proof

for b being Element of G holds x * b = b * x
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;(Conjugate (x ")) . b = b |^ (x ") by Def6;

hence b |^ (x ") = b by A10; :: thesis: verum

proof

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
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;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

proof

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 A6, XBOOLE_0:def 10;
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

then g = id the carrier of G ;

then Conjugate (x ") = 1_ (InnAutGroup G) by A14, Th19;

then f1 . x = 1_ (InnAutGroup G) by A1;

hence q in the carrier of (Ker f1) by A5, A12; :: thesis: verum

end;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

for b being Element of G holds (id the carrier of G) . b = g . b
by A15, A14;
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;(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

then g = id the carrier of G ;

then Conjugate (x ") = 1_ (InnAutGroup G) by A14, Th19;

then f1 . x = 1_ (InnAutGroup G) by A1;

hence q in the carrier of (Ker f1) by A5, A12; :: thesis: verum

hence Ker f1 = center G by GROUP_5:def 10; :: thesis: verum

for q being object st q in the carrier of (InnAutGroup G) holds

ex q1 being object st

( q1 in the carrier of G & q = f1 . q1 )

proof

then
rng f1 = the carrier of (InnAutGroup G)
by FUNCT_2:10;
let q be object ; :: thesis: ( q in the carrier of (InnAutGroup G) implies ex q1 being object st

( q1 in the carrier of G & q = f1 . q1 ) )

assume A17: q in the carrier of (InnAutGroup G) ; :: 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 A16, A17, A19, 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 A1

.= Conjugate b ;

hence q = f1 . q1 by A18, A19, A20, Def6; :: thesis: verum

end;( q1 in the carrier of G & q = f1 . q1 ) )

assume A17: q in the carrier of (InnAutGroup G) ; :: 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 A16, A17, A19, 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 A1

.= Conjugate b ;

hence q = f1 . q1 by A18, A19, A20, Def6; :: thesis: verum

then f1 is onto ;

then InnAutGroup G = Image f1 by GROUP_6:57;

hence InnAutGroup G,G ./. (center G) are_isomorphic by A4, GROUP_6:78; :: thesis: verum