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;

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 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

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 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 H_{1}( 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 = H_{1}(i) ) )
from FINSEQ_1:sch 2();

for x being object st x in rng p1 holds

x in 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

x in {1}

for x being object st x in {1} holds

x in 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 H_{2}( 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 = H_{2}(i) ) )
from FINSEQ_1:sch 2();

for x being object st x in rng p2 holds

x in 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 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

hence contradiction by A4, A5, A8, NAT_D:7, UNIROOTS:60; :: thesis: verum

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;

now :: thesis: not dim (VectSp_over_center R) = 1

then A8:
1 < dim (VectSp_over_center R)
by A6, XXREAL_0:1;assume A7:
dim (VectSp_over_center R) = 1
; :: thesis: contradiction

card the carrier of R = (card the carrier of (center R)) #Z (dim (VectSp_over_center R)) by A2, PREPOWER:36;

then card the carrier of R = card the carrier of (center R) by A7, PREPOWER:35;

hence contradiction by A1, Th21; :: thesis: verum

end;card the carrier of R = (card the carrier of (center R)) #Z (dim (VectSp_over_center R)) by A2, PREPOWER:36;

then card the carrier of R = card the carrier of (center R) by A7, PREPOWER:35;

hence contradiction by A1, Th21; :: thesis: verum

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

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)
;
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;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

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;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

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 ) )

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;( ( 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 ) )

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;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 { X where X is Subset of the carrier of (MultGroup R) : ( X in conjugate_Classes (MultGroup R) & card X = 1 ) }
; :: thesis: x in rng fassume
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;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

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

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 ) } )

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;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;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

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 H

consider p1 being FinSequence such that

A41: ( len p1 = len f1 & ( for i being Nat st i in dom p1 holds

p1 . i = H

for x being object st x in rng p1 holds

x in NAT

proof

then
rng p1 c= NAT
;
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;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

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

for x being object st x in rng c1 holds
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;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

x in {1}

proof

then A48:
rng c1 c= {1}
;
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;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

for x being object st x in {1} holds

x in rng c1

proof

then
{1} c= rng c1
;
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;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

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 H

consider p2 being FinSequence such that

A52: ( len p2 = len f2 & ( for i being Nat st i in dom p2 holds

p2 . i = H

for x being object st x in rng p2 holds

x in NAT

proof

then
rng p2 c= NAT
;
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;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

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

then
card (MultGroup R) = Sum c
by A37, A40, A57, Th6;
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)

end;assume A58: i in dom c ; :: thesis: c . i = card ((f1 ^ f2) . i)

now :: thesis: c . i = card ((f1 ^ f2) . i)end;

hence
c . i = card ((f1 ^ f2) . i)
; :: thesis: verumper cases
( i in dom c1 or ex j being Nat st

( j in dom c2 & i = (len c1) + j ) ) by A58, FINSEQ_1:25;

end;

( 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;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

suppose
ex j being Nat st

( j in dom c2 & i = (len c1) + j ) ; :: thesis: c . i = card ((f1 ^ f2) . i)

( 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;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

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

then
abspnq divides natq1
by A64, A65, Th5, NAT_D:10;
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;

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;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

then
ns < n
by A74, XXREAL_0:1;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 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

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

hence contradiction by A4, A5, A8, NAT_D:7, UNIROOTS:60; :: thesis: verum