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 )
proof
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
proof
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;
a in con_class a by GROUP_3:83;
hence {a} c= con_class a by ZFMISC_1:31; :: thesis: verum
end;
assume A5: con_class a = {a} ; :: thesis: a in center G
now :: thesis: for b being Element of G holds a * b = b * a
let 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;
hence a in center G by Th77; :: thesis: verum