let R be Skew-Field; :: thesis: for s, a being Element of R holds

( a in the carrier of (centralizer s) iff a * s = s * a )

let s, a be Element of R; :: thesis: ( a in the carrier of (centralizer s) iff a * s = s * a )

set cs = centralizer s;

set ccs = the carrier of (centralizer s);

A1: the carrier of (centralizer s) = { x where x is Element of R : x * s = s * x } by Def5;

hence a in the carrier of (centralizer s) by A1; :: thesis: verum

( a in the carrier of (centralizer s) iff a * s = s * a )

let s, a be Element of R; :: thesis: ( a in the carrier of (centralizer s) iff a * s = s * a )

set cs = centralizer s;

set ccs = the carrier of (centralizer s);

A1: the carrier of (centralizer s) = { x where x is Element of R : x * s = s * x } by Def5;

hereby :: thesis: ( a * s = s * a implies a in the carrier of (centralizer s) )

assume
a * s = s * a
; :: thesis: a in the carrier of (centralizer s)assume
a in the carrier of (centralizer s)
; :: thesis: a * s = s * a

then ex x being Element of R st

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

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

end;then ex x being Element of R st

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

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

hence a in the carrier of (centralizer s) by A1; :: thesis: verum