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 Th32;
then A3:
card (MultGroup R) = ((card the carrier of (center R)) |^ (dim (VectSp_over_center R))) - 1
by UNIROOTS:21;
A4:
1 < card the carrier of (center R)
by Th21;
A5:
1 + (- 1) < (card the carrier of (center R)) + (- 1)
by Th21, XREAL_1:10;
then reconsider natq1 = (card the carrier of (center R)) - 1 as Element of NAT by INT_1:16;
0 + 1 < (dim (VectSp_over_center R)) + 1
by Th33, XREAL_1:10;
then A6:
1 <= dim (VectSp_over_center R)
by NAT_1:13;
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 set 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)
by TARSKI:def 3;
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 set 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 let x be
set ;
:: 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
set such that A14:
xx in dom f
and A15:
x = f . xx
by FUNCT_1:def 5;
A16:
x = {xx}
by A11, A12, A14, A15;
A17:
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, A14, A16, ZFMISC_1:37;
reconsider xx =
xx as
Element of
(MultGroup R) by A11, A14, A17;
xx in center (MultGroup R)
by A11, A14, STRUCT_0:def 5;
then
con_class xx = {xx}
by GROUP_5:93;
then A18:
X in conjugate_Classes (MultGroup R)
by A16;
card X = 1
by A16, CARD_1:50;
hence
x in { X where X is Subset of the carrier of (MultGroup R) : ( X in conjugate_Classes (MultGroup R) & card X = 1 ) }
by A18;
:: 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 fthen consider X being
Subset of the
carrier of
(MultGroup R) such that A19:
x = X
and A20:
X in conjugate_Classes (MultGroup R)
and A21:
card X = 1
;
consider a being
Element of the
carrier of
(MultGroup R) such that A22:
con_class a = X
by A20;
A23:
a in con_class a
by GROUP_3:98;
consider xx being
set such that A24:
X = {xx}
by A21, CARD_2:60;
A25:
a = xx
by A22, A23, A24, TARSKI:def 1;
then
a in center (MultGroup R)
by A22, A24, GROUP_5:93;
then A26:
a in the
carrier of
(center (MultGroup R))
by STRUCT_0:def 5;
then
f . a = {a}
by A12;
hence
x in rng f
by A11, A19, A24, A25, A26, FUNCT_1:12;
:: 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 A27:
{ 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 Th38;
then A28:
card { X where X is Subset of the carrier of (MultGroup R) : ( X in conjugate_Classes (MultGroup R) & card X = 1 ) } = natq1
by A27, CARD_1:21;
{ X where X is Subset of the carrier of (MultGroup R) : ( X in conjugate_Classes (MultGroup R) & card X = 1 ) } is finite
by A9;
then consider f1 being FinSequence such that
A29:
rng f1 = { X where X is Subset of the carrier of (MultGroup R) : ( X in conjugate_Classes (MultGroup R) & card X = 1 ) }
and
A30:
f1 is one-to-one
by FINSEQ_4:73;
consider f2 being FinSequence such that
A31:
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
A32:
f2 is one-to-one
by FINSEQ_4:73;
set f = f1 ^ f2;
A33:
rng (f1 ^ f2) = conjugate_Classes (MultGroup R)
by A10, A29, A31, FINSEQ_1:44;
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 A29, A31, XBOOLE_0:def 7;
then A35:
f1 ^ f2 is one-to-one FinSequence of conjugate_Classes (MultGroup R)
by A30, A32, A33, FINSEQ_1:def 4, FINSEQ_3:98;
deffunc H1( set ) -> set = card (f1 . $1);
consider p1 being FinSequence such that
A36:
( 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 set st x in rng p1 holds
x in NAT
then
rng p1 c= NAT
by TARSKI:def 3;
then reconsider c1 = p1 as FinSequence of NAT by FINSEQ_1:def 4;
A43:
len c1 = natq1
by A28, A29, A30, A36, FINSEQ_4:77;
A44:
for i being Element of NAT st i in dom c1 holds
c1 . i = 1
for x being set st x in rng c1 holds
x in {1}
then A47:
rng c1 c= {1}
by TARSKI:def 3;
for x being set st x in {1} holds
x in rng c1
then
{1} c= rng c1
by TARSKI:def 3;
then
rng c1 = {1}
by A47, XBOOLE_0:def 10;
then
c1 = (dom c1) --> 1
by FUNCOP_1:15;
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:110;
then A50:
Sum c1 = natq1
by A28, A29, A30, A36, FINSEQ_4:77;
deffunc H2( set ) -> set = card (f2 . $1);
consider p2 being FinSequence such that
A51:
( 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 set st x in rng p2 holds
x in NAT
then
rng p2 c= NAT
by TARSKI:def 3;
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 A36, A51, FINSEQ_1:35;
then A57:
len c = len (f1 ^ f2)
by FINSEQ_1:35;
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 A33, A35, 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, A50, RVSUM_1:105;
reconsider q = card the carrier of (center R) as non empty Element of NAT ;
reconsider n = dim (VectSp_over_center R) as non empty Element of NAT by Th33, ORDINAL1:def 13;
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:56;
reconsider abspnq = abs pnq as Element of NAT ;
q |^ n <> 0
by PREPOWER:12;
then
q |^ n > 0
;
then
(q |^ n) + 1 > 0 + 1
by XREAL_1:10;
then
q |^ n >= 1
by NAT_1:13;
then
(q |^ n) + (- 1) >= 1 + (- 1)
by XREAL_1:9;
then reconsider qn1 = (q |^ n) - 1 as Element of NAT by INT_1:16;
pnq divides (q |^ n) - 1
by UNIROOTS:62;
then
abspnq divides abs ((q |^ n) - 1)
by INT_2:21;
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 A51, A66;
then A67:
c2 /. i = card (f2 . i)
by A66, PARTFUN1:def 8;
A68:
i in dom f2
by A51, A66, FINSEQ_3:31;
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 A31, FUNCT_1:12;
then
(
f2 . i in conjugate_Classes (MultGroup R) & 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 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:22;
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;
A72:
(card (MultGroup R)) div (card (Centralizer a)) = card (con_class a)
by A70, NAT_D:def 1;
A73:
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:12;
then
q |^ (dim (VectSp_over_center s)) > 0
;
then
(q |^ (dim (VectSp_over_center s))) + 1
> 0 + 1
by XREAL_1:10;
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:9;
then reconsider qns1 =
(q |^ (dim (VectSp_over_center s))) - 1 as
Element of
NAT by INT_1:16;
A74:
card (Centralizer a) =
(card the carrier of (centralizer s)) - 1
by Th31
.=
qns1
by Th34
;
reconsider ns =
dim (VectSp_over_center s) as non
empty Element of
NAT by Th35, ORDINAL1:def 13;
A75:
ns <= n
by Th37, NAT_D:7;
then
ns < n
by A75, XXREAL_0:1;
then
pnq divides qn1 div qns1
by Th37, UNIROOTS:63;
then
abspnq divides abs (qn1 div qns1)
by INT_2:21;
hence
abspnq divides c2 /. i
by A67, A69, A73, A74, ABSVALUE:def 1;
:: thesis: verum
end;
then
abspnq divides Sum c2
by Th5;
then
abspnq divides natq1
by A64, A65, NAT_D:10;
hence
contradiction
by A4, A5, A8, NAT_D:7, UNIROOTS:64; :: thesis: verum