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 ();
set q = card the carrier of ();
set vR = VectSp_over_center R;
set n = dim ;
set Rs = MultGroup R;
set cR = the carrier of R;
set cRs = the carrier of ();
set cZs = the carrier of (center ());
A2: card R = (card the carrier of ()) |^ () by Th31;
then A3: card () = ((card the carrier of ()) |^ ()) - 1 by UNIROOTS:18;
A4: 1 < card the carrier of () by Th20;
A5: 1 + (- 1) < (card the carrier of ()) + (- 1) by ;
then reconsider natq1 = (card the carrier of ()) - 1 as Element of NAT by INT_1:3;
0 + 1 < () + 1 by ;
then A6: 1 <= dim by NAT_1:13;
now :: thesis: not dim = 1
assume A7: dim = 1 ; :: thesis: contradiction
card the carrier of R = (card the carrier of ()) #Z () by ;
then card the carrier of R = card the carrier of () by ;
hence contradiction by A1, Th21; :: thesis: verum
end;
then A8: 1 < dim by ;
set A = { X where X is Subset of the carrier of () : ( X in conjugate_Classes () & card X = 1 ) } ;
set B = () \ { X where X is Subset of the carrier of () : ( X in conjugate_Classes () & card X = 1 ) } ;
for x being object st x in { X where X is Subset of the carrier of () : ( X in conjugate_Classes () & card X = 1 ) } holds
x in conjugate_Classes ()
proof
let x be object ; :: thesis: ( x in { X where X is Subset of the carrier of () : ( X in conjugate_Classes () & card X = 1 ) } implies x in conjugate_Classes () )
assume x in { X where X is Subset of the carrier of () : ( X in conjugate_Classes () & card X = 1 ) } ; :: thesis:
then ex y being Subset of the carrier of () st
( x = y & y in conjugate_Classes () & card y = 1 ) ;
hence x in conjugate_Classes () ; :: thesis: verum
end;
then A9: { X where X is Subset of the carrier of () : ( X in conjugate_Classes () & card X = 1 ) } c= conjugate_Classes () ;
then A10: conjugate_Classes () = { X where X is Subset of the carrier of () : ( X in conjugate_Classes () & card X = 1 ) } \/ (() \ { X where X is Subset of the carrier of () : ( X in conjugate_Classes () & card X = 1 ) } ) by XBOOLE_1:45;
consider f being Function such that
A11: dom f = the carrier of (center ()) and
A12: for x being object st x in the carrier of (center ()) holds
f . x = {x} from 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 ;
f . x2 = {x2} by ;
hence x1 = x2 by ; :: 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 () : ( X in conjugate_Classes () & card X = 1 ) } ) & ( x in { X where X is Subset of the carrier of () : ( X in conjugate_Classes () & 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 () : ( X in conjugate_Classes () & card X = 1 ) } ) & ( x in { X where X is Subset of the carrier of () : ( X in conjugate_Classes () & card X = 1 ) } implies x in rng f ) )
hereby :: thesis: ( x in { X where X is Subset of the carrier of () : ( X in conjugate_Classes () & 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 () : ( X in conjugate_Classes () & 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 ()) c= the carrier of () by GROUP_2:def 5;
then reconsider X = x as Subset of the carrier of () by ;
reconsider xx = xx as Element of () by ;
xx in center () by ;
then con_class xx = {xx} by GROUP_5:81;
then A22: X in conjugate_Classes () by A20;
card X = 1 by ;
hence x in { X where X is Subset of the carrier of () : ( X in conjugate_Classes () & card X = 1 ) } by A22; :: thesis: verum
end;
assume x in { X where X is Subset of the carrier of () : ( X in conjugate_Classes () & card X = 1 ) } ; :: thesis: x in rng f
then consider X being Subset of the carrier of () such that
A23: x = X and
A24: X in conjugate_Classes () and
A25: card X = 1 ;
consider a being Element of the carrier of () 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 ;
A29: a = xx by ;
then a in center () by ;
then A30: a in the carrier of (center ()) ;
then f . a = {a} by A12;
hence x in rng f by ; :: thesis: verum
end;
then rng f = { X where X is Subset of the carrier of () : ( X in conjugate_Classes () & card X = 1 ) } by TARSKI:2;
then A31: { X where X is Subset of the carrier of () : ( X in conjugate_Classes () & card X = 1 ) } , the carrier of (center ()) are_equipotent by ;
card the carrier of (center ()) = natq1 by Th37;
then A32: card { X where X is Subset of the carrier of () : ( X in conjugate_Classes () & card X = 1 ) } = natq1 by ;
consider f1 being FinSequence such that
A33: rng f1 = { X where X is Subset of the carrier of () : ( X in conjugate_Classes () & card X = 1 ) } and
A34: f1 is one-to-one by ;
consider f2 being FinSequence such that
A35: rng f2 = () \ { X where X is Subset of the carrier of () : ( X in conjugate_Classes () & card X = 1 ) } and
A36: f2 is one-to-one by FINSEQ_4:58;
set f = f1 ^ f2;
A37: rng (f1 ^ f2) = conjugate_Classes () by ;
now :: thesis: for x being object holds not x in { X where X is Subset of the carrier of () : ( X in conjugate_Classes () & card X = 1 ) } /\ (() \ { X where X is Subset of the carrier of () : ( X in conjugate_Classes () & card X = 1 ) } )
given x being object such that A38: x in { X where X is Subset of the carrier of () : ( X in conjugate_Classes () & card X = 1 ) } /\ (() \ { X where X is Subset of the carrier of () : ( X in conjugate_Classes () & card X = 1 ) } ) ; :: thesis: contradiction
A39: x in { X where X is Subset of the carrier of () : ( X in conjugate_Classes () & card X = 1 ) } by ;
x in () \ { X where X is Subset of the carrier of () : ( X in conjugate_Classes () & card X = 1 ) } by ;
hence contradiction by A39, XBOOLE_0:def 5; :: thesis: verum
end;
then { X where X is Subset of the carrier of () : ( X in conjugate_Classes () & card X = 1 ) } /\ (() \ { X where X is Subset of the carrier of () : ( X in conjugate_Classes () & card X = 1 ) } ) = {} by XBOOLE_0:def 1;
then rng f1 misses rng f2 by ;
then A40: f1 ^ f2 is one-to-one FinSequence of conjugate_Classes () by ;
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 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:
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 ;
i in dom f1 by ;
then f1 . i in { X where X is Subset of the carrier of () : ( X in conjugate_Classes () & card X = 1 ) } by ;
then ex X being Subset of the carrier of () st
( f1 . i = X & X in conjugate_Classes () & 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 ;
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 ;
then f1 . i in { X where X is Subset of the carrier of () : ( X in conjugate_Classes () & card X = 1 ) } by ;
then ex X being Subset of the carrier of () st
( f1 . i = X & X in conjugate_Classes () & card X = 1 ) ;
hence c1 . i = 1 by ; :: 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 ;
then c1 . (len c1) = x by ;
hence x in rng c1 by ; :: thesis: verum
end;
then {1} c= rng c1 ;
then rng c1 = {1} by ;
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 ;
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 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:
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 ;
i in dom f2 by ;
then f2 . i in () \ { X where X is Subset of the carrier of () : ( X in conjugate_Classes () & card X = 1 ) } by ;
then f2 . i in conjugate_Classes () by XBOOLE_0:def 5;
then consider a being Element of the carrier of () such that
A56: con_class a = f2 . i ;
card () is Element of NAT ;
hence x in NAT by ; :: 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 ;
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 ;
suppose A59: i in dom c1 ; :: thesis: c . i = card ((f1 ^ f2) . i)
then A60: i in dom f1 by ;
c . i = c1 . i by
.= card (f1 . i) by
.= card ((f1 ^ f2) . i) by ;
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 ;
c . i = c2 . j by
.= card (f2 . j) by
.= card ((f1 ^ f2) . i) by ;
hence c . i = card ((f1 ^ f2) . i) ; :: thesis: verum
end;
end;
end;
hence c . i = card ((f1 ^ f2) . i) ; :: thesis: verum
end;
then card () = Sum c by A37, A40, A57, Th6;
then A64: ((card the carrier of ()) |^ ()) - 1 = (Sum c2) + ((card the carrier of ()) - 1) by ;
reconsider q = card the carrier of () as non zero Element of NAT ;
reconsider n = dim as non zero Element of NAT by ;
q in COMPLEX by XCMPLX_0:def 2;
then reconsider qc = q as Element of F_Complex by COMPLFLD:def 1;
set pnq = eval ((),qc);
reconsider pnq = eval ((),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 ;
then A67: c2 /. i = card (f2 . i) by ;
A68: i in dom f2 by ;
then f2 . i in () \ { X where X is Subset of the carrier of () : ( X in conjugate_Classes () & card X = 1 ) } by ;
then f2 . i in conjugate_Classes () by XBOOLE_0:def 5;
then consider a being Element of the carrier of () such that
A69: con_class a = f2 . i ;
reconsider a = a as Element of () ;
reconsider s = a as Element of R by UNIROOTS:19;
set ns = dim ;
set ca = card ();
set oa = card ();
A70: card () = ((card ()) * (card ())) + 0 by Th13;
then A71: (card ()) div (card ()) = card () by NAT_D:def 1;
A72: qn1 div (card ()) = card () by ;
q |^ () <> 0 by PREPOWER:5;
then (q |^ ()) + 1 > 0 + 1 by XREAL_1:8;
then q |^ () >= 1 by NAT_1:13;
then (q |^ ()) + (- 1) >= 1 + (- 1) by XREAL_1:7;
then reconsider qns1 = (q |^ ()) - 1 as Element of NAT by INT_1:3;
A73: card () = (card the carrier of ()) - 1 by Th30
.= qns1 by Th33 ;
reconsider ns = dim as non zero Element of NAT by ;
A74: ns <= n by ;
now :: thesis: not ns = n
assume ns = n ; :: thesis: contradiction
then A75: card (f2 . i) = 1 by ;
A76: f2 . i in () \ { X where X is Subset of the carrier of () : ( X in conjugate_Classes () & card X = 1 ) } by ;
then A77: f2 . i in conjugate_Classes () by XBOOLE_0:def 5;
not f2 . i in { X where X is Subset of the carrier of () : ( X in conjugate_Classes () & card X = 1 ) } by ;
hence contradiction by A75, A77; :: thesis: verum
end;
then ns < n by ;
then pnq divides qn1 div qns1 by ;
then abspnq divides |.(qn1 div qns1).| by INT_2:16;
hence abspnq divides c2 /. i by ; :: thesis: verum
end;
then abspnq divides natq1 by ;
hence contradiction by A4, A5, A8, NAT_D:7, UNIROOTS:60; :: thesis: verum