let R be finite Skew-Field; :: thesis: R is commutative
assume A1: not R is commutative ; :: thesis: contradiction
set Z = center R;
set cZ = the carrier of (center R);
set q = card the carrier of (center R);
set vR = VectSp_over_center R;
set n = dim (VectSp_over_center R);
set Rs = MultGroup R;
set cR = the carrier of R;
set cRs = the carrier of (MultGroup R);
set cZs = the carrier of (center (MultGroup R));
A2: card R = (card the carrier of (center R)) |^ (dim (VectSp_over_center R)) by Th31;
then A3: card (MultGroup R) = ((card the carrier of (center R)) |^ (dim (VectSp_over_center R))) - 1 by UNIROOTS:18;
A4: 1 < card the carrier of (center R) by Th20;
A5: 1 + (- 1) < (card the carrier of (center R)) + (- 1) by Th20, XREAL_1:8;
then reconsider natq1 = (card the carrier of (center R)) - 1 as Element of NAT by INT_1:3;
0 + 1 < (dim (VectSp_over_center R)) + 1 by Th32, XREAL_1:8;
then A6: 1 <= dim (VectSp_over_center R) by NAT_1:13;
dim (VectSp_over_center R) <> 1 by A2, A1, Th21;
then A8: 1 < dim (VectSp_over_center R) by A6, XXREAL_0:1;
set A = { X where X is Subset of the carrier of (MultGroup R) : ( X in conjugate_Classes (MultGroup R) & card X = 1 ) } ;
set B = (conjugate_Classes (MultGroup R)) \ { X where X is Subset of the carrier of (MultGroup R) : ( X in conjugate_Classes (MultGroup R) & card X = 1 ) } ;
for x being object st x in { X where X is Subset of the carrier of (MultGroup R) : ( X in conjugate_Classes (MultGroup R) & card X = 1 ) } holds
x in conjugate_Classes (MultGroup R)
proof
let x be object ; :: thesis: ( x in { X where X is Subset of the carrier of (MultGroup R) : ( X in conjugate_Classes (MultGroup R) & card X = 1 ) } implies x in conjugate_Classes (MultGroup R) )
assume x in { X where X is Subset of the carrier of (MultGroup R) : ( X in conjugate_Classes (MultGroup R) & card X = 1 ) } ; :: thesis: x in conjugate_Classes (MultGroup R)
then ex y being Subset of the carrier of (MultGroup R) st
( x = y & y in conjugate_Classes (MultGroup R) & card y = 1 ) ;
hence x in conjugate_Classes (MultGroup R) ; :: thesis: verum
end;
then A9: { X where X is Subset of the carrier of (MultGroup R) : ( X in conjugate_Classes (MultGroup R) & card X = 1 ) } c= conjugate_Classes (MultGroup R) ;
then A10: conjugate_Classes (MultGroup R) = { X where X is Subset of the carrier of (MultGroup R) : ( X in conjugate_Classes (MultGroup R) & card X = 1 ) } \/ ((conjugate_Classes (MultGroup R)) \ { X where X is Subset of the carrier of (MultGroup R) : ( X in conjugate_Classes (MultGroup R) & card X = 1 ) } ) by XBOOLE_1:45;
consider f being Function such that
A11: dom f = the carrier of (center (MultGroup R)) and
A12: for x being object st x in the carrier of (center (MultGroup R)) holds
f . x = {x} from FUNCT_1:sch 3();
 A13: f is one-to-one
proof
let x1, x2 be object ; :: according to FUNCT_1:def 4 :: thesis: ( not x1 in dom f or not x2 in dom f or not f . x1 = f . x2 or x1 = x2 )
assume that
A14: x1 in dom f and
A15: x2 in dom f and
A16: f . x1 = f . x2 ; :: thesis: x1 = x2
A17: f . x1 = {x1} by A11, A12, A14;
f . x2 = {x2} by A11, A12, A15;
hence x1 = x2 by A16, A17, ZFMISC_1:3; :: thesis: verum
end;
now :: thesis: for x being object holds
( ( x in rng f implies x in { X where X is Subset of the carrier of (MultGroup R) : ( X in conjugate_Classes (MultGroup R) & card X = 1 ) } ) & ( x in { X where X is Subset of the carrier of (MultGroup R) : ( X in conjugate_Classes (MultGroup R) & card X = 1 ) } implies x in rng f ) )
let x be object ; :: thesis: ( ( x in rng f implies x in { X where X is Subset of the carrier of (MultGroup R) : ( X in conjugate_Classes (MultGroup R) & card X = 1 ) } ) & ( x in { X where X is Subset of the carrier of (MultGroup R) : ( X in conjugate_Classes (MultGroup R) & card X = 1 ) } implies x in rng f ) )
hereby :: thesis: ( x in { X where X is Subset of the carrier of (MultGroup R) : ( X in conjugate_Classes (MultGroup R) & card X = 1 ) } implies x in rng f )
assume x in rng f ; :: thesis: x in { X where X is Subset of the carrier of (MultGroup R) : ( X in conjugate_Classes (MultGroup R) & card X = 1 ) }
then consider xx being object such that
A18: xx in dom f and
A19: x = f . xx by FUNCT_1:def 3;
A20: x = {xx} by A11, A12, A18, A19;
A21: the carrier of (center (MultGroup R)) c= the carrier of (MultGroup R) by GROUP_2:def 5;
then reconsider X = x as Subset of the carrier of (MultGroup R) by A11, A18, A20, ZFMISC_1:31;
reconsider xx = xx as Element of (MultGroup R) by A11, A18, A21;
xx in center (MultGroup R) by A11, A18;
then con_class xx = {xx} by GROUP_5:81;
then A22: X in conjugate_Classes (MultGroup R) by A20;
card X = 1 by A20, CARD_1:30;
hence x in { X where X is Subset of the carrier of (MultGroup R) : ( X in conjugate_Classes (MultGroup R) & card X = 1 ) } by A22; :: thesis: verum
end;
assume x in { X where X is Subset of the carrier of (MultGroup R) : ( X in conjugate_Classes (MultGroup R) & card X = 1 ) } ; :: thesis: x in rng f
then consider X being Subset of the carrier of (MultGroup R) such that
A23: x = X and
A24: X in conjugate_Classes (MultGroup R) and
A25: card X = 1 ;
consider a being Element of the carrier of (MultGroup R) such that
A26: con_class a = X by A24;
A27: a in con_class a by GROUP_3:83;
consider xx being object such that
A28: X = {xx} by A25, CARD_2:42;
A29: a = xx by A26, A27, A28, TARSKI:def 1;
then a in center (MultGroup R) by A26, A28, GROUP_5:81;
then A30: a in the carrier of (center (MultGroup R)) ;
then f . a = {a} by A12;
hence x in rng f by A11, A23, A28, A29, A30, FUNCT_1:3; :: thesis: verum
end;
then rng f = { X where X is Subset of the carrier of (MultGroup R) : ( X in conjugate_Classes (MultGroup R) & card X = 1 ) } by TARSKI:2;
then A31: { X where X is Subset of the carrier of (MultGroup R) : ( X in conjugate_Classes (MultGroup R) & card X = 1 ) } , the carrier of (center (MultGroup R)) are_equipotent by A11, A13, WELLORD2:def 4;
card the carrier of (center (MultGroup R)) = natq1 by Th37;
then A32: card { X where X is Subset of the carrier of (MultGroup R) : ( X in conjugate_Classes (MultGroup R) & card X = 1 ) } = natq1 by A31, CARD_1:5;
consider f1 being FinSequence such that
A33: rng f1 = { X where X is Subset of the carrier of (MultGroup R) : ( X in conjugate_Classes (MultGroup R) & card X = 1 ) } and
A34: f1 is one-to-one by A9, FINSEQ_4:58;
consider f2 being FinSequence such that
A35: rng f2 = (conjugate_Classes (MultGroup R)) \ { X where X is Subset of the carrier of (MultGroup R) : ( X in conjugate_Classes (MultGroup R) & card X = 1 ) } and
A36: f2 is one-to-one by FINSEQ_4:58;
set f = f1 ^ f2;
A37: rng (f1 ^ f2) = conjugate_Classes (MultGroup R) by A10, A33, A35, FINSEQ_1:31;
now :: thesis: for x being object holds not x in { X where X is Subset of the carrier of (MultGroup R) : ( X in conjugate_Classes (MultGroup R) & card X = 1 ) } /\ ((conjugate_Classes (MultGroup R)) \ { X where X is Subset of the carrier of (MultGroup R) : ( X in conjugate_Classes (MultGroup R) & card X = 1 ) } )
given x being object such that A38: x in { X where X is Subset of the carrier of (MultGroup R) : ( X in conjugate_Classes (MultGroup R) & card X = 1 ) } /\ ((conjugate_Classes (MultGroup R)) \ { X where X is Subset of the carrier of (MultGroup R) : ( X in conjugate_Classes (MultGroup R) & card X = 1 ) } ) ; :: thesis: contradiction
A39: x in { X where X is Subset of the carrier of (MultGroup R) : ( X in conjugate_Classes (MultGroup R) & card X = 1 ) } by A38, XBOOLE_0:def 4;
x in (conjugate_Classes (MultGroup R)) \ { X where X is Subset of the carrier of (MultGroup R) : ( X in conjugate_Classes (MultGroup R) & card X = 1 ) } by A38, XBOOLE_0:def 4;
hence contradiction by A39, XBOOLE_0:def 5; :: thesis: verum
end;
then { X where X is Subset of the carrier of (MultGroup R) : ( X in conjugate_Classes (MultGroup R) & card X = 1 ) } /\ ((conjugate_Classes (MultGroup R)) \ { X where X is Subset of the carrier of (MultGroup R) : ( X in conjugate_Classes (MultGroup R) & card X = 1 ) } ) = {} by XBOOLE_0:def 1;
then rng f1 misses rng f2 by A33, A35, XBOOLE_0:def 7;
then A40: f1 ^ f2 is one-to-one FinSequence of conjugate_Classes (MultGroup R) by A34, A36, A37, FINSEQ_1:def 4, FINSEQ_3:91;
deffunc H1( set ) -> set = card (f1 . $1);
consider p1 being FinSequence such that
A41: ( len p1 = len f1 & ( for i being Nat st i in dom p1 holds
p1 . i = H1(i) ) ) from FINSEQ_1:sch 2();
 for x being object st x in rng p1 holds
x in NAT
proof
let x be object ; :: thesis: ( x in rng p1 implies x in NAT )
assume x in rng p1 ; :: thesis: x in NAT
then consider i being Nat such that
A42: i in dom p1 and
A43: p1 . i = x by FINSEQ_2:10;
A44: x = card (f1 . i) by A41, A42, A43;
i in dom f1 by A41, A42, FINSEQ_3:29;
then f1 . i in { X where X is Subset of the carrier of (MultGroup R) : ( X in conjugate_Classes (MultGroup R) & card X = 1 ) } by A33, FUNCT_1:3;
then ex X being Subset of the carrier of (MultGroup R) st
( f1 . i = X & X in conjugate_Classes (MultGroup R) & card X = 1 ) ;
hence x in NAT by A44; :: thesis: verum
end;
then rng p1 c= NAT ;
then reconsider c1 = p1 as FinSequence of NAT by FINSEQ_1:def 4;
A45: len c1 = natq1 by A32, A33, A34, A41, FINSEQ_4:62;
A46: for i being Element of NAT st i in dom c1 holds
c1 . i = 1
proof
let i be Element of NAT ; :: thesis: ( i in dom c1 implies c1 . i = 1 )
assume A47: i in dom c1 ; :: thesis: c1 . i = 1
i in dom f1 by A41, A47, FINSEQ_3:29;
then f1 . i in { X where X is Subset of the carrier of (MultGroup R) : ( X in conjugate_Classes (MultGroup R) & card X = 1 ) } by A33, FUNCT_1:3;
then ex X being Subset of the carrier of (MultGroup R) st
( f1 . i = X & X in conjugate_Classes (MultGroup R) & card X = 1 ) ;
hence c1 . i = 1 by A41, A47; :: thesis: verum
end;
for x being object st x in rng c1 holds
x in {1}
proof
let x be object ; :: thesis: ( x in rng c1 implies x in {1} )
assume x in rng c1 ; :: thesis: x in {1}
then ex i being Nat st
( i in dom c1 & x = c1 . i ) by FINSEQ_2:10;
then x = 1 by A46;
hence x in {1} by TARSKI:def 1; :: thesis: verum
end;
then A48: rng c1 c= {1} ;
for x being object st x in {1} holds
x in rng c1
proof
let x be object ; :: thesis: ( x in {1} implies x in rng c1 )
assume A49: x in {1} ; :: thesis: x in rng c1
A50: Seg (len c1) = dom c1 by FINSEQ_1:def 3;
then c1 . (len c1) = 1 by A5, A45, A46, FINSEQ_1:3;
then c1 . (len c1) = x by A49, TARSKI:def 1;
hence x in rng c1 by A5, A45, A50, FINSEQ_1:3, FUNCT_1:3; :: thesis: verum
end;
then {1} c= rng c1 ;
then rng c1 = {1} by A48, XBOOLE_0:def 10;
then c1 = (dom c1) --> 1 by FUNCOP_1:9;
then c1 = (Seg (len c1)) --> 1 by FINSEQ_1:def 3;
then c1 = (len c1) |-> 1 by FINSEQ_2:def 2;
then Sum c1 = (len c1) * 1 by RVSUM_1:80;
then A51: Sum c1 = natq1 by A32, A33, A34, A41, FINSEQ_4:62;
deffunc H2( set ) -> set = card (f2 . $1);
consider p2 being FinSequence such that
A52: ( len p2 = len f2 & ( for i being Nat st i in dom p2 holds
p2 . i = H2(i) ) ) from FINSEQ_1:sch 2();
 for x being object st x in rng p2 holds
x in NAT
proof
let x be object ; :: thesis: ( x in rng p2 implies x in NAT )
assume x in rng p2 ; :: thesis: x in NAT
then consider i being Nat such that
A53: i in dom p2 and
A54: p2 . i = x by FINSEQ_2:10;
A55: x = card (f2 . i) by A52, A53, A54;
i in dom f2 by A52, A53, FINSEQ_3:29;
then f2 . i in (conjugate_Classes (MultGroup R)) \ { X where X is Subset of the carrier of (MultGroup R) : ( X in conjugate_Classes (MultGroup R) & card X = 1 ) } by A35, FUNCT_1:3;
then f2 . i in conjugate_Classes (MultGroup R) by XBOOLE_0:def 5;
then consider a being Element of the carrier of (MultGroup R) such that
A56: con_class a = f2 . i ;
card (con_class a) is Element of NAT ;
hence x in NAT by A55, A56; :: thesis: verum
end;
then rng p2 c= NAT ;
then reconsider c2 = p2 as FinSequence of NAT by FINSEQ_1:def 4;
set c = c1 ^ c2;
reconsider c = c1 ^ c2 as FinSequence of NAT ;
len c = (len f1) + (len f2) by A41, A52, FINSEQ_1:22;
then A57: len c = len (f1 ^ f2) by FINSEQ_1:22;
for i being Element of NAT st i in dom c holds
c . i = card ((f1 ^ f2) . i)
proof
let i be Element of NAT ; :: thesis: ( i in dom c implies c . i = card ((f1 ^ f2) . i) )
assume A58: i in dom c ; :: thesis: c . i = card ((f1 ^ f2) . i)
now :: thesis: c . i = card ((f1 ^ f2) . i)
per cases ( i in dom c1 or ex j being Nat st
( j in dom c2 & i = (len c1) + j ) ) by A58, FINSEQ_1:25;
suppose A59: i in dom c1 ; :: thesis: c . i = card ((f1 ^ f2) . i)
then A60: i in dom f1 by A41, FINSEQ_3:29;
c . i = c1 . i by A59, FINSEQ_1:def 7
.= card (f1 . i) by A41, A59
.= card ((f1 ^ f2) . i) by A60, FINSEQ_1:def 7 ;
hence c . i = card ((f1 ^ f2) . i) ; :: thesis: verum
end;
suppose ex j being Nat st
( j in dom c2 & i = (len c1) + j ) ; :: thesis: c . i = card ((f1 ^ f2) . i)
then consider j being Nat such that
A61: j in dom c2 and
A62: i = (len c1) + j ;
A63: j in dom f2 by A52, A61, FINSEQ_3:29;
c . i = c2 . j by A61, A62, FINSEQ_1:def 7
.= card (f2 . j) by A52, A61
.= card ((f1 ^ f2) . i) by A41, A62, A63, FINSEQ_1:def 7 ;
hence c . i = card ((f1 ^ f2) . i) ; :: thesis: verum
end;
end;
end;
hence c . i = card ((f1 ^ f2) . i) ; :: thesis: verum
end;
then card (MultGroup R) = Sum c by A37, A40, A57, Th6;
then A64: ((card the carrier of (center R)) |^ (dim (VectSp_over_center R))) - 1 = (Sum c2) + ((card the carrier of (center R)) - 1) by A3, A51, RVSUM_1:75;
reconsider q = card the carrier of (center R) as non zero Element of NAT ;
reconsider n = dim (VectSp_over_center R) as non zero Element of NAT by Th32, ORDINAL1:def 12;
q in COMPLEX by XCMPLX_0:def 2;
then reconsider qc = q as Element of F_Complex by COMPLFLD:def 1;
set pnq = eval ((cyclotomic_poly n),qc);
reconsider pnq = eval ((cyclotomic_poly n),qc) as Integer by UNIROOTS:52;
reconsider abspnq = |.pnq.| as Element of NAT ;
q |^ n <> 0 by PREPOWER:5;
then (q |^ n) + 1 > 0 + 1 by XREAL_1:8;
then q |^ n >= 1 by NAT_1:13;
then (q |^ n) + (- 1) >= 1 + (- 1) by XREAL_1:7;
then reconsider qn1 = (q |^ n) - 1 as Element of NAT by INT_1:3;
pnq divides (q |^ n) - 1 by UNIROOTS:58;
then abspnq divides |.((q |^ n) - 1).| by INT_2:16;
then A65: abspnq divides qn1 by ABSVALUE:def 1;
for i being Element of NAT st i in dom c2 holds
abspnq divides c2 /. i
proof
let i be Element of NAT ; :: thesis: ( i in dom c2 implies abspnq divides c2 /. i )
assume A66: i in dom c2 ; :: thesis: abspnq divides c2 /. i
c2 . i = card (f2 . i) by A52, A66;
then A67: c2 /. i = card (f2 . i) by A66, PARTFUN1:def 6;
A68: i in dom f2 by A52, A66, FINSEQ_3:29;
then f2 . i in (conjugate_Classes (MultGroup R)) \ { X where X is Subset of the carrier of (MultGroup R) : ( X in conjugate_Classes (MultGroup R) & card X = 1 ) } by A35, FUNCT_1:3;
then f2 . i in conjugate_Classes (MultGroup R) by XBOOLE_0:def 5;
then consider a being Element of the carrier of (MultGroup R) such that
A69: con_class a = f2 . i ;
reconsider a = a as Element of (MultGroup R) ;
reconsider s = a as Element of R by UNIROOTS:19;
set ns = dim (VectSp_over_center s);
set ca = card (con_class a);
set oa = card (Centralizer a);
A70: card (MultGroup R) = ((card (con_class a)) * (card (Centralizer a))) + 0 by Th13;
then A71: (card (MultGroup R)) div (card (Centralizer a)) = card (con_class a) by NAT_D:def 1;
A72: qn1 div (card (Centralizer a)) = card (con_class a) by A3, A70, NAT_D:def 1;
q |^ (dim (VectSp_over_center s)) <> 0 by PREPOWER:5;
then (q |^ (dim (VectSp_over_center s))) + 1 > 0 + 1 by XREAL_1:8;
then q |^ (dim (VectSp_over_center s)) >= 1 by NAT_1:13;
then (q |^ (dim (VectSp_over_center s))) + (- 1) >= 1 + (- 1) by XREAL_1:7;
then reconsider qns1 = (q |^ (dim (VectSp_over_center s))) - 1 as Element of NAT by INT_1:3;
A73: card (Centralizer a) = (card the carrier of (centralizer s)) - 1 by Th30
.= qns1 by Th33 ;
reconsider ns = dim (VectSp_over_center s) as non zero Element of NAT by Th34, ORDINAL1:def 12;
A74: ns <= n by Th36, NAT_D:7;
now :: thesis: not ns = n
assume ns = n ; :: thesis: contradiction
then A75: card (f2 . i) = 1 by A3, A69, A71, A73, NAT_2:3;
A76: f2 . i in (conjugate_Classes (MultGroup R)) \ { X where X is Subset of the carrier of (MultGroup R) : ( X in conjugate_Classes (MultGroup R) & card X = 1 ) } by A35, A68, FUNCT_1:3;
then A77: f2 . i in conjugate_Classes (MultGroup R) by XBOOLE_0:def 5;
not f2 . i in { X where X is Subset of the carrier of (MultGroup R) : ( X in conjugate_Classes (MultGroup R) & card X = 1 ) } by A76, XBOOLE_0:def 5;
hence contradiction by A75, A77; :: thesis: verum
end;
then ns < n by A74, XXREAL_0:1;
then pnq divides qn1 div qns1 by Th36, UNIROOTS:59;
then abspnq divides |.(qn1 div qns1).| by INT_2:16;
hence abspnq divides c2 /. i by A67, A69, A72, A73, ABSVALUE:def 1; :: thesis: verum
end;
then abspnq divides natq1 by A64, A65, Th5, NAT_D:10;
hence contradiction by A4, A5, A8, NAT_D:7, UNIROOTS:60; :: thesis: verum