let G be Group; :: thesis: for a being Element of G holds

( a in center G iff con_class a = {a} )

let a be Element of G; :: thesis: ( a in center G iff con_class a = {a} )

thus ( a in center G implies con_class a = {a} ) :: thesis: ( con_class a = {a} implies a in center G )

( a in center G iff con_class a = {a} )

let a be Element of G; :: thesis: ( a in center G iff con_class a = {a} )

thus ( a in center G implies con_class a = {a} ) :: thesis: ( con_class a = {a} implies a in center G )

proof

assume A5:
con_class a = {a}
; :: thesis: a in center G
assume A1:
a in center G
; :: thesis: con_class a = {a}

thus con_class a c= {a} :: according to XBOOLE_0:def 10 :: thesis: {a} c= con_class a

hence {a} c= con_class a by ZFMISC_1:31; :: thesis: verum

end;thus con_class a c= {a} :: according to XBOOLE_0:def 10 :: thesis: {a} c= con_class a

proof

a in con_class a
by GROUP_3:83;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in con_class a or x in {a} )

assume x in con_class a ; :: thesis: x in {a}

then consider b being Element of G such that

A2: b = x and

A3: a,b are_conjugated by GROUP_3:80;

consider c being Element of G such that

A4: a = b |^ c by A3;

a = (c ") * (b * c) by A4, GROUP_1:def 3;

then c * a = b * c by GROUP_1:13;

then a * c = b * c by A1, Th77;

then a = b by GROUP_1:6;

hence x in {a} by A2, TARSKI:def 1; :: thesis: verum

end;assume x in con_class a ; :: thesis: x in {a}

then consider b being Element of G such that

A2: b = x and

A3: a,b are_conjugated by GROUP_3:80;

consider c being Element of G such that

A4: a = b |^ c by A3;

a = (c ") * (b * c) by A4, GROUP_1:def 3;

then c * a = b * c by GROUP_1:13;

then a * c = b * c by A1, Th77;

then a = b by GROUP_1:6;

hence x in {a} by A2, TARSKI:def 1; :: thesis: verum

hence {a} c= con_class a by ZFMISC_1:31; :: thesis: verum

now :: thesis: for b being Element of G holds a * b = b * a

hence
a in center G
by Th77; :: thesis: verumlet b be Element of G; :: thesis: a * b = b * a

a |^ b in con_class a by GROUP_3:82;

then a |^ b = a by A5, TARSKI:def 1;

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

hence a * b = b * a by GROUP_1:13; :: thesis: verum

end;a |^ b in con_class a by GROUP_3:82;

then a |^ b = a by A5, TARSKI:def 1;

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

hence a * b = b * a by GROUP_1:13; :: thesis: verum