:: Witt's Proof of the {W}edderburn Theorem
:: by Broderick Arneson , Matthias Baaz and Piotr Rudnicki
::
:: Received December 30, 2003
:: Copyright (c) 2003-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, SUBSET_1, REAL_1, ARYTM_3, NEWTON, CARD_1, XXREAL_0,
PREPOWER, NAT_1, RELAT_1, ARYTM_1, INT_1, FUNCT_2, XBOOLE_0, FUNCT_1,
TARSKI, FUNCT_4, FUNCOP_1, FINSET_1, FINSEQ_1, PARTFUN1, CARD_3,
ORDINAL4, EQREL_1, ZFMISC_1, GROUP_1, GROUP_5, STRUCT_0, GROUP_2,
GROUP_3, VECTSP_1, RLVECT_5, RLVECT_3, RLSUB_1, SUPINF_2, FINSEQ_2,
RLVECT_2, VALUED_1, VECTSP_2, ALGSTR_0, REALSET1, MESFUNC1, BINOP_1,
RLVECT_1, LATTICES, UNIROOTS, COMPLFLD, POLYNOM2, COMPLEX1, WEDDWITT,
XCMPLX_0, FUNCSDOM;
notations TARSKI, XBOOLE_0, SUBSET_1, CARD_1, ORDINAL1, NUMBERS, XCMPLX_0,
ZFMISC_1, XXREAL_0, XREAL_0, INT_1, INT_2, NAT_1, NAT_D, FINSET_1,
BINOP_1, RELAT_1, REALSET1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2,
FINSEQ_1, FINSEQ_2, RVSUM_1, COMPLFLD, POLYNOM4, STRUCT_0, ALGSTR_0,
RLVECT_1, GROUP_1, VECTSP_1, VECTSP_2, GROUP_2, PREPOWER, FUNCT_4,
UNIROOTS, VECTSP_6, VECTSP_7, GROUP_3, GROUP_5, MATRLIN, VECTSP_9,
EQREL_1, FUNCOP_1, VECTSP_4, WSIERP_1, NEWTON;
constructors WELLORD2, BINOP_1, FUNCT_4, NAT_D, NEWTON, VECTSP_1,
PREPOWER, WSIERP_1, REALSET2, VECTSP_6, VECTSP_7, GROUP_5,
MONOID_0, POLYNOM4, UPROOTS, UNIROOTS, BINOP_2, VECTSP_9,
RELSET_1, REAL_1;
registrations XBOOLE_0, SUBSET_1, ORDINAL1, RELSET_1, FUNCOP_1, FINSET_1,
XXREAL_0, XREAL_0, NAT_1, INT_1, CARD_1, FINSEQ_1, EQREL_1, FINSEQ_2,
NEWTON, STRUCT_0, VECTSP_1, COMPLFLD, GROUP_2, MONOID_0, UNIROOTS,
VALUED_0, ALGSTR_0, PREPOWER, RVSUM_1;
requirements NUMERALS, BOOLE, SUBSET, ARITHM, REAL;
definitions TARSKI, VECTSP_1, FUNCT_1, RLVECT_1, GROUP_1, ALGSTR_0;
equalities VECTSP_1, BINOP_1, REALSET1, GROUP_3, GROUP_2, STRUCT_0, ALGSTR_0,
FUNCOP_1, ORDINAL1;
expansions TARSKI, VECTSP_1, FUNCT_1, GROUP_1, GROUP_2, STRUCT_0;
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, COMPLFLD, INT_1,
RVSUM_1, FINSEQ_3, FINSEQ_2, FINSEQ_4, INT_2, ABSVALUE, WSIERP_1, NAT_2,
PEPIN, FUNCT_7, RLVECT_1, NEWTON, FINSET_1, FUNCOP_1, VECTSP_2, CARD_2,
MATRLIN, WELLORD2, FUNCT_5, AFINSQ_1, FUNCT_4, GROUP_2, VECTSP_4,
VECTSP_7, VECTSP_9, EQREL_1, GROUP_3, FRAENKEL, VECTSP_6, GROUP_5,
UNIROOTS, XCMPLX_0, XREAL_1, XXREAL_0, ORDINAL1, NAT_D, STRUCT_0,
PARTFUN1, ALGSTR_0, XTUPLE_0, SUBSET_1;
schemes NAT_1, FUNCT_1, FUNCT_2, FINSEQ_1;
begin :: Preliminaries
theorem Th1:
for a being Element of NAT, q being Real st 1 < q & q |^ a = 1 holds a = 0
proof
let a be Element of NAT, q be Real such that
A1: 1 < q and
A2: (q |^ a) = 1 and
A3: a <> 0;
a < 1 + 1 by A1,A2,PREPOWER:13;
then a <= 0 + 1 by NAT_1:13;
then a = 1 by A3,NAT_1:8;
then (q #Z a) = q by PREPOWER:35;
hence contradiction by A1,A2,PREPOWER:36;
end;
theorem 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;
set xNak = x |^ (a*k + r);
0+1 <= k by A2,NAT_1:13;
then k = k-'1+1 by XREAL_1:235;
then xNak = (x #Z (a + (a*(k-'1)+r))) by PREPOWER:36;
then xNak = (x #Z a)*(x #Z (a*(k-'1)+r)) by A1,PREPOWER:44;
then xNak = (x |^ a)*(x #Z (a*(k-'1)+r)) by PREPOWER:36;
hence thesis by PREPOWER:36;
end;
theorem Th3:
for q, a, b being Element of NAT
st 0 < a & 1 < q & (q |^ a) -' 1 divides (q |^ b)-'1 holds a divides b
proof
let q,a,b be Element of NAT such that
A1: 0 < a and
A2: 1 < q and
A3: (q |^ a)-'1 divides (q |^ b)-'1;
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;
A4: b = a*(b div a) + r by A1,NAT_D:2;
then
A5: ex k being Nat st P[k] by A3;
consider k being Nat such that
A6: P[k] and
A7: for n being Nat st P[n] holds k <= n from NAT_1:sch 5(A5);
now per cases;
suppose
A8: k = 0;
A9: now
assume
A10: 0 <> qNr-'1;
r < a by A1,NAT_D:1;
then consider m being Nat such that
A11: a = r + m by NAT_1:10;
A12: m <> 0 by A1,A11,NAT_D:1;
A13: (q |^ (r + m)) = (q #Z (r + m)) by PREPOWER:36;
A14: (q #Z (r + m)) = (q #Z r)*(q #Z m) by A2,PREPOWER:44;
A15: (q #Z r) = (q |^ r) by PREPOWER:36;
A16: (q #Z m) = (q |^ m) by PREPOWER:36;
A17: (q |^ m) >= 1 by A2,PREPOWER:11;
m in NAT by ORDINAL1:def 12;
then (q |^ m) <> 1 by A2,A12,Th1;
then (q |^ m) > 1 by A17,XXREAL_0:1;
then
A18: qNr < qNa by A2,A11,A13,A14,A15,A16,PREPOWER:39,XREAL_1:155;
then 0+ 1 <= qNa by NAT_1:13;
then qNa-'1 = qNa-1 by XREAL_1:233;
then
A19: qNa-'1 = qNa+(-1);
0+1 <= qNr by A10,NAT_2:8;
then qNr-'1 = qNr-1 by XREAL_1:233;
then qNr-'1 = qNr+(-1);
then qNr-'1 < qNa-'1 by A18,A19,XREAL_1:8;
hence contradiction by A6,A8,A10,NAT_D:7;
end;
0 < qNr by A2,PREPOWER:6;
then 0+1<=qNr by NAT_1:13;
then qNr-1+1 = 1 by A9,XREAL_1:233;
then r = 0 by A2,Th1;
hence thesis by A4,NAT_D:3;
end;
suppose
A20: k <> 0;
then consider j being Nat such that
A21: k = j + 1 by NAT_1:6;
A22: k-1 = j by A21;
0+1<=k by A20,NAT_1:13;
then
A23: k-'1 = j by A22,XREAL_1:233;
set qNaj = (q |^ (a*j + r));
set qNak = (q |^ (a*k + r));
set qNak1= (q |^ (a*(k-'1)+r));
A24: not qNa-'1 divides qNaj-'1 by A7,A21,XREAL_1:29;
(qNa-'1) divides -(qNa-'1) by INT_2:10;
then
A25: (qNa-'1) divides (qNak-'1)+(-(qNa-'1)) by A6,WSIERP_1:4;
A26: 0 < qNak by A2,PREPOWER:6;
A27: 0 < qNa by A2,PREPOWER:6;
0+1<=qNak by A26,NAT_1:13;
then
A28: (qNak-'1)=(qNak-1) by XREAL_1:233;
A29: 0+1<=qNa by A27,NAT_1:13;
(qNak-1) - (qNa-1) = qNak-qNa;
then (qNak-1) - (qNa-1) = qNa*qNak1-qNa*1 by A2,A20,Th2;
then
A30: (qNak-'1)-(qNa-'1) = qNa*(qNak1-1) by A28,A29,XREAL_1:233;
0 < qNak1 by A2,PREPOWER:6;
then 0+1<= qNak1 by NAT_1:13;
then
A31: (qNak-'1)-(qNa-'1)= qNa*(qNak1-'1) by A30,XREAL_1:233;
0 < qNa by A2,PREPOWER:6;
then 0+1 <= qNa by NAT_1:13;
then qNa-'1+1 = qNa by XREAL_1:235;
then qNa-'1,qNa are_coprime by PEPIN:1;
hence thesis by A23,A24,A25,A31,INT_2:25;
end;
end;
hence thesis;
end;
theorem Th4:
for n, q being Nat st 0 < q holds card Funcs(n,q) = q |^ n
proof
let n,q be Nat such that
A1: 0 < q;
reconsider q as Element of NAT by ORDINAL1:def 12;
defpred P[Nat] means card Funcs($1,q) = q|^$1;
Funcs({},q) = {{}} by FUNCT_5:57;
then card Funcs(0,q) = 1 by CARD_1:30
.= q #Z 0 by PREPOWER:34
.= q |^ 0 by PREPOWER:36;
then
A2: P[0];
A3: for n being Nat st P[n] holds P[n+1]
proof
let n be Nat such that
A4: P[n];
reconsider n as Element of NAT by ORDINAL1:def 12;
reconsider q9 = q as non empty set by A1;
defpred R[object, object] means
ex x being Function of n+1,q st $1 = x & $2 = x | n;
A5: for x being object st x in Funcs(n+1,q9)
ex y being object st y in Funcs(n,q9) & R[x,y]
proof
let x be object;
assume x in Funcs(n+1,q9);
then consider f being Function such that
A6: x = f and
A7: dom f = n+1 and
A8: rng f c= q9 by FUNCT_2:def 2;
reconsider f as Function of n+1,q9 by A7,A8,FUNCT_2:2;
not n in n;
then
A9: n misses {n} by ZFMISC_1:50;
Segm(n+1) /\ n = (Segm n \/ {n}) /\ n by AFINSQ_1:2;
then (n+1) /\ n = (n /\ n) \/ ({n} /\ n) by XBOOLE_1:23;
then (n+1) /\ n = n \/ {} by A9,XBOOLE_0:def 7;
then
A10: dom (f|n) = n by A7,RELAT_1:61;
rng (f|n) c= q9;
then (f|n) in Funcs(n,q9) by A10,FUNCT_2:def 2;
hence thesis by A6;
end;
consider G being Function of Funcs(n+1,q9), Funcs(n,q9) such that
A11: for x being object st x in Funcs(n+1,q9) holds R[x,G.x]
from FUNCT_2:sch 1(A5);
for x being object st x in Funcs(n,q9) holds x in rng G
proof
let x be object such that
A12: x in Funcs(n,q9);
consider y being object such that
A13: y in q9 by XBOOLE_0:def 1;
reconsider g=x as Element of Funcs(n,q9) by A12;
set fx = g+* (n .--> y);
for y being set st y in q holds g +* (n .--> y) in (G"{g})
proof
let y be set such that
A14: y in q;
consider f being Function such that
A15: f = g+*(n.-->y);
A16: dom g = n by FUNCT_2:def 1;
A17: dom (n.-->y) = {n};
then dom f = Segm n \/ {n} by A15,A16,FUNCT_4:def 1;
then
A18: dom f = Segm(n+1) by AFINSQ_1:2;
rng (n.-->y) = {y} by FUNCOP_1:8;
then
A19: rng f c= (rng g \/ {y}) by A15,FUNCT_4:17;
{y} c= q by A14,ZFMISC_1:31;
then (rng g \/ {y}) c= q by XBOOLE_1:8;
then rng f c= q by A19;
then
A20: f in Funcs(n+1,q) by A18,FUNCT_2:def 2;
then reconsider f as Function of n+1,q by FUNCT_2:66;
not n in n;
then n misses {n} by ZFMISC_1:50;
then
A21: f|n = g by A15,A16,A17,FUNCT_4:33;
R[f,G.f] by A11,A20;
then
A22: G.f in {x} by A21,TARSKI:def 1;
dom G = Funcs(n+1,q) by FUNCT_2:def 1;
hence thesis by A15,A20,A22,FUNCT_1:def 7;
end;
then g +* (n .--> y) in (G"{g}) by A13;
then consider b being object such that
A23: b in rng G and
A24: [fx,b] in G and b in {g} by RELAT_1:131;
fx in dom G by A24,FUNCT_1:1;
then R[fx,G.fx] by A11;
then
A25: fx|n = b by A24,FUNCT_1:1;
A26: dom g = n by FUNCT_2:def 1;
A27: dom (n .--> y) = {n};
not n in n;
then n misses {n} by ZFMISC_1:50;
hence thesis by A23,A25,A26,A27,FUNCT_4:33;
end;
then Funcs(n,q9) c= rng G;
then
A28: rng G = Funcs(n,q9) by XBOOLE_0:def 10;
A29: for x being Element of Funcs(n,q9)
holds G"{x} is finite & card (G"{x}) = q
proof
let x be Element of Funcs(n,q9);
deffunc HH(object) = x +* (n .--> $1);
A30: for y being object st y in q holds HH(y) in (G"{x})
proof
let y be object such that
A31: y in q;
consider f being Function such that
A32: f = x+*(n.-->y);
A33: dom x = n by FUNCT_2:def 1;
A34: dom (n.-->y) = {n};
then dom f = Segm n \/ {n} by A32,A33,FUNCT_4:def 1;
then
A35: dom f = Segm(n+1) by AFINSQ_1:2;
rng (n.-->y) = {y} by FUNCOP_1:8;
then
A36: rng f c= (rng x \/ {y}) by A32,FUNCT_4:17;
{y} c= q by A31,ZFMISC_1:31;
then (rng x \/ {y}) c= q by XBOOLE_1:8;
then rng f c= q by A36;
then
A37: f in Funcs(n+1,q) by A35,FUNCT_2:def 2;
then reconsider f as Function of n+1,q by FUNCT_2:66;
not n in n;
then n misses {n} by ZFMISC_1:50;
then
A38: f|n = x by A32,A33,A34,FUNCT_4:33;
R[f,G.f] by A11,A37;
then
A39: G.f in {x} by A38,TARSKI:def 1;
dom G = Funcs(n+1,q) by FUNCT_2:def 1;
hence thesis by A32,A37,A39,FUNCT_1:def 7;
end;
consider H being Function of q, (G"{x}) such that
A40: for y being object st y in q holds H.y = HH(y) from FUNCT_2:sch 2(A30);
A41: for c being object st c in G"{x}
ex y being object st y in q & H.y = c
proof
let c be object;
assume
A42: c in G"{x};
then consider f being Function of n+1,q9 such that
A43: c = f and
A44: G.c = f|n by A11;
take y = f.n;
G.c in {x} by A42,FUNCT_1:def 7;
then
A45: G.c = x by TARSKI:def 1;
Segm(n+1) = Segm n \/ {n} by AFINSQ_1:2;
then dom f = n \/ {n} by FUNCT_2:def 1;
then
A46: f = f|n +* (n .--> (f.n)) by FUNCT_7:14;
A47: n in Segm(n+1) by NAT_1:45;
hence y in q by FUNCT_2:5;
thus thesis by A40,A43,A44,A45,A46,A47,FUNCT_2:5;
end;
{x} c= rng G by A28,ZFMISC_1:31;
then
A48: G"{x} <> {} by RELAT_1:139;
A49: rng H = G"{x} by A41,FUNCT_2:10;
A50: dom H = q by A48,FUNCT_2:def 1;
for x1,x2 being object st x1 in dom H & x2 in dom H & H.x1 = H.x2
holds x1 = x2
proof
let x1,x2 be object such that
A51: x1 in dom H and
A52: x2 in dom H and
A53: H.x1 = H.x2;
A54: H.x2 = x +* (n .--> x2) by A40,A52;
A55: dom (n .--> x1) = {n};
A56: dom (n .--> x2) = {n};
set fx1 = x +* (n .--> x1);
set fx2 = x +* (n .--> x2);
A57: fx1 = fx2 by A40,A51,A53,A54;
A58: (n .--> x1).n = x1 by FUNCOP_1:72;
A59: (n .--> x2).n = x2 by FUNCOP_1:72;
A60: n in {n} by TARSKI:def 1;
then fx1.n = x1 by A55,A58,FUNCT_4:13;
hence thesis by A56,A57,A59,A60,FUNCT_4:13;
end;
then H is one-to-one;
then q, H.:q are_equipotent by A50,CARD_1:33;
then q, rng H are_equipotent by A50,RELAT_1:113;
hence thesis by A49,CARD_1:def 2;
end;
A61: for x,y being set st x is Element of Funcs(n,q9) &
y is Element of Funcs(n,q9) & x<>y holds (G"{x}) misses (G"{y})
proof
let x,y be set such that x is Element of Funcs(n,q9) and
y is Element of Funcs(n,q9) and
A62: 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 object such that
A63: f in (G"{x} /\ G"{y}) by XBOOLE_0:def 1;
f in G"{x} by A63,XBOOLE_0:def 4;
then
A64: G.f in {x} by FUNCT_1:def 7;
reconsider f as Function of n+1,q by A63,FUNCT_2:66;
f in Funcs(n+1,q) by A1,FUNCT_2:8;
then
A65: R[f, G.f] by A11;
then
A66: f|n = x by A64,TARSKI:def 1;
f in G"{y} by A63,XBOOLE_0:def 4;
then G.f in {y} by FUNCT_1:def 7;
hence contradiction by A62,A65,A66,TARSKI:def 1;
end;
hence thesis;
end;
reconsider X = the set of all G"{x} where x is Element of Funcs(n,q9)
as set;
A67: for y being object holds y in union X implies y in Funcs(n+1,q)
proof
let x be object;
assume x in union X;
then consider Y being set such that
A68: x in Y and
A69: Y in X by TARSKI:def 4;
ex z being Element of Funcs(n,q) st ( G"{z} = Y) by A69;
hence thesis by A68;
end;
for y being object holds y in Funcs(n+1,q) implies y in union X
proof
let x be object;
assume x in Funcs(n+1,q);
then consider f being Function of n+1,q such that
A70: x = f and
A71: G.x = f|n by A11;
A72: f in Funcs(n+1,q) by A1,FUNCT_2:8;
then
A73: f in dom G by FUNCT_2:def 1;
G.f in {f|n} by A70,A71,TARSKI:def 1;
then
A74: f in G"{f|n} by A73,FUNCT_1:def 7;
ex y being object st ( y in Funcs(n,q9))&( R[f,y]) by A5,A72;
then G"{f|n} in X;
hence thesis by A70,A74,TARSKI:def 4;
end;
then
A75: union X = Funcs(n+1,q) by A67,TARSKI:2;
Funcs(n+1,q) is finite by FRAENKEL:6;
then reconsider X as finite set by A75,FINSET_1:7;
A76: card X = q|^n
proof
deffunc FF(object) = G"{$1};
A77: for x being object st x in Funcs(n,q) holds FF(x) in X;
consider F being Function of Funcs(n,q),X such that
A78: for x being object st x in Funcs(n,q) holds F.x = FF(x)
from FUNCT_2:sch 2(A77);
A79: for c being object st c in X
ex x being object st x in Funcs(n,q) & c = F.x
proof
let c be object;
assume c in X;
then consider y being Element of Funcs(n,q) such that
A80: c = G"{y};
F.y = c by A78,A80;
hence thesis;
end;
set gg = the Element of Funcs(n, q9);
A81: G"{gg} in X;
A82: rng F = X by A79,FUNCT_2:10;
A83: dom F = Funcs(n,q) by A81,FUNCT_2:def 1;
for x1,x2 being object st x1 in dom F & x2 in dom F & F.x1 = F. x2
holds x1 = x2
proof
let x1,x2 be object such that
A84: x1 in dom F and
A85: x2 in dom F and
A86: F.x1 = F.x2;
F.x1 = G"{x1} by A78,A84;
then
A87: G"{x1} = G"{x2} by A78,A85,A86;
now
assume x1<>x2;
then (G"{x1}) misses (G"{x2}) by A61,A84,A85;
then G"{x1} /\ G"{x1} = {} by A87,XBOOLE_0:def 7;
hence contradiction by A29,A84,CARD_1:27;
end;
hence thesis;
end;
then F is one-to-one;
then Funcs(n,q), F.:(Funcs(n,q)) are_equipotent by A83,CARD_1:33;
then Funcs(n,q), rng F are_equipotent by A83,RELAT_1:113;
hence thesis by A4,A82,CARD_1:5;
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;
assume Y in X;
then consider x being Element of Funcs(n,q9) such that
A88: Y=G"{x};
A89: Y is finite by A29,A88;
A90: card Y = q by A29,A88;
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
A91: Z in X and
A92: Y <> Z;
consider y being Element of Funcs(n,q9) such that
A93: Z=G"{y} by A91;
A94: card Z = q by A29,A93;
now per cases;
suppose x=y;
hence Y misses Z by A88,A92,A93;
end;
suppose x<>y;
hence Y misses Z by A61,A88,A93;
end;
end;
hence thesis by A90,A94,CARD_1:5;
end;
hence thesis by A89,A90;
end;
then ex C being finite set st
C = union X & card C = q * card X by GROUP_2:156;
hence thesis by A75,A76,NEWTON:6;
end;
for n being Nat holds P[n] from NAT_1:sch 2(A2,A3);
hence thesis;
end;
theorem Th5: :: SumDivision:
for f being FinSequence of NAT, i being Element of NAT
st for j being Element of 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 Element of NAT st for j being Element of NAT st j in dom f
holds i divides f/.j holds i divides Sum f;
A1: P[0]
proof
let f be FinSequence of NAT;
assume len f = 0;
then
A2: f = <*>NAT;
let i be Element of NAT such that
for j being Element of NAT st j in dom f holds i divides f/.j;
Sum f = 0 by A2,RVSUM_1:72;
hence thesis by NAT_D:6;
end;
A3: for k being Nat st P[k] holds P[k+1]
proof
let k be Nat such that
A4: P[k];
let f be FinSequence of NAT such that
A5: len f = k+1;
let i be Element of NAT such that
A6: for j being Element of NAT st j in dom f holds i divides f/.j;
f <> {} by A5;
then consider q being FinSequence, x being object such that
A7: f=q^<*x*> by FINSEQ_1:46;
reconsider f1=q as FinSequence of NAT by A7,FINSEQ_1:36;
reconsider f2=<*x*> as FinSequence of NAT by A7,FINSEQ_1:36;
k + 1 = len f1 + len f2 by A5,A7,FINSEQ_1:22;
then
A8: k + 1 = len f1 + 1 by FINSEQ_1:39;
for j being Element of NAT st j in dom f1 holds i divides f1/.j
proof
let j be Element of NAT such that
A9: j in dom f1;
A10: dom f1 c= dom f by A7,FINSEQ_1:26;
then f/.j = f.j by A9,PARTFUN1:def 6
.= f1.j by A7,A9,FINSEQ_1:def 7
.= f1/.j by A9,PARTFUN1:def 6;
hence thesis by A6,A9,A10;
end;
then
A11: i divides Sum f1 by A4,A8;
rng f2 c= NAT by FINSEQ_1:def 4;
then {x} c= NAT by FINSEQ_1:38;
then reconsider m=x as Element of NAT by ZFMISC_1:31;
A12: f.(len f) = m by A5,A7,A8,FINSEQ_1:42;
len f in Seg len f by A5,FINSEQ_1:3;
then
A13: len f in dom f by FINSEQ_1:def 3;
then f/.(len f) = f.(len f) by PARTFUN1:def 6;
then
A14: i divides m by A6,A12,A13;
Sum f = Sum f1 + m by A7,RVSUM_1:74;
hence thesis by A11,A14,NAT_D:8;
end;
A15: for k being Nat holds P[k] from NAT_1:sch 2(A1,A3);
let f be FinSequence of NAT, i be Element of NAT such that
A16: for j being Element of NAT st j in dom f holds i divides f/.j;
len f = len f;
hence thesis by A15,A16;
end;
theorem Th6: :: 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 Element of 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 Element of NAT st i in dom c holds c.i = card (f.i)
holds card X = Sum c;
A1: P[0]
proof
let X be finite set;
let z be a_partition of X such that
A2: card z = 0;
let f be FinSequence of z such that
f is one-to-one and rng f = z;
let c be FinSequence of NAT such that
A3: len c = len f
and for i being Element of NAT st i in dom c holds c.i = card (f.i);
A4: z = {} by A2;
A5: X = {} by A2;
c = {} by A3,A4;
hence thesis by A5,RVSUM_1:72;
end;
A6: for k being Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume
A7: P[k];
let X be finite set;
let Z be a_partition of X such that
A8: card Z = k + 1;
let f be FinSequence of Z such that
A9: f is one-to-one and
A10: rng f = Z;
let c be FinSequence of NAT such that
A11: len c = len f and
A12: for i being Element of NAT st i in dom c holds c.i = card (f.i);
A13: len f = k + 1 by A8,A9,A10,FINSEQ_4:62;
A14: Z <> {} by A8;
reconsider Z as non empty set by A8;
reconsider f as FinSequence of Z;
reconsider X as non empty finite set by A14;
reconsider fk = f|(Seg k) as FinSequence of Z by FINSEQ_1:18;
A15: len fk = k by A13,FINSEQ_3:53;
A16: f = fk ^ <*f.(k+1)*> by A13,FINSEQ_3:55;
reconsider Zk = rng fk as finite set;
reconsider fk as FinSequence of Zk by FINSEQ_1:def 4;
A17: fk is one-to-one by A9,FUNCT_1:52;
then
A18: card Zk = k by A15,FINSEQ_4:62;
reconsider Xk = union Zk as finite set;
A19: now
A20: 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
A21: a in Zk;
A22: a in Z by A21;
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
A23: b in Zk;
A24: a in Z by A21;
b in Z by A23;
hence thesis by A24,EQREL_1:def 4;
end;
hence thesis by A22;
end;
Zk c= bool union Zk by ZFMISC_1:82;
hence Zk is a_partition of Xk by A20,EQREL_1:def 4;
end;
reconsider ck = c|(Seg k) as FinSequence of NAT by FINSEQ_1:18;
A25: len ck = len fk by A11,A13,A15,FINSEQ_3:53;
for i being Element of NAT st i in dom ck holds ck.i = card (fk.i)
proof
let i be Element of NAT;
assume
A26: i in dom ck;
A27: k <= k+1 by NAT_1:11;
then dom ck = (Seg k) by A11,A13,FINSEQ_1:17;
then
A28: dom ck = dom fk by A13,A27,FINSEQ_1:17;
A29: dom ck c= dom c by RELAT_1:60;
ck.i = c.i by A26,FUNCT_1:47;
then ck.i = card (f.i) by A12,A26,A29;
hence thesis by A26,A28,FUNCT_1:47;
end;
then
A30: card Xk = Sum ck by A7,A17,A18,A19,A25;
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
A31: x in Zk;
A32: x in Z by A31;
dom f = Seg(len f) by FINSEQ_1:def 3;
then
A33: fk1 in rng f by A13,FINSEQ_1:4,FUNCT_1:3;
consider i being Nat such that
A34: i in dom fk and
A35: fk.i = x by A31,FINSEQ_2:10;
now
assume
A36: fk.i = fk1;
A37: dom fk = Seg k by A15,FINSEQ_1:def 3;
A38: i in Seg k by A15,A34,FINSEQ_1:def 3;
i <= k by A34,A37,FINSEQ_1:1;
then
A39: i < k+1 by NAT_1:13;
A40: dom f = Seg (k + 1) by A13,FINSEQ_1:def 3;
k <= k + 1 by NAT_1:12;
then
A41: Seg k c= Seg (k+1) by FINSEQ_1:5;
A42: (k+1) in dom f by A40,FINSEQ_1:4;
fk.i = f.i by A34,FUNCT_1:47;
hence contradiction by A9,A36,A38,A39,A40,A41,A42;
end;
hence thesis by A10,A32,A33,A35,EQREL_1:def 4;
end;
then
A43: fk1 misses Xk by ZFMISC_1:80;
dom f = Seg(len f) by FINSEQ_1:def 3;
then fk1 in rng f by A13,FINSEQ_1:4,FUNCT_1:3;
then reconsider fk1 as finite set;
A44: Z = rng fk \/ rng <*fk1*> by A10,A16,FINSEQ_1:31
.= Zk \/ {fk1} by FINSEQ_1:39;
A45: X = union Z by EQREL_1:def 4
.= union Zk \/ union {fk1} by A44,ZFMISC_1:78
.= Xk \/ fk1 by ZFMISC_1:25;
k+1 in Seg(k+1) by FINSEQ_1:4;
then
A46: k+1 in dom c by A11,A13,FINSEQ_1:def 3;
rng ck c= REAL;
then reconsider ckc=ck as FinSequence of REAL by FINSEQ_1:def 4;
card X = Sum ck + card fk1 by A30,A43,A45,CARD_2:40
.= Sum ck + c.(k+1) by A12,A46
.= Sum (ckc^<*(c.(k+1))*>) by RVSUM_1:74
.= Sum c by A11,A13,FINSEQ_3:55;
hence thesis;
end;
A47: for k being Nat holds P[k] from NAT_1:sch 2(A1, A6);
let X be finite set, Y be a_partition of X;
card Y = card Y;
hence thesis by A47;
end;
begin :: Class formula for groups
registration
let G be finite Group;
cluster center G -> finite;
correctness;
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};
A1: a*1_G = a by GROUP_1:def 4;
1_G*a = a by GROUP_1:def 4;
then
A2: 1_G in Car by A1;
for x being object st x in Car holds x in the carrier of G
proof
let x be object;
assume x in Car;
then ex g being Element of G st ( x = g)&( a*g = g*a);
hence thesis;
end;
then
A3: Car is Subset of G by TARSKI:def 3;
A4: 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
A5: g1 in Car and
A6: g2 in Car;
A7: ex z1 being Element of G st ( z1=g1)&( z1*a = a*z1) by A5;
A8: ex z2 being Element of G st ( z2=g2)&( z2*a = a*z2) by A6;
a*(g1*g2) = (g1*a)*g2 by A7,GROUP_1:def 3
.= g1*(g2*a) by A8,GROUP_1:def 3
.= g1*g2*a by GROUP_1:def 3;
hence thesis;
end;
for g being Element of G st g in Car holds g" in Car
proof
let g be Element of G;
assume g in Car;
then
A9: ex z1 being Element of G st ( z1=g)&( z1*a = a*z1);
g"*(g*a) = a by GROUP_3:1;
then g"*((a*g)*g") = a*g" by A9,GROUP_1:def 3;
then g"*a = a* g" by GROUP_3:1;
hence thesis;
end;
hence thesis by A2,A3,A4,GROUP_2:52;
end;
uniqueness
proof
let H1,H2 be strict Subgroup of G such that
A10: the carrier of H1 = { b where b is Element of G: a*b = b*a} and
A11: 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
by A10,A11;
hence thesis;
end;
end;
registration
let G be finite Group;
let a be Element of G;
cluster Centralizer a -> finite;
correctness;
end;
theorem Th7:
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
A1: 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 A1;
then ex b being Element of G st b = x & a*b = b*a;
hence thesis;
end;
theorem Th8:
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;
A1: the carrier of Centralizer a =
{ b where b is Element of G : a*b = b*a } by Def1;
hereby
assume a*x = x*a;
then x in the carrier of Centralizer a by A1;
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 A1;
hence thesis;
end;
registration
let G be Group, a be Element of G;
cluster con_class a -> non empty;
correctness by GROUP_3:83;
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
:Def2:
for x being Element of G holds it.x = a |^ x;
existence
proof
defpred P[Element of G, set] means $2 = a |^ $1;
A1: 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:82;
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 FUNCT_2:sch 3(A1);
hence thesis;
end;
uniqueness
proof
let it1, it2 be Function of the carrier of G, con_class a such that
A2: for x being Element of G holds it1.x = a |^ x and
A3: for x being Element of G holds it2.x = a |^ x;
A4: dom it1 = the carrier of G by FUNCT_2:def 1;
A5: dom it2 = the carrier of G by FUNCT_2:def 1;
for x being object st x in dom it1 holds it1.x = it2.x
proof
let x be object;
assume x in dom it1;
then reconsider y=x as Element of G;
it1.y = a |^ y by A2;
hence thesis by A3;
end;
hence thesis by A4,A5;
end;
end;
theorem Th9: :: Br1:
for G being finite Group, a being Element of G, x being Element of con_class a
holds card (a-con_map"{x}) = card Centralizer a
proof
let G be finite Group, a be Element of G, x be Element of con_class a;
ex b being Element of G st ( b = x)&( a,b are_conjugated) by GROUP_3:80;
then consider d being Element of G such that
A1: x = a |^ d by GROUP_3:74;
reconsider Cad = (Centralizer a)*d as Subset of G;
A2: ex B,C being finite set st ( B = d*(Centralizer a))&( C =
Cad)&( card Centralizer a = card B)&( card Centralizer a = card C) by
GROUP_2:133;
for g being object holds g in a-con_map"{x} iff g in Cad
proof
let g be object;
A3: now
assume
A4: g in a-con_map"{x};
then a-con_map.g in {x} by FUNCT_1:def 7;
then
A5: a-con_map.g = x by TARSKI:def 1;
reconsider y=g as Element of G by A4;
A6: a-con_map.g = a |^ y by Def2;
A7: y*((d"*a)*d) = y*(d"*a)*d by GROUP_1:def 3
.= y*d"*a*d by GROUP_1:def 3;
y*((y"*a)*y) = y*(y"*a)*y by GROUP_1:def 3
.= a*y by GROUP_3:1;
then y*d"*a*d*d" = a*(y*d") by A1,A5,A6,A7,GROUP_1:def 3;
then (y*d")*a = a*(y*d") by GROUP_3:1;
then (y*d") is Element of Centralizer a by Th8;
then consider z being Element of G such that
A8: z in the carrier of Centralizer a and
A9: y*d" = z;
A10: z in Centralizer a by A8;
reconsider z as Element of G;
y = z*d by A9,GROUP_3:1;
hence g in Cad by A10,GROUP_2:104;
end;
now
assume g in Cad;
then consider z being Element of G such that
A11: g = z*d and
A12: z in Centralizer a by GROUP_2:104;
reconsider y=g as Element of G by A11;
y*d" = z by A11,GROUP_3:1;
then y*d" in carr(Centralizer a) by A12;
then (y*d")*a = a*(y*d") by Th8;
then (y*d")*a*d = a*((y*d")*d) by GROUP_1:def 3;
then (y*d")*a*d = a*y by GROUP_3:1;
then (y*d")*(a*d) = a*y by GROUP_1:def 3;
then y"*((y*d")*(a*d)) = y"*a*y by GROUP_1:def 3;
then (y"*(y*d"))*(a*d) = y"*a*y by GROUP_1:def 3;
then d"*(a*d) = y"*a*y by GROUP_3:1;
then x = a|^y by A1,GROUP_1:def 3;
then a-con_map.y = x by Def2;
then
A13: 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 A13,FUNCT_1:def 7;
end;
hence thesis by A3;
end;
hence thesis by A2,TARSKI:2;
end;
theorem Th10: :: 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
A1: x <> y;
now
assume ex g being object st g in (a-con_map"{x}) /\ (a-con_map"{y });
then consider g being set such that
A2: g in (a-con_map"{x}) /\ (a-con_map"{y});
A3: g in a-con_map"{x} by A2,XBOOLE_0:def 4;
A4: g in a-con_map"{y} by A2,XBOOLE_0:def 4;
a-con_map.g in {x} by A3,FUNCT_1:def 7;
then
A5: a-con_map.g = x by TARSKI:def 1;
a-con_map.g in {y} by A4,FUNCT_1:def 7;
hence contradiction by A1,A5,TARSKI:def 1;
end;
then (a-con_map"{x}) /\ (a-con_map"{y}) = {} by XBOOLE_0:def 1;
hence thesis by XBOOLE_0:def 7;
end;
theorem Th11: :: Br3:
for G being Group, a being Element of G
holds the set of all a-con_map"{x} where x is Element of con_class a
is a_partition of the carrier of G
proof
let G be Group, a be Element of G;
reconsider X =
the set of all a-con_map"{x} where x is Element of con_class a as set;
A1: for y being object holds y in union X implies y in the carrier of G
proof
let x be object;
assume x in union X;
then consider Y being set such that
A2: x in Y and
A3: Y in X by TARSKI:def 4;
ex z being Element of con_class a st ( a-con_map"{z} = Y) by A3;
hence thesis by A2;
end;
for y being object holds y in the carrier of G implies y in union X
proof
let x be object;
assume x in the carrier of G;
then reconsider y=x as Element of G;
consider z being Element of G such that
A4: z in con_class a and
A5: z = a|^y by GROUP_3:82;
a-con_map.y = z by A5,Def2;
then
A6: a-con_map.y in {z} by TARSKI:def 1;
dom(a-con_map) = the carrier of G by FUNCT_2:def 1;
then
A7: y in a-con_map"{z} by A6,FUNCT_1:def 7;
a-con_map"{z} in X by A4;
hence thesis by A7,TARSKI:def 4;
end;
then
A8: union X = the carrier of G by A1,TARSKI:2;
A9: 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;
assume A in X;
then consider x being Element of con_class a such that
A10: A = a-con_map"{x};
a,x are_conjugated by GROUP_3:81;
then consider g being Element of G such that
A11: x = a |^ g by GROUP_3:74;
a-con_map.g = x by A11,Def2;
then
A12: a-con_map.g in {x} by TARSKI:def 1;
A13: dom (a-con_map) = the carrier of G by FUNCT_2:def 1;
for B being Subset of G st B in X holds A=B or A misses B
proof
let B be Subset of G;
assume B in X;
then ex y being Element of con_class a st ( B = a-con_map"{y});
hence thesis by A10,Th10;
end;
hence thesis by A10,A12,A13,FUNCT_1:def 7;
end;
X c= bool union X by ZFMISC_1:82;
hence thesis by A8,A9,EQREL_1:def 4;
end;
theorem Th12:
for G being finite Group, a being Element of G
holds card the set of all a-con_map"{x} where x is Element of con_class a
= card con_class a
proof
let G be finite Group, a be Element of G;
reconsider X = the set of all
a-con_map"{x} where x is Element of con_class a
as a_partition of the carrier of G by Th11;
deffunc FF(object) = a-con_map"{$1};
A1: for x being object 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 object st x in con_class a holds F.x = FF(x)
from FUNCT_2:sch 2
(A1);
for c being object st c in X
ex x being object st x in con_class a & c = F.x
proof
let c be object such that
A3: c in X;
reconsider c as Subset of G by A3;
consider y being Element of con_class a such that
A4: c = a-con_map"{y} by A3;
F.y = c by A2,A4;
hence thesis;
end;
then
A5: rng F = X by FUNCT_2:10;
A6: dom F = con_class a by FUNCT_2:def 1;
for x1,x2 being object
st x1 in dom F & x2 in dom F & F.x1=F.x2 holds x1 = x2
proof
let x1,x2 be object such that
A7: x1 in dom F and
A8: x2 in dom F and
A9: F.x1 = F.x2;
reconsider y1=x1 as Element of con_class a by A7;
reconsider y2=x2 as Element of con_class a by A8;
A10: a-con_map"{y1} = F.y1 by A2;
A11: a-con_map"{y2} = F.y2 by A2;
now
assume y1<>y2;
then (a-con_map"{y1}) misses (a-con_map"{y2}) by Th10;
then ((a-con_map"{y1}) /\ (a-con_map"{y2})) = {} by XBOOLE_0:def 7;
hence contradiction by A9,A10,A11;
end;
hence thesis;
end;
then F is one-to-one;
then con_class a, F.:(con_class a) are_equipotent by A6,CARD_1:33;
then con_class a, rng F are_equipotent by A6,RELAT_1:113;
hence thesis by A5,CARD_1:5;
end;
theorem Th13:
for G being finite Group, a being Element of G
holds card G = card con_class a * card Centralizer a
proof
let G be finite Group, a be Element of G;
reconsider
X = the set of all a-con_map"{x} where x is Element of con_class a
as a_partition of the carrier of G by Th11;
A1: for
A being set st A in X holds A is finite & card A = card Centralizer a &
for B being set st B in X & A<>B holds A misses B
proof
let A be set such that
A2: A in X;
reconsider A as Subset of G by A2;
ex x being Element of con_class a st ( A = a-con_map"{x}) by A2;
hence thesis by A2,Th9,EQREL_1:def 4;
end;
reconsider k = card Centralizer a as Element of NAT;
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
A3: Y in X;
reconsider Y as finite set by A3;
A4: card Y = card Centralizer a by A1,A3;
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
A5: Z in X and
A6: Y<>Z;
A7: card Y = card Centralizer a by A1,A3;
card Z = card Centralizer a by A1,A5;
hence thesis by A1,A3,A5,A6,A7,CARD_1:5;
end;
hence thesis by A4;
end;
then consider C being finite set such that
A8: C = union X and
A9: card C = card X * k by GROUP_2:156;
card G = card C by A8,EQREL_1:def 4
.= card con_class a * card
Centralizer a by A9,Th12;
hence thesis;
end;
definition
let G be Group;
func conjugate_Classes G -> a_partition of the carrier of G equals
the set of all con_class a where a is Element of G;
correctness
proof
set cG = the carrier of G;
set C = the set of all con_class a where a is Element of G;
A1: C c= bool cG
proof
let x be object;
assume x in C;
then ex a being Element of cG st x = con_class a;
hence thesis;
end;
now
let x be object;
hereby
assume x in union C;
then consider S being set such that
A2: x in S and
A3: S in C by TARSKI:def 4;
ex a being Element of G st S=con_class a by A3;
hence x in cG by A2;
end;
assume x in cG;
then reconsider x9=x as Element of cG;
reconsider S = con_class x9 as Subset of cG;
A4: S in C;
x9 in con_class x9 by GROUP_3:83;
hence x in union C by A4,TARSKI:def 4;
end;
then
A5: union C = cG by TARSKI:2;
now
let A be Subset of cG;
assume
A6: A in C;
then
A7: ex a being Element of cG st A = con_class a;
consider a being Element of cG such that
A8: A = con_class a by A6;
thus A<>{} by A7;
let B be Subset of cG;
assume B in C;
then consider b being Element of cG such that
A9: B = con_class b;
assume
A10: A <> B;
assume A meets B;
then consider x being object such that
A11: x in A and
A12: x in B by XBOOLE_0:3;
reconsider x as Element of cG by A11;
A13: x,a are_conjugated by A8,A11,GROUP_3:81;
x,b are_conjugated by A9,A12,GROUP_3:81;
then
A14: a,b are_conjugated by A13,GROUP_3:77;
now
let c be object;
hereby
assume
A15: c in A;
then reconsider c9=c as Element of cG;
c9,a are_conjugated by A8,A15,GROUP_3:81;
then c9,b are_conjugated by A14,GROUP_3:77;
hence c in B by A9,GROUP_3:81;
end;
assume
A16: c in B;
then reconsider c9=c as Element of cG;
c9,b are_conjugated by A9,A16,GROUP_3:81;
then c9,a are_conjugated by A14,GROUP_3:77;
hence c in A by A8,GROUP_3:81;
end;
hence contradiction by A10,TARSKI:2;
end;
hence thesis by A1,A5,EQREL_1:def 4;
end;
end;
theorem :: 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 Element of NAT st i in dom c
holds c.i = card (f.i) holds card G = Sum c by Th6;
begin :: Centers and centralizers of skew fields
theorem Th15: :: 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
A1: V is finite-dimensional and
A2: n = dim V and
A3: q = card the carrier of F;
consider B being finite Subset of V such that
A4: B is Basis of V by A1,MATRLIN:def 1;
A5: B is linearly-independent by A4,VECTSP_7:def 3;
A6: Lin(B) = the ModuleStr of V by A4,VECTSP_7:def 3;
A7: card B = n by A1,A2,A4,VECTSP_9:def 1;
now per cases;
suppose
A8: n = 0;
then (Omega).V = (0).V by A1,A2,VECTSP_9:29;
then the ModuleStr of V = (0).V by VECTSP_4:def 4;
then the carrier of V = {0.V} by VECTSP_4:def 3;
then card the carrier of V = 1 by CARD_1:30
.= q #Z 0 by PREPOWER:34
.= q |^ 0 by PREPOWER:36;
hence thesis by A8;
end;
suppose n <> 0;
then
A9: B <> 0 by A7;
consider bf being FinSequence such that
A10: rng bf = B and
A11: bf is one-to-one by FINSEQ_4:58;
len bf = n by A7,A10,A11,FINSEQ_4:62;
then
A12: Seg n = dom bf by FINSEQ_1:def 3;
reconsider Vbf = bf as FinSequence of the carrier of V by A10,
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);
A13: 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(object) = f.(union (Vbf"{$1}));
A14: for x being object st x in B holds LC(x) in the carrier of F
proof
let x be object;
assume x in B;
then consider i being object such that
A15: Vbf"{x} = {i} by A10,A11,FUNCT_1:74;
A16: union (Vbf"{x}) = i by A15,ZFMISC_1:25;
i in Vbf"{x} by A15,TARSKI:def 1;
then i in dom Vbf by FUNCT_1:def 7;
then i in dom f by A12,FINSEQ_2:124;
then f.i in rng f by FUNCT_1:3;
hence thesis by A16;
end;
consider lc being Function of B, the carrier of F such that
A17: for y being object st y in B holds lc.y = LC(y)
from FUNCT_2:sch 2
(A14);
set ll=lc +* (((the carrier of V)\B) --> 0.F);
A18: dom (((the carrier of V)\B) --> 0.F) = (the carrier of V)\B;
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
A19: dom ll = the carrier of V by XBOOLE_1:12;
rng ll c= rng lc \/ rng (((the carrier of V)\B)--> 0.F)
by FUNCT_4:17;
then ll is Function of the carrier of V,the carrier of F
by A19,FUNCT_2:2,XBOOLE_1:1;
then
A20: ll is Element of Funcs(the carrier of V, the carrier of F)
by FUNCT_2:8;
A21: for i being set st i in dom f holds ll.(Vbf.i) = f.i
proof
let i be set;
assume i in dom f;
then
A22: i in dom Vbf by A12,FINSEQ_2:124;
then Vbf.i in B by A10,FUNCT_1:3;
then consider y being Element of B such that
A23: y = Vbf.i;
A24: Vbf.i in {y} by A23,TARSKI:def 1;
consider ee being object such that
A25: Vbf"{y} c= {ee} by A11,FUNCT_1:89;
A26: i in Vbf"{y} by A22,A24,FUNCT_1:def 7;
then {i} c= {ee} by A25,ZFMISC_1:31;
then i = ee by ZFMISC_1:18;
then
A27: Vbf"{y} = {i} by A25,A26,ZFMISC_1:33;
not y in (the carrier of V)\B by A9,XBOOLE_0:def 5;
then ll.y = lc.y by A18,FUNCT_4:11;
then ll.y = f.(union (Vbf"{y})) by A9,A17;
hence thesis by A23,A27,ZFMISC_1:25;
end;
A28: for v being Element of V st not v in B holds ll.v = 0.F
proof
let v be Element of V;
assume not v in B;
then
A29: v in (the carrier of V)\B by XBOOLE_0:def 5;
then ll.v=(((the carrier of V)\B)-->0.F).v by A18,FUNCT_4:13;
hence thesis by A29,FUNCOP_1:7;
end;
then reconsider L=ll as Linear_Combination of V by A20,VECTSP_6:def 1
;
for v being Element of V holds v in Carrier(L) implies v in B
proof
let v be Element of V;
assume
A30: v in Carrier(L);
now
assume not v in B;
then ll.v = 0.F by A28;
hence contradiction by A30,VECTSP_6:2;
end;
hence thesis;
end;
then Carrier(L) c= B;
then L is Linear_Combination of B by VECTSP_6:def 4;
hence thesis by A21;
end;
then consider lc being Linear_Combination of B such that
A31: 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 A6,A31;
end;
consider G being Function of ntocF,cLinB such that
A32: for tup being Element of ntocF holds P[tup, G.tup]
from FUNCT_2:sch 3(A13);
A33: dom G = ntocF by FUNCT_2:def 1;
A34: for L being Linear_Combination of B holds ex nt being Element of ntocF st
for i being object st i in dom nt holds nt.i = L.(Vbf.i)
proof
let L be Linear_Combination of B;
deffunc F(object) = L.(Vbf.$1);
A35: for x being object st x in Seg n holds F(x) in the carrier of F
proof
let x be object;
assume x in Seg n;
then Vbf.x in rng Vbf by A12,FUNCT_1:3;
then consider vv be Element of V such that
A36: Vbf.x = vv;
L.vv in the carrier of F;
hence thesis by A36;
end;
consider f being Function of Seg n, the carrier of F such that
A37: for x being object st x in Seg n holds f.x = F(x)
from FUNCT_2:sch 2(A35
);
A38: dom f = Seg n by FUNCT_2:def 1;
A39: rng f c= the carrier of F;
A40: n is Element of NAT by ORDINAL1:def 12;
f is FinSequence-like by A38,FINSEQ_1:def 2;
then reconsider ff=f as FinSequence of the carrier of F
by A39,FINSEQ_1:def 4;
len ff = n by A38,A40,FINSEQ_1:def 3;
then ff is Element of ntocF by FINSEQ_2:92;
hence thesis by A37,A38;
end;
:: Show G is surjective
for c being object st c in cLinB
ex x being object st x in ntocF & c = G.x
proof
let c be object;
assume c in cLinB;
then c in (Lin(B));
then consider l being Linear_Combination of B such that
A41: c = Sum(l) by VECTSP_7:7;
Carrier(l) c= rng Vbf by A10,VECTSP_6:def 4;
then
A42: Sum(l (#) Vbf) = Sum(l) by A11,VECTSP_9:3;
consider t being Element of ntocF such that
A43: for i being object st i in dom t holds t.i = l.(Vbf.i) by A34;
consider lc being Linear_Combination of B such that
A44: for i being set st i in dom t holds lc.(Vbf.i) = t.i and
A45: G.t = Sum(lc (#) Vbf) by A32;
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 object such that
A46: [x,v] in Vbf by XTUPLE_0:def 13;
A47: x in dom Vbf by A46,FUNCT_1:1;
A48: Vbf.x = v by A46,FUNCT_1:1;
A49: x in dom t by A12,A47,FINSEQ_2:124;
then l.(Vbf.x) = t.x by A43;
hence thesis by A44,A48,A49;
end;
suppose
A50: not v in rng Vbf;
now
assume
A51: v in Carrier(l);
Carrier(l) c= rng Vbf by A10,VECTSP_6:def 4;
hence contradiction by A50,A51;
end;
then
A52: l.v = 0.F by VECTSP_6:2;
now
assume
A53: v in Carrier(lc);
Carrier(lc) c= rng Vbf by A10,VECTSP_6:def 4;
hence contradiction by A50,A53;
end;
hence thesis by A52,VECTSP_6:2;
end;
end;
hence thesis;
end;
then G.t = Sum(l (#) Vbf) by A45,VECTSP_6:def 7;
hence thesis by A41,A42;
end;
then
A54: rng G = cLinB by FUNCT_2:10;
:: Show G is injective
for x1,x2 being object st x1 in dom G & x2 in dom G & G.x1 = G.x2
holds x1 = x2
proof
let x1,x2 be object such that
A55: x1 in dom G and
A56: x2 in dom G and
A57: G.x1 = G.x2;
reconsider t1=x1 as Element of ntocF by A55;
reconsider t2=x2 as Element of ntocF by A56;
consider L1 being Linear_Combination of B such that
A58: for i being set st i in dom t1 holds L1.(Vbf.i) = t1.i and
A59: G.t1 = Sum(L1 (#) Vbf) by A32;
consider L2 being Linear_Combination of B such that
A60: for i being set st i in dom t2 holds L2.(Vbf.i) = t2.i and
A61: G.t2 = Sum(L2 (#) Vbf) by A32;
Carrier(L1) c= rng Vbf by A10,VECTSP_6:def 4;
then
A62: Sum(L1) = Sum(L1 (#) Vbf) by A11,VECTSP_9:3;
Carrier(L2) c= rng Vbf by A10,VECTSP_6:def 4;
then Sum(L2) = Sum(L2 (#) Vbf) by A11,VECTSP_9:3;
then Sum(L1) - Sum(L2) = 0.V by A57,A59,A61,A62,VECTSP_1:19;
then
A63: Sum(L1 - L2) = 0.V by VECTSP_6:47;
(L1 - L2) is Linear_Combination of B by VECTSP_6:42;
then
A64: Carrier(L1 - L2) = {} by A5,A63,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 VECTSP_6:42;
LL.v = 0.F by A64,VECTSP_6:2;
then 0.F = L1.v - L2.v by VECTSP_6:40;
hence thesis by VECTSP_1:27;
end;
then
A65: L1 = L2 by VECTSP_6:def 7;
A66: dom t1 = Seg n by FINSEQ_2:124;
A67: dom t2 = Seg n by FINSEQ_2:124;
for k being Nat st k in dom t1 holds t1.k = t2.k
proof
let k be Nat such that
A68: k in dom t1;
t1.k = L1.(Vbf.k) by A58,A68;
hence thesis by A60,A65,A66,A67,A68;
end;
hence thesis by A67,FINSEQ_1:13,FINSEQ_2:124;
end;
then G is one-to-one;
then ntocF, G.:(ntocF) are_equipotent by A33,CARD_1:33;
then
A69: ntocF, cLinB are_equipotent by A33,A54,RELAT_1:113;
A70: card (Seg n) = card n by FINSEQ_1:55;
A71: card q = card the carrier of F by A3;
card (ntocF) = card Funcs (Seg n, the carrier of F) by FINSEQ_2:93
.= card Funcs (n, q) by A70,A71,FUNCT_5:61
.= q |^ n by A3,Th4;
hence thesis by A6,A69,CARD_1:5;
end;
end;
hence thesis;
end;
definition
let R be associative well-unital right_complementable
add-associative right_zeroed right-distributive left-distributive
non empty doubleLoopStr;
func center R -> commutative strict non empty doubleLoopStr means
:Def4:
the carrier of it = {x where x is Element of R:
for s being Element of R holds x*s = s*x} &
the addF of it = (the addF of R)||the carrier of it &
the multF of it = (the multF of R)||the carrier of it &
0.it = 0.R &
1.it = 1.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};
for s being Element of cR holds (0.R)*s = s*(0.R);
then
A1: 0.R in ccs;
then reconsider ccs as non empty set;
A2: ccs c= cR
proof
let x be object;
assume x in ccs;
then ex x9 being Element of cR st
x9=x & for s being Element of R holds x9*s = s*x9;
hence thesis;
end;
set acs = (the addF of R)||ccs;
set mcs = (the multF of R)||ccs;
set Zs = 0.R;
set Us = 1.R;
A3: [:ccs,ccs:] c= [:cR,cR:]
proof
let x be object;
assume x in [:ccs,ccs:];
then ex a,b being object st ( a in ccs)&( b in ccs)&( x =[a,b]) by
ZFMISC_1:def 2;
hence thesis by A2,ZFMISC_1:def 2;
end;
then reconsider acs as Function of [:ccs,ccs:],cR by FUNCT_2:32;
rng acs c= ccs
proof
let y be object;
assume y in rng acs;
then consider x being object such that
A4: x in dom acs and
A5: y = acs.x by FUNCT_1:def 3;
consider a,b being object such that
A6: a in ccs and
A7: b in ccs and
A8: x = [a,b] by A4,ZFMISC_1:def 2;
reconsider a,b as Element of cR by A2,A6,A7;
A9: ex a9 being Element of cR st a9=a &
for s being Element of R holds a9*s = s*a9 by A6;
A10: ex b9 being Element of cR st b9=b &
for s being Element of R holds b9*s = s*b9 by A7;
[a,b] in [:ccs,ccs:] by A6,A7,ZFMISC_1:def 2;
then
A11: a+b = acs.x by A8,FUNCT_1:49;
now
let s be Element of cR;
thus (a+b)*s=a*s+b*s by VECTSP_1:def 3
.= s*a+b*s by A9
.= s*a+s*b by A10
.=s*(a+b) by VECTSP_1:def 2;
end;
hence thesis by A5,A11;
end;
then reconsider acs as BinOp of ccs by FUNCT_2:6;
reconsider mcs as Function of [:ccs,ccs:],cR by A3,FUNCT_2:32;
rng mcs c= ccs
proof
let y be object;
assume y in rng mcs;
then consider x being object such that
A12: x in dom mcs and
A13: y = mcs.x by FUNCT_1:def 3;
consider a,b being object such that
A14: a in ccs and
A15: b in ccs and
A16: x = [a,b] by A12,ZFMISC_1:def 2;
reconsider a,b as Element of cR by A2,A14,A15;
A17: ex a9 being Element of cR st a9=a &
for s being Element of R holds a9*s = s*a9 by A14;
A18: ex b9 being Element of cR st b9=b &
for s being Element of R holds b9*s = s*b9 by A15;
[a,b] in [:ccs,ccs:] by A14,A15,ZFMISC_1:def 2;
then
A19: a*b = mcs.x by A16,FUNCT_1:49;
now
let s be Element of cR;
thus (a*b)*s=a*(b*s) by GROUP_1:def 3
.= a*(s*b) by A18
.= (a*s)*b by GROUP_1:def 3
.= (s*a)*b by A17
.= s*(a*b) by GROUP_1:def 3;
end;
hence thesis by A13,A19;
end;
then reconsider mcs as BinOp of ccs by FUNCT_2:6;
reconsider Zs as Element of ccs by A1;
for s being Element of cR holds (1.R)*s = s*(1.R);
then Us in ccs;
then reconsider Us as Element of ccs;
reconsider cs = doubleLoopStr (# ccs, acs, mcs, Us, Zs #)
as strict non empty doubleLoopStr;
set ccs1 = the carrier of cs;
A20: now
let x,s be Element of cR;
assume x in ccs;
then ex x9 being Element of cR st x9=x &
for s being Element of R holds x9*s = s*x9;
hence x*s=s*x;
end;
A21: now
let a,b be Element of cR, c,d be Element of ccs1 such that
A22: a=c and
A23: b=d;
[c,d] in [:ccs,ccs:] by ZFMISC_1:def 2;
hence a*b= c*d by A22,A23,FUNCT_1:49;
end;
cs is commutative
proof
let x,y be Element of ccs1;
reconsider x9=x,y9=y as Element of cR by A2;
thus x*y = x9*y9 by A21
.= y9*x9 by A20
.= y*x by A21;
end;
then reconsider cs as commutative strict non empty doubleLoopStr;
take cs;
thus thesis;
end;
uniqueness;
end;
Lm1:
for R being right_complementable Abelian add-associative right_zeroed
associative well-unital distributive non empty doubleLoopStr
for x being Element of center R
holds x is Element of R
proof
let R be right_complementable Abelian add-associative right_zeroed
associative well-unital distributive non empty doubleLoopStr;
let x be Element of center R;
x in the carrier of center R;
then x in {y where y is Element of R:
for s being Element of R holds y * s = s * y} by Def4;
then ex y being Element of R st y = x
& (for s being Element of R holds y * s = s * y);
hence x is Element of R;
end;
Lm2:
for R being right_complementable Abelian add-associative right_zeroed
associative well-unital distributive non empty doubleLoopStr
for x,y being Element of center R
for a,b being Element of R
st x = a & y = b
holds a + b = x + y & a * b = x * y
proof
let R be right_complementable Abelian add-associative right_zeroed
associative well-unital distributive non empty doubleLoopStr;
let x,y be Element of center R;
let a,b be Element of R;
assume A1: x = a & y = b;
set ccR = the carrier of center R;
A2: [x,y] in [:ccR,ccR:] by ZFMISC_1:87;
the addF of (center R) = (the addF of R)||(the carrier of (center R))
by Def4;
hence x + y = a + b by A1, A2, FUNCT_1:49;
the multF of (center R) = (the multF of R)||(the carrier of (center R))
by Def4;
hence x * y = a * b by A1, A2, FUNCT_1:49;
end;
Lm3:
for R being right_complementable Abelian add-associative right_zeroed
associative well-unital distributive non empty doubleLoopStr
for a,b being Element of R
st a in center R
holds a * b = b * a
proof
let R be right_complementable Abelian add-associative right_zeroed
associative well-unital distributive non empty doubleLoopStr;
let a,b be Element of R;
assume A1: a in center R;
then a in the carrier of center R;
then a in {x where x is Element of R:
for s being Element of R holds x*s = s*x} by Def4;
then ex x being Element of R st (x = a) & (for s being Element
of R holds x*s=s*x);
hence a * b = b * a;
end;
registration
let R be right_complementable Abelian add-associative right_zeroed
associative well-unital distributive non empty doubleLoopStr;
cluster center R -> right_complementable;
correctness
proof
for x being Element of center R
holds x is right_complementable
proof
let x be Element of center R;
reconsider a = x as Element of R by Lm1;
consider b being Element of R such that
A1: a + b = 0.R by ALGSTR_0:def 11;
A2: for s being Element of R holds b * s = s * b
proof
let s be Element of R;
x in the carrier of center R;
then x in {x9 where x9 is Element of R:
for s9 being Element of R holds x9*s9 = s9*x9} by Def4;
then ex x9 being Element of R st x9 = x &
for s9 being Element of R holds x9*s9 = s9*x9;
then A3: a * s = s * a;
(0.R) * s = s * (0.R);
then (a * s) + (b * s) = s * (a + b) by A1, VECTSP_1:def 3;
then (a * s) + (b * s) = (s * a) + (s * b) by VECTSP_1:def 2;
then (-(a * s) + a * s) + b * s = -(s * a) + (s * a + s * b)
by A3, RLVECT_1:def 3;
then (0.R) + (b * s) = -(s*a) + (s*a + s*b) by RLVECT_1:5;
then b*s = -(s*a) + (s*a + s*b) by RLVECT_1:4;
then b*s = (-(s*a) + s*a) + s*b by RLVECT_1:def 3;
then b*s = 0.R + s*b by RLVECT_1:5;
hence b * s = s * b by RLVECT_1:4;
end;
then b in {x9 where x9 is Element of R:
for s being Element of R holds x9*s = s*x9};
then b in the carrier of center R by Def4;
then reconsider y = b as Element of center R;
x + y = a + b by Lm2
.= 0.(center R) by A1, Def4;
hence x is right_complementable by ALGSTR_0:def 11;
end;
hence thesis by ALGSTR_0:def 16;
end;
cluster center R -> Abelian;
correctness
proof
for x,y being Element of center R
holds x + y = y + x
proof
let x,y be Element of center R;
reconsider a = x, b = y as Element of R by Lm1;
thus x + y = a + b by Lm2
.= b + a
.= y + x by Lm2;
end;
hence thesis by RLVECT_1:def 2;
end;
cluster center R -> add-associative;
correctness
proof
for x,y,z being Element of center R
holds (x + y) + z = x + (y + z)
proof
let x,y,z be Element of center R;
reconsider a = x, b = y, c = z as Element of R by Lm1;
A1: y + z = b + c by Lm2;
x + y = a + b by Lm2;
hence (x + y) + z = (a + b) + c by Lm2
.= a + (b + c) by RLVECT_1:def 3
.= x + (y + z) by A1, Lm2;
end;
hence thesis by RLVECT_1:def 3;
end;
cluster center R -> right_zeroed;
correctness
proof
for v being Element of center R
holds v + 0.(center R) = v
proof
let v be Element of center R;
reconsider a = v as Element of R by Lm1;
0.(center R) = 0.R by Def4;
hence v + 0.(center R) = a + 0.R by Lm2
.= a by RLVECT_1:def 4
.= v;
end;
hence thesis by RLVECT_1:def 4;
end;
cluster center R -> associative;
correctness
proof
for x,y,z being Element of center R
holds (x * y) * z = x * (y * z)
proof
let x,y,z be Element of center R;
reconsider a = x, b = y, c = z as Element of R by Lm1;
A1: y * z = b * c by Lm2;
x * y = a * b by Lm2;
hence (x * y) * z = (a * b) * c by Lm2
.= a * (b * c) by GROUP_1:def 3
.= x * (y * z) by A1, Lm2;
end;
hence thesis;
end;
cluster center R -> well-unital;
correctness
proof
for x being Element of center R
holds x * 1.(center R) = x & (1.(center R)) * x = x
proof
let x be Element of center R;
reconsider a = x as Element of R by Lm1;
A1: 1.R = 1.(center R) by Def4;
hence x * 1.(center R) = a * 1.R by Lm2
.= a
.= x;
thus (1.(center R)) * x = (1.R) * a by A1, Lm2
.= a
.= x;
end;
hence thesis;
end;
cluster center R -> distributive;
correctness
proof
for x,y,z being Element of center R
holds x * (y + z) = x*y + x*z
& (y + z)*x = (y * x) + (z * x)
proof
let x,y,z be Element of center R;
reconsider a = x, b = y, c = z as Element of R by Lm1;
A1: b + c = y + z & a * b = x * y & a * c = x * z by Lm2;
hence x * (y + z) = a * (b + c) by Lm2
.= a * b + a * c by VECTSP_1:def 7
.= x*y + x*z by A1,Lm2;
A2: b + c = y + z & b*a = y*x & c*a = z*x by Lm2;
hence (y + z)*x = (b + c)*a by Lm2
.= b * a + c * a by VECTSP_1:def 7
.= (y * x) + (z * x) by A2,Lm2;
end;
hence thesis;
end;
end;
registration
let R be Skew-Field;
cluster center R -> non degenerated;
correctness
proof
1.R = 1.(center R) & 0.R = 0.(center R) by Def4;
hence thesis;
end;
cluster center R -> almost_left_invertible;
correctness
proof
for x being Element of center R st x <> 0.(center R)
holds x is left_invertible
proof
let x be Element of center R;
assume A1: x <> 0.(center R);
ex y being Element of center R st y * x = 1.(center R)
proof
reconsider a = x as Element of R by Lm1;
A2: 0.R = 0.(center R) by Def4;
then A3: a <> 0.R by A1;
then consider b being Element of R such that
A4: b * a = 1.R by ALGSTR_0:def 39,def 27;
A5: a in center R;
then A6: a * b = 1.R by A4, Lm3;
for s being Element of R holds b*s = s*b
proof
let s be Element of R;
(1.R) * s = s * (1.R);
then (a * b) * s = (s * a) * b by A6,GROUP_1:def 3
.= (a * s) * b by A5, Lm3;
then ((a ")*(a * b))*s = (a ")*((a * s) * b) by GROUP_1:def 3
.= ((a ")*(a * s))*b by GROUP_1:def 3
.= (((a ")*a) * s) * b by GROUP_1:def 3
.= ((1_R) * s) * b by A3, VECTSP_2:9
.= s * b;
hence s * b = ((a ")*(a * b))*s
.= (((a ") * a) * b)*s by GROUP_1:def 3
.= ((1_R) * b) * s by A3, VECTSP_2:9
.= b * s;
end;
then b in {x9 where x9 is Element of R:
for s being Element of R holds x9*s = s*x9};
then b in the carrier of center R by Def4;
then reconsider y = b as Element of center R;
take y;
thus y * x = b * a by Lm2
.= 1.R by A4
.= 1.(center R) by Def4;
end;
hence x is left_invertible by ALGSTR_0:def 27;
end;
hence thesis by ALGSTR_0:def 39;
end;
end;
theorem Th16: :: Center0:
for R being Ring holds the carrier of center R c= the carrier of R
proof
let R be Ring;
for x being object st x in the carrier of center R
holds x in the carrier of R
proof
let y be object;
assume y in the carrier of center R;
then
y in {x where x is Element of R: for s being Element of R holds x*s = s*x}
by Def4;
then ex x being Element of R st ( x = y)&( for s being Element
of R holds x*s = s*x);
hence thesis;
end;
hence thesis;
end;
registration
let R be finite Skew-Field;
cluster center R -> finite;
correctness
proof
the carrier of center R c= the carrier of R by Th16;
hence thesis;
end;
end;
theorem Th17: :: Center1:
for R being Ring, 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 Ring, y be Element of R;
hereby
assume y in center R;
then y in the carrier of center R;
then y in {x where x is Element of R:
for s being Element of R holds x*s = s*x} by Def4;
then ex x being Element of R st ( x = y)&( for s being Element
of R holds x*s=s*x);
hence for s being Element of R holds y*s = s*y;
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 Def4;
hence y in center R;
end;
hence thesis;
end;
theorem Th18: :: Center1a:
for R being Ring holds 0.R in center R
proof
let R be Ring;
for s being Element of R holds 0.R*s = s*0.R;
hence thesis by Th17;
end;
theorem Th19: :: Center1b:
for R being Ring holds 1_R in center R
proof
let R be Ring;
for s being Element of R holds (1_R)*s = s*(1_R);
hence thesis by Th17;
end;
theorem Th20: :: Center2:
for R being finite Skew-Field holds 1 < card (the carrier of center R)
proof
let R be finite Skew-Field;
A1: card {0.R, 1.R} = 2 by CARD_2:57;
0.R in center R by Th18;
then
A2: 0.R in the carrier of center R;
for s being Element of R holds (1.R)*s = s*(1.R);
then 1.R in center R by Th17;
then 1.R in the carrier of center R;
then {0.R, 1.R} c= the carrier of center R by A2,ZFMISC_1:32;
then 2 <= card the carrier of center R by A1,NAT_1:43;
hence thesis by XXREAL_0:2;
end;
theorem Th21: :: 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
A1: card X = card Y;
A2: Y c= X by Th16;
card (X \ Y) = card X - card X by A1,Th16,CARD_2:44;
then X \ Y = {};
then X c= Y by XBOOLE_1:37;
then
A3: X = Y by A2,XBOOLE_0:def 10;
for x being Element of X holds for s being Element of X holds x*s=s*x
by A3,STRUCT_0:def 5,Th17;
hence R is commutative;
end;
now
assume
A4: R is commutative;
for x being object st x in X holds x in Y
proof
let x be object such that
A5: 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 A4;
then x in center R by Th17;
hence thesis;
end;
then x is Element of Y by A5;
hence thesis;
end;
then
A6: X c= Y;
Y c= X by Th16;
hence card Y = card X by A6,XBOOLE_0:def 10;
end;
hence thesis;
end;
theorem Th22: :: 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;
A1: the carrier of center MultGroup R c= the carrier of MultGroup R
by GROUP_2:def 5;
A2: the carrier of MultGroup R = NonZero R by UNIROOTS:def 1;
A3: (the carrier of MultGroup R)\/ {0.R} = the carrier of R by UNIROOTS:15;
A4: the carrier of center R c= the carrier of R by Th16;
A5: (the carrier of center MultGroup R) \/ {0.R} c= the carrier of center R
proof
let x be object;
assume
A6: x in (the carrier of center MultGroup R) \/ {0.R};
per cases by A6,XBOOLE_0:def 3;
suppose
A7: x in the carrier of center MultGroup R;
then reconsider a = x as Element of MultGroup R by A1;
A8: a in center MultGroup R by A7;
reconsider a1 = a as Element of R by UNIROOTS:19;
now
let b be Element of R;
thus a1*b = b*a1
proof
per cases by A3,XBOOLE_0:def 3;
suppose b in (the carrier of MultGroup R);
then reconsider b1 = b as Element of MultGroup R;
thus a1*b = a*b1 by UNIROOTS:16
.= b1*a by A8,GROUP_5:77
.= b*a1 by UNIROOTS:16;
end;
suppose b in {0.R};
then
A9: b = 0.R by TARSKI:def 1;
hence a1*b = 0.R
.= b*a1 by A9;
end;
end;
end;
then a1 in center R by Th17;
hence thesis;
end;
suppose x in {0.R};
then x = 0.R by TARSKI:def 1;
then x in center R by Th18;
hence thesis;
end;
end;
the carrier of center R c= (the carrier of center MultGroup R) \/ {0.R}
proof
let x be object;
assume
A10: x in the carrier of center R;
then reconsider a = x as Element of center R;
reconsider a1 = a as Element of R by A4;
per cases;
suppose a1 = 0.R;
then a1 in {0.R} by TARSKI:def 1;
hence thesis by XBOOLE_0:def 3;
end;
suppose a1 <> 0.R;
then not a1 in {0.R} by TARSKI:def 1;
then reconsider a2 = a1 as Element of MultGroup R by A2,XBOOLE_0:def 5;
now
let b be Element of MultGroup R;
b in the carrier of MultGroup R;
then reconsider b1 = b as Element of R by A2;
A11: x in center R by A10;
thus a2*b=a1*b1 by UNIROOTS:16
.= b1*a1 by A11,Th17
.= b*a2 by UNIROOTS:16;
end;
then a1 in center MultGroup R by GROUP_5:77;
then a1 in the carrier of center MultGroup R;
hence thesis by XBOOLE_0:def 3;
end;
end;
hence thesis by A5,XBOOLE_0:def 10;
end;
definition
let R be Skew-Field, s be Element of R;
func centralizer s -> strict Skew-Field means
:Def5:
the carrier of it = {x where x is Element of R: x*s = s*x} &
the addF of it = (the addF of R)||the carrier of it &
the multF of it = (the multF of R)||the carrier of it & 0.it = 0.R &
1.it = 1.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 = s*(0.R);
then 0.R in ccs;
then reconsider ccs as non empty set;
A2: ccs c= cR
proof
let x be object;
assume x in ccs;
then ex x9 being Element of cR st x9=x & x9*s=s*x9;
hence thesis;
end;
set acs = (the addF of R)||ccs;
set mcs = (the multF of R)||ccs;
set Zs = 0.R;
set Us = 1.R;
A3: [:ccs,ccs:] c= [:cR,cR:]
proof
let x be object;
assume x in [:ccs,ccs:];
then ex a,b being object st ( a in ccs)&( b in ccs)&( x =[a,b]) by
ZFMISC_1:def 2;
hence thesis by A2,ZFMISC_1:def 2;
end;
then reconsider acs as Function of [:ccs,ccs:],cR by FUNCT_2:32;
rng acs c= ccs
proof
let y be object;
assume y in rng acs;
then consider x being object such that
A4: x in dom acs and
A5: y = acs.x by FUNCT_1:def 3;
consider a,b being object such that
A6: a in ccs and
A7: b in ccs and
A8: x = [a,b] by A4,ZFMISC_1:def 2;
reconsider a,b as Element of cR by A2,A6,A7;
A9: ex a9 being Element of cR st a9=a & a9*s=s*a9 by A6;
A10: ex b9 being Element of cR st b9=b & b9*s=s*b9 by A7;
[a,b] in [:ccs,ccs:] by A6,A7,ZFMISC_1:def 2;
then
A11: a+b = acs.x by A8,FUNCT_1:49;
(a+b)*s=s*a+s*b by A9,A10,VECTSP_1:def 3
.=s*(a+b) by VECTSP_1:def 2;
hence thesis by A5,A11;
end;
then reconsider acs as BinOp of ccs by FUNCT_2:6;
reconsider mcs as Function of [:ccs,ccs:],cR by A3,FUNCT_2:32;
rng mcs c= ccs
proof
let y be object;
assume y in rng mcs;
then consider x being object such that
A12: x in dom mcs and
A13: y = mcs.x by FUNCT_1:def 3;
consider a,b being object such that
A14: a in ccs and
A15: b in ccs and
A16: x = [a,b] by A12,ZFMISC_1:def 2;
reconsider a,b as Element of cR by A2,A14,A15;
A17: ex a9 being Element of cR st a9=a & a9*s=s*a9 by A14;
A18: ex b9 being Element of cR st b9=b & b9*s=s*b9 by A15;
[a,b] in [:ccs,ccs:] by A14,A15,ZFMISC_1:def 2;
then
A19: a*b = mcs.x by A16,FUNCT_1:49;
(a*b)*s=a*(s*b) by A18,GROUP_1:def 3
.= (a*s)*b by GROUP_1:def 3
.= s*(a*b) by A17,GROUP_1:def 3;
hence thesis by A13,A19;
end;
then reconsider mcs as BinOp of ccs by FUNCT_2:6;
(0.R)*s = s*(0.R);
then Zs in ccs;
then reconsider Zs as Element of ccs;
(1.R)*s = s
.= s*(1.R);
then Us in ccs;
then reconsider Us as Element of ccs;
reconsider cs = doubleLoopStr (# ccs, acs, mcs, Us, Zs #)
as non empty doubleLoopStr;
A20: now
let x, e be Element of cs;
assume
A21: e = 1.R;
A22: [x,e] in [:ccs,ccs:] by ZFMISC_1:87;
A23: [e,x] in [:ccs,ccs:] by ZFMISC_1:87;
reconsider y=x as Element of R by A2;
thus x*e = y*1.R by A21,A22,FUNCT_1:49
.= x;
thus e*x = 1.R*y by A21,A23,FUNCT_1:49
.= x;
end;
A24: cs is well-unital by A20;
set ccs1 = the carrier of cs;
A25: now
let x be Element of cR;
assume x in ccs;
then ex x9 being Element of cR st x9=x & x9*s = s*x9;
hence x*s=s*x;
end;
A26: now
let a,b be Element of cR, c,d be Element of ccs1 such that
A27: a=c and
A28: b=d;
[c,d] in [:ccs,ccs:] by ZFMISC_1:def 2;
hence a*b= c*d by A27,A28,FUNCT_1:49;
end;
A29: for a,b being Element of cR, c,d be Element of ccs1 st a=c & b=d
holds a+b = c+d
proof
let a,b being Element of cR, c,d be Element of ccs1 such that
A30: a=c and
A31: b=d;
[c,d] in [:ccs,ccs:] by ZFMISC_1:def 2;
hence thesis by A30,A31,FUNCT_1:49;
end;
A32: cs is Abelian
proof
let x,y be Element of ccs1;
reconsider x9=x,y9=y as Element of cR by A2;
thus x+y = y9+x9 by A29
.= y+x by A29;
end;
A33: cs is add-associative
proof
let x,y,z be Element of ccs1;
reconsider x9=x,y9=y,z9=z as Element of cR by A2;
A34: x9+y9=x+y by A29;
A35: y9+z9=y+z by A29;
thus (x+y)+z = (x9+y9)+z9 by A29,A34
.= x9+(y9+z9) by RLVECT_1:def 3
.= x+(y+z) by A29,A35;
end;
A36: cs is right_zeroed
proof
let x be Element of ccs1;
reconsider x9=x as Element of cR by A2;
thus x + 0.cs = x9+0.R by A29
.= x by RLVECT_1:def 4;
end;
A37: cs is right_complementable
proof
let x be Element of ccs1;
reconsider x9=x as Element of cR by A2;
consider y9 being Element of cR such that
A38: x9 + y9 = 0.R by ALGSTR_0:def 11;
A39: s*x9=x9*s by A25;
0.R*s = s*0.R;
then x9*s+y9*s=s*(x9+y9) by A38,VECTSP_1:def 3;
then x9*s+y9*s=s*x9+s*y9 by VECTSP_1:def 2;
then (-(x9*s)+x9*s)+y9*s=-(s*x9)+(s*x9+s*y9) by A39,RLVECT_1:def 3;
then 0.R+y9*s=-(s*x9)+(s*x9+s*y9) by RLVECT_1:5;
then y9*s=-(s*x9)+(s*x9+s*y9) by RLVECT_1:4;
then y9*s=(-(s*x9)+s*x9)+s*y9 by RLVECT_1:def 3;
then y9*s=0.R+s*y9 by RLVECT_1:5;
then y9*s=s*y9 by RLVECT_1:4;
then y9 in ccs1;
then reconsider y=y9 as Element of ccs1;
x9+y9=x+y by A29;
hence ex y being Element of ccs1 st x + y = 0.cs by A38;
end;
A40: cs is associative
proof
let x,y,z be Element of ccs1;
reconsider x9=x,y9=y,z9=z as Element of cR by A2;
A41: x9*y9=x*y by A26;
A42: y9*z9=y*z by A26;
thus (x*y)*z = (x9*y9)*z9 by A26,A41
.= x9*(y9*z9) by GROUP_1:def 3
.= x*(y*z) by A26,A42;
end;
A43: cs is distributive
proof
let x,y,z be Element of ccs1;
reconsider x9=x,y9=y,z9=z as Element of cR by A2;
A44: y+z=y9+z9 by A29;
A45: x9*y9=x*y by A26;
A46: x9*z9=x*z by A26;
A47: y9*x9=y*x by A26;
A48: z9*x9=z*x by A26;
thus x*(y+z) = x9*(y9+z9) by A26,A44
.= x9*y9+x9*z9 by VECTSP_1:def 7
.= x*y+x*z by A29,A45,A46;
thus (y+z)*x = (y9+z9)*x9 by A26,A44
.= y9*x9+z9*x9 by VECTSP_1:def 7
.= y*x+z*x by A29,A47,A48;
end;
A49: cs is almost_left_invertible
proof
let x be Element of ccs1 such that
A50: x <> 0.cs;
reconsider x9=x as Element of cR by A2;
consider y9 being Element of cR such that
A51: y9*x9=1.R by A50,VECTSP_1:def 9;
A52: x9*y9=1.R by A51,VECTSP_2:7;
(1.R)*s = s
.= s*(1.R);
then x9*y9*s = (s*x9)*y9 by A52,GROUP_1:def 3;
then x9*y9*s = x9*s*y9 by A25;
then x9"*(x9*y9)*s = x9"*(x9*s*y9) by GROUP_1:def 3;
then x9"*(x9*y9)*s = x9"*(x9*s)*y9 by GROUP_1:def 3;
then x9"*x9*y9*s = x9"*(x9*s)*y9 by GROUP_1:def 3;
then x9"*x9*y9*s = x9"*x9*s*y9 by GROUP_1:def 3;
then (1_R)*y9*s = x9"*x9*s*y9 by A50,VECTSP_2:9;
then (1_R)*y9*s = (1_R)*s*y9 by A50,VECTSP_2:9;
then y9*s = (1_R)*s*y9;
then y9*s=s*y9;
then y9 in ccs1;
then reconsider y=y9 as Element of ccs1;
take y;
thus thesis by A26,A51;
end;
cs is non degenerated;
hence thesis by A24,A32,A33,A36,A37,A40,A43,A49;
end;
uniqueness;
end;
theorem Th23: :: 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;
A1: ccs = {x where x is Element of R: x*s = s*x} by Def5;
let x be object;
assume x in the carrier of centralizer s;
then ex a being Element of R st a=x & a*s=s*a by A1;
hence thesis;
end;
theorem Th24: :: 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;
A1: ccs = {x where x is Element of R: x*s = s*x} by Def5;
hereby
assume a in the carrier of centralizer s;
then ex x being Element of R st a=x & x*s=s*x by A1;
hence a*s = s*a;
end;
assume a*s = s*a;
hence thesis by A1;
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 object;
assume
A1: x in the carrier of center R;
the carrier of center R c= the carrier of R by Th16;
then reconsider a = x as Element of R by A1;
a in center R by A1;
then a*s=s*a by Th17;
hence thesis by Th24;
end;
theorem Th26: :: 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
A1: a in the carrier of center R and
A2: b in the carrier of centralizer s;
set cs = centralizer s;
set ccs = the carrier of cs;
A3: ccs = {x where x is Element of R: x*s = s*x} by Def5;
A4: a in center R by A1;
a*b*s=a*(b*s) by GROUP_1:def 3
.= (b*s)*a by A4,Th17
.= (s*b)*a by A2,Th24
.= s*(b*a) by GROUP_1:def 3
.= s*(a*b) by A4,Th17;
hence thesis by A3;
end;
theorem Th27: :: 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;
A1: 0.R = 0.centralizer s by Def5;
1.centralizer s = 1_R by Def5;
hence thesis by A1;
end;
registration
let R be finite Skew-Field;
let s be Element of R;
cluster centralizer s -> finite;
correctness by Th23,FINSET_1:1;
end;
theorem Th28: :: 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;
A1: card {0.R, 1.R} = 2 by CARD_2:57;
A2: 0.R is Element of centralizer s by Th27;
1_R is Element of centralizer s by Th27;
then {0.R, 1_R} c= the carrier of centralizer s by A2,ZFMISC_1:32;
then 2 <= card the carrier of centralizer s by A1,NAT_1:43;
hence thesis by XXREAL_0:2;
end;
theorem Th29: :: 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
A1: t = s;
set ct = Centralizer t, cs = centralizer s;
set cct = the carrier of ct, ccs = the carrier of cs;
A2: the carrier of MultGroup R = NonZero R by UNIROOTS:def 1;
A3: cct = { b where b is Element of MultGroup R : t*b = b*t } by Def1;
A4: ccs = {x where x is Element of R: x*s = s*x} by Def5;
now
let x be object;
hereby
assume x in ccs;
then consider c being Element of R such that
A5: c = x and
A6: c*s=s*c by A4;
per cases;
suppose c = 0.R;
then c in {0.R} by TARSKI:def 1;
hence x in cct \/ {0.R} by A5,XBOOLE_0:def 3;
end;
suppose c <> 0.R;
then not c in {0.R} by TARSKI:def 1;
then reconsider c1 = c as Element of MultGroup R by A2,XBOOLE_0:def 5;
t*c1 = s*c by A1,UNIROOTS:16
.= c1*t by A1,A6,UNIROOTS:16;
then c in cct by A3;
hence x in cct \/ {0.R} by A5,XBOOLE_0:def 3;
end;
end;
assume
A7: x in cct \/ {0.R};
per cases by A7,XBOOLE_0:def 3;
suppose x in cct;
then consider b being Element of MultGroup R such that
A8: x = b and
A9: t*b = b*t by A3;
reconsider b1 = b as Element of R by UNIROOTS:19;
b1*s = t*b by A1,A9,UNIROOTS:16
.= s*b1 by A1,UNIROOTS:16;
hence x in ccs by A4,A8;
end;
suppose x in {0.R};
then
A10: x = 0.R by TARSKI:def 1;
0.R*s = s*0.R;
hence x in ccs by A4,A10;
end;
end;
hence thesis by TARSKI:2;
end;
theorem Th30: :: Central2:
for R being finite Skew-Field, s being Element of R,
t being Element of MultGroup R st t = s
holds card 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
A1: 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 = NonZero R by UNIROOTS:def 1;
then not 0.R in the carrier of MultGroup R by ZFMISC_1:56;
then not 0.R in MultGroup R;
then not 0.R in ct by Th7;
then
A2: not 0.R in cct;
cct \/ {0.R} = ccs by A1,Th29;
then card ccs = card cct +1 by A2,CARD_2:41;
hence thesis;
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
:Def6:
the addLoopStr of it = the addLoopStr of R &
the lmult of it = (the multF 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 multF of R)|[:ccR, ccs:];
A1: ccR c= the carrier of R by Th16;
A2: dom (the multF 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 object;
assume x in [:ccR, ccs:];
then ex x1, x2 being object st ( x1 in ccR)&( x2 in ccs)&( x = [x1,
x2]) by ZFMISC_1:def 2;
hence thesis by A1,ZFMISC_1:def 2;
end;
then
A3: dom lm = [:ccR, ccs:] by A2,RELAT_1:62;
now
let x be object;
assume
A4: x in [:ccR, ccs:];
then consider x1, x2 being object such that
A5: x1 in ccR and
A6: x2 in ccs and
A7: x = [x1,x2] by ZFMISC_1:def 2;
reconsider x1 as Element of R by A1,A5;
reconsider x2 as Element of R by A6;
lm.x = x1*x2 by A4,A7,FUNCT_1:49;
hence lm.x in ccs;
end;
then reconsider lm as Function of [:ccR,ccs:], ccs by A3,FUNCT_2:3;
set Vos = ModuleStr(# ccs, the addF of R, 0.R, lm #);
set cV = the carrier of Vos;
A8: Vos is vector-distributive scalar-distributive scalar-associative
scalar-unital
proof
A9: the multF of cR = (the multF of R)||ccR by Def4;
A10: the addF of cR = (the addF of R)||ccR by Def4;
thus Vos is vector-distributive
proof
let x be Element of ccR, v,w be Element of cV;
reconsider xx=x as Element of R by A1;
reconsider vv=v, ww=w as Element of R;
A11: [x,w] in [:ccR,ccs:] by ZFMISC_1:def 2;
A12: [x,v+w] in [:ccR,ccs:] by ZFMISC_1:def 2;
A13: [x,v] in [:ccR,ccs:] by ZFMISC_1:def 2;
thus x*(v+w) = xx*(vv+ww) by A12,FUNCT_1:49
.= xx*vv+xx*ww by VECTSP_1:def 2
.= (the addF of R).[x*v,(the multF of R).[xx,ww]] by A13,FUNCT_1:49
.= x*v+x*w by A11,FUNCT_1:49;
end;
thus Vos is scalar-distributive
proof
let x,y be Element of ccR, v be Element of cV;
reconsider xx=x, yy=y as Element of R by A1;
reconsider vv=v as Element of R;
A14: [y,v] in [:ccR,ccs:] by ZFMISC_1:def 2;
A15: [x,v] in [:ccR,ccs:] by ZFMISC_1:def 2;
A16: [x+y,v] in [:ccR,ccs:] by ZFMISC_1:def 2;
A17: [x,y] in [:ccR,ccR:] by ZFMISC_1:def 2;
thus (x+y)*v =
(the multF of R).[(the addF of cR).[x,y],vv] by A16,FUNCT_1:49
.= (xx+yy)*vv by A10,A17,FUNCT_1:49
.= xx*vv+yy*vv by VECTSP_1:def 3
.= (the addF of R).[x*v,(the multF of R).[yy,vv]] by A15,FUNCT_1:49
.= x*v+y*v by A14,FUNCT_1:49;
end;
thus Vos is scalar-associative
proof
let x,y be Element of ccR, v be Element of cV;
reconsider xx=x, yy=y as Element of R by A1;
reconsider vv=v as Element of R;
A18: [x,y*v] in [:ccR,ccs:] by ZFMISC_1:def 2;
A19: [y,v] in [:ccR,ccs:] by ZFMISC_1:def 2;
A20: [x*y,v] in [:ccR,ccs:] by ZFMISC_1:def 2;
A21: [x,y] in [:ccR,ccR:] by ZFMISC_1:def 2;
thus (x*y)*v =
(the multF of R).[(the multF of cR).(x,y),vv] by A20,FUNCT_1:49
.= xx*yy*vv by A9,A21,FUNCT_1:49
.= xx*(yy*vv) by GROUP_1:def 3
.= (the multF of R).[xx,lm.(y,v)] by A19,FUNCT_1:49
.= x*(y*v) by A18,FUNCT_1:49;
end;
let v be Element of cV;
reconsider vv=v as Element of R;
1_R in center R by Th19;
then 1_R in ccR;
then
A22: [1_ R,vv] in [:ccR, ccs:] by ZFMISC_1:def 2;
thus (1.cR)*v = lm.(1.R,vv) by Def4
.= (1.R)*vv by A22,FUNCT_1:49
.= v;
end;
A23: 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 = uu+vv+ww .= uu+(vv+ww) by RLVECT_1:def 3
.= u + (v + w);
end;
A24: Vos is right_zeroed
proof
let v be Element of cV;
reconsider vv = v as Element of ccs;
thus v + 0.Vos = vv+0.R .= v by RLVECT_1:def 4;
end;
A25: 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
A26: vv + ww = 0.R by ALGSTR_0:def 11;
reconsider w = ww as Element of cV;
v+w = 0.Vos by A26;
hence ex w being Element of cV st v + w = 0.Vos;
end;
Vos is Abelian
proof
let v,w be Element of cV;
reconsider vv = v, ww = w as Element of ccs;
thus v+w = ww + vv by RLVECT_1:2
.= w+v;
end;
hence thesis by A8,A23,A24,A25;
end;
uniqueness;
end;
theorem Th31: :: 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 vR = VectSp_over_center R;
A1: the addLoopStr of vR = the addLoopStr of R by Def6;
set B = the Basis of vR;
B is finite by A1;
then vR is finite-dimensional by MATRLIN:def 1;
hence thesis by A1,Th15;
end;
theorem Th32: :: 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 R = q |^ n by Th31;
then
A1: card Rs = (q |^ n) - 1 by UNIROOTS:18;
now
assume
A2: n = 0;
q |^ n = q #Z n by PREPOWER:36;
then card Rs = 1 - 1 by A1,A2,PREPOWER:34;
hence contradiction by GROUP_1:45;
end;
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
:Def7:
the addLoopStr of it = the addLoopStr of centralizer s &
the lmult of it = (the multF 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 multF of R)|[:ccR, ccs:];
A1: ccR c= the carrier of R by Th16;
A2: ccs c= the carrier of R by Th23;
A3: dom (the multF 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 object;
assume x in [:ccR, ccs:];
then ex x1, x2 being object st ( x1 in ccR)&( x2 in ccs)&( x = [x1,
x2]) by ZFMISC_1:def 2;
hence thesis by A1,A2,ZFMISC_1:def 2;
end;
then
A4: dom lm = [:ccR, ccs:] by A3,RELAT_1:62;
now
let x be object;
assume
A5: x in [:ccR, ccs:];
then consider x1, x2 being object such that
A6: x1 in ccR and
A7: x2 in ccs and
A8: x = [x1,x2] by ZFMISC_1:def 2;
reconsider x1 as Element of R by A1,A6;
reconsider x2 as Element of R by A2,A7;
lm.x = x1*x2 by A5,A8,FUNCT_1:49;
hence lm.x in ccs by A6,A7,Th26;
end;
then reconsider lm as Function of [:ccR,ccs:], ccs by A4,FUNCT_2:3;
set Vos = ModuleStr(#
the carrier of centralizer s, the addF of centralizer s,
0.centralizer s, lm #);
set cV = the carrier of Vos;
set aV = the addF of Vos;
A9: Vos is vector-distributive scalar-distributive scalar-associative
scalar-unital
proof
A10: the multF of cR = (the multF of R)||ccR by Def4;
A11: the addF of cR = (the addF of R)||ccR by Def4;
A12: the addF of cs = (the addF of R)||ccs by Def5;
thus Vos is vector-distributive
proof
let x be Element of ccR, v,w be Element of cV;
reconsider xx=x as Element of R by A1;
reconsider vv=v, ww=w as Element of R by A2;
A13: [x,w] in [:ccR,ccs:] by ZFMISC_1:def 2;
A14: [x,v+w] in [:ccR,ccs:] by ZFMISC_1:def 2;
A15: [v,w] in [:ccs,ccs:] by ZFMISC_1:def 2;
A16: [x,v] in [:ccR,ccs:] by ZFMISC_1:def 2;
A17: [x*v,x*w] in [:ccs,ccs:] by ZFMISC_1:def 2;
thus x*(v+w) = (the multF of R).[x,aV.[v,w]] by A14,FUNCT_1:49
.= xx*(vv+ww) by A12,A15,FUNCT_1:49
.= xx*vv+xx*ww by VECTSP_1:def 2
.= (the addF of R).[x*v,(the multF of R).[xx,ww]] by A16,FUNCT_1:49
.= (the addF of R).[x*v,x*w] by A13,FUNCT_1:49
.= x*v+x*w by A12,A17,FUNCT_1:49;
end;
thus Vos is scalar-distributive
proof
let x,y be Element of ccR, v be Element of cV;
reconsider xx=x, yy=y as Element of R by A1;
reconsider vv=v as Element of R by A2;
A18: [y,v] in [:ccR,ccs:] by ZFMISC_1:def 2;
A19: [x,v] in [:ccR,ccs:] by ZFMISC_1:def 2;
A20: [x+y,v] in [:ccR,ccs:] by ZFMISC_1:def 2;
A21: [x,y] in [:ccR,ccR:] by ZFMISC_1:def 2;
A22: [x*v,y*v] in [:ccs,ccs:] by ZFMISC_1:def 2;
thus (x+y)*v =
(the multF of R).[(the addF of cR).[x,y],vv] by A20,FUNCT_1:49
.= (xx+yy)*vv by A11,A21,FUNCT_1:49
.= xx*vv+yy*vv by VECTSP_1:def 3
.= (the addF of R).[x*v,(the multF of R).[yy,vv]] by A19,FUNCT_1:49
.= (the addF of R).[x*v,lm.(y,v)] by A18,FUNCT_1:49
.= x*v+y*v by A12,A22,FUNCT_1:49;
end;
thus Vos is scalar-associative
proof
let x,y be Element of ccR, v be Element of cV;
reconsider xx=x, yy=y as Element of R by A1;
reconsider vv=v as Element of R by A2;
A23: [x,y*v] in [:ccR,ccs:] by ZFMISC_1:def 2;
A24: [y,v] in [:ccR,ccs:] by ZFMISC_1:def 2;
A25: [x*y,v] in [:ccR,ccs:] by ZFMISC_1:def 2;
A26: [x,y] in [:ccR,ccR:] by ZFMISC_1:def 2;
thus (x*y)*v =
(the multF of R).[(the multF of cR).(x,y),vv] by A25,FUNCT_1:49
.= xx*yy*vv by A10,A26,FUNCT_1:49
.= xx*(yy*vv) by GROUP_1:def 3
.= (the multF of R).[xx,lm.(y,v)] by A24,FUNCT_1:49
.= x*(y*v) by A23,FUNCT_1:49;
end;
let v be Element of cV;
reconsider vv=v as Element of R by A2;
1_R in center R by Th19;
then 1_R in ccR;
then
A27: [1_R,vv] in [:ccR, ccs:] by ZFMISC_1:def 2;
thus (1.cR)*v = lm.(1.R,vv) by Def4
.= (1.R)*vv by A27,FUNCT_1:49
.= v;
end;
A28: 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 = uu+vv+ww .= uu+(vv+ww) by RLVECT_1:def 3
.= u + (v + w);
end;
A29: Vos is right_zeroed
proof
let v be Element of cV;
reconsider vv = v as Element of ccs;
thus v + 0.Vos = vv+0.cs .= v by RLVECT_1:def 4;
end;
A30: 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
A31: vv + ww = 0.cs by ALGSTR_0:def 11;
reconsider w = ww as Element of cV;
v+w = 0.Vos by A31;
hence ex w being Element of cV st v + w = 0.Vos;
end;
Vos is Abelian
proof
let v,w be Element of cV;
reconsider vv = v, ww = w as Element of ccs;
thus v+w = ww + vv by RLVECT_1:2
.= w+v;
end;
hence thesis by A9,A28,A29,A30;
end;
uniqueness;
end;
theorem Th33: :: 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 vR = VectSp_over_center s;
A1: the addLoopStr of vR = the addLoopStr of centralizer s by Def7;
set B = the Basis of vR;
B is finite by A1;
then vR is finite-dimensional by MATRLIN:def 1;
hence thesis by A1,Th15;
end;
theorem Th34: :: 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;
now
assume
A1: ns = 0;
q |^ ns = q #Z ns by PREPOWER:36;
then q |^ ns = 1 by A1,PREPOWER:34;
then card the carrier of centralizer s = 1 by Th33;
hence contradiction by Th28;
end;
hence thesis;
end;
theorem Th35: :: 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
A1: 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;
reconsider s=r as Element of MultGroup R by A1;
card R = q |^ n by Th31;
then card G = (q |^ n) - 1 by UNIROOTS:18;
then q |^ n - 1 = card con_class s * card Centralizer s by Th13;
then card Centralizer s divides (q |^ n - 1) by INT_1:def 3;
then (qr - 1) divides (q |^ n -1) by Th30;
hence thesis by Th33;
end;
theorem Th36: :: 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
A1: s is Element of MultGroup R;
set n = dim VectSp_over_center R;
set ns= dim VectSp_over_center s;
set q = card the carrier of center R;
A2: n in NAT by ORDINAL1:def 12;
A3: ns in NAT by ORDINAL1:def 12;
A4: 0 < ns by Th34;
A5: 1 < q by Th20;
0 < q |^ ns by PREPOWER:6;
then 0+1 < q |^ ns + 1 by XREAL_1:8;
then
A6: 1 <= q |^ ns by NAT_1:13;
0 < q |^ n by PREPOWER:6;
then 0+1 < q |^ n + 1 by XREAL_1:8;
then 1 <= q |^ n by NAT_1:13;
then
A7: (q |^ n - 1) = (q |^ n -' 1) by XREAL_1:233;
(q |^ ns - 1) = (q |^ ns -' 1) by A6,XREAL_1:233;
hence thesis by A1,A2,A3,A4,A5,A7,Th3,Th35;
end;
theorem Th37: :: 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;
A1: the carrier of MultGroup R = NonZero R by UNIROOTS:def 1;
the carrier of center MultGroup R c= the carrier of MultGroup R
by GROUP_2:def 5;
then
A2: not 0.R in the carrier of center MultGroup R by A1,ZFMISC_1:56;
the carrier of center R = (the carrier of center MultGroup R) \/ {0.R}
by Th22;
then card the carrier of center R = card (the carrier of center MultGroup
R) + 1 by A2,CARD_2:41;
hence thesis;
end;
begin :: Witt's proof of Wedderburn's theorem
::$N Wedderburn Theorem
theorem
for R being finite Skew-Field holds R is commutative
proof
let R be finite Skew-Field such that
A1: 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;
A2: card R = q |^ n by Th31;
then
A3: card Rs = (q |^ n) - 1 by UNIROOTS:18;
A4: 1 < q by Th20;
A5: 1+-1 < q + -1 by Th20,XREAL_1:8;
then reconsider natq1 = q - 1 as Element of NAT by INT_1:3;
0+1 < n + 1 by Th32,XREAL_1:8;
then
A6: 1 <= n by NAT_1:13;
n <> 1 by A2,A1,Th21;
then
A8: 1 < n by A6,XXREAL_0:1;
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 object st x in A holds x in conjugate_Classes Rs
proof
let x be object;
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
A9: A c= conjugate_Classes Rs;
then
A10: conjugate_Classes Rs = A \/ B by XBOOLE_1:45;
consider f being Function such that
A11: dom f = cZs and
A12: for x being object st x in cZs holds f.x = {x} from FUNCT_1:sch 3;
A13: f is one-to-one
proof
let x1,x2 be object;
assume that
A14: x1 in dom f and
A15: x2 in dom f and
A16: f.x1 = f.x2;
A17: f.x1 = {x1} by A11,A12,A14;
f.x2 = {x2} by A11,A12,A15;
hence thesis by A16,A17,ZFMISC_1:3;
end;
now
let x be object;
hereby
assume x in rng f;
then consider xx being object such that
A18: xx in dom f and
A19: x = f.xx by FUNCT_1:def 3;
A20: x = {xx} by A11,A12,A18,A19;
A21: cZs c= cRs by GROUP_2:def 5;
then reconsider X = x as Subset of cRs by A11,A18,A20,ZFMISC_1:31;
reconsider xx as Element of Rs by A11,A18,A21;
xx in center Rs by A11,A18;
then con_class xx = {xx} by GROUP_5:81;
then
A22: X in conjugate_Classes Rs by A20;
card X = 1 by A20,CARD_1:30;
hence x in A by A22;
end;
assume x in A;
then consider X being Subset of cRs such that
A23: x = X and
A24: X in conjugate_Classes Rs and
A25: card X = 1;
consider a being Element of cRs such that
A26: con_class a = X by A24;
A27: a in con_class a by GROUP_3:83;
consider xx being object such that
A28: X = {xx} by A25,CARD_2:42;
A29: a = xx by A26,A27,A28,TARSKI:def 1;
then a in center Rs by A26,A28,GROUP_5:81;
then
A30: a in cZs;
then f.a = {a} by A12;
hence x in rng f by A11,A23,A28,A29,A30,FUNCT_1:3;
end;
then rng f = A by TARSKI:2;
then
A31: A, cZs are_equipotent by A11,A13,WELLORD2:def 4;
card cZs = natq1 by Th37;
then
A32: card A = natq1 by A31,CARD_1:5;
consider f1 being FinSequence such that
A33: rng f1 = A and
A34: f1 is one-to-one by A9,FINSEQ_4:58;
consider f2 being FinSequence such that
A35: rng f2 = B and
A36: f2 is one-to-one by FINSEQ_4:58;
set f = f1^f2;
A37: rng f = conjugate_Classes Rs by A10,A33,A35,FINSEQ_1:31;
now
given x being object such that
A38: x in A /\ B;
A39: x in A by A38,XBOOLE_0:def 4;
x in B by A38,XBOOLE_0:def 4;
hence contradiction by A39,XBOOLE_0:def 5;
end;
then A /\ B = {} by XBOOLE_0:def 1;
then rng f1 misses rng f2 by A33,A35,XBOOLE_0:def 7;
then
A40: f is one-to-one FinSequence of conjugate_Classes Rs
by A34,A36,A37,FINSEQ_1:def 4,FINSEQ_3:91;
deffunc F(set) = card(f1.$1);
consider p1 being FinSequence such that
A41: len p1 = len f1 & for i being Nat st i in dom p1 holds p1.i = F(i)
from FINSEQ_1:sch 2;
for x being object st x in rng p1 holds x in NAT
proof
let x be object;
assume x in rng p1;
then consider i being Nat such that
A42: i in dom p1 and
A43: p1.i = x by FINSEQ_2:10;
A44: x = card(f1.i) by A41,A42,A43;
i in dom f1 by A41,A42,FINSEQ_3:29;
then f1.i in A by A33,FUNCT_1:3;
then ex X being Subset of cRs st ( f1.i = X)&( X in
conjugate_Classes Rs)&( card X = 1);
hence thesis by A44;
end;
then rng p1 c= NAT;
then reconsider c1=p1 as FinSequence of NAT by FINSEQ_1:def 4;
A45: len c1 = natq1 by A32,A33,A34,A41,FINSEQ_4:62;
A46: for i being Element of NAT st i in dom c1 holds c1.i = 1
proof
let i be Element of NAT such that
A47: i in dom c1;
i in dom f1 by A41,A47,FINSEQ_3:29;
then f1.i in A by A33,FUNCT_1:3;
then ex X being Subset of cRs
st f1.i = X & X in conjugate_Classes Rs & card X = 1;
hence thesis by A41,A47;
end;
for x being object st x in rng c1 holds x in {1}
proof
let x be object;
assume x in rng c1;
then ex i being Nat st ( i in dom c1)&( x = c1.i) by FINSEQ_2:10;
then x = 1 by A46;
hence thesis by TARSKI:def 1;
end;
then
A48: rng c1 c= {1};
for x being object st x in {1} holds x in rng c1
proof
let x be object such that
A49: x in {1};
A50: Seg len c1 = dom c1 by FINSEQ_1:def 3;
then c1.(len c1) = 1 by A5,A45,A46,FINSEQ_1:3;
then c1.(len c1) = x by A49,TARSKI:def 1;
hence thesis by A5,A45,A50,FINSEQ_1:3,FUNCT_1:3;
end;
then {1}c= rng c1;
then rng c1={1} by A48,XBOOLE_0:def 10;
then c1 = (dom c1) --> 1 by FUNCOP_1:9;
then c1 = Seg (len c1) --> 1 by FINSEQ_1:def 3;
then c1 = (len c1) |-> 1 by FINSEQ_2:def 2;
then Sum c1 = (len c1)*1 by RVSUM_1:80;
then
A51: Sum c1 = natq1 by A32,A33,A34,A41,FINSEQ_4:62;
deffunc P2(set) = card(f2.$1);
consider p2 being FinSequence such that
A52: len p2 = len f2 & for i being Nat st i in dom p2 holds p2.i = P2(i)
from FINSEQ_1:sch 2;
for x being object st x in rng p2 holds x in NAT
proof
let x be object;
assume x in rng p2;
then consider i being Nat such that
A53: i in dom p2 and
A54: p2.i = x by FINSEQ_2:10;
A55: x = card(f2.i) by A52,A53,A54;
i in dom f2 by A52,A53,FINSEQ_3:29;
then f2.i in conjugate_Classes Rs \ A by A35,FUNCT_1:3;
then f2.i in conjugate_Classes Rs by XBOOLE_0:def 5;
then consider a being Element of cRs such that
A56: con_class a = f2.i;
card con_class a is Element of NAT;
hence thesis by A55,A56;
end;
then rng p2 c= NAT;
then reconsider c2=p2 as FinSequence of NAT by FINSEQ_1:def 4;
set c = c1^c2;
reconsider c as FinSequence of NAT;
len c = len f1 + len f2 by A41,A52,FINSEQ_1:22;
then
A57: len c = len f by FINSEQ_1:22;
for i being Element of NAT st i in dom c holds c.i = card (f.i)
proof
let i be Element of NAT such that
A58: i in dom c;
now per cases by A58,FINSEQ_1:25;
suppose
A59: i in dom c1;
then
A60: i in dom f1 by A41,FINSEQ_3:29;
c.i = c1.i by A59,FINSEQ_1:def 7
.= card(f1.i) by A41,A59
.= card(f.i) by A60,FINSEQ_1:def 7;
hence thesis;
end;
suppose ex j being Nat st j in dom c2 & i = len c1 + j;
then consider j being Nat such that
A61: j in dom c2 and
A62: i = len c1 + j;
A63: j in dom f2 by A52,A61,FINSEQ_3:29;
c.i = c2.j by A61,A62,FINSEQ_1:def 7
.= card(f2.j) by A52,A61
.= card(f.i) by A41,A62,A63,FINSEQ_1:def 7;
hence thesis;
end;
end;
hence thesis;
end;
then card Rs = Sum c by A37,A40,A57,Th6;
then
A64: (q |^ n) - 1 = Sum c2 + (q - 1) by A3,A51,RVSUM_1:75;
reconsider q as non zero Element of NAT;
reconsider n as non zero Element of NAT by Th32,ORDINAL1:def 12;
q in COMPLEX by XCMPLX_0:def 2;
then reconsider qc=q as Element of F_Complex by COMPLFLD:def 1;
set pnq = eval(cyclotomic_poly n,qc);
reconsider pnq as Integer by UNIROOTS:52;
reconsider abspnq = |.pnq.| as Element of NAT;
(q |^ n) <> 0 by PREPOWER:5;
then (q |^ n)+1 > 0+1 by XREAL_1:8;
then (q |^ n) >= 1 by NAT_1:13;
then (q |^ n) +- 1 >= 1 +- 1 by XREAL_1:7;
then reconsider qn1=((q |^ n) - 1) as Element of NAT by INT_1:3;
pnq divides (q |^ n) - 1 by UNIROOTS:58;
then abspnq divides |.(q |^ n) - 1 .| by INT_2:16;
then
A65: abspnq divides qn1 by ABSVALUE:def 1;
for i being Element of NAT st i in dom c2 holds abspnq divides c2/.i
proof
let i be Element of NAT such that
A66: i in dom c2;
c2.i = card (f2.i) by A52,A66;
then
A67: c2/.i = card (f2.i) by A66,PARTFUN1:def 6;
A68: i in dom f2 by A52,A66,FINSEQ_3:29;
then f2.i in conjugate_Classes Rs \ A by A35,FUNCT_1:3;
then f2.i in conjugate_Classes Rs by XBOOLE_0:def 5;
then consider a being Element of cRs such that
A69: con_class a = f2.i;
reconsider a as Element of Rs;
reconsider s=a as Element of R by UNIROOTS:19;
set ns = dim VectSp_over_center s;
set ca = card con_class a;
set oa = card Centralizer a;
A70: card Rs = ca * oa + 0 by Th13;
then
A71: (card Rs) div oa = ca;
A72: qn1 div oa = ca by A3,A70;
(q |^ ns) <> 0 by PREPOWER:5;
then (q |^ ns)+1 > 0+1 by XREAL_1:8;
then (q |^ ns) >= 1 by NAT_1:13;
then (q |^ ns) +- 1 >= 1 +- 1 by XREAL_1:7;
then reconsider qns1=(q |^ ns - 1) as Element of NAT by INT_1:3;
A73: oa = (card the carrier of (centralizer s)) - 1 by Th30
.= qns1 by Th33;
reconsider ns as non zero Element of NAT by Th34,ORDINAL1:def 12;
A74: ns <= n by Th36,NAT_D:7;
now
assume ns = n;
then
A75: card (f2.i) = 1 by A3,A69,A71,A73,NAT_2:3;
A76: f2.i in B by A35,A68,FUNCT_1:3;
then
A77: f2.i in conjugate_Classes Rs by XBOOLE_0:def 5;
not f2.i in A by A76,XBOOLE_0:def 5;
hence contradiction by A75,A77;
end;
then ns < n by A74,XXREAL_0:1;
then pnq divides ((qn1 qua Integer) div qns1) by Th36,UNIROOTS:59;
then abspnq divides |.qn1 div qns1.| by INT_2:16;
hence thesis by A67,A69,A72,A73,ABSVALUE:def 1;
end;
then abspnq divides natq1 by A64,A65,Th5,NAT_D:10;
hence contradiction by A4,A5,A8,NAT_D:7,UNIROOTS:60;
end;
theorem
for R being Skew-Field holds 1.center R = 1.R by Def4;
theorem
for R being Skew-Field, s being Element of R holds 1.centralizer s = 1.R
by Def5;
:: new, 2025-05-05
theorem
for R being right_complementable Abelian add-associative right_zeroed
associative well-unital distributive non empty doubleLoopStr
for x being Element of center R
holds x is Element of R by Lm1;
:: new, 2025-05-05
theorem
for R being right_complementable Abelian add-associative right_zeroed
associative well-unital distributive non empty doubleLoopStr
for x,y being Element of center R
for a,b being Element of R
st x = a & y = b
holds a + b = x + y & a * b = x * y by Lm2;
:: new, 2025-05-05
theorem
for R being right_complementable Abelian add-associative right_zeroed
associative well-unital distributive non empty doubleLoopStr
for a,b being Element of R
st a in center R
holds a * b = b * a by Lm3;