let G be Group; :: thesis: Centralizer ((Omega). G) = center G
for g being Element of G holds
( g in Centralizer ((Omega). G) iff g in center G )

proof

let g be Element of G; :: thesis: ( g in Centralizer ((Omega). G) iff g in center G )
thus ( g in Centralizer ((Omega). G) implies g in center G ) :: thesis: ( g in center G implies g in Centralizer ((Omega). G) )

proof

assume A1: g in Centralizer ((Omega). G) ; :: thesis: g in center G
for a being Element of G holds g * a = a * g

proof

let a be Element of G; :: thesis: g * a = a * g
a in (Omega). G ;
hence g * a = a * g by A1, Th60; :: thesis: verum

end;

hence g in center G by GROUP_5:77; :: thesis: verum

end;

thus ( g in center G implies g in Centralizer ((Omega). G) ) :: thesis: verum

proof

assume g in center G ; :: thesis: g in Centralizer ((Omega). G)
then for b being Element of G st b in (Omega). G holds
g * b = b * g by GROUP_5:77;
then g is Element of (Centralizer ((Omega). G)) by Th60;
hence g in Centralizer ((Omega). G) ; :: thesis: verum

end;

end;

hence Centralizer ((Omega). G) = center G ; :: thesis: verum