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

( a * x = x * a iff x is Element of (Centralizer a) )

let a, x be Element of G; :: thesis: ( a * x = x * a iff x is Element of (Centralizer a) )

A1: the carrier of (Centralizer a) = { b where b is Element of G : a * b = b * a } by Def1;

then x in the carrier of (Centralizer a) ;

then ex b being Element of G st

( b = x & a * b = b * a ) by A1;

hence a * x = x * a ; :: thesis: verum

( a * x = x * a iff x is Element of (Centralizer a) )

let a, x be Element of G; :: thesis: ( a * x = x * a iff x is Element of (Centralizer a) )

A1: the carrier of (Centralizer a) = { b where b is Element of G : a * b = b * a } by Def1;

hereby :: thesis: ( x is Element of (Centralizer a) implies a * x = x * a )

assume
x is Element of (Centralizer a)
; :: thesis: a * x = x * aassume
a * x = x * a
; :: thesis: x is Element of (Centralizer a)

then x in the carrier of (Centralizer a) by A1;

hence x is Element of (Centralizer a) ; :: thesis: verum

end;then x in the carrier of (Centralizer a) by A1;

hence x is Element of (Centralizer a) ; :: thesis: verum

then x in the carrier of (Centralizer a) ;

then ex b being Element of G st

( b = x & a * b = b * a ) by A1;

hence a * x = x * a ; :: thesis: verum