let R be finite Skew-Field; R is commutative
assume A1:
not R is commutative
; 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)
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
now 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 ;
( ( 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 ( 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
;
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;
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 ) }
;
x in rng fthen 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;
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;
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
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
for x being object st x in rng c1 holds
x in {1}
then A48:
rng c1 c= {1}
;
for x being object st x in {1} holds
x in rng c1
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
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)
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 ;
( i in dom c2 implies abspnq divides c2 /. i )
assume A66:
i in dom c2
;
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;
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;
verum
end;
then
abspnq divides natq1
by A64, A65, Th5, NAT_D:10;
hence
contradiction
by A4, A5, A8, NAT_D:7, UNIROOTS:60; verum