let R be finite Skew-Field; :: thesis: ( card the carrier of (center R) = card the carrier of R iff R is commutative )

set X = the carrier of R;

set Y = the carrier of (center R);

set X = the carrier of R;

set Y = the carrier of (center R);

hereby :: thesis: ( R is commutative implies card the carrier of (center R) = card the carrier of R )

assume A1:
card the carrier of R = card the carrier of (center R)
; :: thesis: R is commutative

A2: the carrier of (center R) c= the carrier of R by Th16;

card ( the carrier of R \ the carrier of (center R)) = (card the carrier of R) - (card the carrier of R) by A1, Th16, CARD_2:44;

then the carrier of R \ the carrier of (center R) = {} ;

then the carrier of R c= the carrier of (center R) by XBOOLE_1:37;

then A3: the carrier of R = the carrier of (center R) by A2, XBOOLE_0:def 10;

for x, s being Element of the carrier of R holds x * s = s * x by A3, STRUCT_0:def 5, Th17;

hence R is commutative ; :: thesis: verum

end;A2: the carrier of (center R) c= the carrier of R by Th16;

card ( the carrier of R \ the carrier of (center R)) = (card the carrier of R) - (card the carrier of R) by A1, Th16, CARD_2:44;

then the carrier of R \ the carrier of (center R) = {} ;

then the carrier of R c= the carrier of (center R) by XBOOLE_1:37;

then A3: the carrier of R = the carrier of (center R) by A2, XBOOLE_0:def 10;

for x, s being Element of the carrier of R holds x * s = s * x by A3, STRUCT_0:def 5, Th17;

hence R is commutative ; :: thesis: verum

now :: thesis: ( R is commutative implies card the carrier of (center R) = card the carrier of R )

hence
( R is commutative implies card the carrier of (center R) = card the carrier of R )
; :: thesis: verumassume A4:
R is commutative
; :: thesis: card the carrier of (center R) = card the carrier of R

for x being object st x in the carrier of R holds

x in the carrier of (center R)

the carrier of (center R) c= the carrier of R by Th16;

hence card the carrier of (center R) = card the carrier of R by A6, XBOOLE_0:def 10; :: thesis: verum

end;for x being object st x in the carrier of R holds

x in the carrier of (center R)

proof

then A6:
the carrier of R c= the carrier of (center R)
;
let x be object ; :: thesis: ( x in the carrier of R implies x in the carrier of (center R) )

assume A5: x in the carrier of R ; :: thesis: x in the carrier of (center R)

for x being Element of the carrier of R holds x is Element of the carrier of (center R)

hence x in the carrier of (center R) ; :: thesis: verum

end;assume A5: x in the carrier of R ; :: thesis: x in the carrier of (center R)

for x being Element of the carrier of R holds x is Element of the carrier of (center R)

proof

then
x is Element of the carrier of (center R)
by A5;
let x be Element of the carrier of R; :: thesis: x is Element of the carrier of (center R)

for y being Element of the carrier of R holds x * y = y * x by A4;

then x in center R by Th17;

hence x is Element of the carrier of (center R) ; :: thesis: verum

end;for y being Element of the carrier of R holds x * y = y * x by A4;

then x in center R by Th17;

hence x is Element of the carrier of (center R) ; :: thesis: verum

hence x in the carrier of (center R) ; :: thesis: verum

the carrier of (center R) c= the carrier of R by Th16;

hence card the carrier of (center R) = card the carrier of R by A6, XBOOLE_0:def 10; :: thesis: verum