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);
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;
now :: thesis: ( R is commutative implies card the carrier of (center R) = card the carrier of R )
assume 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)
proof
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)
proof
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;
then x is Element of the carrier of (center R) by A5;
hence x in the carrier of (center R) ; :: thesis: verum
end;
then A6: the carrier of R c= 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;
hence ( R is commutative implies card the carrier of (center R) = card the carrier of R ) ; :: thesis: verum