Copyright (c) 2003 Association of Mizar Users
environ
vocabulary WEDDWITT, ARYTM_1, ARYTM_3, FINSEQ_1, RELAT_1, FUNCT_1, RLVECT_1,
BOOLE, FINSEQ_2, FINSEQ_4, COMPLEX1, BINOP_1, VECTSP_1, LATTICES,
COMPLFLD, GROUP_1, REALSET1, INT_1, NAT_1, TARSKI, CARD_1, GROUP_2,
POLYNOM2, FUNCT_4, VECTSP_2, FUNCOP_1, SEQ_1, FUNCT_2, ABSVALUE,
UNIROOTS, PREPOWER, FINSET_1, CAT_1, RLSUB_1, GROUP_5, RLVECT_2,
SETFAM_1, VECTSP_9, RLVECT_3, MATRLIN, SUBSET_1, EQREL_1, GROUP_3;
notation TARSKI, XBOOLE_0, SUBSET_1, STRUCT_0, NUMBERS, ARYTM_0, XREAL_0,
ZFMISC_1, REAL_1, INT_1, INT_2, NAT_1, RLVECT_1, VECTSP_1, VECTSP_2,
BINOP_1, RELAT_1, FUNCT_1, FUNCT_2, FINSEQ_1, FINSEQ_2, FINSEQ_4,
BINARITH, RVSUM_1, COMPLFLD, POLYNOM4, CARD_1, GROUP_2, PREPOWER,
FINSET_1, GROUP_1, FUNCT_4, CQC_LANG, WSIERP_1, UNIROOTS, SETFAM_1,
VECTSP_6, VECTSP_7, GROUP_3, GROUP_5, VECTSP_9, EQREL_1, FRAENKEL,
FUNCOP_1, VECTSP_4, EULER_2;
constructors ARYTM_0, REAL_1, MONOID_0, WELLORD2, INT_2, COMPLSP1, BINARITH,
POLYNOM4, COMPLEX1, POLYNOM5, PREPOWER, DOMAIN_1, PRE_CIRC, FINSEQOP,
ALGSTR_1, RLVECT_2, CQC_LANG, WSIERP_1, UPROOTS, UNIROOTS, BINOP_1,
VECTSP_6, VECTSP_7, VECTSP_9, GROUP_5, EQREL_1, EULER_2;
clusters STRUCT_0, RELSET_1, BINARITH, VECTSP_1, VECTSP_2, FINSEQ_2, POLYNOM1,
MONOID_0, NAT_1, INT_1, POLYNOM5, FINSEQ_1, FINSET_1, CARD_1, FSM_1,
FUNCT_1, NUMBERS, SUBSET_1, ORDINAL2, CQC_LANG, UNIROOTS, GROUP_2,
REAL_1, FUNCOP_1;
requirements NUMERALS, BOOLE, SUBSET, ARITHM, REAL;
definitions TARSKI, VECTSP_1, FUNCT_1, RLVECT_1;
theorems GROUP_1, CARD_1, FINSEQ_1, ZFMISC_1, NAT_1, FUNCT_1, FUNCT_2,
RELAT_1, TARSKI, XBOOLE_0, XBOOLE_1, VECTSP_1, PREPOWER, RELSET_1,
COMPLFLD, BINOP_1, REAL_1, XCMPLX_1, REAL_2, INT_1, XCMPLX_0, SCMFSA_7,
AMI_5, AXIOMS, RVSUM_1, FINSEQ_3, FINSEQ_2, FINSEQ_4, INT_2, SCMFSA9A,
SCPINVAR, ABSVALUE, WSIERP_1, NAT_2, PEPIN, FUNCT_7, RLVECT_1, NEWTON,
FINSET_1, CARD_4, FUNCOP_1, VECTSP_2, CARD_2, GRAPH_5, SUBSET_1,
CQC_LANG, WELLORD2, EULER_2, FUNCT_5, AFINSQ_1, FUNCT_4, GROUP_2,
VECTSP_4, VECTSP_7, VECTSP_9, EQREL_1, SETFAM_1, GROUP_3, FRAENKEL,
VECTSP_6, GROUP_5, UNIROOTS;
schemes NAT_1, FUNCT_1, FUNCT_2, FINSEQ_1;
begin :: Preliminaries
theorem Th1: :: Th1:
for a being Nat, q being Real st 1 < q & q |^ a = 1 holds a = 0
proof let a be Nat, q be Real such that
X0: 1 < q and
X1: (q |^ a) = 1 and
A3: a <> 0;
a < 1 + 1 by X0,X1, PREPOWER:21; then
A1: a <= 0 + 1 by NAT_1:38;
0 < a by A3, NAT_1:19; then a = 1 by A1, NAT_1:26; then
A4: (q #Z a) = q by PREPOWER:45;
q <> 0 by X0;
hence contradiction by X0,X1,PREPOWER:46,A4;
end;
theorem Th2: :: Th2:
for a, k, r being Nat, x being Real
st 1 < x & 0 < k holds x |^ (a*k + r) = (x |^ a)*(x |^ (a*(k-'1)+r))
proof let a,k,r be Nat, x be Real such that
A1: 1 < x and
A2: 0 < k;
A3: 0 <> x by A1;
set xNak = x |^ (a*k + r);
0+1 <= k by NAT_1:38, A2; then k = k-'1+1 by AMI_5:4; then
xNak = (x |^ (a*(k-'1)+a*1 + r)) by XCMPLX_1:8; then
xNak = (x #Z (a + a*(k-'1) + r)) by A3,PREPOWER:46; then
xNak = (x #Z (a + (a*(k-'1)+r))) by XCMPLX_1:1; then
xNak = (x #Z a)*(x #Z (a*(k-'1)+r)) by A3,PREPOWER:54; then
xNak = (x |^ a)*(x #Z (a*(k-'1)+r)) by PREPOWER:46,A3;
hence thesis by PREPOWER:46,A3;
end;
theorem Th3: :: Th3:
for q, a, b being Nat
st 0 < a & 1 < q & (q |^ a) -' 1 divides (q |^ b)-'1 holds a divides b
proof let q,a,b be Nat such that
X1: 0 < a and
X2: 1 < q and
X3: (q |^ a)-'1 divides (q |^ b)-'1;
X4: 0 <> q by X2; then
X5: 0 < q by NAT_1:19;
set r = b mod a; set qNa = q |^ a; set qNr = q |^ r;
defpred P[Nat] means qNa-'1 divides (q |^ (a*$1 + r))-'1;
A1: b = a*(b div a) + r by NAT_1:47, X1; then
A2: ex k being Nat st P[k] by X3;
consider k being Nat such that
A4a: P[k] and
A4b: for n being Nat st P[n] holds k <= n from Min(A2);
now per cases;
suppose B0: k = 0;
B1: now assume A6: 0 <> qNr-'1; then
B2: 0 < qNr-'1 by NAT_1:19; qNr <> 0 by NAT_2:10, A6; then
B3: 0 < qNr by NAT_1:19; r < a by NAT_1:46, X1;
then consider m being Nat such that
C2: a = r + m by NAT_1:28;
C3: m <> 0 by X1,NAT_1:46, C2;
C5: (q |^ (r + m)) = (q #Z (r + m)) by PREPOWER:46, X4;
C6: (q #Z (r + m)) = (q #Z r)*(q #Z m) by PREPOWER:54,X4;
C7: (q #Z r) = (q |^ r) by X4, PREPOWER:46;
C8: (q #Z m) = (q |^ m) by X4, PREPOWER:46;
0 < q by X4,NAT_1:19; then
C9: (q #Z r) > 0 by PREPOWER:49;
C10:(q |^ m) >= 1 by X2,PREPOWER:19;
(q |^ m) <> 1 by X2,C3,Th1; then
(q |^ m) > 1 by C10,REAL_1:def 5; then
JJ: qNr < qNa by REAL_2:144,C2,C7,C8,C6,C9,C5; then
0 < qNa by B3,AXIOMS:22; then 0+1 <= qNa by NAT_1:38; then
qNa-'1 = qNa-1 by SCMFSA_7:3; then
LL: qNa-'1 = qNa+(-1) by XCMPLX_0:def 8;
0+1 <= qNr by NAT_1:38,B3; then qNr-'1 = qNr-1 by SCMFSA_7:3;
then qNr-'1 = qNr+(-1) by XCMPLX_0:def 8; then
qNr-'1 < qNa-'1 by JJ,LL,REAL_1:67;
hence contradiction by B2, NAT_1:54,A4a,B0;
end; 0 < qNr by PREPOWER:13, X5; then 0+1<=qNr by NAT_1:38; then
JJ: qNr-1+1 = 1 by B1, SCMFSA_7:3; qNr-1+1 = qNr+1-1 by XCMPLX_1:29;
then qNr = 0 + 1 by JJ, XCMPLX_1:26; then r = 0 by Th1, X2;
hence a divides b by A1, NAT_1:49;
suppose B0: k <> 0; then
TT0: 0 < k by NAT_1:19; consider j being Nat such that
B1: k = j + 1 by B0, NAT_1:22;
TT2: k-1 = j by XCMPLX_1:26,B1; 0+1<=k by TT0,NAT_1:38; then
TT1: k-'1 = j by TT2,SCMFSA_7:3;
set qNaj = (q |^ (a*j + r)); set qNak = (q |^ (a*k + r));
set qNak1= (q |^ (a*(k-'1)+r));
j < k by REAL_1:69, B1; then
B2: not qNa-'1 divides qNaj-'1 by A4b;
Y3: (qNa-'1) divides (qNak-'1 qua Integer) by A4a, SCPINVAR:2;
(qNa-'1) divides -(qNa-'1) by INT_2:14; then
(qNa-'1) divides (qNak-'1)+(-(qNa-'1)) by Y3, WSIERP_1:9; then
G0: (qNa-'1) divides (qNak-'1) - (qNa-'1) by XCMPLX_0:def 8;
Y1: 0 < qNak by PREPOWER:13,X5;
Y2: 0 < qNa by PREPOWER:13,X5; 0+1<=qNak by NAT_1:38,Y1; then
Y3: (qNak-'1)=(qNak-1) by SCMFSA_7:3;
0+1<=qNa by NAT_1:38,Y2; then
G1: (qNak-'1)-(qNa-'1)=(qNak-1)-(qNa-1) by Y3,SCMFSA_7:3;
(qNak-1) - (qNa-1) = qNak-qNa by XCMPLX_1:22; then
(qNak-1) - (qNa-1) = qNa*qNak1-qNa*1 by Th2,X2,TT0; then
Y5: (qNak-'1)-(qNa-'1) = qNa*(qNak1-1) by G1,XCMPLX_1:40;
0 < qNak1 by X5,PREPOWER:13; then 0+1<= qNak1 by NAT_1:38; then
G2: (qNak-'1)-(qNa-'1)= qNa*(qNak1-'1) by Y5,SCMFSA_7:3;
0 < qNa by PREPOWER:13,X5; then 0+1 <= qNa by NAT_1:38; then
qNa-'1+1 = qNa by AMI_5:4; then
qNa-'1,qNa are_relative_prime by PEPIN:1; then
(qNa-'1 qua Integer),qNa are_relative_prime by EULER_2:1; then
(qNa-'1 qua Integer) divides qNak1-'1 by G0,G2,INT_2:40;
hence a divides b by B2,TT1,SCPINVAR:2;
end;
hence thesis;
end;
theorem Lm1: :: Lm1:
for n, q being Nat st 0 < q holds Card Funcs(n,q) = q |^ n
proof let n,q be Nat such that B0: 0 < q;
defpred P[Nat] means Card Funcs($1,q) = q|^$1;
P0: P[0] proof Funcs({},q) = {{}} by FUNCT_5:64;
hence Card Funcs(0,q) = 1 by CARD_1:79 .= q #Z 0 by PREPOWER:44
.= q |^ 0 by B0,PREPOWER:46;
end;
P1: for n being Nat st P[n] holds P[n+1]
proof let n be Nat such that
A0: P[n];
reconsider q' = q as non empty set by B0;
defpred R[set, set] means
ex x being Function of n+1,q st $1 = x & $2 = x | n;
PP: for x being set st x in Funcs(n+1,q')
ex y being set st y in Funcs(n,q') & R[x,y]
proof let x be set such that C0: x in Funcs(n+1,q');
consider f being Function such that
C1: x = f and C2: dom f = n+1 & rng f c= q' by C0,FUNCT_2:def 2;
reconsider f as Function of n+1,q' by C2,FUNCT_2:4;
not n in n; then
C6: n misses {n} by ZFMISC_1:56;
(n+1) /\ n = (n \/ {n}) /\ n by AFINSQ_1:4; then
(n+1) /\ n = (n /\ n) \/ ({n} /\ n) by XBOOLE_1:23; then
(n+1) /\ n = n \/ {} by C6,XBOOLE_0:def 7; then
C3: dom (f|n) = n by C2,FUNCT_1:68;
rng (f|n) c= rng f by FUNCT_1:76; then
rng (f|n) c= q' by C2,XBOOLE_1:1; then
(f|n) in Funcs(n,q') by C3, FUNCT_2:def 2;
hence thesis by C1;
end;
consider G being Function of Funcs(n+1,q'), Funcs(n,q') such that
A1: for x being set st x in Funcs(n+1,q') holds R[x,G.x] from FuncEx1(PP);
A2: rng G = Funcs(n,q') proof
C0: rng G c= Funcs(n,q') by RELSET_1:12;
for x being set st x in Funcs(n,q')
holds x in rng G
proof let x be set such that D0: x in Funcs(n,q');
not (not ex y being set st y in q') by XBOOLE_0:def 1; then
consider y being set such that V0: y in q';
reconsider g=x as Element of Funcs(n,q') by D0;
set fx = g+* (n .--> y);
LF: for y being set st y in q holds g +* (n .--> y) in (G"{g})
proof let y be set such that D0: y in q;
consider f being Function such that
D1: f = g+*(n.-->y);
D9: dom g = n & dom (n.-->y) = {n} by FUNCT_2:def 1,CQC_LANG:5; then
dom f = n \/ {n} by D1,FUNCT_4:def 1; then
D3: dom f = n+1 by AFINSQ_1:4;
rng (n.-->y) = {y} by CQC_LANG:5; then
D5: rng f c= (rng g \/ {y}) by D1,FUNCT_4:18;
consider gg being Function such that
Z7: gg = g & dom gg = n & rng gg c= q by FUNCT_2:def 2;
Z8: rng g c= q & y in q by D0, Z7; then
{y} c= q by ZFMISC_1:37; then
(rng g \/ {y}) c= q by Z8,XBOOLE_1:8; then
rng f c= q by D5,XBOOLE_1:1; then
D2: f in Funcs(n+1,q) by D3,FUNCT_2:def 2; then
reconsider f as Function of n+1,q by FUNCT_2:121;
not n in n; then n misses {n} by ZFMISC_1:56; then
D4: f|n = g by D1,D9,FUNCT_4:34; R[f,G.f] by A1,D2; then
G1: G.f in {x} by D4,TARSKI:def 1;
dom G = Funcs(n+1,q) by FUNCT_2:def 1;
hence thesis by D1,D2,G1,FUNCT_1:def 13;
end;
g +* (n .--> y) in (G"{g}) by V0,LF; then
consider b being set such that
D3: b in rng G & [fx,b] in G & b in {g} by RELAT_1:166;
D4: b in rng G & fx in dom G & G.fx = b by D3,FUNCT_1:8;
dom G = Funcs(n+1,q') by FUNCT_2:def 1; then
fx in Funcs(n+1,q') by D4; then
R[fx,G.fx] by A1; then G.fx = fx|n; then
D5: fx|n = b by D4;
D6: dom g = n & dom (n .--> y) = {n} by FUNCT_2:def 1, CQC_LANG:5;
not n in n; then n misses {n} by ZFMISC_1:56; then
fx|n = x by FUNCT_4:34,D6; then b = x by D5;
hence x in rng G by D4;
end; then C1: Funcs(n,q') c= rng G by TARSKI:def 3;
thus thesis by C0,C1,XBOOLE_0:def 10;
end;
A3: for x being Element of Funcs(n,q')
holds G"{x} is finite & Card (G"{x}) = q
proof let x be Element of Funcs(n,q');
deffunc HH(set) = x +* (n .--> $1);
LF: for y being set st y in q holds HH(y) in (G"{x})
proof let y be set such that D0: y in q;
consider f being Function such that
D1: f = x+*(n.-->y);
D9: dom x = n & dom (n.-->y) = {n} by FUNCT_2:def 1,CQC_LANG:5; then
dom f = n \/ {n} by D1,FUNCT_4:def 1; then
D3: dom f = n+1 by AFINSQ_1:4;
rng (n.-->y) = {y} by CQC_LANG:5; then
D5: rng f c= (rng x \/ {y}) by D1,FUNCT_4:18;
consider gg being Function such that
Z7: gg = x & dom gg = n & rng gg c= q by FUNCT_2:def 2;
Z8: rng x c= q & y in q by D0, Z7; then
{y} c= q by ZFMISC_1:37; then
(rng x \/ {y}) c= q by Z8,XBOOLE_1:8; then
rng f c= q by D5,XBOOLE_1:1; then
D2: f in Funcs(n+1,q) by D3,FUNCT_2:def 2; then
reconsider f as Function of n+1,q by FUNCT_2:121;
not n in n; then n misses {n} by ZFMISC_1:56; then
D4: f|n = x by D1,D9,FUNCT_4:34; R[f,G.f] by A1,D2; then
G1: G.f in {x} by D4,TARSKI:def 1;
dom G = Funcs(n+1,q) by FUNCT_2:def 1;
hence thesis by D1,D2,G1,FUNCT_1:def 13;
end;
consider H being Function of q, (G"{x}) such that
C0: for y being set st y in q holds H.y = HH(y) from Lambda1(LF);
C1: for c being set st c in G"{x} ex y being set st y in q & H.y = c
proof let c be set; assume
D0: c in G"{x}; c in Funcs(n+1,q) by D0;
then consider f being Function of n+1,q' such that
D0a: c = f and
D0b: G.c = f|n by A1;
take y = f.n;
c in dom G & G.c in {x} by D0,FUNCT_1:def 13; then
D1: G.c = x by TARSKI:def 1;
n+1 = n \/ {n} by AFINSQ_1:4; then
dom f = n \/ {n} by FUNCT_2:def 1; then
D2: f = f|n +* (n .--> (f.n)) by FUNCT_7:15;
n in n+1 by AFINSQ_1:1;
hence y in q by FUNCT_2:7;
hence H.y = c by C0, D1, D2, D0a, D0b;
end;
x in rng G by A2; then
{x}<>{} & {x} c= rng G by ZFMISC_1:37; then
CC: G"{x} <> {} by RELAT_1:174; then
C3: rng H = G"{x} by C1,FUNCT_2:16;
C5: dom H = q by CC,FUNCT_2:def 1; then
C6: q c= dom H;
for x1,x2 being set st x1 in dom H & x2 in dom H & H.x1 = H.x2
holds x1 = x2
proof let x1,x2 be set such that
D0: x1 in dom H and D1: x2 in dom H and D2: H.x1 = H.x2;
D3: H.x1 = x +* (n .--> x1) by C0,C5,D0;
D4: H.x2 = x +* (n .--> x2) by C0,C5,D1;
D5: dom x = n by FUNCT_2:def 1;
D6: dom (n .--> x1) = {n} & dom (n .--> x2) = {n} by CQC_LANG:5;
set fx1 = x +* (n .--> x1);
set fx2 = x +* (n .--> x2);
n+1 = n \/ {n} by AFINSQ_1:4; then
D7: dom fx1 = n+1 & dom fx2 = n+1 by D5,D6,FUNCT_4:def 1;
Z1: fx1 = fx2 by D3,D4,D2;
_Z3: (n .--> x1).n = x1 & (n .--> x2).n = x2 by CQC_LANG:6;
Z4: n in {n} by TARSKI:def 1;
Z2a:fx1.n = x1 by _Z3, Z4,D6,FUNCT_4:14;
Z2b:fx2.n = x2 by _Z3, Z4,D6,FUNCT_4:14;
D8: n in dom fx1 & n in dom fx2 by AFINSQ_1:1,D7; then
[n,x1] in fx1 by Z2a,FUNCT_1:def 4; then
D9: [n,x1] in fx2 by Z1;
[n,x2] in fx2 by Z2b,D8,FUNCT_1:def 4;
hence thesis by D9,FUNCT_1:def 1;
end;
then H is one-to-one by FUNCT_1:def 8;
then q, H.:q are_equipotent by C6,CARD_1:60;
then q, rng H are_equipotent by C5,RELAT_1:146;
then q, G"{x} are_equipotent by C3;
then Card (G"{x}) = Card q by CARD_1:21; then
B5: Card (G"{x}) = q by CARD_1:66;
G"{x} is finite by B5,CARD_4:1;
hence thesis by B5;
end;
A4: for x,y being set st x is Element of Funcs(n,q') &
y is Element of Funcs(n,q') & x<>y holds (G"{x}) misses (G"{y})
proof let x,y be set such that x is Element of Funcs(n,q') and
y is Element of Funcs(n,q') and C2: x <> y;
now assume not (G"{x}) misses (G"{y}); then
not (G"{x}) /\ (G"{y}) = {} by XBOOLE_0:def 7; then
consider f being set such that
D2: f in (G"{x} /\ G"{y}) by XBOOLE_0:def 1;
f in G"{x} by D2,XBOOLE_0:def 3; then
D3: f in dom G & G.f in {x} by FUNCT_1:def 13; then
f in Funcs(n+1,q) by FUNCT_2:def 1; then
reconsider f as Function of n+1,q by FUNCT_2:121;
f in Funcs(n+1,q) by B0, FUNCT_2:11; then R[f, G.f] by A1; then
D4: G.f = f|n; then
D5: f|n = x by D3, TARSKI:def 1;
f in G"{y} by D2,XBOOLE_0:def 3; then
G.f in {y} by FUNCT_1:def 13; then f|n = y by D4, TARSKI:def 1;
hence contradiction by C2,D5;
end;
hence thesis;
end;
reconsider X = {G"{x} where x is Element of Funcs(n,q'):
not contradiction} as set;
A6: union X = Funcs(n+1,q) proof
C0: for y being set holds y in union X implies y in Funcs(n+1,q)
proof let x be set such that B0: x in union X;
consider Y being set such that
B1: x in Y and B2: Y in X by B0,TARSKI:def 4;
consider z being Element of Funcs(n,q) such that
B3: G"{z} = Y by B2;
thus thesis by B1,B3;
end;
for y being set holds y in Funcs(n+1,q) implies y in union X
proof let x be set such that B1: x in Funcs(n+1,q);
consider f being Function of n+1,q such that
D0: x = f & G.x = f|n by A1,B1;
D2: f in Funcs(n+1,q) by B0,FUNCT_2:11;
dom G = Funcs(n+1,q) by FUNCT_2:def 1; then
f in dom G & G.f in {f|n} by D0,D2,TARSKI:def 1; then
D3: f in G"{f|n} by FUNCT_1:def 13;
consider y being set such that
D4: y in Funcs(n,q') & R[f,y] by D2,PP;
G"{f|n} in X by D4;
hence thesis by D0,D3,TARSKI:def 4;
end;hence thesis by C0,TARSKI:2;
end; Funcs(n+1,q) is finite by FRAENKEL:16; then
reconsider X as finite set by A6,FINSET_1:25;
A5: card X = q|^n proof
deffunc FF(set) = G"{$1};
LF: for x being set st x in Funcs(n,q) holds FF(x) in X;
consider F being Function of Funcs(n,q),X such that
C0: for x being set st x in Funcs(n,q) holds F.x = FF(x)
from Lambda1(LF);
C1: for c being set st c in X ex x being set st
x in Funcs(n,q) & c = F.x
proof let c be set such that D0: c in X;
consider y being Element of Funcs(n,q) such that
D1: c = G"{y} by D0; F.y = c by C0,D1;
hence thesis;
end;
consider gg being Element of Funcs(n, q');
G"{gg} in X; then
CC: X <> {}; then
C3: rng F = X by C1,FUNCT_2:16;
C5: dom F = Funcs(n,q) by CC,FUNCT_2:def 1; then
C6: Funcs(n,q) c= dom F;
for x1,x2 being set st x1 in dom F & x2 in dom F & F.x1 = F.x2
holds x1 = x2
proof let x1,x2 be set such that
D0: x1 in dom F and D1: x2 in dom F and D2: F.x1 = F.x2;
D8: x1 in Funcs(n,q) by C5, D0; then
D3: F.x1 = G"{x1} by C0;
D9: x2 in Funcs(n,q) by C5, D1; then
D5: G"{x1} = G"{x2} by C0,D2,D3;
now assume E0: x1<>x2;
(G"{x1}) misses (G"{x2}) by A4, E0, D8,D9; then
E3: G"{x1} /\ G"{x1} = {} by D5,XBOOLE_0:def 7;
G"{x1} = {} by E3; then
q = 0 by D8,A3,CARD_1:78;
hence contradiction by E3;
end;
hence thesis;
end; then
F is one-to-one by FUNCT_1:def 8;
then Funcs(n,q), F.:(Funcs(n,q)) are_equipotent by C6,CARD_1:60;
then Funcs(n,q), rng F are_equipotent by C5,RELAT_1:146;
then Funcs(n,q), X are_equipotent by C3;
hence card X = q|^n by CARD_1:21,A0;
end;
(for Y being set st Y in X ex B being finite set st B = Y & card B=q &
for Z being set st Z in X & Y <> Z
holds Y,Z are_equipotent & Y misses Z)
proof let Y be set such that B0: Y in X;
consider x being Element of Funcs(n,q') such that
C0: Y=G"{x} by B0;
C1: Y is finite & Card Y = q by A3,C0; then
B1: ex B being finite set st B = Y & card B=q;
B2: for Z being set st Z in X & Y <> Z
holds Y,Z are_equipotent & Y misses Z
proof let Z be set such that D0: Z in X and D1: Y <> Z;
consider y being Element of Funcs(n,q') such that
D2: Z=G"{y} by D0;
D3: Z is finite & Card Z = q by A3,D2;
D4: Y,Z are_equipotent by D3,C1,CARD_1:21;
now per cases;
suppose x=y; hence Y misses Z by D1,D2,C0;
suppose x<>y;hence Y misses Z by D2,C0,A4;
end;hence thesis by D4;
end;thus thesis by B1,B2;
end;
then consider C being finite set such that
A9: C = union X & card C = q * card X by GROUP_2:186;
Card union X = q|^(n+1) by A5, A9, NEWTON:11; then
Card Funcs(n+1,q) = q|^(n+1) by A6;
hence thesis;
end;
for n being Nat holds P[n] from Ind(P0,P1);
hence thesis;
end;
theorem SumDivision: :: SumDivision:
for f being FinSequence of NAT, i being Nat
st for j being Nat st j in dom f holds i divides f/.j holds i divides Sum f
proof
defpred P[Nat] means for f being FinSequence of NAT st len f = $1
for i being Nat st for j being Nat st j in dom f holds i divides f/.j
holds i divides Sum f;
P0: P[0] proof let f be FinSequence of NAT such that A0: len f = 0;
let i be Nat such that
for j being Nat st j in dom f holds i divides f/.j;
f = <*>REAL by A0,FINSEQ_1:32; then Sum f = 0 by RVSUM_1:102; then
i divides Sum f by NAT_1:53;
hence thesis;
end;
P1: for k being Nat st P[k] holds P[k+1]
proof let k be Nat such that
A0: P[k];
let f be FinSequence of NAT such that A1: len f = k+1;
let i be Nat such that
A2: for j being Nat st j in dom f holds i divides f/.j;
C0: len f <> 0 by A1;
f <> {} by A1,FINSEQ_1:25; then
consider q being FinSequence, x being set such that
A3: f=q^<*x*> by FINSEQ_1:63;
reconsider f1=q as FinSequence of NAT by A3,FINSEQ_1:50;
reconsider f2=<*x*> as FinSequence of NAT by A3,FINSEQ_1:50;
k + 1 = len f1 + len f2 by A1,A3,FINSEQ_1:35; then
k + 1 = len f1 + 1 by FINSEQ_1:56; then
k = len f1 + 1 - 1 by XCMPLX_1:26; then
A4: k = len f1 by XCMPLX_1:26;
for j being Nat st j in dom f1 holds i divides f1/.j
proof let j be Nat such that B0: j in dom f1;
dom f1 c= dom f by A3,FINSEQ_1:39; then
B1: j in dom f by B0;
f/.j = f.j by B1,FINSEQ_4:def 4 .= f1.j by B0,A3,FINSEQ_1:def 7
.= f1/.j by B0,FINSEQ_4:def 4;
hence thesis by B1,A2;
end; then
A5: i divides Sum f1 by A0,A4;
rng f2 c= NAT by FINSEQ_1:def 4; then {x} c= NAT by FINSEQ_1:55; then
reconsider m=x as Nat by ZFMISC_1:37;
A6: f.(len f) = m by A1,A3,A4,FINSEQ_1:59;
len f in Seg len f by C0,FINSEQ_1:5; then
A7: len f in dom f by FINSEQ_1:def 3; then
A8: f/.(len f) = f.(len f) by FINSEQ_4:def 4;
A9: i divides m by A2,A6,A7,A8;
rng f c= NAT & rng f1 c= NAT by FINSEQ_1:def 4; then
rng f c= REAL & rng f1 c= REAL by XBOOLE_1:1; then
f is FinSequence of REAL & f1 is FinSequence of REAL by FINSEQ_1:def 4;
then Sum f = Sum f1 + m by A3,RVSUM_1:104;
hence thesis by A5,A9,NAT_1:55;
end;
P: for k being Nat holds P[k] from Ind(P0,P1);
let f be FinSequence of NAT, i be Nat such that
A0: for j being Nat st j in dom f holds i divides f/.j;
len f = len f;
hence thesis by P,A0;
end;
theorem Partition1: :: Partition1:
for X being finite set, Y being a_partition of X,
f being FinSequence of Y st f is one-to-one & rng f = Y
for c being FinSequence of NAT st len c = len f &
for i being Nat st i in dom c holds c.i = Card (f.i)
holds card X = Sum c
proof
defpred P[Nat] means
for X being finite set, z being a_partition of X st card z = $1
for f being FinSequence of z st f is one-to-one & rng f = z
for c being FinSequence of NAT st len c = len f &
for i being Nat st i in dom c holds c.i = Card (f.i)
holds Card X = Sum c;
P0: P[0] proof let X be finite set;
let z be a_partition of X such that A1: card z = 0;
let f be FinSequence of z such that A2: f is one-to-one & rng f = z;
let c be FinSequence of NAT such that A3: len c = len f &
for i being Nat st i in dom c holds c.i = Card (f.i);
B0: z = {} by A1, GRAPH_5:5;
B1: union z = {} by A1,GRAPH_5:5,ZFMISC_1:2;
B2: X = {} by B1, EQREL_1:def 6; f = {} by B0,A2,FINSEQ_1:27;
hence thesis by A3,B2,CARD_1:78,FINSEQ_1:25,RVSUM_1:102;
end;
P1: for k being Nat st P[k] holds P[k+1]
proof let k be Nat; assume
A0: P[k];
let X be finite set;
let Z be a_partition of X such that A1: card Z = k + 1;
let f be FinSequence of Z such that
A2: f is one-to-one and A3: rng f = Z;
let c be FinSequence of NAT such that A4: len c = len f and
A5: for i being Nat st i in dom c holds c.i = Card (f.i);
A6: len f = k + 1 by A1,A2,A3,FINSEQ_4:77;
AA: Z <> {} by A1, GRAPH_5:5;
reconsider Z as non empty set by A1,GRAPH_5:5;
reconsider f as FinSequence of Z;
A7: X <> {} by EQREL_1:def 6,AA; then reconsider X as non empty finite set;
reconsider fk = f|(Seg k) as FinSequence of Z by FINSEQ_1:23;
D0: len fk = k by A6, FINSEQ_3:59;
DZ: f = fk ^ <*f.(k+1)*> by A6, FINSEQ_3:61;
reconsider Zk = rng fk as finite set;
DC: Zk c= Z by A3,FUNCT_1:76; then
union Zk c= union Z by ZFMISC_1:95; then
DF: union Zk c= X by EQREL_1:def 6;
reconsider fk as FinSequence of Zk by FINSEQ_1:def 4;
D1: fk is one-to-one by A2, FUNCT_1:84;
D2: card Zk = k by D0,D1,FINSEQ_4:77;
reconsider Xk = union Zk as finite set by DF, FINSET_1:13;
now per cases;
suppose A1: Zk = {}; consider B being a_partition of Xk;
B = {} by A1,ZFMISC_1:2,EQREL_1:def 6;
hence Zk is a_partition of Xk by A1;
suppose Zk <> {}; then
consider x being set such that A2: x in Zk by XBOOLE_0:def 1;
x in Z by A2,DC; then x <> {} by EQREL_1:def 6, A7; then
consider y being set such that A1: y in x by XBOOLE_0:def 1;
A0: Xk <> {} by A1, A2, TARSKI:def 4;
A2: for a being Subset of Xk st a in Zk
holds a<>{} & for b being Subset of Xk st b in Zk
holds a=b or (a misses b)
proof let a be Subset of Xk such that B0: a in Zk;
a in Z by B0,DC; then
C0: a <> {} by EQREL_1:def 6, A7;
for b being Subset of Xk st b in Zk holds a=b or (a misses b)
proof let b be Subset of Xk such that B1: b in Zk;
a in Z & b in Z by B0, B1, DC;
hence thesis by A7,EQREL_1:def 6;
end; hence thesis by C0;
end;
Zk c= bool union Zk by ZFMISC_1:100; then
Zk is Subset-Family of Xk by SETFAM_1:def 7; then
Zk is a_partition of Xk by A0,A2,EQREL_1:def 6;
hence Zk is a_partition of Xk;
end; then D4: Zk is a_partition of Xk;
reconsider ck = c|(Seg k) as FinSequence of NAT by FINSEQ_1:23;
D5: c = ck ^ <*c.(k+1)*> by A4,A6,FINSEQ_3:61;
D6: len ck = len fk by D0, A6, A4, FINSEQ_3:59;
D7: for i being Nat st i in dom ck holds ck.i = Card (fk.i)
proof let i be Nat; assume A1: i in dom ck;
A0: k <= k+1 by NAT_1:29; then
dom ck = (Seg k) by A4, A6,FINSEQ_1:21; then
AA: dom ck = dom fk by A0, A6,FINSEQ_1:21;
AB: dom ck c= dom c by FUNCT_1:76;
ck.i = c.i by A1, FUNCT_1:70; then
A2: ck.i = Card (f.i) by A1,A5,AB;
fk.i = f.i by A1,AA,FUNCT_1:70;
hence ck.i = Card (fk.i) by A2;
end;
D8: card Xk = Sum ck by A0,D4,D2,D1,D6,D7;
reconsider fk1 = f.(k+1) as set;
for x being set st x in Zk holds x misses fk1
proof let x being set such that B1: x in Zk;
B2: x in Z by DC,B1;
BC: k+1 in Seg(k+1) by FINSEQ_1:6;
dom f = Seg(len f) by FINSEQ_1:def 3; then
B3: fk1 in rng f by A6,BC,FUNCT_1:12; then
B4: fk1 is Subset of X by A3;
consider i being Nat such that
C0: i in dom fk & fk.i = x by FINSEQ_2:11,B1;
now assume E0: fk.i = fk1;
EQ: dom fk = Seg k by D0, FINSEQ_1:def 3;
EB: i in Seg k by C0, D0, FINSEQ_1:def 3;
i <= k by EQ,C0,FINSEQ_1:3; then
ZZ: i < k+1 by NAT_1:38;
EC: dom f = Seg (k + 1) by A6,FINSEQ_1:def 3;
k <= k + 1 by NAT_1:37; then
ED: Seg k c= Seg (k+1) by FINSEQ_1:7;
EE: (k+1) in dom f by EC,FINSEQ_1:6;
fk.i = f.i by EB, EQ, FUNCT_1:70;
hence contradiction by ZZ,E0,EB,EC,ED,EE,A2,FUNCT_1:def 8;
end; hence thesis by A3,B2,B3,B4,C0,EQREL_1:def 6;
end; then C0: fk1 misses Xk by ZFMISC_1:98;
CZ: union Z = X by EQREL_1:def 6;
BC: k+1 in Seg(k+1) by FINSEQ_1:6;
dom f = Seg(len f) by FINSEQ_1:def 3; then
fk1 in rng f by A6,BC,FUNCT_1:12; then
reconsider fk1 as finite set by A3,CZ,FINSET_1:25;
C1: Z = rng fk \/ rng <*fk1*> by A3,DZ, FINSEQ_1:44
.= Zk \/ {fk1} by FINSEQ_1:56;
C2: X = union Z by EQREL_1:def 6
.= union Zk \/ union {fk1} by C1,ZFMISC_1:96.= Xk \/ fk1 by ZFMISC_1:31;
k+1 in Seg(k+1) by FINSEQ_1:6; then
C4: k+1 in dom c by A4,A6,FINSEQ_1:def 3;
rng ck c= NAT by FINSEQ_1:def 4; then rng ck c= REAL by XBOOLE_1:1;
then reconsider ckc=ck as FinSequence of REAL by FINSEQ_1:def 4;
card X = Sum ck + card fk1 by D8, C0,C2,CARD_2:53
.= Sum ck + c.(k+1) by A5,C4
.= Sum (ckc^<*(c.(k+1)) qua Real*>) by RVSUM_1:104 .= Sum c by D5;
hence thesis;
end;
Z0: for k being Nat holds P[k] from Ind(P0, P1);
let X be finite set, Y be a_partition of X;
card Y = card Y;
hence thesis by Z0;
end;
begin :: Class formula for groups
definition
cluster finite Group;
existence proof consider G being Group; (1).G is finite by GROUP_2:80;
hence thesis;
end;
end;
definition
let G be finite Group;
cluster center G -> finite;
correctness by GROUP_2:48;
end;
definition let G be Group, a be Element of G;
func Centralizer a -> strict Subgroup of G means :Def1:
the carrier of it = { b where b is Element of G : a*b = b*a };
existence proof set Car = { b where b is Element of G : a*b = b*a};
a*1.G = a & 1.G*a = a by GROUP_1:def 4; then 1.G in Car; then
B: Car is non empty;
for x being set st x in Car holds x in the carrier of G
proof let x be set such that A0: x in Car;
consider g being Element of G such that A1: x = g & a*g = g*a by A0;
thus thesis by A1;
end; then
D: Car is Subset of G by TARSKI:def 3;
E: for g1,g2 being Element of G st g1 in Car & g2 in Car
holds g1 * g2 in Car
proof let g1,g2 be Element of G such that
A0: g1 in Car and A1: g2 in Car;
consider z1 being Element of G such that
A2: z1=g1 & z1*a = a*z1 by A0;
consider z2 being Element of G such that
A3: z2=g2 & z2*a = a*z2 by A1;
a*(g1*g2) = (g1*a)*g2 by A2, VECTSP_1:def 16
.= g1*(g2*a) by A3, VECTSP_1:def 16 .= g1*g2*a by VECTSP_1:def 16;
hence thesis;
end;
F: for g being Element of G st g in Car holds g" in Car
proof let g be Element of G such that
A0: g in Car;
consider z1 being Element of G such that
A2: z1=g & z1*a = a*z1 by A0;
g"*(g*a) = a by GROUP_3:1; then
g"*((a*g)*g") = a*g" by A2,VECTSP_1:def 16; then g"*a = a*g" by GROUP_3:1;
hence thesis;
end;
ex H being strict Subgroup of G st the carrier of H=Car by B,D,E,F,GROUP_2:61;
hence thesis;
end;
uniqueness proof let H1,H2 be strict Subgroup of G such that
A: the carrier of H1 = { b where b is Element of G: a*b = b*a} and
B: the carrier of H2 = { b where b is Element of G: a*b = b*a};
for g being Element of G holds g in H1 iff g in H2
proof let g be Element of G;
hereby assume g in H1; then
A2: g in the carrier of H1 by RLVECT_1:def 1;
consider b being Element of G such that
A4: b = g and A5: a*b = b*a by A, A2; g in the carrier of H2 by B,A4,A5;
hence g in H2 by RLVECT_1:def 1;
end;
now assume g in H2; then
A2: g in the carrier of H2 by RLVECT_1:def 1;
consider b being Element of G such that
A4: b = g and A5: a*b = b*a by B, A2; g in the carrier of H1 by A,A4,A5;
hence g in H1 by RLVECT_1:def 1;
end;
hence thesis;
end;
hence thesis by GROUP_2:def 6;
end;
end;
definition let G be finite Group;
let a be Element of G;
cluster Centralizer a -> finite;
correctness by GROUP_2:48;
end;
theorem GCTR2: :: GCTR2:
for G being Group, a being Element of G, x being set
st x in Centralizer a holds x in G
proof let G be Group, a be Element of G, x be set; assume
AA: x in Centralizer a;
the carrier of Centralizer a =
{ b where b is Element of G : a*b = b*a } by Def1; then
x in { b where b is Element of G : a*b = b*a } by AA, RLVECT_1:def 1;
then ex b being Element of G st b = x & a*b = b*a;
hence x in G by RLVECT_1:def 1;
end;
theorem GCTR1: :: GCTR1:
for G being Group, a, x being Element of G
holds a*x = x*a iff x is Element of Centralizer a
proof let G be Group, a, x be Element of G;
A: the carrier of Centralizer a =
{ b where b is Element of G : a*b = b*a } by Def1;
set x' = x;
hereby assume a*x = x*a; then a*x' = x'*a;
then x in the carrier of Centralizer a by A;
hence x is Element of Centralizer a;
end;
assume x is Element of Centralizer a; then x in the carrier of Centralizer a;
then ex b being Element of G st b = x & a*b = b*a by A;
hence a*x = x*a;
end;
definition
let G be Group, a be Element of G;
cluster con_class a -> non empty;
correctness by GROUP_3:98;
end;
definition let G be Group, a be Element of G;
func a-con_map -> Function of the carrier of G, con_class a means :Def0:
for x being Element of G holds it.x = a |^ x;
existence proof
defpred P[Element of G, set] means $2 = a |^ $1;
P1: for x being Element of G
ex y being Element of con_class a st P[x,y]
proof let x be Element of G;
a |^ x in con_class a by GROUP_3:97;
hence thesis;
end;
ex f being Function of the carrier of G, con_class a st
for x being Element of G holds P[x,f.x] from FuncExD(P1);
hence thesis;
end;
uniqueness
proof let it1, it2 be Function of the carrier of G, con_class a such that
A: for x being Element of G holds it1.x = a |^ x and
B: for x being Element of G holds it2.x = a |^ x;
C: dom it1 = the carrier of G & dom it2 = the carrier of G by FUNCT_2:def 1;
D: for x being set st x in dom it1 holds it1.x = it2.x
proof let x be set such that A1: x in dom it1;
x in the carrier of G by FUNCT_2:def 1,A1; then
reconsider y=x as Element of G;
it1.y = a |^ y & it2.y = a |^ y by A,B;
hence thesis;
end;
thus thesis by C,D,FUNCT_1:9;
end;
end;
theorem Br1: :: Br1:
for G being finite Group, a being Element of G, x being Element of con_class a
holds card (a-con_map"{x}) = ord Centralizer a
proof let G be finite Group, a be Element of G, x be Element of con_class a;
consider b being Element of G such that
Y0: b = x and Y1: a,b are_conjugated by GROUP_3:95;
consider d being Element of G such that
Y2: x = a |^ d by Y0,Y1,GROUP_3:88;
Y3: x = d"*a*d by GROUP_3:20,Y2;
reconsider Cad = (Centralizer a)*d as Subset of G;
consider B,C being finite set such that B = d*(Centralizer a) and
F0: C = Cad and ord Centralizer a = card B and
F2: ord Centralizer a = card C by GROUP_2:156;
for g being set holds g in a-con_map"{x} iff g in Cad
proof let g be set;
G1: now assume B0: g in a-con_map"{x}; then
g in dom (a-con_map) & a-con_map.g in {x} by FUNCT_1:def 13; then
H0: a-con_map.g = x by TARSKI:def 1;
reconsider y=g as Element of G by B0;
a-con_map.g = a |^ y by Def0; then
B1: y"*a*y = d"*a*d by H0,Y3,GROUP_3:20;
B2: y*((d"*a)*d) = y*(d"*a)*d by VECTSP_1:def 16
.= y*d"*a*d by VECTSP_1:def 16;
B3: y*((y"*a)*y) = y*(y"*a)*y by VECTSP_1:def 16 .= a*y by GROUP_3:1;
y*d"*a*d = a*y by B1,B2,B3; then
y*d"*a*d*d" = a*(y*d") by VECTSP_1:def 16; then
(y*d")*a = a*(y*d") by GROUP_3:1; then
(y*d") is Element of Centralizer a by GCTR1; then
consider z being Element of G such that
T0: z in the carrier of Centralizer a and T1: y*d" = z;
z in carr(Centralizer a) by T0,GROUP_2:def 9; then
TF: z in Centralizer a by GROUP_2:88;
reconsider z as Element of G;
y = z*d by GROUP_3:1,T1;
hence g in Cad by TF, GROUP_2:126;
end;
now assume g in Cad; then
consider z being Element of G such that
B0: g = z*d and B1: z in Centralizer a by GROUP_2:126;
reconsider y=g as Element of G by B0;
y*d" = z*d*d" by B0; then y*d" = z by GROUP_3:1; then
y*d" in Centralizer a by B1; then
y*d" in carr(Centralizer a) by GROUP_2:88; then
y*d" is Element of Centralizer a by GROUP_2:def 9; then
y*d" is Element of Centralizer a; then
(y*d")*a = a*(y*d") by GCTR1; then
(y*d")*a*d = a*((y*d")*d) by VECTSP_1:def 16; then
(y*d")*a*d = a*y by GROUP_3:1; then
(y*d")*(a*d) = a*y by VECTSP_1:def 16; then
y"*((y*d")*(a*d)) = y"*a*y by VECTSP_1:def 16; then
(y"*(y*d"))*(a*d) = y"*a*y by VECTSP_1:def 16; then
d"*(a*d) = y"*a*y by GROUP_3:1; then
d"*a*d = y"*a*y by VECTSP_1:def 16; then
x = a|^y by Y3,GROUP_3:20; then a-con_map.y = x by Def0; then
G1: a-con_map.y in {x} by TARSKI:def 1;
dom (a-con_map) = the carrier of G by FUNCT_2:def 1;
hence g in a-con_map"{x} by G1,FUNCT_1:def 13;
end;
hence thesis by G1;
end;
hence thesis by F0,F2,TARSKI:2;
end;
theorem Br2: :: Br2:
for G being Group, a being Element of G, x, y being Element of con_class a
st x<>y holds (a-con_map"{x}) misses (a-con_map"{y})
proof let G be Group, a be Element of G,
x,y be Element of con_class a such that A0: x <> y;
now assume ex g being set st g in (a-con_map"{x}) /\ (a-con_map"{y}); then
consider g being set such that
B0: g in (a-con_map"{x}) /\ (a-con_map"{y});
B1: g in a-con_map"{x} & g in a-con_map"{y} by B0,XBOOLE_0:def 3;
a-con_map.g in {x} by B1,FUNCT_1:def 13; then
B3: a-con_map.g = x by TARSKI:def 1;
a-con_map.g in {y} by B1,FUNCT_1:def 13; then
a-con_map.g = y by TARSKI:def 1;
hence contradiction by A0,B3;
end; then (a-con_map"{x}) /\ (a-con_map"{y}) = {} by XBOOLE_0:def 1;
hence thesis by XBOOLE_0:def 7;
end;
theorem Br3: :: Br3:
for G being Group, a being Element of G
holds { a-con_map"{x} where x is Element of con_class a : not contradiction }
is a_partition of the carrier of G
proof let G be Group, a be Element of G; reconsider X =
{a-con_map"{x} where x is Element of con_class a:not contradiction} as set;
A1: union X = the carrier of G proof
C0: for y being set holds y in union X implies y in the carrier of G
proof let x be set such that B0: x in union X;
consider Y being set such that
B1: x in Y and B2: Y in X by B0,TARSKI:def 4;
consider z being Element of con_class a such that
B3: a-con_map"{z} = Y by B2;
thus thesis by B1,B3;
end;
for y being set holds y in the carrier of G implies y in union X
proof let x be set such that B0: x in the carrier of G;
reconsider y=x as Element of G by B0;
a |^ y in con_class a by GROUP_3:97; then
consider z being Element of G such that
B1: z in con_class a and B2: z = a|^y;
a-con_map.y = z by Def0,B2; then
B5: a-con_map.y in {z} by TARSKI:def 1;
dom(a-con_map) = the carrier of G by FUNCT_2:def 1; then
B3: y in a-con_map"{z} by B5,FUNCT_1:def 13;
a-con_map"{z} in X by B1;
hence thesis by B3,TARSKI:def 4;
end;hence thesis by C0,TARSKI:2;
end;
A2: for A being Subset of G st A in X holds A<>{} &
for B being Subset of G st B in X holds A=B or A misses B
proof let A be Subset of G such that B0: A in X;
consider x being Element of con_class a such that
C0: A = a-con_map"{x} by B0;
a,x are_conjugated by GROUP_3:96; then
consider g being Element of G such that
C1: x = a |^ g by GROUP_3:88;
a-con_map.g = x by Def0, C1; then
G1: a-con_map.g in {x} by TARSKI:def 1;
dom (a-con_map) = the carrier of G by FUNCT_2:def 1; then
g in a-con_map"{x} by G1,FUNCT_1:def 13; then
B1: A <> {} by C0;
B2: for B being Subset of G st B in X
holds A=B or A misses B
proof let B be Subset of G such that D0: B in X;
consider y being Element of con_class a such that
D1: B = a-con_map"{y} by D0;
now per cases;
suppose x = y; hence A=B or A misses B by C0,D1;
suppose x<> y; thus A=B or A misses B by Br2,C0,D1;
end; hence thesis;
end; thus thesis by B1,B2;
end;
X c= bool union X by ZFMISC_1:100; then
X is Subset-Family of the carrier of G by A1,SETFAM_1:def 7; then
X is a_partition of the carrier of G by EQREL_1:def 6,A1,A2;
hence thesis;
end;
theorem Br4: :: Br4:
for G being finite Group, a being Element of G
holds Card { a-con_map"{x} where x is Element of con_class a :
not contradiction} = card con_class a
proof let G be finite Group, a be Element of G;
reconsider X = { a-con_map"{x} where x is Element of con_class a:
not contradiction} as a_partition of the carrier of G by Br3;
deffunc FF(set) = a-con_map"{$1};
LF: for x being set st x in con_class a holds FF(x) in X;
consider F being Function of con_class a, X such that
A2: for x being set st x in con_class a holds F.x = FF(x) from Lambda1(LF);
consider y being Element of con_class a;
for c being set st c in X ex x being set st x in con_class a & c = F.x
proof let c be set such that C0: c in X;
reconsider c as Subset of G by C0;
consider y being Element of con_class a such that
C1: c = a-con_map"{y} by C0; F.y = c by C1,A2;
hence thesis;
end; then
A3: rng F = X by FUNCT_2:16;
A5: dom F = con_class a by FUNCT_2:def 1; then
A6: con_class a c= dom F;
for x1,x2 being set st x1 in dom F & x2 in dom F & F.x1=F.x2 holds x1 = x2
proof let x1,x2 be set such that
B0: x1 in dom F and B1: x2 in dom F and B2: F.x1 = F.x2;
reconsider y1=x1 as Element of con_class a by B0,A5;
reconsider y2=x2 as Element of con_class a by B1,A5;
a-con_map"{y1} = F.y1 & a-con_map"{y2} = F.y2 by A2; then
B4: a-con_map"{y1} = a-con_map"{y2} by B2;
now assume Y0: y1<>y2;
(a-con_map"{y1}) misses (a-con_map"{y2}) by Y0,Br2; then
C1: ((a-con_map"{y1}) /\ (a-con_map"{y2})) = {} by XBOOLE_0:def 7;
consider d being Element of G such that
Y7: d = y1 & a,d are_conjugated by GROUP_3:95;
d,a are_conjugated by Y7; then
consider g being Element of G such that
Y8: d = a |^ g by GROUP_3:def 7;
a-con_map.g = y1 by Y7,Y8,Def0; then
G2: a-con_map.g in {y1} by TARSKI:def 1;
dom (a-con_map) = the carrier of G by FUNCT_2:def 1; then
g in a-con_map"{y1} by G2,FUNCT_1:def 13;
hence contradiction by B4,C1;
end; hence thesis;
end; then A7: F is one-to-one by FUNCT_1:def 8;
con_class a, F.:(con_class a) are_equipotent by A6,A7,CARD_1:60; then
con_class a, rng F are_equipotent by A5,RELAT_1:146; then
con_class a, X are_equipotent by A3;
hence thesis by CARD_1:21;
end;
theorem OrdGroup1: :: OrdGroup1:
for G being finite Group, a being Element of G
holds ord G = card con_class a * ord Centralizer a
proof let G be finite Group, a be Element of G;
reconsider
X = {a-con_map"{x} where x is Element of con_class a: not contradiction}
as a_partition of the carrier of G by Br3;
A0: card X = card con_class a by Br4;
A1: union X = the carrier of G by EQREL_1:def 6;
AA: for A being set st A in X holds A is finite & Card A = ord Centralizer a &
for B being set st B in X & A<>B holds A misses B
proof let A be set such that D0: A in X;
A is Element of X by D0; then
reconsider A as Subset of G;
consider x being Element of con_class a such that
BB: A = a-con_map"{x} by D0;
D2: Card A = ord Centralizer a by Br1,BB;
for B being set st B in X & A<>B holds A misses B by EQREL_1:def 6,D0;
hence thesis by D2;
end;
reconsider k = ord Centralizer a as Nat;
A2: for Y being set st Y in X ex B being finite set st B = Y & card B = k &
for Z being set st Z in X & Y <> Z holds Y,Z are_equipotent & Y misses Z
proof let Y be set such that C0: Y in X;
reconsider Y as finite set by AA,C0;
Card Y = ord Centralizer a by C0,AA; then
D0: ex B being finite set st B=Y & card B = ord Centralizer a;
for Z being set st Z in X & Y<>Z holds Y,Z are_equipotent & Y misses Z
proof let Z be set such that E0: Z in X and E1: Y<>Z;
E2: Card Y = ord Centralizer a by C0,AA;
Card Z = ord Centralizer a by E0,AA; then
D0: Y,Z are_equipotent by E2, CARD_1:21;
Y misses Z by C0,E0,E1,AA;
hence thesis by D0;
end;
hence thesis by D0;
end; consider C being finite set such that
B0: C = union X and B1: card C = card X * k by A2, GROUP_2:186;
ord G = card C by B0,A1, GROUP_1:def 14 .= card con_class a * k by A0,B1
.= card con_class a * ord Centralizer a;
hence thesis;
end;
definition let G be Group;
func conjugate_Classes G -> a_partition of the carrier of G equals :CDEF:
{S where S is Subset of G :
ex a being Element of G st S = con_class a };
correctness proof set cG = the carrier of G;
set C = {S where S is Subset of cG:
ex a being Element of G st S=con_class a };
C c= bool cG proof let x be set; assume x in C; then
consider S being Subset of cG such that
A1: S=x and ex a being Element of cG st S = con_class a;
thus thesis by A1;
end; then
A: C is Subset-Family of cG by SETFAM_1:def 7;
now let x be set;
hereby assume x in union C; then consider S being set such that
B1: x in S and
A1: S in C by TARSKI:def 4;
consider S' being Subset of cG such that
C1: S' = S and ex a being Element of G st S'=con_class a
by A1;
thus x in cG by C1, B1;
end;
assume x in cG; then reconsider x'=x as Element of cG;
reconsider S = con_class x' as Subset of cG;
A1: S in C; x' in con_class x' by GROUP_3:98;
hence x in union C by A1, TARSKI:def 4;
end; then
C: union C = cG by TARSKI:2;
now let A be Subset of cG; assume A in C; then
consider A' being Subset of cG such that
A1: A' = A and
B1: ex a being Element of cG st A' = con_class a;
consider a being Element of cG such that
B1a: A' = con_class a by B1;
thus A<>{} by A1,B1;
let B be Subset of cG; assume B in C; then
consider B' being Subset of cG such that
C1: B' = B and
D1: ex a being Element of cG st B' = con_class a;
consider b being Element of cG such that
D1a: B' = con_class b by D1;
assume
E1: A <> B; assume A meets B; then consider x being set such that
F1: x in A & x in B by XBOOLE_0:3;
x in cG by F1; then reconsider x as Element of cG;
G1: x,a are_conjugated by A1, F1, B1a, GROUP_3:96;
H1: x,b are_conjugated by C1, F1, D1a, GROUP_3:96;
I1: a,b are_conjugated by G1,H1,GROUP_3:91;
now let c be set;
hereby assume
A2: c in A; then c in cG; then
reconsider c'=c as Element of cG;
c',a are_conjugated by A1, A2, B1a, GROUP_3:96; then
c',b are_conjugated by I1, GROUP_3:91;
hence c in B by C1, D1a, GROUP_3:96;
end;
assume
A2: c in B; then c in cG; then
reconsider c'=c as Element of cG;
c',b are_conjugated by C1, A2, D1a, GROUP_3:96; then
c',a are_conjugated by I1, GROUP_3:91;
hence c in A by A1, B1a, GROUP_3:96;
end;
hence contradiction by E1,TARSKI:2;
end;
hence C is a_partition of cG by A, C, EQREL_1:def 6;
end;
end;
theorem Conj1: :: Conj1:
for G being Group, x being set
holds x in conjugate_Classes G iff ex a being Element of G st con_class a = x
proof let G be Group, x be set;
A: conjugate_Classes G = {S where S is Subset of G :
ex a being Element of G st S = con_class a } by CDEF;
hereby assume x in conjugate_Classes G; then
ex S being Subset of G st
x=S & ex a being Element of G st S = con_class a by A;
hence ex a being Element of G st con_class a = x;
end;
given a being Element of G such that
A1: con_class a = x;
thus x in conjugate_Classes G by A1, A;
end;
theorem ClassFormula: :: :: ClassFormula Class formula for finite groups
for G being finite Group, f being FinSequence of conjugate_Classes G
st f is one-to-one & rng f = conjugate_Classes G
for c being FinSequence of NAT
st len c = len f & for i being Nat st i in dom c holds c.i = Card (f.i)
holds ord G = Sum c
proof let G be finite Group;
let f be FinSequence of conjugate_Classes G such that
A0: f is one-to-one and A1: rng f = conjugate_Classes G;
let c be FinSequence of NAT such that
A2: len c = len f and A3: for i being Nat st i in dom c holds c.i = Card (f.i);
reconsider X = the carrier of G as finite set;
card X = Sum c by A0,A1,A2,A3,Partition1; then
ord G = Sum c by GROUP_1:def 14;
hence thesis;
end;
begin :: Centers and centralizers of skew fields
theorem DIM: :: DIM:
for F being finite Field, V being VectSp of F, n, q being Nat
st V is finite-dimensional & n = dim V & q = Card the carrier of F
holds Card the carrier of V = q |^ n
proof let F be finite Field, V be VectSp of F, n, q be Nat such that
A: V is finite-dimensional and
B: n = dim V and
C: q = Card the carrier of F;
consider B being finite Subset of V such that
B1: B is Basis of V by A, VECTSP_9:def 1;
D: B is linearly-independent by B1, VECTSP_7:def 3;
E: Lin(B) = the VectSpStr of V by B1, VECTSP_7:def 3;
F: Card B = n by A, B, B1, VECTSP_9:def 2;
q <> 0 by C,GRAPH_5:5; then
G: q > 0 by NAT_1:19;
now per cases;
suppose Y0: n = 0;
(Omega).V = (0).V by A,B,Y0,VECTSP_9:33; then
Y1: the VectSpStr of V = (0).V by VECTSP_4:def 4;
the carrier of V = {0.V} by Y1, VECTSP_4:def 3; then
Card the carrier of V = 1 by CARD_1:79
.= q #Z 0 by PREPOWER:44 .= q |^ 0 by G,PREPOWER:46;
hence thesis by Y0;
suppose n <> 0; then
BBB: B <> 0 by F,CARD_4:17;
consider bf being FinSequence such that
Y0: rng bf = B and Y1: bf is one-to-one by FINSEQ_4:73;
len bf = n by F,Y0,Y1,FINSEQ_4:77; then
Y2: Seg n = dom bf by FINSEQ_1:def 3;
Y3: rng bf c= the carrier of V by Y0; then
reconsider Vbf = bf as FinSequence of the carrier of V by FINSEQ_1:def 4;
set cLinB = the carrier of Lin(B);
set ntocF = n-tuples_on the carrier of F;
defpred P[Function, set] means
ex lc being Linear_Combination of B st
(for i being set st i in dom $1 holds lc.(Vbf.i) = $1.i) &
$2 = Sum(lc (#) Vbf);
P1: for x being Element of ntocF ex y being Element of cLinB st P[x,y]
proof let f be Element of ntocF;
ex lc being Linear_Combination of B st
for i being set st i in dom f holds lc.(Vbf.i) = f.i
proof
deffunc LC(set) = f.(union (Vbf"{$1}));
P1: for x being set st x in B holds LC(x) in the carrier of F
proof let x be set such that E0: x in B;
consider i being set such that
E1: Vbf"{x} = {i} by E0,Y0,Y1,FUNCT_1:144;
E2: union (Vbf"{x}) = i by E1,ZFMISC_1:31;
i in Vbf"{x} by E1,TARSKI:def 1; then
i in dom Vbf & Vbf.i in {x} by FUNCT_1:def 13; then
E3: i in dom Vbf & Vbf.i = x by TARSKI:def 1;
i in dom f by E3,Y2,FINSEQ_2:144; then
E4: f.i in rng f by FUNCT_1:12;
rng f c= the carrier of F by RELSET_1:12;
hence thesis by E2, E4;
end;
consider lc being Function of B, the carrier of F such that
D0: for y being set st y in B holds lc.y = LC(y) from Lambda1(P1);
set ll=lc +* (((the carrier of V)\B) --> 0.F);
Z9: dom (((the carrier of V)\B) --> 0.F) = (the carrier of V)\B
by FUNCOP_1:19; then
dom ll = dom lc \/ ((the carrier of V)\B) by FUNCT_4:def 1; then
dom ll = B \/ ((the carrier of V)\B) by FUNCT_2:def 1; then
dom ll = B \/ (the carrier of V) by XBOOLE_1:39; then
Lb1:dom ll = the carrier of V by XBOOLE_1:12;
Z0: rng (((the carrier of V)\B) --> 0.F) c= {0.F} by FUNCOP_1:19;
{0.F} c= the carrier of F by ZFMISC_1:37; then
Z1: rng (((the carrier of V)\B) --> 0.F) c= the carrier of F
by Z0, XBOOLE_1:1;
Z2: rng lc c= the carrier of F by RELSET_1:12;
_Z3: rng ll c= rng lc \/ rng (((the carrier of V)\B)--> 0.F)
by FUNCT_4:18;
rng lc \/ rng (((the carrier of V)\B)--> 0.F) c=
the carrier of F by Z1,Z2,XBOOLE_1:8; then
Lb2:rng ll c= the carrier of F by _Z3,XBOOLE_1:1;
ll is Function of the carrier of V,the carrier of F
by Lb1, Lb2,FUNCT_2:4; then
D2: ll is Element of Funcs(the carrier of V, the carrier of F)
by FUNCT_2:11;
D1: for i being set st i in dom f holds ll.(Vbf.i) = f.i
proof let i be set such that E0: i in dom f;
Ea: i in dom Vbf by E0,Y2,FINSEQ_2:144;
Vbf.i in B by Y0,Ea, FUNCT_1:12; then
consider y being Element of B such that
E1: y = Vbf.i;
Eb: Vbf.i in {y} by E1,TARSKI:def 1;
consider ee being set such that
E4: Vbf"{y} c= {ee} by Y1,FUNCT_1:159;
E5: i in Vbf"{y} by Ea,Eb,FUNCT_1:def 13; then
{i} c= {ee} by E4,ZFMISC_1:37; then
i = ee by ZFMISC_1:24; then
E2: Vbf"{y} = {i} by E4,E5,ZFMISC_1:39;
not y in (the carrier of V)\B by BBB,XBOOLE_0:def 4; then
ll.y = lc.y by Z9,FUNCT_4:12; then
ll.y = f.(union (Vbf"{y})) by D0,BBB;
hence thesis by E1,E2,ZFMISC_1:31;
end;
D3: for v being Element of V st not v in B
holds ll.v = 0.F
proof let v be Element of V;
assume E0: not v in B;
E1: v in (the carrier of V)\B by E0,XBOOLE_0:def 4; then
ll.v=(((the carrier of V)\B)-->0.F).v by Z9,FUNCT_4:14;
hence thesis by E1,FUNCOP_1:13;
end; then
reconsider L=ll as Linear_Combination of V by D2,VECTSP_6:def 4;
for v being Element of V
holds v in Carrier(L) implies v in B
proof let v be Element of V;
assume E0: v in Carrier(L);
now assume E1: not v in B;
ll.v = 0.F by E1,D3;
hence contradiction by E0,VECTSP_6:20;
end;
hence thesis;
end; then Carrier(L) c= B by SUBSET_1:7; then
L is Linear_Combination of B by VECTSP_6:def 7;
hence thesis by D1;
end;
then consider lc being Linear_Combination of B such that
C1: for i being set st i in dom f holds lc.(Vbf.i) = f.i;
ex y being Element of V st y = Sum(lc (#) Vbf);
hence thesis by E,C1;
end;
consider G being Function of ntocF,cLinB such that
GD: for tup being Element of ntocF holds P[tup, G.tup] from FuncExD(P1);
G0: dom G = ntocF by FUNCT_2:def 1; then G1: ntocF c= dom G;
H1: for L being Linear_Combination of B holds
ex nt being Element of ntocF st
for i being set st i in dom nt holds nt.i = L.(Vbf.i)
proof let L be Linear_Combination of B;
deffunc F(set) = L.(Vbf.$1);
P1: for x being set st x in Seg n holds F(x) in the carrier of F
proof let x be set such that C0: x in Seg n;
Vbf.x in rng Vbf by C0,Y2,FUNCT_1:12; then
consider vv be Element of V such that
C1: Vbf.x = vv by Y3;
L.vv in the carrier of F;
hence thesis by C1;
end;
consider f being Function of Seg n, the carrier of F such that
D0: for x being set st x in Seg n holds f.x = F(x) from Lambda1(P1);
D1: dom f = Seg n by FUNCT_2:def 1; then
D2: for x being set st x in dom f holds f.x = L.(Vbf.x) by D0;
D3: rng f c= the carrier of F by RELSET_1:12;
f is FinSequence-like by D1,FINSEQ_1:def 2; then
reconsider ff=f as FinSequence of the carrier of F
by D3,FINSEQ_1:def 4;
len ff = n by D1,FINSEQ_1:def 3; then
ff is Element of ntocF by FINSEQ_2:110;
hence thesis by D2;
end;
:: Show G is surjective
for c being set st c in cLinB ex x being set st x in ntocF & c = G.x
proof let c be set such that C0: c in cLinB;
c in (Lin(B)) by C0, RLVECT_1:def 1; then
consider l being Linear_Combination of B such that
C1: c = Sum(l) by VECTSP_7:12;
Carrier(l) c= rng Vbf by Y0,VECTSP_6:def 7; then
C3: Sum(l (#) Vbf) = Sum(l) by VECTSP_9:7,Y1;
consider t being Element of ntocF such that
C2: for i being set st i in dom t holds t.i = l.(Vbf.i) by H1;
consider lc being Linear_Combination of B such that
C4: (for i being set st i in dom t holds lc.(Vbf.i) = t.i) and
C5: G.t = Sum(lc (#) Vbf) by GD;
for v being Element of V holds l.v = lc.v
proof let v be Element of V;
now per cases;
suppose v in rng Vbf; then
consider x being set such that
E0: [x,v] in Vbf by RELAT_1:def 5;
E1: x in dom Vbf & Vbf.x = v by E0,FUNCT_1:8;
E3: x in dom t by E1,Y2,FINSEQ_2:144; then
l.(Vbf.x) = t.x by C2;
hence thesis by E1,C4,E3;
suppose E0: not v in rng Vbf;
now assume F0: v in Carrier(l);
Carrier(l) c= rng Vbf by Y0,VECTSP_6:def 7;
hence contradiction by E0,F0;
end; then
E1: l.v = 0.F by VECTSP_6:20;
now assume F0: v in Carrier(lc);
Carrier(lc) c= rng Vbf by Y0,VECTSP_6:def 7;
hence contradiction by E0,F0;
end;
hence thesis by E1,VECTSP_6:20;
end;
hence thesis;
end; then G.t = Sum(l (#) Vbf) by C5,VECTSP_6:def 10;
hence thesis by C1,C3;
end; then
G2: rng G = cLinB by FUNCT_2:16;
:: Show G is injective
for x1,x2 being set st x1 in dom G & x2 in dom G & G.x1 = G.x2
holds x1 = x2
proof let x1,x2 be set such that
C0: x1 in dom G and C1: x2 in dom G and C2: G.x1 = G.x2;
reconsider t1=x1 as Element of ntocF by C0,FUNCT_2:def 1;
reconsider t2=x2 as Element of ntocF by C1,FUNCT_2:def 1;
reconsider v1=G.t1 as Element of Lin(B);
reconsider v2=G.t2 as Element of Lin(B);
consider L1 being Linear_Combination of B such that
S1: (for i being set st i in dom t1 holds L1.(Vbf.i) = t1.i) &
G.t1 = Sum(L1 (#) Vbf) by GD;
consider L2 being Linear_Combination of B such that
S2: (for i being set st i in dom t2 holds L2.(Vbf.i) = t2.i) &
G.t2 = Sum(L2 (#) Vbf) by GD;
Carrier(L1) c= rng Vbf by Y0,VECTSP_6:def 7; then
S3: Sum(L1) = Sum(L1 (#) Vbf) by Y1,VECTSP_9:7;
Carrier(L2) c= rng Vbf by Y0, VECTSP_6:def 7; then
Sum(L2) = Sum(L2 (#) Vbf) by Y1,VECTSP_9:7; then
Sum(L1) = Sum(L2) by S3, S1, S2, C2; then
Sum(L1) - Sum(L2) = 0.V by VECTSP_1:66; then
S3: Sum(L1 - L2) = 0.V by VECTSP_6:80;
Sa: (L1 - L2) is Linear_Combination of B by VECTSP_6:75; then
SS: Carrier(L1 - L2) = {} by D, S3, VECTSP_7:def 1;
for v being Element of V holds L1.v = L2.v
proof let v be Element of V;
reconsider LL = L1 - L2 as Linear_Combination of B by Sa;
LL.v = 0.F by SS, VECTSP_6:20; then
0.F = L1.v - L2.v by VECTSP_6:73; then
L1.v = L2.v by VECTSP_1:84;
hence thesis;
end; then
S5: L1 = L2 by VECTSP_6:def 10;
S4: dom t1 = Seg n & dom t2 = Seg n by FINSEQ_2:144;
(for k being Nat st k in dom t1 holds t1.k = t2.k)
proof let k be Nat such that T0: k in dom t1;
t1.k = L1.(Vbf.k) by T0,S1; then
t1.k = t2.k by T0,S2,S4,S5;
hence thesis;
end;
hence thesis by S4,FINSEQ_1:17;
end; then
G is one-to-one by FUNCT_1:def 8; then
ntocF, G.:(ntocF) are_equipotent by G1,CARD_1:60; then
ntocF, rng G are_equipotent by G0,RELAT_1:146; then
ntocF, cLinB are_equipotent by G2; then
J: Card cLinB = Card (ntocF) by CARD_1:21;
Card q = q by CARD_1:66; then
I: Card (Seg n) = Card n & Card q = Card the carrier of F by C,FINSEQ_1:76;
Card (ntocF)
= Card Funcs (Seg n, the carrier of F) by FINSEQ_2:111
.= Card Funcs (n, q) by I,FUNCT_5:68
.= q |^ n by Lm1,G;
hence thesis by E,J;
end;
hence thesis;
end;
definition
let R be Skew-Field;
func center R -> strict Field means :DefCenter:
the carrier of it = {x where x is Element of R:
for s being Element of R holds x*s = s*x} &
the add of it = (the add of R) | [:the carrier of it,the carrier of it:] &
the mult of it = (the mult of R) | [:the carrier of it,the carrier of it:]&
the Zero of it = the Zero of R &
the unity of it = the unity of R;
existence proof
set cR = the carrier of R;
set ccs = {x where x is Element of R:
for s being Element of R holds x*s = s*x};
now let s be Element of cR;
thus (0.R)*s = 0.R by VECTSP_1:39 .= s*(0.R) by VECTSP_1:36;
end; then
K: 0.R in ccs; then
reconsider ccs as non empty set;
N: ccs c= cR proof let x be set; assume x in ccs; then
ex x' being Element of cR st
x'=x & for s being Element of R holds x'*s = s*x';
hence thesis;
end;
set acs = (the add of R) | [:ccs,ccs:];
set mcs = (the mult of R) | [:ccs,ccs:];
set Zs = the Zero of R; set Us = the unity of R;
B: [:ccs,ccs:] c= [:cR,cR:] proof let x be set; assume x in [:ccs,ccs:];
then consider a,b being set such that
A1: a in ccs & b in ccs and
B1: x =[a,b] by ZFMISC_1:def 2;
a in cR & b in cR by N, A1;
hence x in [:cR,cR:] by B1, ZFMISC_1:def 2;
end;
reconsider acs as Function of [:ccs,ccs:],cR by B, FUNCT_2:38;
rng acs c= ccs proof let y be set; assume y in rng acs; then
consider x being set such that
A1: x in dom acs and
A1a: y = acs.x by FUNCT_1:def 5;
dom acs = [:ccs,ccs:] by FUNCT_2:def 1;
then consider a,b being set such that
C1: a in ccs & b in ccs and
D1: x = [a,b] by A1, ZFMISC_1:def 2;
a in cR & b in cR by C1, N; then
reconsider a,b as Element of cR;
E1: ex a' being Element of cR st a'=a &
for s being Element of R holds a'*s = s*a' by C1;
F1: ex b' being Element of cR st b'=b &
for s being Element of R holds b'*s = s*b' by C1;
G1: [a,b] in [:ccs,ccs:] by C1,ZFMISC_1:def 2;
H1: a+b = (the add of R).[a,b] by RLVECT_1:def 3
.= acs.x by D1, G1, FUNCT_1:72;
now let s be Element of cR;
thus (a+b)*s=a*s+b*s by VECTSP_1:def 12
.= s*a+b*s by E1 .= s*a+s*b by F1 .=s*(a+b) by VECTSP_1:def 11;
end;
hence y in ccs by H1, A1a;
end; then
acs is Function of [:ccs,ccs:],ccs by FUNCT_2:8; then
reconsider acs as BinOp of ccs;
reconsider mcs as Function of [:ccs,ccs:],cR by B, FUNCT_2:38;
rng mcs c= ccs proof let y be set; assume y in rng mcs; then
consider x being set such that
A1: x in dom mcs and
A1a: y = mcs.x by FUNCT_1:def 5;
dom mcs = [:ccs,ccs:] by FUNCT_2:def 1;
then consider a,b being set such that
C1: a in ccs & b in ccs and
D1: x = [a,b] by A1, ZFMISC_1:def 2;
a in cR & b in cR by C1, N; then
reconsider a,b as Element of cR;
E1: ex a' being Element of cR st a'=a &
for s being Element of R holds a'*s = s*a' by C1;
F1: ex b' being Element of cR st b'=b &
for s being Element of R holds b'*s = s*b' by C1;
G1: [a,b] in [:ccs,ccs:] by C1,ZFMISC_1:def 2;
H1: a*b = (the mult of R).(a,b) by VECTSP_1:def 10
.= (the mult of R).[a,b] by BINOP_1:def 1
.= mcs.x by D1, G1, FUNCT_1:72;
now let s be Element of cR;
thus (a*b)*s=a*(b*s) by VECTSP_1:def 16
.= a*(s*b) by F1 .= (a*s)*b by VECTSP_1:def 16 .= (s*a)*b by E1
.= s*(a*b) by VECTSP_1:def 16;
end;
hence y in ccs by H1, A1a;
end; then
mcs is Function of [:ccs,ccs:],ccs by FUNCT_2:8; then
reconsider mcs as BinOp of ccs;
O1a: Zs = 0.R by RLVECT_1:def 2;
Q1a: Us = 1_ R by VECTSP_1:def 9;
reconsider Zs as Element of ccs by O1a,K;
now let s be Element of cR;
thus (1_ R)*s = s by VECTSP_1:def 19 .= s*(1_ R) by VECTSP_1:def 13;
end; then
Us in ccs by Q1a; then
reconsider Us as Element of ccs;
reconsider cs = doubleLoopStr (# ccs, acs, mcs, Us, Zs #)
as non empty doubleLoopStr;
O1: 0.cs = Zs by RLVECT_1:def 2;
Q1: 1_ cs = Us by VECTSP_1:def 9;
set ccs1 = the carrier of cs;
L: now let x,s be Element of cR; assume x in ccs; then
ex x' being Element of cR st x'=x &
for s being Element of R holds x'*s = s*x';
hence x*s=s*x;
end;
M: now let a,b be Element of cR, c,d be Element of ccs1 such that
A1: a=c & b=d;
B1: [c,d] in [:ccs,ccs:] by ZFMISC_1:def 2;
thus a*b=(the mult of R).(a,b) by VECTSP_1:def 10
.= (the mult of R).[a,b] by BINOP_1:def 1
.= mcs.[c,d] by A1,B1, FUNCT_1:72 .= mcs.(c,d) by BINOP_1:def 1
.= c*d by VECTSP_1:def 10;
end;
A: now let a,b being Element of cR, c,d be Element of ccs1 such that
A1: a=c & b=d;
B1: [c,d] in [:ccs,ccs:] by ZFMISC_1:def 2;
thus a+b= (the add of R).[a,b] by RLVECT_1:def 3
.= acs.[c,d] by A1,B1, FUNCT_1:72 .= c+d by RLVECT_1:def 3;
end;
T: cs is Abelian proof let x,y be Element of ccs1;
x in ccs1 & y in ccs1; then x in cR & y in cR by N; then
reconsider x'=x,y'=y as Element of cR;
thus x+y = y'+x' by A .= y+x by A;
end;
P: cs is add-associative proof let x,y,z be Element of ccs1;
x in ccs1 & y in ccs1 & z in ccs1; then x in cR & y in cR & z in cR by N;
then reconsider x'=x,y'=y,z'=z as Element of cR;
B2: x'+y'=x+y by A; C2: y'+z'=y+z by A;
thus (x+y)+z = (x'+y')+z' by B2,A .= x'+(y'+z') by RLVECT_1:def 6
.= x+(y+z) by C2,A;
end;
R: cs is right_zeroed proof let x be Element of ccs1;
x in ccs1; then x in cR by N; then reconsider x'=x as Element of cR;
thus x + 0.cs = x'+0.R by A, O1,O1a .= x by RLVECT_1:def 7;
end;
S: cs is right_complementable proof let x be Element of ccs1;
x in ccs1; then x in cR by N; then reconsider x'=x as Element of cR;
consider y' being Element of cR such that
A2: x' + y' = 0.R by RLVECT_1:def 8;
now let s be Element of cR;
B2: s*x'=x'*s by L;
0.R*s=0.R by VECTSP_1:39 .= s*0.R by VECTSP_1:36; then
(x'+y')*s=s*(x'+y') by A2; then
x'*s+y'*s=s*(x'+y') by VECTSP_1:def 12; then
x'*s+y'*s=s*x'+s*y' by VECTSP_1:def 11; then
-(x'*s)+(x'*s+y'*s)=-(s*x')+(s*x'+s*y') by B2; then
(-(x'*s)+x'*s)+y'*s=-(s*x')+(s*x'+s*y') by RLVECT_1:def 6; then
0.R+y'*s=-(s*x')+(s*x'+s*y') by RLVECT_1:16; then
y'*s=-(s*x')+(s*x'+s*y') by RLVECT_1:10; then
y'*s=(-(s*x')+s*x')+s*y' by RLVECT_1:def 6; then
y'*s=0.R+s*y' by RLVECT_1:16;
hence y'*s=s*y' by RLVECT_1:10;
end; then y' in ccs1; then reconsider y=y' as Element of ccs1;
x'+y'=x+y by A;
hence ex y being Element of ccs1 st x + y = 0.cs by A2,O1,O1a;
end;
U: cs is associative proof let x,y,z be Element of ccs1;
x in ccs1 & y in ccs1 & z in ccs1; then x in cR & y in cR & z in cR by N;
then reconsider x'=x,y'=y,z'=z as Element of cR;
B2: x'*y'=x*y by M; C2: y'*z'=y*z by M;
thus (x*y)*z = (x'*y')*z' by B2,M .= x'*(y'*z') by VECTSP_1:def 16
.= x*(y*z) by C2,M;
end;
W: cs is left_unital proof let x be Element of ccs1;
x in ccs1; then x in cR by N; then reconsider x'=x as Element of cR;
thus (1_ cs) * x = (1_ R)*x' by Q1,Q1a,M .= x by VECTSP_1:def 19;
end;
X: cs is distributive proof let x,y,z be Element of ccs1;
x in ccs1 & y in ccs1 & z in ccs1; then x in cR & y in cR & z in cR by N;
then reconsider x'=x,y'=y,z'=z as Element of cR;
A2: y+z=y'+z' by A; B2: x'*y'=x*y by M; C2: x'*z'=x*z by M;
D2: y'*x'=y*x by M; E2: z'*x'=z*x by M;
thus x*(y+z) = x'*(y'+z') by A2, M .= x'*y'+x'*z' by VECTSP_1:def 18
.= x*y+x*z by B2,C2,A;
thus (y+z)*x = (y'+z')*x' by A2,M .= y'*x'+z'*x' by VECTSP_1:def 18
.= y*x+z*x by D2,E2,A;
end;
Y: cs is Field-like proof let x be Element of ccs1 such that
A2: x <> 0.cs;
x in ccs1; then x in cR by N; then reconsider x'=x as Element of cR;
consider y' being Element of cR such that
B2: x'*y'=1_ R by O1, O1a,A2, VECTSP_1:def 20;
now let s be Element of cR;
(1_ R)*s = s by VECTSP_1:def 19 .= s*(1_ R) by VECTSP_1:def 13; then
x'*y'*s = (s*x')*y' by B2, VECTSP_1:def 16; then
x'*y'*s = x'*s*y' by L; then x'"*(x'*y'*s) = x'"*(x'*s*y'); then
x'"*(x'*y')*s = x'"*(x'*s*y') by VECTSP_1:def 16; then
x'"*(x'*y')*s = x'"*(x'*s)*y' by VECTSP_1:def 16; then
x'"*x'*y'*s = x'"*(x'*s)*y' by VECTSP_1:def 16; then
x'"*x'*y'*s = x'"*x'*s*y' by VECTSP_1:def 16; then
(1_ R)*y'*s = x'"*x'*s*y' by A2, O1,O1a,VECTSP_2:43; then
(1_ R)*y'*s = (1_ R)*s*y' by A2, O1,O1a,VECTSP_2:43; then
y'*s = (1_ R)*s*y' by VECTSP_1:def 19;
hence y'*s=s*y' by VECTSP_1:def 19;
end; then y' in ccs1; then reconsider y=y' as Element of ccs1;
take y;
thus x*y= 1_ cs by B2,Q1,Q1a,M;
end;
Z: cs is commutative proof let x,y be Element of ccs1;
x in ccs1 & y in ccs1; then x in cR & y in cR by N;
then reconsider x'=x,y'=y as Element of cR;
thus x*y = x'*y' by M .= y'*x' by L .= y*x by M;
end;
0.R <> 1_ R by VECTSP_1:def 21; then
cs is non degenerated by O1,O1a,Q1,Q1a,VECTSP_1:def 21;
hence thesis by P,R,S,T,U,W,X,Y, Z;
end;
uniqueness;
end;
theorem Center0: :: Center0:
for R being Skew-Field holds the carrier of center R c= the carrier of R
proof let R be Skew-Field;
for x being set st x in the carrier of center R holds x in the carrier of R
proof let y be set such that
A0: y in the carrier of center R;
y in {x where x is Element of R: for s being Element of R holds x*s = s*x}
by A0,DefCenter; then
consider x being Element of R such that
A1: x = y and for s being Element of R holds x*s = s*x;
thus thesis by A1;
end;
hence thesis by TARSKI:def 3;
end;
definition let R be finite Skew-Field;
cluster center R -> finite;
correctness proof
the carrier of center R c= the carrier of R by Center0; then
the carrier of center R is finite by FINSET_1:13;
hence thesis by GROUP_1:def 13;
end;
end;
theorem Center1: :: Center1:
for R being Skew-Field, y being Element of R
holds y in center R iff for s being Element of R holds y*s = s*y
proof let R be Skew-Field, y be Element of R;
hereby assume y in center R; then
y in the carrier of center R by RLVECT_1:def 1; then
y in {x where x is Element of R:
for s being Element of R holds x*s = s*x}
by DefCenter; then
consider x being Element of R such that
A0: x = y and A1: for s being Element of R holds x*s=s*x;
thus for s being Element of R holds y*s = s*y by A0,A1;
end;
now assume for s being Element of R holds y*s = s*y;
then y in {x where x is Element of R:
for s being Element of R holds x*s = s*x};
then y is Element of center R by DefCenter;
then y in the carrier of center R;
hence y in center R by RLVECT_1:def 1;
end;
hence thesis;
end;
theorem Center1a: :: Center1a:
for R being Skew-Field holds 0.R in center R
proof let R be Skew-Field;
for s being Element of R holds 0.R*s = s*0.R
proof let s be Element of R;
0.R*s = 0.R by VECTSP_1:39 .= s*0.R by VECTSP_1:36;
hence thesis;
end;
hence thesis by Center1;
end;
theorem Center1b: :: Center1b:
for R being Skew-Field holds 1_ R in center R
proof let R be Skew-Field;
for s being Element of R holds (1_ R)*s = s*(1_ R)
proof let s be Element of R;
(1_ R)*s = s by VECTSP_1:def 19 .= s*(1_ R) by VECTSP_1:def 13;
hence thesis;
end;
hence thesis by Center1;
end;
theorem Center2: :: Center2:
for R being finite Skew-Field holds 1 < card (the carrier of center R)
proof let R be finite Skew-Field;
0.R <> 1_ R by VECTSP_1:def 21; then
A1: card {0.R, 1_ R} = 2 by CARD_2:76;
0.R in center R by Center1a; then
A2: 0.R in the carrier of center R by RLVECT_1:def 1;
for s being Element of R holds (1_ R)*s = s*(1_ R)
proof let s be Element of R;
s*(1_ R) = s by VECTSP_1:def 13 .= (1_ R)*s by VECTSP_1:def 19;
hence thesis;
end; then
1_ R in center R by Center1; then
1_ R in the carrier of center R by RLVECT_1:def 1; then
{0.R, 1_ R} c= the carrier of center R by A2,ZFMISC_1:38; then
2 <= card the carrier of center R by A1,CARD_1:80;
hence thesis by AXIOMS:22;
end;
theorem Center3: :: Center3:
for R being finite Skew-Field holds
card the carrier of center R = card the carrier of R iff R is commutative
proof let R be finite Skew-Field;
set X = the carrier of R; set Y = the carrier of center R;
hereby assume A0: card X = card Y;
A1: Y c= X by Center0; then
card (X \ Y) = card X - card X by A0,CARD_2:63; then
card (X \ Y) = 0 by XCMPLX_1:14; then X \ Y = {} by CARD_4:17; then
X c= Y by XBOOLE_1:37; then
A2: X = Y by A1, XBOOLE_0:def 10;
for x being Element of X
holds for s being Element of X holds x*s=s*x
proof let x be Element of X; x in center R by A2,RLVECT_1:def 1;
hence thesis by Center1;
end;
hence R is commutative by VECTSP_1:def 17;
end;
now assume A0: R is commutative;
for x being set st x in X holds x in Y
proof let x be set such that B0: x in X;
for x being Element of X holds x is Element of Y
proof let x be Element of X;
for y being Element of X holds x*y = y*x by A0,VECTSP_1:def 17;
then x in center R by Center1;
hence thesis by RLVECT_1:def 1;
end; then x is Element of Y by B0;
hence thesis;
end; then
A1: X c= Y by TARSKI:def 3; Y c= X by Center0;
hence card Y = card X by A1,XBOOLE_0:def 10;
end;
hence thesis;
end;
theorem Center4: :: Center4:
for R being Skew-Field
holds the carrier of center R = (the carrier of center MultGroup R) \/ {0.R}
proof let R being Skew-Field;
AA: the carrier of center MultGroup R c= the carrier of MultGroup R
by GROUP_2:def 5;
AB: the carrier of MultGroup R = (the carrier of R) \ {0.R} by UNIROOTS:def 1;
AC: (the carrier of MultGroup R)\/ {0.R} = the carrier of R by UNIROOTS:18;
AD: the carrier of center R c= the carrier of R by Center0;
A:(the carrier of center MultGroup R) \/ {0.R} c= the carrier of center R
proof
let x be set;
assume x in (the carrier of center MultGroup R) \/ {0.R}; then
A1: x in the carrier of center MultGroup R or x in {0.R} by XBOOLE_0:def 2;
per cases by A1;
suppose S1: x in the carrier of center MultGroup R; then
x in the carrier of MultGroup R by AA; then
reconsider a = x as Element of MultGroup R;
a in center MultGroup R by S1, RLVECT_1:def 1; then
A2: for b being Element of MultGroup R holds a*b = b*a by GROUP_5:89;
a is Element of R by UNIROOTS:22; then
reconsider a1 = a as Element of R;
now let b be Element of R;
A3: b in (the carrier of MultGroup R) or b in {0.R} by AC,XBOOLE_0:def 2;
thus a1*b = b*a1 proof
per cases by A3;
suppose b in (the carrier of MultGroup R); then
reconsider b1 = b as Element of MultGroup R;
thus a1*b = a*b1 by UNIROOTS:19 .= b1*a by A2 .= b*a1 by UNIROOTS:19;
suppose b in {0.R}; then
A4: b = 0.R by TARSKI:def 1;
thus a1*b = 0.R by A4, VECTSP_1:36 .= b*a1 by A4, VECTSP_1:39;
end;
end; then
a1 in center R by Center1;
hence thesis by RLVECT_1:def 1;
suppose x in {0.R}; then x = 0.R by TARSKI:def 1;
then x in center R by Center1a;
hence x in the carrier of center R by RLVECT_1:def 1;
end;
the carrier of center R c= (the carrier of center MultGroup R) \/ {0.R}
proof
let x be set; assume
A2: x in the carrier of center R; then
reconsider a = x as Element of center R;
a in the carrier of R by A2, AD; then
reconsider a1 = a as Element of R;
per cases;
suppose a1 = 0.R; then a1 in {0.R} by TARSKI:def 1;
hence x in (the carrier of center MultGroup R) \/ {0.R} by XBOOLE_0:def 2;
suppose a1 <> 0.R; then
A3: not a1 in {0.R} by TARSKI:def 1;
a1 in the carrier of MultGroup R by A3, AB, XBOOLE_0:def 4; then
reconsider a2 = a1 as Element of MultGroup R;
now let b be Element of MultGroup R;
B4: b in the carrier of MultGroup R;
the carrier of MultGroup R c= (the carrier of R) by AB, XBOOLE_1:36;
then b in the carrier of R by B4;
then reconsider b1 = b as Element of R;
A4: x in center R by A2, RLVECT_1:def 1;
thus a2*b=a1*b1 by UNIROOTS:19 .= b1*a1 by A4, Center1
.= b*a2 by UNIROOTS:19;
end; then
a1 in center MultGroup R by GROUP_5:89; then
a1 in the carrier of center MultGroup R by RLVECT_1:def 1;
hence x in (the carrier of center MultGroup R) \/ {0.R} by XBOOLE_0:def 2;
end;
hence thesis by A, XBOOLE_0:def 10;
end;
definition
let R be Skew-Field, s be Element of R;
func centralizer s -> strict Skew-Field means :DefCentral:
the carrier of it = {x where x is Element of R: x*s = s*x} &
the add of it = (the add of R) | [:the carrier of it,the carrier of it:] &
the mult of it = (the mult of R) | [:the carrier of it,the carrier of it:]&
the Zero of it = the Zero of R &
the unity of it = the unity of R;
existence proof
set cR = the carrier of R;
set ccs = {x where x is Element of R: x*s = s*x};
(0.R)*s = 0.R by VECTSP_1:39 .= s*(0.R) by VECTSP_1:36; then
0.R in ccs; then
reconsider ccs as non empty set;
N: ccs c= cR proof let x be set; assume x in ccs; then
ex x' being Element of cR st x'=x & x'*s=s*x';
hence thesis;
end;
set acs = (the add of R) | [:ccs,ccs:];
set mcs = (the mult of R) | [:ccs,ccs:];
set Zs = the Zero of R; set Us = the unity of R;
B: [:ccs,ccs:] c= [:cR,cR:] proof let x be set; assume x in [:ccs,ccs:];
then consider a,b being set such that
A1: a in ccs & b in ccs and
B1: x =[a,b] by ZFMISC_1:def 2;
a in cR & b in cR by N, A1;
hence x in [:cR,cR:] by B1, ZFMISC_1:def 2;
end;
reconsider acs as Function of [:ccs,ccs:],cR by B, FUNCT_2:38;
rng acs c= ccs proof let y be set; assume y in rng acs; then
consider x being set such that
A1: x in dom acs and
A1a: y = acs.x by FUNCT_1:def 5;
dom acs = [:ccs,ccs:] by FUNCT_2:def 1;
then consider a,b being set such that
C1: a in ccs & b in ccs and
D1: x = [a,b] by A1, ZFMISC_1:def 2;
a in cR & b in cR by C1, N; then
reconsider a,b as Element of cR;
E1: ex a' being Element of cR st a'=a & a'*s=s*a' by C1;
F1: ex b' being Element of cR st b'=b & b'*s=s*b' by C1;
G1: [a,b] in [:ccs,ccs:] by C1,ZFMISC_1:def 2;
H1: a+b = (the add of R).[a,b] by RLVECT_1:def 3
.= acs.x by D1, G1, FUNCT_1:72;
(a+b)*s=s*a+s*b by E1,F1,VECTSP_1:def 12
.=s*(a+b) by VECTSP_1:def 11;
hence y in ccs by H1, A1a;
end; then
acs is Function of [:ccs,ccs:],ccs by FUNCT_2:8; then
reconsider acs as BinOp of ccs;
reconsider mcs as Function of [:ccs,ccs:],cR by B, FUNCT_2:38;
rng mcs c= ccs proof let y be set; assume y in rng mcs; then
consider x being set such that
A1: x in dom mcs and
A1a: y = mcs.x by FUNCT_1:def 5;
dom mcs = [:ccs,ccs:] by FUNCT_2:def 1;
then consider a,b being set such that
C1: a in ccs & b in ccs and
D1: x = [a,b] by A1, ZFMISC_1:def 2;
a in cR & b in cR by C1, N; then
reconsider a,b as Element of cR;
E1: ex a' being Element of cR st a'=a & a'*s=s*a' by C1;
F1: ex b' being Element of cR st b'=b & b'*s=s*b' by C1;
G1: [a,b] in [:ccs,ccs:] by C1,ZFMISC_1:def 2;
H1: a*b = (the mult of R).(a,b) by VECTSP_1:def 10
.= (the mult of R).[a,b] by BINOP_1:def 1
.= mcs.x by D1, G1, FUNCT_1:72;
(a*b)*s=a*(s*b) by F1,VECTSP_1:def 16 .= (a*s)*b by VECTSP_1:def 16
.= s*(a*b) by E1, VECTSP_1:def 16;
hence y in ccs by H1, A1a;
end; then
mcs is Function of [:ccs,ccs:],ccs by FUNCT_2:8; then
reconsider mcs as BinOp of ccs;
O1a: Zs = 0.R by RLVECT_1:def 2;
Q1a: Us = 1_ R by VECTSP_1:def 9;
(0.R)*s = 0.R by VECTSP_1:39 .= s*(0.R) by VECTSP_1:36; then
Zs in ccs by O1a; then
reconsider Zs as Element of ccs;
(1_ R)*s = s by VECTSP_1:def 19 .= s*(1_ R) by VECTSP_1:def 13; then
Us in ccs by Q1a; then
reconsider Us as Element of ccs;
reconsider cs = doubleLoopStr (# ccs, acs, mcs, Us, Zs #)
as non empty doubleLoopStr;
O1: 0.cs = Zs by RLVECT_1:def 2;
Q1: 1_ cs = Us by VECTSP_1:def 9;
set ccs1 = the carrier of cs;
L: now let x be Element of cR; assume x in ccs; then
ex x' being Element of cR st x'=x & x'*s = s*x';
hence x*s=s*x;
end;
M: now let a,b be Element of cR, c,d be Element of ccs1 such that
A1: a=c & b=d;
B1: [c,d] in [:ccs,ccs:] by ZFMISC_1:def 2;
thus a*b=(the mult of R).(a,b) by VECTSP_1:def 10
.= (the mult of R).[a,b] by BINOP_1:def 1
.= mcs.[c,d] by A1,B1, FUNCT_1:72 .= mcs.(c,d) by BINOP_1:def 1
.= c*d by VECTSP_1:def 10;
end;
A: now let a,b being Element of cR, c,d be Element of ccs1 such that
A1: a=c & b=d;
B1: [c,d] in [:ccs,ccs:] by ZFMISC_1:def 2;
thus a+b= (the add of R).[a,b] by RLVECT_1:def 3
.= acs.[c,d] by A1,B1, FUNCT_1:72 .= c+d by RLVECT_1:def 3;
end;
T: cs is Abelian proof let x,y be Element of ccs1;
x in ccs1 & y in ccs1; then x in cR & y in cR by N; then
reconsider x'=x,y'=y as Element of cR;
thus x+y = y'+x' by A .= y+x by A;
end;
P: cs is add-associative proof let x,y,z be Element of ccs1;
x in ccs1 & y in ccs1 & z in ccs1; then x in cR & y in cR & z in cR by N;
then reconsider x'=x,y'=y,z'=z as Element of cR;
B2: x'+y'=x+y by A; C2: y'+z'=y+z by A;
thus (x+y)+z = (x'+y')+z' by B2,A .= x'+(y'+z') by RLVECT_1:def 6
.= x+(y+z) by C2,A;
end;
R: cs is right_zeroed proof let x be Element of ccs1;
x in ccs1; then x in cR by N; then reconsider x'=x as Element of cR;
thus x + 0.cs = x'+0.R by A, O1,O1a .= x by RLVECT_1:def 7;
end;
S: cs is right_complementable proof let x be Element of ccs1;
x in ccs1; then x in cR by N; then reconsider x'=x as Element of cR;
consider y' being Element of cR such that
A2: x' + y' = 0.R by RLVECT_1:def 8;
B2: s*x'=x'*s by L;
0.R*s=0.R by VECTSP_1:39 .= s*0.R by VECTSP_1:36; then
(x'+y')*s=s*(x'+y') by A2; then
x'*s+y'*s=s*(x'+y') by VECTSP_1:def 12; then
x'*s+y'*s=s*x'+s*y' by VECTSP_1:def 11; then
-(x'*s)+(x'*s+y'*s)=-(s*x')+(s*x'+s*y') by B2; then
(-(x'*s)+x'*s)+y'*s=-(s*x')+(s*x'+s*y') by RLVECT_1:def 6; then
0.R+y'*s=-(s*x')+(s*x'+s*y') by RLVECT_1:16; then
y'*s=-(s*x')+(s*x'+s*y') by RLVECT_1:10; then
y'*s=(-(s*x')+s*x')+s*y' by RLVECT_1:def 6; then
y'*s=0.R+s*y' by RLVECT_1:16; then y'*s=s*y' by RLVECT_1:10; then
y' in ccs1; then reconsider y=y' as Element of ccs1;
x'+y'=x+y by A;
hence ex y being Element of ccs1 st x + y = 0.cs by A2,O1,O1a;
end;
U: cs is associative proof let x,y,z be Element of ccs1;
x in ccs1 & y in ccs1 & z in ccs1; then x in cR & y in cR & z in cR by N;
then reconsider x'=x,y'=y,z'=z as Element of cR;
B2: x'*y'=x*y by M; C2: y'*z'=y*z by M;
thus (x*y)*z = (x'*y')*z' by B2,M .= x'*(y'*z') by VECTSP_1:def 16
.= x*(y*z) by C2,M;
end;
V: cs is right_unital proof let x be Element of ccs1;
x in ccs1; then x in cR by N; then reconsider x'=x as Element of cR;
thus x*(1_ cs) = x'*(1_ R) by Q1,Q1a,M .= x by VECTSP_1:def 13;
end;
W: cs is left_unital proof let x be Element of ccs1;
x in ccs1; then x in cR by N; then reconsider x'=x as Element of cR;
thus (1_ cs) * x = (1_ R)*x' by Q1,Q1a,M .= x by VECTSP_1:def 19;
end;
X: cs is distributive proof let x,y,z be Element of ccs1;
x in ccs1 & y in ccs1 & z in ccs1; then x in cR & y in cR & z in cR by N;
then reconsider x'=x,y'=y,z'=z as Element of cR;
A2: y+z=y'+z' by A; B2: x'*y'=x*y by M; C2: x'*z'=x*z by M;
D2: y'*x'=y*x by M; E2: z'*x'=z*x by M;
thus x*(y+z) = x'*(y'+z') by A2, M .= x'*y'+x'*z' by VECTSP_1:def 18
.= x*y+x*z by B2,C2,A;
thus (y+z)*x = (y'+z')*x' by A2,M .= y'*x'+z'*x' by VECTSP_1:def 18
.= y*x+z*x by D2,E2,A;
end;
Y: cs is Field-like proof let x be Element of ccs1 such that
A2: x <> 0.cs;
x in ccs1; then x in cR by N; then reconsider x'=x as Element of cR;
consider y' being Element of cR such that
B2: x'*y'=1_ R by O1, O1a,A2, VECTSP_1:def 20;
(1_ R)*s = s by VECTSP_1:def 19 .= s*(1_ R) by VECTSP_1:def 13; then
x'*y'*s = (s*x')*y' by B2, VECTSP_1:def 16; then
x'*y'*s = x'*s*y' by L; then x'"*(x'*y'*s) = x'"*(x'*s*y'); then
x'"*(x'*y')*s = x'"*(x'*s*y') by VECTSP_1:def 16; then
x'"*(x'*y')*s = x'"*(x'*s)*y' by VECTSP_1:def 16; then
x'"*x'*y'*s = x'"*(x'*s)*y' by VECTSP_1:def 16; then
x'"*x'*y'*s = x'"*x'*s*y' by VECTSP_1:def 16; then
(1_ R)*y'*s = x'"*x'*s*y' by A2, O1,O1a,VECTSP_2:43; then
(1_ R)*y'*s = (1_ R)*s*y' by A2, O1,O1a,VECTSP_2:43; then
y'*s = (1_ R)*s*y' by VECTSP_1:def 19; then
y'*s=s*y' by VECTSP_1:def 19; then y' in ccs1; then
reconsider y=y' as Element of ccs1;
take y;
thus x*y= 1_ cs by B2,Q1,Q1a,M;
end;
0.R <> 1_ R by VECTSP_1:def 21; then
cs is non degenerated by O1,O1a,Q1,Q1a,VECTSP_1:def 21;
hence thesis by P,R,S,T,U,V,W,X,Y;
end;
uniqueness;
end;
theorem Central00: :: Central00:
for R be Skew-Field, s be Element of R
holds the carrier of centralizer s c= the carrier of R
proof let R be Skew-Field, s be Element of R;
set cs = centralizer s; set ccs = the carrier of cs;
C: ccs = {x where x is Element of R: x*s = s*x} by DefCentral;
let x be set;
assume x in the carrier of centralizer s; then
ex a being Element of R st a=x & a*s=s*a by C;
hence x in the carrier of R;
end;
theorem Central02a: :: Central02a:
for R be Skew-Field, s, a be Element of R
holds a in the carrier of centralizer s iff a*s = s*a
proof let R be Skew-Field, s, a be Element of R;
set cs = centralizer s; set ccs = the carrier of cs;
C: ccs = {x where x is Element of R: x*s = s*x} by DefCentral;
hereby assume a in the carrier of centralizer s; then
ex x being Element of R st a=x & x*s=s*x by C;
hence a*s = s*a;
end;
assume a*s = s*a;
hence a in the carrier of centralizer s by C;
end;
theorem :: Central02b:
for R be Skew-Field, s be Element of R
holds the carrier of center R c= the carrier of centralizer s
proof let R be Skew-Field, s be Element of R;
let x be set; assume
A: x in the carrier of center R;
the carrier of center R c= the carrier of R by Center0; then
x in the carrier of R by A; then
reconsider a = x as Element of R;
a in center R by A, RLVECT_1:def 1; then
a*s=s*a by Center1;
hence x in the carrier of centralizer s by Central02a;
end;
theorem Central02: :: Central02:
for R be Skew-Field, s, a, b be Element of R
st a in the carrier of center R & b in the carrier of centralizer s
holds a*b in the carrier of centralizer s
proof let R be Skew-Field, s, a, b be Element of R such that
A: a in the carrier of center R and
B: b in the carrier of centralizer s;
set cs = centralizer s; set ccs = the carrier of cs;
C: ccs = {x where x is Element of R: x*s = s*x} by DefCentral;
D: a in center R by A, RLVECT_1:def 1;
a*b*s=a*(b*s) by VECTSP_1:def 16
.= (b*s)*a by D, Center1
.= (s*b)*a by B, Central02a
.= s*(b*a) by VECTSP_1:def 16
.= s*(a*b) by D, Center1;
hence a*b in the carrier of centralizer s by C;
end;
theorem Central0: :: Central0:
for R be Skew-Field, s be Element of R
holds 0.R is Element of centralizer s & 1_ R is Element of centralizer s
proof let R be Skew-Field, s be Element of R;
0.R*s = 0.R by VECTSP_1:39 .= s*0.R by VECTSP_1:36; then
0.R in {x where x is Element of R: x*s = s*x}; then
A1: 0.R is Element of centralizer s by DefCentral;
s*(1_ R) = s by VECTSP_1:def 13 .= (1_ R)*s by VECTSP_1:def 19; then
1_ R in {x where x is Element of R: x*s = s*x}; then
1_ R is Element of centralizer s by DefCentral;
hence thesis by A1;
end;
definition let R be finite Skew-Field;
let s be Element of R;
cluster centralizer s -> finite;
correctness proof
the carrier of centralizer s c= the carrier of R by Central00; then
the carrier of centralizer s is finite by FINSET_1:13;
hence thesis by GROUP_1:def 13;
end;
end;
theorem Central1: :: Central1:
for R be finite Skew-Field, s be Element of R
holds 1 < card (the carrier of centralizer s)
proof let R be finite Skew-Field, s be Element of R;
0.R <> 1_ R by VECTSP_1:def 21; then
A1: card {0.R, 1_ R} = 2 by CARD_2:76;
0.R is Element of centralizer s &
1_ R is Element of centralizer s by Central0; then
{0.R, 1_ R} c= the carrier of centralizer s by ZFMISC_1:38; then
2 <= card the carrier of centralizer s by A1,CARD_1:80;
hence thesis by AXIOMS:22;
end;
theorem Central2a: :: Central2a:
for R being Skew-Field, s being Element of R, t being Element of MultGroup R
st t = s
holds the carrier of centralizer s = (the carrier of Centralizer t) \/ {0.R}
proof let R be Skew-Field, s be Element of R,
t be Element of MultGroup R such that
A: t = s;
set ct = Centralizer t, cs = centralizer s;
set cct = the carrier of ct, ccs = the carrier of cs;
AA: the carrier of MultGroup R = (the carrier of R) \ {0.R} by UNIROOTS:def 1;
C: cct = { b where b is Element of MultGroup R : t*b = b*t } by Def1;
D: ccs = {x where x is Element of R: x*s = s*x} by DefCentral;
now let x be set;
hereby assume x in ccs; then
consider c being Element of R such that
A1: c = x and
B1: c*s=s*c by D;
per cases;
suppose c = 0.R; then c in {0.R} by TARSKI:def 1;
hence x in cct \/ {0.R} by A1, XBOOLE_0:def 2;
suppose c <> 0.R; then not c in {0.R} by TARSKI:def 1; then
c in the carrier of MultGroup R by AA, XBOOLE_0:def 4; then
reconsider c1 = c as Element of MultGroup R;
t*c1 = s*c by A, UNIROOTS:19 .= c1*t by B1, A, UNIROOTS:19; then
c in cct by C;
hence x in cct \/ {0.R} by A1, XBOOLE_0:def 2;
end;
assume x in cct \/ {0.R}; then
A1: x in cct or x in {0.R} by XBOOLE_0:def 2;
per cases by A1;
suppose x in cct; then consider b being Element of MultGroup R such that
A2: x = b and
B2: t*b = b*t by C;
reconsider b1 = b as Element of R by UNIROOTS:22;
b1*s = t*b by A, B2, UNIROOTS:19 .= s*b1 by A, UNIROOTS:19;
hence x in ccs by A2, D;
suppose x in {0.R}; then
A2: x = 0.R by TARSKI:def 1;
0.R*s = 0.R by VECTSP_1:39 .= s*0.R by VECTSP_1:36;
hence x in ccs by A2, D;
end;
hence thesis by TARSKI:2;
end;
theorem Central2: :: Central2:
for R being finite Skew-Field, s being Element of R,
t being Element of MultGroup R st t = s
holds ord Centralizer t = card (the carrier of centralizer s) - 1
proof let R be finite Skew-Field, s be Element of R,
t be Element of MultGroup R such that
A: t = s;
set ct = Centralizer t, cs = centralizer s;
set cct = the carrier of ct, ccs = the carrier of cs;
the carrier of MultGroup R = (the carrier of R) \ {0.R}
by UNIROOTS:def 1; then
not 0.R in the carrier of MultGroup R by ZFMISC_1:64; then
not 0.R in MultGroup R by RLVECT_1:def 1; then
not 0.R in ct by GCTR2; then
B: not 0.R in cct by RLVECT_1:def 1;
cct \/ {0.R} = ccs by A, Central2a; then
Z: card ccs = card cct +1 by B, CARD_2:54;
thus ord Centralizer t = card cct by GROUP_1:def 14
.= card (ccs) - 1 by Z, XCMPLX_1:26;
end;
begin :: Vector spaces over centers of skew fields
definition
let R be Skew-Field;
func VectSp_over_center R -> strict VectSp of center R means :LVSOC:
the LoopStr of it = the LoopStr of R &
the lmult of it = (the mult of R )
| [:the carrier of center R, the carrier of R:];
existence proof
set cR = center R; set ccR = the carrier of cR;
set ccs = the carrier of R;
set lm = (the mult of R)|[:ccR, ccs:];
D1a: ccR c= the carrier of R by Center0;
B1: dom (the mult of R) = [:the carrier of R,the carrier of R:]
by FUNCT_2:def 1;
[:ccR, ccs:] c= [:the carrier of R,the carrier of R:] proof
let x be set; assume x in [:ccR, ccs:]; then
consider x1, x2 being set such that
A2: x1 in ccR and
B2: x2 in ccs and
C2: x = [x1,x2] by ZFMISC_1:def 2;
x1 in the carrier of R & x2 in the carrier of R by A2, D1a, B2;
hence thesis by C2, ZFMISC_1:def 2;
end; then
A1: dom lm = [:ccR, ccs:] by B1, RELAT_1:91;
now let x be set; assume
D2: x in [:ccR, ccs:]; then
consider x1, x2 being set such that
A2: x1 in ccR and
B2: x2 in ccs and
C2: x = [x1,x2] by ZFMISC_1:def 2;
reconsider x1 as Element of R by A2, D1a;
reconsider x2 as Element of R by B2;
lm.x = (the mult of R).x by D2, FUNCT_1:72
.= (the mult of R).(x1,x2) by C2, BINOP_1:def 1
.= x1*x2 by VECTSP_1:def 10;
hence lm.x in ccs;
end; then
reconsider lm as Function of [:ccR,ccs:], ccs by A1, FUNCT_2:5;
set Vos = VectSpStr(#
ccs, the add of R,
the Zero of R, lm #);
set cV = the carrier of Vos;
set aV = the add of Vos, ac = the add of R;
set ZV = the Zero of Vos, Zc = the Zero of R;
A: Vos is VectSp-like proof
let x,y be Element of ccR, v,w be Element of cV;
D1: x in ccR & y in ccR;
x in the carrier of R & y in the carrier of R by D1, D1a; then
reconsider xx=x, yy=y as Element of R;
reconsider vv=v, ww=w as Element of R;
A1: the mult of cR = (the mult of R) | [:ccR,ccR:] by DefCenter;
B1: the add of cR = (the add of R) | [:ccR,ccR:] by DefCenter;
O1: [x,w] in [:ccR,ccs:] by ZFMISC_1:def 2;
P1: [x,v+w] in [:ccR,ccs:] by ZFMISC_1:def 2;
S1: [y,v] in [:ccR,ccs:] by ZFMISC_1:def 2;
T1: [x,v] in [:ccR,ccs:] by ZFMISC_1:def 2;
W1: [x+y,v] in [:ccR,ccs:] by ZFMISC_1:def 2;
V1: [x,y*v] in [:ccR,ccs:] by ZFMISC_1:def 2;
U1: [y,v] in [:ccR,ccs:] by ZFMISC_1:def 2;
X1: [x*y,v] in [:ccR,ccs:] by ZFMISC_1:def 2;
Y1: [x,y] in [:ccR,ccR:] by ZFMISC_1:def 2;
thus x*(v+w) = lm.(x,v+w) by VECTSP_1:def 24
.= lm.[x,v+w] by BINOP_1:def 1
.= (the mult of R).[x,v+w] by P1, FUNCT_1:72
.= (the mult of R).[x,(the add of R).[vv,ww]] by RLVECT_1:def 3
.= (the mult of R).[x,vv+ww] by RLVECT_1:def 3
.= (the mult of R).(xx,vv+ww) by BINOP_1:def 1
.= xx*(vv+ww) by VECTSP_1:def 10
.= xx*vv+xx*ww by VECTSP_1:def 11
.= (the add of R).[xx*vv,xx*ww] by RLVECT_1:def 3
.= (the add of R).[(the mult of R).(xx,vv),xx*ww] by VECTSP_1:def 10
.= (the add of R).[(the mult of R).[xx,vv],xx*ww] by BINOP_1:def 1
.= (the add of R).[lm.[x,v],xx*ww] by T1, FUNCT_1:72
.= (the add of R).[lm.(x,v),xx*ww] by BINOP_1:def 1
.= (the add of R).[x*v,xx*ww] by VECTSP_1:def 24
.= (the add of R).[x*v,(the mult of R).(xx,ww)] by VECTSP_1:def 10
.= (the add of R).[x*v,(the mult of R).[xx,ww]] by BINOP_1:def 1
.= (the add of R).[x*v,lm.[x,w]] by O1, FUNCT_1:72
.= (the add of R).[x*v,lm.(x,w)] by BINOP_1:def 1
.= aV.[x*v,x*w] by VECTSP_1:def 24
.= x*v+x*w by RLVECT_1:def 3;
thus (x+y)*v = lm.(x+y,v) by VECTSP_1:def 24
.= lm.[x+y,v] by BINOP_1:def 1
.= (the mult of R).[x+y,vv] by W1, FUNCT_1:72
.= (the mult of R).[(the add of cR).[x,y],vv] by RLVECT_1:def 3
.= (the mult of R).[(the add of R).[xx,yy],vv] by B1, Y1, FUNCT_1:72
.= (the mult of R).[xx+yy,vv] by RLVECT_1:def 3
.= (the mult of R).(xx+yy,vv) by BINOP_1:def 1
.= (xx+yy)*vv by VECTSP_1:def 10
.= xx*vv+yy*vv by VECTSP_1:def 12
.= (the add of R).[xx*vv,yy*vv] by RLVECT_1:def 3
.= (the add of R).[(the mult of R).(xx,vv),yy*vv] by VECTSP_1:def 10
.= (the add of R).[(the mult of R).[xx,vv],yy*vv] by BINOP_1:def 1
.= (the add of R).[lm.[x,v],yy*vv] by T1, FUNCT_1:72
.= (the add of R).[lm.(x,v),yy*vv] by BINOP_1:def 1
.= (the add of R).[x*v,yy*vv] by VECTSP_1:def 24
.= (the add of R).[x*v,(the mult of R).(yy,vv)] by VECTSP_1:def 10
.= (the add of R).[x*v,(the mult of R).[yy,vv]] by BINOP_1:def 1
.= (the add of R).[x*v,lm.[y,v]] by S1, FUNCT_1:72
.= (the add of R).[x*v,lm.(y,v)] by BINOP_1:def 1
.= aV.[x*v,y*v] by VECTSP_1:def 24
.= x*v+y*v by RLVECT_1:def 3;
thus (x*y)*v = lm.(x*y,v) by VECTSP_1:def 24
.= lm.[x*y,v] by BINOP_1:def 1
.= (the mult of R).[x*y,vv] by X1, FUNCT_1:72
.= (the mult of R).[(the mult of cR).(x,y),vv] by VECTSP_1:def 10
.= (the mult of R).[(the mult of cR).[x,y],vv] by BINOP_1:def 1
.= (the mult of R).[(the mult of R).[xx,yy],vv] by A1, Y1, FUNCT_1:72
.= (the mult of R).[(the mult of R).(xx,yy),vv] by BINOP_1:def 1
.= (the mult of R).[xx*yy,vv] by VECTSP_1:def 10
.= (the mult of R).(xx*yy,vv) by BINOP_1:def 1
.= xx*yy*vv by VECTSP_1:def 10
.= xx*(yy*vv) by VECTSP_1:def 16
.= (the mult of R).(xx,yy*vv) by VECTSP_1:def 10
.= (the mult of R).[xx,yy*vv] by BINOP_1:def 1
.= (the mult of R).[xx,(the mult of R).(yy,vv)] by VECTSP_1:def 10
.= (the mult of R).[xx,(the mult of R).[y,v]] by BINOP_1:def 1
.= (the mult of R).[xx,lm.[y,v]] by U1, FUNCT_1:72
.= (the mult of R).[xx,lm.(y,v)] by BINOP_1:def 1
.= (the mult of R).[x,y*v] by VECTSP_1:def 24
.= lm.[x,y*v] by V1, FUNCT_1:72
.= lm.(x,y*v) by BINOP_1:def 1
.= x*(y*v) by VECTSP_1:def 24;
1_ R in center R by Center1b; then 1_ R in ccR by RLVECT_1:def 1; then
the unity of R in ccR by VECTSP_1:def 9; then
Y1: [the unity of R,vv] in [:ccR, ccs:] by ZFMISC_1:def 2;
thus (1_ cR)*v = lm.(1_ cR,v) by VECTSP_1:def 24
.= lm.(the unity of cR,vv) by VECTSP_1:def 9
.= lm.(the unity of R,vv) by DefCenter
.= lm.[the unity of R,vv] by BINOP_1:def 1
.= (the mult of R).[the unity of R,vv] by Y1, FUNCT_1:72
.= (the mult of R).(the unity of R,vv) by BINOP_1:def 1
.= (the mult of R).(1_ R,vv) by VECTSP_1:def 9
.= (1_ R)*vv by VECTSP_1:def 10
.= v by VECTSP_1:def 19;
end;
B: Vos is add-associative proof let u,v,w be Element of cV;
reconsider uu=u,vv=v, ww=w as Element of ccs;
thus (u + v) + w = aV.(u+v,w) by RLVECT_1:5
.= ac.(ac.(uu,vv),ww) by RLVECT_1:5 .= ac.(uu+vv,ww) by RLVECT_1:5
.= uu+vv+ww by RLVECT_1:5 .= uu+(vv+ww) by RLVECT_1:def 6
.= ac.(uu,vv+ww) by RLVECT_1:5 .= aV.(u,aV.(v,w)) by RLVECT_1:5
.= aV.(u,v+w) by RLVECT_1:5 .= u + (v + w) by RLVECT_1:5;
end;
C: Vos is right_zeroed proof let v be Element of cV;
reconsider vv = v as Element of ccs;
thus v + 0.Vos = aV.(v,0.Vos) by RLVECT_1:5
.= ac.(vv,Zc) by RLVECT_1:def 2 .= ac.(vv,0.R) by RLVECT_1:def 2
.= vv+0.R by RLVECT_1:5 .= v by RLVECT_1:def 7;
end;
D: Vos is right_complementable proof let v be Element of cV;
reconsider vv = v as Element of ccs;
consider ww being Element of ccs such that
A1: vv + ww = 0.R by RLVECT_1:def 8;
reconsider w = ww as Element of cV;
v+w = ac.(vv,ww) by RLVECT_1:5 .= 0.R by A1, RLVECT_1:5
.= Zc by RLVECT_1:def 2 .= 0.Vos by RLVECT_1:def 2;
hence ex w being Element of cV st v + w = 0.Vos;
end;
E: Vos is Abelian proof let v,w be Element of cV;
reconsider vv = v, ww = w as Element of ccs;
thus v+w = ac.(vv,ww) by RLVECT_1:5 .= ww + vv by RLVECT_1:5
.= aV.(w,v) by RLVECT_1:5 .= w+v by RLVECT_1:5;
end;
thus thesis by A,B,C,D,E;
end;
uniqueness;
end;
theorem CardCenter1: :: CardCenter1:
for R being finite Skew-Field
holds card the carrier of R =
(card (the carrier of center R)) |^ (dim VectSp_over_center R)
proof let R be finite Skew-Field;
set Z = center R; set cZ = the carrier of Z; set q = card cZ;
set vR = VectSp_over_center R; set n = dim vR;
the LoopStr of vR = the LoopStr of R by LVSOC; then
A1: the carrier of vR = the carrier of R;
reconsider cvRS = [#]the carrier of vR as Subset of vR;
consider B being Basis of vR;
S3: B is finite by A1, FINSET_1:13;
vR is finite-dimensional by S3, VECTSP_9:def 1;
then Card the carrier of R = q |^ n by A1, DIM;
hence thesis;
end;
theorem DimCenter: :: DimCenter:
for R being finite Skew-Field holds 0 < dim VectSp_over_center R
proof let R be finite Skew-Field;
set q = card the carrier of center R; set n = dim VectSp_over_center R;
set Rs = MultGroup R;
card the carrier of R = q |^ n by CardCenter1; then
A1: ord Rs = (q |^ n) - 1 by UNIROOTS:21;
1 < q by Center2; then A3: 0 <> q;
now assume C0: n = 0; (q |^ n) - 1 = (q #Z n) - 1 by A3,PREPOWER:46; then
ord Rs = 1 - 1 by A1, C0, PREPOWER:44;
hence contradiction by GROUP_1:90;
end; then 0 < n by NAT_1:19;
hence thesis;
end;
definition let R be Skew-Field, s be Element of R;
func VectSp_over_center s -> strict VectSp of center R means :LVO:
the LoopStr of it = the LoopStr of centralizer s &
the lmult of it = (the mult of R)
| [:the carrier of center R, the carrier of centralizer s:];
existence proof
set cR = center R; set ccR = the carrier of cR;
set cs = centralizer s; set ccs = the carrier of cs;
set lm = (the mult of R)|[:ccR, ccs:];
D1a: ccR c= the carrier of R by Center0;
E1a: ccs c= the carrier of R by Central00;
B1: dom (the mult of R) = [:the carrier of R,the carrier of R:]
by FUNCT_2:def 1;
[:ccR, ccs:] c= [:the carrier of R,the carrier of R:] proof
let x be set; assume x in [:ccR, ccs:]; then
consider x1, x2 being set such that
A2: x1 in ccR and
B2: x2 in ccs and
C2: x = [x1,x2] by ZFMISC_1:def 2;
x1 in the carrier of R & x2 in the carrier of R by A2, D1a, B2, E1a;
hence thesis by C2, ZFMISC_1:def 2;
end; then
A1: dom lm = [:ccR, ccs:] by B1, RELAT_1:91;
now let x be set; assume
D2: x in [:ccR, ccs:]; then
consider x1, x2 being set such that
A2: x1 in ccR and
B2: x2 in ccs and
C2: x = [x1,x2] by ZFMISC_1:def 2;
reconsider x1 as Element of R by A2, D1a;
reconsider x2 as Element of R by B2, E1a;
lm.x = (the mult of R).x by D2, FUNCT_1:72
.= (the mult of R).(x1,x2) by C2, BINOP_1:def 1
.= x1*x2 by VECTSP_1:def 10;
hence lm.x in ccs by A2, B2, Central02;
end; then
reconsider lm as Function of [:ccR,ccs:], ccs by A1, FUNCT_2:5;
set Vos = VectSpStr(#
the carrier of centralizer s, the add of centralizer s,
the Zero of centralizer s, lm #);
set cV = the carrier of Vos;
set aV = the add of Vos, ac = the add of centralizer s;
set ZV = the Zero of Vos, Zc = the Zero of centralizer s;
A: Vos is VectSp-like proof
let x,y be Element of ccR, v,w be Element of cV;
D1: x in ccR & y in ccR;
x in the carrier of R & y in the carrier of R by D1, D1a; then
reconsider xx=x, yy=y as Element of R;
E1: v in ccs & w in ccs;
reconsider vv=v, ww=w as Element of R by E1, E1a;
A1: the mult of cR = (the mult of R) | [:ccR,ccR:] by DefCenter;
B1: the add of cR = (the add of R) | [:ccR,ccR:] by DefCenter;
C1: the add of cs = (the add of R) | [:ccs,ccs:] by DefCentral;
N1: [x*v,x*w] in [:ccs,ccs:] by ZFMISC_1:def 2;
O1: [x,w] in [:ccR,ccs:] by ZFMISC_1:def 2;
P1: [x,v+w] in [:ccR,ccs:] by ZFMISC_1:def 2;
Q1: [v,w] in [:ccs,ccs:] by ZFMISC_1:def 2;
R1: [x*v,y*v] in [:ccs,ccs:] by ZFMISC_1:def 2;
S1: [y,v] in [:ccR,ccs:] by ZFMISC_1:def 2;
T1: [x,v] in [:ccR,ccs:] by ZFMISC_1:def 2;
W1: [x+y,v] in [:ccR,ccs:] by ZFMISC_1:def 2;
V1: [x,y*v] in [:ccR,ccs:] by ZFMISC_1:def 2;
U1: [y,v] in [:ccR,ccs:] by ZFMISC_1:def 2;
X1: [x*y,v] in [:ccR,ccs:] by ZFMISC_1:def 2;
Y1: [x,y] in [:ccR,ccR:] by ZFMISC_1:def 2;
thus x*(v+w) = lm.(x,v+w) by VECTSP_1:def 24
.= lm.[x,v+w] by BINOP_1:def 1
.= (the mult of R).[x,v+w] by P1, FUNCT_1:72
.= (the mult of R).[x,aV.[v,w]] by RLVECT_1:def 3
.= (the mult of R).[x,(the add of R).[vv,ww]] by C1,Q1,FUNCT_1:72
.= (the mult of R).[x,vv+ww] by RLVECT_1:def 3
.= (the mult of R).(xx,vv+ww) by BINOP_1:def 1
.= xx*(vv+ww) by VECTSP_1:def 10
.= xx*vv+xx*ww by VECTSP_1:def 11
.= (the add of R).[xx*vv,xx*ww] by RLVECT_1:def 3
.= (the add of R).[(the mult of R).(xx,vv),xx*ww] by VECTSP_1:def 10
.= (the add of R).[(the mult of R).[xx,vv],xx*ww] by BINOP_1:def 1
.= (the add of R).[lm.[x,v],xx*ww] by T1, FUNCT_1:72
.= (the add of R).[lm.(x,v),xx*ww] by BINOP_1:def 1
.= (the add of R).[x*v,xx*ww] by VECTSP_1:def 24
.= (the add of R).[x*v,(the mult of R).(xx,ww)] by VECTSP_1:def 10
.= (the add of R).[x*v,(the mult of R).[xx,ww]] by BINOP_1:def 1
.= (the add of R).[x*v,lm.[x,w]] by O1, FUNCT_1:72
.= (the add of R).[x*v,lm.(x,w)] by BINOP_1:def 1
.= (the add of R).[x*v,x*w] by VECTSP_1:def 24
.= ac.[x*v,x*w] by C1, N1, FUNCT_1:72
.= x*v+x*w by RLVECT_1:def 3;
thus (x+y)*v = lm.(x+y,v) by VECTSP_1:def 24
.= lm.[x+y,v] by BINOP_1:def 1
.= (the mult of R).[x+y,vv] by W1, FUNCT_1:72
.= (the mult of R).[(the add of cR).[x,y],vv] by RLVECT_1:def 3
.= (the mult of R).[(the add of R).[xx,yy],vv] by B1, Y1, FUNCT_1:72
.= (the mult of R).[xx+yy,vv] by RLVECT_1:def 3
.= (the mult of R).(xx+yy,vv) by BINOP_1:def 1
.= (xx+yy)*vv by VECTSP_1:def 10
.= xx*vv+yy*vv by VECTSP_1:def 12
.= (the add of R).[xx*vv,yy*vv] by RLVECT_1:def 3
.= (the add of R).[(the mult of R).(xx,vv),yy*vv] by VECTSP_1:def 10
.= (the add of R).[(the mult of R).[xx,vv],yy*vv] by BINOP_1:def 1
.= (the add of R).[lm.[x,v],yy*vv] by T1, FUNCT_1:72
.= (the add of R).[lm.(x,v),yy*vv] by BINOP_1:def 1
.= (the add of R).[x*v,yy*vv] by VECTSP_1:def 24
.= (the add of R).[x*v,(the mult of R).(yy,vv)] by VECTSP_1:def 10
.= (the add of R).[x*v,(the mult of R).[yy,vv]] by BINOP_1:def 1
.= (the add of R).[x*v,lm.[y,v]] by S1, FUNCT_1:72
.= (the add of R).[x*v,lm.(y,v)] by BINOP_1:def 1
.= (the add of R).[x*v,y*v] by VECTSP_1:def 24
.= ac.[x*v,y*v] by C1, R1, FUNCT_1:72
.= x*v+y*v by RLVECT_1:def 3;
thus (x*y)*v = lm.(x*y,v) by VECTSP_1:def 24
.= lm.[x*y,v] by BINOP_1:def 1
.= (the mult of R).[x*y,vv] by X1, FUNCT_1:72
.= (the mult of R).[(the mult of cR).(x,y),vv] by VECTSP_1:def 10
.= (the mult of R).[(the mult of cR).[x,y],vv] by BINOP_1:def 1
.= (the mult of R).[(the mult of R).[xx,yy],vv] by A1, Y1, FUNCT_1:72
.= (the mult of R).[(the mult of R).(xx,yy),vv] by BINOP_1:def 1
.= (the mult of R).[xx*yy,vv] by VECTSP_1:def 10
.= (the mult of R).(xx*yy,vv) by BINOP_1:def 1
.= xx*yy*vv by VECTSP_1:def 10
.= xx*(yy*vv) by VECTSP_1:def 16
.= (the mult of R).(xx,yy*vv) by VECTSP_1:def 10
.= (the mult of R).[xx,yy*vv] by BINOP_1:def 1
.= (the mult of R).[xx,(the mult of R).(yy,vv)] by VECTSP_1:def 10
.= (the mult of R).[xx,(the mult of R).[y,v]] by BINOP_1:def 1
.= (the mult of R).[xx,lm.[y,v]] by U1, FUNCT_1:72
.= (the mult of R).[xx,lm.(y,v)] by BINOP_1:def 1
.= (the mult of R).[x,y*v] by VECTSP_1:def 24
.= lm.[x,y*v] by V1, FUNCT_1:72
.= lm.(x,y*v) by BINOP_1:def 1
.= x*(y*v) by VECTSP_1:def 24;
1_ R in center R by Center1b; then 1_ R in ccR by RLVECT_1:def 1; then
the unity of R in ccR by VECTSP_1:def 9; then
Y1: [the unity of R,vv] in [:ccR, ccs:] by ZFMISC_1:def 2;
thus (1_ cR)*v = lm.(1_ cR,v) by VECTSP_1:def 24
.= lm.(the unity of cR,vv) by VECTSP_1:def 9
.= lm.(the unity of R,vv) by DefCenter
.= lm.[the unity of R,vv] by BINOP_1:def 1
.= (the mult of R).[the unity of R,vv] by Y1, FUNCT_1:72
.= (the mult of R).(the unity of R,vv) by BINOP_1:def 1
.= (the mult of R).(1_ R,vv) by VECTSP_1:def 9
.= (1_ R)*vv by VECTSP_1:def 10
.= v by VECTSP_1:def 19;
end;
B: Vos is add-associative proof let u,v,w be Element of cV;
reconsider uu=u,vv=v, ww=w as Element of ccs;
thus (u + v) + w = aV.(u+v,w) by RLVECT_1:5
.= ac.(ac.(uu,vv),ww) by RLVECT_1:5 .= ac.(uu+vv,ww) by RLVECT_1:5
.= uu+vv+ww by RLVECT_1:5 .= uu+(vv+ww) by RLVECT_1:def 6
.= ac.(uu,vv+ww) by RLVECT_1:5 .= aV.(u,aV.(v,w)) by RLVECT_1:5
.= aV.(u,v+w) by RLVECT_1:5 .= u + (v + w) by RLVECT_1:5;
end;
C: Vos is right_zeroed proof let v be Element of cV;
reconsider vv = v as Element of ccs;
thus v + 0.Vos = aV.(v,0.Vos) by RLVECT_1:5
.= ac.(vv,Zc) by RLVECT_1:def 2 .= ac.(vv,0.cs) by RLVECT_1:def 2
.= vv+0.cs by RLVECT_1:5 .= v by RLVECT_1:def 7;
end;
D: Vos is right_complementable proof let v be Element of cV;
reconsider vv = v as Element of ccs;
consider ww being Element of ccs such that
A1: vv + ww = 0.cs by RLVECT_1:def 8;
reconsider w = ww as Element of cV;
v+w = ac.(vv,ww) by RLVECT_1:5 .= 0.cs by A1, RLVECT_1:5
.= Zc by RLVECT_1:def 2 .= 0.Vos by RLVECT_1:def 2;
hence ex w being Element of cV st v + w = 0.Vos;
end;
E: Vos is Abelian proof let v,w be Element of cV;
reconsider vv = v, ww = w as Element of ccs;
thus v+w = ac.(vv,ww) by RLVECT_1:5 .= ww + vv by RLVECT_1:5
.= aV.(w,v) by RLVECT_1:5 .= w+v by RLVECT_1:5;
end;
thus thesis by A,B,C,D,E;
end;
uniqueness;
end;
theorem CardCentral: :: CardCentral:
for R being finite Skew-Field, s being Element of R
holds card the carrier of (centralizer s) =
(card (the carrier of center R)) |^ (dim VectSp_over_center s)
proof let R be finite Skew-Field, s be Element of R;
set Z = center R;
set cZ = the carrier of Z;
set q = card cZ;
set vR = VectSp_over_center s;
the LoopStr of vR = the LoopStr of centralizer s by LVO; then
A1: the carrier of vR = the carrier of centralizer s;
set n = dim vR;
reconsider cvRS = [#]the carrier of vR as Subset of vR;
consider B being Basis of vR;
S3: B is finite by A1, FINSET_1:13;
vR is finite-dimensional by S3, VECTSP_9:def 1; then
Card the carrier of (centralizer s) = q |^ n by A1, DIM;
hence thesis;
end;
theorem DimCentral: :: DimCentral:
for R being finite Skew-Field, s being Element of R
holds 0 < dim VectSp_over_center s
proof let R be finite Skew-Field, s be Element of R;
set q = card the carrier of center R; set ns= dim VectSp_over_center s;
1 < q by Center2; then A1: 0 <> q;
now assume A2: ns = 0; q |^ ns = q #Z ns by A1,PREPOWER:46; then
q |^ ns = 1 by A2,PREPOWER:44; then
card the carrier of centralizer s = 1 by CardCentral;
hence contradiction by Central1;
end;
hence thesis by NAT_1:19;
end;
theorem Skew1: :: Skew1:
for R being finite Skew-Field, r being Element of R
st r is Element of MultGroup R
holds
((card (the carrier of center R)) |^ (dim VectSp_over_center r) - 1) divides
((card (the carrier of center R)) |^ (dim VectSp_over_center R) - 1)
proof let R be finite Skew-Field, r be Element of R such that
A0: r is Element of MultGroup R;
set G = MultGroup R; set q = card (the carrier of center R);
set qr= card (the carrier of centralizer r);
set n = dim VectSp_over_center R; set ns= dim VectSp_over_center r;
reconsider s=r as Element of MultGroup R by A0;
card the carrier of R = q |^ n by CardCenter1; then
ord G = (q |^ n) - 1 by UNIROOTS:21; then
q |^ n - 1 = card con_class s * ord Centralizer s by OrdGroup1; then
ord Centralizer s divides (q |^ n - 1) by INT_1:def 9; then
(qr - 1) divides (q |^ n -1) by Central2; then
(q |^ ns - 1) divides (q |^ n - 1) by CardCentral;
hence thesis;
end;
theorem Skew2: :: Skew2:
for R being finite Skew-Field, s being Element of R
st s is Element of MultGroup R
holds (dim VectSp_over_center s) divides (dim VectSp_over_center R)
proof let R be finite Skew-Field, s be Element of R such that
A0: s is Element of MultGroup R;
set Vs= VectSp_over_center s; set n = dim VectSp_over_center R;
set ns= dim VectSp_over_center s; set q = card the carrier of center R;
A1: 0 < n & 0 < ns by DimCenter,DimCentral;
A2: 1 < q by Center2; then
B2: 0 < q by AXIOMS:22; then
0 < q |^ ns by PREPOWER:13; then 0+1 < q |^ ns + 1 by REAL_1:67; then
A3: 1 <= q |^ ns by NAT_1:38;
0 < q |^ n by B2,PREPOWER:13; then 0+1 < q |^ n + 1 by REAL_1:67; then
A4: 1 <= q |^ n by NAT_1:38;
A5: (q |^ n - 1) = (q |^ n -' 1) by A4,SCMFSA_7:3;
A6: (q |^ ns - 1) = (q |^ ns -' 1) by A3,SCMFSA_7:3;
(q |^ ns - 1) divides (q |^ n - 1) by A0,Skew1; then
(q |^ ns -'1) divides (q |^ n -'1) by A5,A6,SCPINVAR:2; then
ns divides n by A1,A2,Th3;
hence thesis;
end;
theorem MGC1: :: MGC1:
for R being finite Skew-Field holds
card the carrier of center MultGroup R = card (the carrier of center R) - 1
proof let R be finite Skew-Field;
the carrier of MultGroup R = (the carrier of R) \ {0.R}
by UNIROOTS:def 1; then
B: not 0.R in the carrier of MultGroup R by ZFMISC_1:64;
the carrier of center MultGroup R c= the carrier of MultGroup R
by GROUP_2:def 5; then
A: not 0.R in the carrier of center MultGroup R by B;
the carrier of center R = (the carrier of center MultGroup R) \/ {0.R}
by Center4; then
card the carrier of center R = card (the carrier of center MultGroup R) + 1
by A, CARD_2:54; then card (the carrier of center R)-1 =
card (the carrier of center MultGroup R)+1-1;
hence thesis by XCMPLX_1:26;
end;
begin :: Witt's proof of Wedderburn's theorem
theorem
for R being finite Skew-Field holds R is commutative
proof let R be finite Skew-Field such that
B0: not R is commutative;
set Z = center R; set cZ = the carrier of Z;
set q = card cZ; set vR = VectSp_over_center R;
set n = dim vR; set Rs = MultGroup R;
set cR = the carrier of R; set cRs = the carrier of Rs;
set cZs = the carrier of center Rs;
A0: card cR = q |^ n by CardCenter1; then
A1: ord Rs = (q |^ n) - 1 by UNIROOTS:21;
A2: 1 < q by Center2; then
A3: 0 <> q;
1+-1 < q + -1 by A2,REAL_1:67; then
_Z3: 1-1 < q - 1 by XCMPLX_0:def 8; then
reconsider nat_q1 = q - 1 as Nat by INT_1:16;
B1a: 0 < n by DimCenter; then 0+1 < n + 1 by REAL_1:67; then
B1: 1 <= n by NAT_1:38;
now assume C0: n = 1;
card cR = (q #Z n ) by A3,A0,PREPOWER:46; then
card cR = q by C0,PREPOWER:45;
hence contradiction by Center3,B0;
end; then
B2: 1 < n by B1, REAL_1:def 5;
set A = {X where X is Subset of cRs :
X in conjugate_Classes Rs & card X = 1};
set B = conjugate_Classes Rs \ A;
for x being set st x in A holds x in conjugate_Classes Rs
proof let x be set; assume x in A; then
ex y being Subset of cRs
st x=y & y in conjugate_Classes Rs & Card y = 1;
hence thesis;
end; then
B3: A c= conjugate_Classes Rs by TARSKI:def 3; then
B4: conjugate_Classes Rs = A \/ B by XBOOLE_1:45;
consider f being Function such that
ZA1: dom f = cZs and
ZA4: for x being set st x in cZs holds f.x = {x} from Lambda;
ZA3: f is one-to-one proof let x1,x2 be set;
assume x1 in dom f & x2 in dom f & f.x1 = f.x2;
then f.x1 = {x1} & f.x2 = {x2} & f.x1 = f.x2 by ZA4, ZA1;
hence x1 = x2 by ZFMISC_1:6;
end;
now let x be set;
hereby assume x in rng f; then consider xx being set such that
A5: xx in dom f and
B5: x = f.xx by FUNCT_1:def 5;
C5: x = {xx} by ZA1, A5, B5, ZA4;
D5: cZs c= cRs by GROUP_2:def 5;
{xx} c= cZs by A5,ZA1,ZFMISC_1:37;
then reconsider X = x as Subset of cRs by C5, D5, XBOOLE_1:1;
E5: xx is Element of center Rs by A5, ZA1;
reconsider xx as Element of Rs by A5, D5, ZA1;
xx in center Rs by E5, RLVECT_1:def 1; then
con_class xx = {xx} by GROUP_5:93; then
D5: X in conjugate_Classes Rs by C5, Conj1; card X = 1 by C5, CARD_1:79;
hence x in A by D5;
end;
assume x in A; then consider X being Subset of cRs such that
A5': x = X and
A5: X in conjugate_Classes Rs and
B5: card X = 1;
consider a being Element of cRs such that
C5: con_class a = X by A5, Conj1;
D5: a in con_class a by GROUP_3:98;
consider xx being set such that
E5: X = {xx} by B5, CARD_2:60;
F5: a = xx by E5, D5, C5, TARSKI:def 1; then
a in center Rs by E5, C5, GROUP_5:93; then
G5: a in cZs by RLVECT_1:def 1; then f.a = {a} by ZA4;
hence x in rng f by A5', E5, F5, G5, ZA1, FUNCT_1:12;
end; then
ZA2: rng f = A by TARSKI:2;
Z0: A, cZs are_equipotent by ZA1, ZA2, ZA3, WELLORD2:def 4;
card cZs = nat_q1 by MGC1; then
B5: Card A = nat_q1 by Z0, CARD_1:21;
A is finite by B3,FINSET_1:13; then
consider f1 being FinSequence such that
D1: rng f1 = A and D0: f1 is one-to-one by FINSEQ_4:73;
consider f2 being FinSequence such that
D3: rng f2 = B and D2: f2 is one-to-one by FINSEQ_4:73;
set f = f1^f2;
D4: rng f = conjugate_Classes Rs by B4,D1,D3,FINSEQ_1:44;
now given x being set such that
E0: x in A /\ B; x in A & x in B by E0,XBOOLE_0:def 3;
hence contradiction by XBOOLE_0:def 4;
end;
then A /\ B = {} by XBOOLE_0:def 1;
then rng f1 misses rng f2 by D1,D3,XBOOLE_0:def 7; then
D5: f is one-to-one FinSequence of conjugate_Classes Rs
by D0,D2,D4,FINSEQ_3:98,FINSEQ_1:def 4;
deffunc F(set) = Card(f1.$1);
consider p1 being FinSequence such that
D6: len p1 = len f1 &
for i being Nat st i in Seg len f1 holds p1.i = F(i) from SeqLambda;
D8: dom p1 = Seg len f1 by D6,FINSEQ_1:def 3;
for x being set st x in rng p1 holds x in NAT proof let x be set such that
E0: x in rng p1;
consider i being Nat such that
E1: i in dom p1 & p1.i = x by E0,FINSEQ_2:11;
E2: x = Card(f1.i) by E1,D6,D8;
i in dom f1 by D6,E1,FINSEQ_3:31; then f1.i in A by D1,FUNCT_1:12; then
consider X being Subset of cRs such that
E1: f1.i = X & X in conjugate_Classes Rs & card X = 1;
thus thesis by E1,E2;
end;
then rng p1 c= NAT by TARSKI:def 3; then
reconsider c1=p1 as FinSequence of NAT by FINSEQ_1:def 4;
D7: for i being Nat st i in dom c1 holds c1.i = Card(f1.i) by D6,D8;
D9: len c1 = nat_q1 by B5,D6,D0,D1,FINSEQ_4:77;
D11: for i being Nat st i in dom c1 holds c1.i = 1 proof
let i be Nat such that
E0: i in dom c1;
i in dom f1 by FINSEQ_3:31,D6,E0; then f1.i in A by D1,FUNCT_1:12;
then ex X being Subset of cRs
st f1.i = X & X in conjugate_Classes Rs & card X = 1;
hence thesis by E0,D6,D8;
end;
for x being set st x in rng c1 holds x in {1} proof
let x be set; assume x in rng c1; then consider i being Nat such that
E1: i in dom c1 & x = c1.i by FINSEQ_2:11;
x = 1 by E1,D11;
hence thesis by TARSKI:def 1;
end; then
D10: rng c1 c= {1} by TARSKI:def 3;
for x being set st x in {1} holds x in rng c1 proof
let x be set such that
E0: x in {1};
Seg len c1 = dom c1 by FINSEQ_1:def 3; then
E2: len c1 in dom c1 by D9,_Z3,FINSEQ_1:5; then
c1.(len c1) = 1 by D11; then c1.(len c1) = x by E0,TARSKI:def 1;
hence thesis by E2,FUNCT_1:12;
end;
then {1}c= rng c1 by TARSKI:def 3; then rng c1={1} by D10,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
F1: Sum c1 = nat_q1 by B5,D6,D0,D1,FINSEQ_4:77;
deffunc P2(set) = Card(f2.$1);
consider p2 being FinSequence such that
D8: len p2 = len f2 &
for i being Nat st i in Seg len f2 holds p2.i = P2(i) from SeqLambda;
H8: dom p2 = Seg len f2 by D8,FINSEQ_1:def 3;
for x being set st x in rng p2 holds x in NAT proof
let x be set; assume x in rng p2; then consider i being Nat such that
E1: i in dom p2 & p2.i = x by FINSEQ_2:11;
E2: x = Card(f2.i) by E1,D8,H8;
i in dom f2 by D8,E1,FINSEQ_3:31; then
f2.i in conjugate_Classes Rs \ A by D3,FUNCT_1:12; then
f2.i in conjugate_Classes Rs by XBOOLE_0:def 4; then
consider a being Element of cRs such that
E3: con_class a = f2.i by Conj1;
card con_class a is Nat;
hence thesis by E2,E3;
end; then rng p2 c= NAT by TARSKI:def 3; then
reconsider c2=p2 as FinSequence of NAT by FINSEQ_1:def 4;
D9: for i being Nat st i in dom c2 holds c2.i = Card(f2.i) by D8,H8;
set c = c1^c2;
reconsider c as FinSequence of NAT;
len c = len f1 + len f2 by D6,D8,FINSEQ_1:35; then
B3: len c = len f by FINSEQ_1:35;
for i being Nat st i in dom c holds c.i = Card (f.i) proof
let i be Nat such that
C0: i in dom c;
now per cases by C0,FINSEQ_1:38;
suppose D0: i in dom c1;
D1: i in dom f1 by D0,D6,FINSEQ_3:31;
c.i = c1.i by D0,FINSEQ_1:def 7 .= Card(f1.i) by D0,D7
.= Card(f.i) by D1,FINSEQ_1:def 7;
hence thesis;
suppose ex j being Nat st j in dom c2 & i = len c1 + j; then
consider j being Nat such that
D0: j in dom c2 and D1: i = len c1 + j;
D2: j in dom f2 by D0,D8,FINSEQ_3:31;
c.i = c2.j by D0,D1,FINSEQ_1:def 7 .= Card(f2.j) by D0,D8,H8
.= Card(f.i) by D1,D2,D6,FINSEQ_1:def 7;
hence thesis;
end;
hence thesis;
end; then
B5: ord Rs = Sum c by D4, D5, B3, ClassFormula;
rng c1 c= NAT & rng c2 c= NAT by FINSEQ_1:def 4; then
rng c1 c= REAL & rng c2 c= REAL by XBOOLE_1:1; then
c1 is FinSequence of REAL&c2 is FinSequence of REAL by FINSEQ_1:def 4;then
B6: (q |^ n) - 1 = Sum c2 + (q - 1) by A1,B5,F1,RVSUM_1:105;
reconsider q as non empty Nat by A3;
reconsider n as non empty Nat by DimCenter;
consider qc being Element of COMPLEX such that
B8: qc = q & qc = [*q,0*] by UNIROOTS:6;
reconsider qc as Element of F_Complex by COMPLFLD:def 1;
set pnq = eval(cyclotomic_poly n,qc);
reconsider pnq as Integer by B8, UNIROOTS:56;
reconsider abs_pnq = abs(pnq) as Nat;
reconsider nat_aq1 = abs(q-1) as Nat;
(q |^ n) <> 0 by PREPOWER:12; then (q |^ n) > 0 by NAT_1:19; then
(q |^ n)+1 > 0+1 by REAL_1:67; then (q |^ n) >= 1 by NAT_1:38; then
(q |^ n) +- 1 >= 1 +- 1 by REAL_1:55; then
X0: (q |^ n) - 1 >= 0 by XCMPLX_0:def 8; then
reconsider qn1=((q |^ n) - 1) as Nat by INT_1:16;
pnq divides (q |^ n) - 1 by B8,UNIROOTS:62; then
abs_pnq divides abs((q |^ n) - 1) by INT_2:21; then
Y0: abs_pnq divides qn1 by X0, ABSVALUE:def 1;
for i being Nat st i in dom c2 holds abs_pnq divides c2/.i proof
let i be Nat such that C0: i in dom c2;
c2.i = Card (f2.i) by C0,D9; then
C1: c2/.i = Card (f2.i) by C0,FINSEQ_4:def 4;
C1b: i in dom f2 by C0,D8,FINSEQ_3:31; then
f2.i in conjugate_Classes Rs \ A by D3, FUNCT_1:12; then
f2.i in conjugate_Classes Rs & not f2.i in A by XBOOLE_0:def 4;
then consider a being Element of cRs such that
C3: con_class a = f2.i by Conj1;
reconsider a as Element of Rs;
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 = ord Centralizer a;
C4: ord Rs = ca * oa + 0 by OrdGroup1;
oa <> 0 by GROUP_1:90; then 0 < oa by NAT_1:19; then
(ord Rs) div oa = ca by C4,NAT_1:def 1; then
C5: qn1 div oa = ca by A1;
(q |^ ns) <> 0 by PREPOWER:12; then (q |^ ns) > 0 by NAT_1:19; then
(q |^ ns)+1 > 0+1 by REAL_1:67; then (q |^ ns) >= 1 by NAT_1:38;
then (q |^ ns) +- 1 >= 1 +- 1 by REAL_1:55; then
(q |^ ns) - 1 >= 0 by XCMPLX_0:def 8; then
reconsider qns1=(q |^ ns - 1) as Nat by INT_1:16;
oa = (card the carrier of (centralizer s)) - 1 by Central2
.= qns1 by CardCentral; then qn1 div qns1 = ca by C5; then
C6: qn1 div qns1 = c2/.i by C1,C3;
C7: (qn1 qua Integer) div qns1 = qn1 div qns1 by SCMFSA9A:5;
C8: qn1 div qns1 >= 0 by NAT_1:18;
reconsider ns as non empty Nat by DimCentral;
C9: ns divides n by Skew2;
D1: ns <= n by B1a, C9, NAT_1:54;
now assume A4: ns = n;
now assume qn1 = 0; then q |^ n - 1 + 1 = 0+1; then
q |^ n = 1 by XCMPLX_1:27;
hence contradiction by B1a, A2, PEPIN:26;
end; then
B2: Card (f2.i) = 1 by C1, A4, C6, NAT_2:5;
f2.i in B by C1b, D3, FUNCT_1:12; then
f2.i in conjugate_Classes Rs & not f2.i in A by XBOOLE_0:def 4;
hence contradiction by B2;
end; then
ns < n by D1, REAL_1:def 5; then
pnq divides ((qn1 qua Integer) div qns1) by C9, B8, UNIROOTS:63; then
abs_pnq divides abs(((qn1 qua Integer) div qns1)) by INT_2:21; then
abs_pnq divides abs(qn1 div qns1) by C7; then
abs_pnq divides (qn1 div qns1) by C8,ABSVALUE:def 1;
hence thesis by C6;
end;
then abs_pnq divides Sum c2 by SumDivision; then
Z1: abs_pnq divides nat_q1 by Y0, B6, NAT_1:57;
abs_pnq > q - 1 by A2, B2, B8, UNIROOTS:64;
hence contradiction by Z1, _Z3, NAT_1:54;
end;