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

for t being Element of (MultGroup R) st t = s holds

the carrier of (centralizer s) = the carrier of (Centralizer t) \/ {(0. R)}

let s be Element of R; :: thesis: for t being Element of (MultGroup R) st t = s holds

the carrier of (centralizer s) = the carrier of (Centralizer t) \/ {(0. R)}

let t be Element of (MultGroup R); :: thesis: ( t = s implies the carrier of (centralizer s) = the carrier of (Centralizer t) \/ {(0. R)} )

assume A1: t = s ; :: thesis: the carrier of (centralizer s) = the carrier of (Centralizer t) \/ {(0. R)}

set ct = Centralizer t;

set cs = centralizer s;

set cct = the carrier of (Centralizer t);

set ccs = the carrier of (centralizer s);

A2: the carrier of (MultGroup R) = NonZero R by UNIROOTS:def 1;

A3: the carrier of (Centralizer t) = { b where b is Element of (MultGroup R) : t * b = b * t } by Def1;

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

for t being Element of (MultGroup R) st t = s holds

the carrier of (centralizer s) = the carrier of (Centralizer t) \/ {(0. R)}

let s be Element of R; :: thesis: for t being Element of (MultGroup R) st t = s holds

the carrier of (centralizer s) = the carrier of (Centralizer t) \/ {(0. R)}

let t be Element of (MultGroup R); :: thesis: ( t = s implies the carrier of (centralizer s) = the carrier of (Centralizer t) \/ {(0. R)} )

assume A1: t = s ; :: thesis: the carrier of (centralizer s) = the carrier of (Centralizer t) \/ {(0. R)}

set ct = Centralizer t;

set cs = centralizer s;

set cct = the carrier of (Centralizer t);

set ccs = the carrier of (centralizer s);

A2: the carrier of (MultGroup R) = NonZero R by UNIROOTS:def 1;

A3: the carrier of (Centralizer t) = { b where b is Element of (MultGroup R) : t * b = b * t } by Def1;

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

now :: thesis: for x being object holds

( ( x in the carrier of (centralizer s) implies x in the carrier of (Centralizer t) \/ {(0. R)} ) & ( x in the carrier of (Centralizer t) \/ {(0. R)} implies x in the carrier of (centralizer s) ) )

hence
the carrier of (centralizer s) = the carrier of (Centralizer t) \/ {(0. R)}
by TARSKI:2; :: thesis: verum( ( x in the carrier of (centralizer s) implies x in the carrier of (Centralizer t) \/ {(0. R)} ) & ( x in the carrier of (Centralizer t) \/ {(0. R)} implies x in the carrier of (centralizer s) ) )

let x be object ; :: thesis: ( ( x in the carrier of (centralizer s) implies x in the carrier of (Centralizer t) \/ {(0. R)} ) & ( x in the carrier of (Centralizer t) \/ {(0. R)} implies b_{1} in the carrier of (centralizer s) ) )

_{1} in the carrier of (centralizer s)

end;hereby :: thesis: ( x in the carrier of (Centralizer t) \/ {(0. R)} implies b_{1} in the carrier of (centralizer s) )

assume A7:
x in the carrier of (Centralizer t) \/ {(0. R)}
; :: thesis: bassume
x in the carrier of (centralizer s)
; :: thesis: x in the carrier of (Centralizer t) \/ {(0. R)}

then consider c being Element of R such that

A5: c = x and

A6: c * s = s * c by A4;

end;then consider c being Element of R such that

A5: c = x and

A6: c * s = s * c by A4;

per cases
( c = 0. R or c <> 0. R )
;

end;

suppose
c = 0. R
; :: thesis: x in the carrier of (Centralizer t) \/ {(0. R)}

then
c in {(0. R)}
by TARSKI:def 1;

hence x in the carrier of (Centralizer t) \/ {(0. R)} by A5, XBOOLE_0:def 3; :: thesis: verum

end;hence x in the carrier of (Centralizer t) \/ {(0. R)} by A5, XBOOLE_0:def 3; :: thesis: verum

suppose
c <> 0. R
; :: thesis: x in the carrier of (Centralizer t) \/ {(0. R)}

then
not c in {(0. R)}
by TARSKI:def 1;

then reconsider c1 = c as Element of (MultGroup R) by A2, XBOOLE_0:def 5;

t * c1 = s * c by A1, UNIROOTS:16

.= c1 * t by A1, A6, UNIROOTS:16 ;

then c in the carrier of (Centralizer t) by A3;

hence x in the carrier of (Centralizer t) \/ {(0. R)} by A5, XBOOLE_0:def 3; :: thesis: verum

end;then reconsider c1 = c as Element of (MultGroup R) by A2, XBOOLE_0:def 5;

t * c1 = s * c by A1, UNIROOTS:16

.= c1 * t by A1, A6, UNIROOTS:16 ;

then c in the carrier of (Centralizer t) by A3;

hence x in the carrier of (Centralizer t) \/ {(0. R)} by A5, XBOOLE_0:def 3; :: thesis: verum

per cases
( x in the carrier of (Centralizer t) or x in {(0. R)} )
by A7, XBOOLE_0:def 3;

end;

suppose
x in the carrier of (Centralizer t)
; :: thesis: b_{1} in the carrier of (centralizer s)

then consider b being Element of (MultGroup R) such that

A8: x = b and

A9: t * b = b * t by A3;

reconsider b1 = b as Element of R by UNIROOTS:19;

b1 * s = t * b by A1, A9, UNIROOTS:16

.= s * b1 by A1, UNIROOTS:16 ;

hence x in the carrier of (centralizer s) by A4, A8; :: thesis: verum

end;A8: x = b and

A9: t * b = b * t by A3;

reconsider b1 = b as Element of R by UNIROOTS:19;

b1 * s = t * b by A1, A9, UNIROOTS:16

.= s * b1 by A1, UNIROOTS:16 ;

hence x in the carrier of (centralizer s) by A4, A8; :: thesis: verum

suppose
x in {(0. R)}
; :: thesis: b_{1} in the carrier of (centralizer s)

then A10:
x = 0. R
by TARSKI:def 1;

(0. R) * s = s * (0. R) ;

hence x in the carrier of (centralizer s) by A4, A10; :: thesis: verum

end;(0. R) * s = s * (0. R) ;

hence x in the carrier of (centralizer s) by A4, A10; :: thesis: verum