:: WEDDWITT semantic presentation
begin
theorem Th1: :: WEDDWITT:1
for a being Element of NAT
for q being Real st 1 < q & q |^ a = 1 holds
a = 0
proof
let a be Element of NAT ; ::_thesis: for q being Real st 1 < q & q |^ a = 1 holds
a = 0
let q be Real; ::_thesis: ( 1 < q & q |^ a = 1 implies a = 0 )
assume that
A1: 1 < q and
A2: q |^ a = 1 and
A3: a <> 0 ; ::_thesis: contradiction
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; ::_thesis: verum
end;
theorem Th2: :: WEDDWITT:2
for a, k, r being Nat
for 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; ::_thesis: for x being Real st 1 < x & 0 < k holds
x |^ ((a * k) + r) = (x |^ a) * (x |^ ((a * (k -' 1)) + r))
let x be Real; ::_thesis: ( 1 < x & 0 < k implies x |^ ((a * k) + r) = (x |^ a) * (x |^ ((a * (k -' 1)) + r)) )
assume that
A1: 1 < x and
A2: 0 < k ; ::_thesis: x |^ ((a * k) + r) = (x |^ a) * (x |^ ((a * (k -' 1)) + r))
set xNak = x |^ ((a * k) + r);
0 + 1 <= k by A2, NAT_1:13;
then k = (k -' 1) + 1 by XREAL_1:235;
then x |^ ((a * k) + r) = x #Z (a + ((a * (k -' 1)) + r)) by PREPOWER:36;
then x |^ ((a * k) + r) = (x #Z a) * (x #Z ((a * (k -' 1)) + r)) by A1, PREPOWER:44;
then x |^ ((a * k) + r) = (x |^ a) * (x #Z ((a * (k -' 1)) + r)) by PREPOWER:36;
hence x |^ ((a * k) + r) = (x |^ a) * (x |^ ((a * (k -' 1)) + r)) by PREPOWER:36; ::_thesis: verum
end;
theorem Th3: :: WEDDWITT:3
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 ; ::_thesis: ( 0 < a & 1 < q & (q |^ a) -' 1 divides (q |^ b) -' 1 implies a divides b )
assume that
A1: 0 < a and
A2: 1 < q and
A3: (q |^ a) -' 1 divides (q |^ b) -' 1 ; ::_thesis: a divides b
set r = b mod a;
set qNa = q |^ a;
set qNr = q |^ (b mod a);
defpred S1[ Nat] means (q |^ a) -' 1 divides (q |^ ((a * $1) + (b mod a))) -' 1;
A4: b = (a * (b div a)) + (b mod a) by A1, NAT_D:2;
then A5: ex k being Nat st S1[k] by A3;
consider k being Nat such that
A6: S1[k] and
A7: for n being Nat st S1[n] holds
k <= n from NAT_1:sch_5(A5);
now__::_thesis:_a_divides_b
percases ( k = 0 or k <> 0 ) ;
supposeA8: k = 0 ; ::_thesis: a divides b
A9: now__::_thesis:_not_0_<>_(q_|^_(b_mod_a))_-'_1
assume A10: 0 <> (q |^ (b mod a)) -' 1 ; ::_thesis: contradiction
b mod a < a by A1, NAT_D:1;
then consider m being Nat such that
A11: a = (b mod a) + m by NAT_1:10;
A12: m <> 0 by A1, A11, NAT_D:1;
A13: q |^ ((b mod a) + m) = q #Z ((b mod a) + m) by PREPOWER:36;
A14: q #Z ((b mod a) + m) = (q #Z (b mod a)) * (q #Z m) by A2, PREPOWER:44;
A15: q #Z (b mod a) = q |^ (b mod a) 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: q |^ (b mod a) < q |^ a by A2, A11, A13, A14, A15, A16, PREPOWER:39, XREAL_1:155;
then 0 + 1 <= q |^ a by NAT_1:13;
then (q |^ a) -' 1 = (q |^ a) - 1 by XREAL_1:233;
then A19: (q |^ a) -' 1 = (q |^ a) + (- 1) ;
0 + 1 <= q |^ (b mod a) by A10, NAT_2:8;
then (q |^ (b mod a)) -' 1 = (q |^ (b mod a)) - 1 by XREAL_1:233;
then (q |^ (b mod a)) -' 1 = (q |^ (b mod a)) + (- 1) ;
then (q |^ (b mod a)) -' 1 < (q |^ a) -' 1 by A18, A19, XREAL_1:8;
hence contradiction by A6, A8, A10, NAT_D:7; ::_thesis: verum
end;
0 < q |^ (b mod a) by A2, PREPOWER:6;
then 0 + 1 <= q |^ (b mod a) by NAT_1:13;
then ((q |^ (b mod a)) - 1) + 1 = 1 by A9, XREAL_1:233;
then b mod a = 0 by A2, Th1;
hence a divides b by A4, NAT_D:3; ::_thesis: verum
end;
supposeA20: k <> 0 ; ::_thesis: a divides b
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) + (b mod a));
set qNak = q |^ ((a * k) + (b mod a));
set qNak1 = q |^ ((a * (k -' 1)) + (b mod a));
A24: not (q |^ a) -' 1 divides (q |^ ((a * j) + (b mod a))) -' 1 by A7, A21, XREAL_1:29;
(q |^ a) -' 1 divides - ((q |^ a) -' 1) by INT_2:10;
then A25: (q |^ a) -' 1 divides ((q |^ ((a * k) + (b mod a))) -' 1) + (- ((q |^ a) -' 1)) by A6, WSIERP_1:4;
A26: 0 < q |^ ((a * k) + (b mod a)) by A2, PREPOWER:6;
A27: 0 < q |^ a by A2, PREPOWER:6;
0 + 1 <= q |^ ((a * k) + (b mod a)) by A26, NAT_1:13;
then A28: (q |^ ((a * k) + (b mod a))) -' 1 = (q |^ ((a * k) + (b mod a))) - 1 by XREAL_1:233;
A29: 0 + 1 <= q |^ a by A27, NAT_1:13;
((q |^ ((a * k) + (b mod a))) - 1) - ((q |^ a) - 1) = (q |^ ((a * k) + (b mod a))) - (q |^ a) ;
then ((q |^ ((a * k) + (b mod a))) - 1) - ((q |^ a) - 1) = ((q |^ a) * (q |^ ((a * (k -' 1)) + (b mod a)))) - ((q |^ a) * 1) by A2, A20, Th2;
then A30: ((q |^ ((a * k) + (b mod a))) -' 1) - ((q |^ a) -' 1) = (q |^ a) * ((q |^ ((a * (k -' 1)) + (b mod a))) - 1) by A28, A29, XREAL_1:233;
0 < q |^ ((a * (k -' 1)) + (b mod a)) by A2, PREPOWER:6;
then 0 + 1 <= q |^ ((a * (k -' 1)) + (b mod a)) by NAT_1:13;
then A31: ((q |^ ((a * k) + (b mod a))) -' 1) - ((q |^ a) -' 1) = (q |^ a) * ((q |^ ((a * (k -' 1)) + (b mod a))) -' 1) by A30, XREAL_1:233;
0 < q |^ a by A2, PREPOWER:6;
then 0 + 1 <= q |^ a by NAT_1:13;
then ((q |^ a) -' 1) + 1 = q |^ a by XREAL_1:235;
then (q |^ a) -' 1,q |^ a are_relative_prime by PEPIN:1;
hence a divides b by A23, A24, A25, A31, INT_2:25; ::_thesis: verum
end;
end;
end;
hence a divides b ; ::_thesis: verum
end;
theorem Th4: :: WEDDWITT:4
for n, q being Nat st 0 < q holds
card (Funcs (n,q)) = q |^ n
proof
let n, q be Nat; ::_thesis: ( 0 < q implies card (Funcs (n,q)) = q |^ n )
assume A1: 0 < q ; ::_thesis: card (Funcs (n,q)) = q |^ n
reconsider q = q as Element of NAT by ORDINAL1:def_12;
defpred S1[ 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: S1[ 0 ] ;
A3: for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be Nat; ::_thesis: ( S1[n] implies S1[n + 1] )
assume A4: S1[n] ; ::_thesis: S1[n + 1]
reconsider n = n as Element of NAT by ORDINAL1:def_12;
reconsider q9 = q as non empty set by A1;
defpred S2[ set , set ] means ex x being Function of (n + 1),q st
( $1 = x & $2 = x | n );
A5: for x being set st x in Funcs ((n + 1),q9) holds
ex y being set st
( y in Funcs (n,q9) & S2[x,y] )
proof
let x be set ; ::_thesis: ( x in Funcs ((n + 1),q9) implies ex y being set st
( y in Funcs (n,q9) & S2[x,y] ) )
assume x in Funcs ((n + 1),q9) ; ::_thesis: ex y being set st
( y in Funcs (n,q9) & S2[x,y] )
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 = 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;
(n + 1) /\ n = (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 ex y being set st
( y in Funcs (n,q9) & S2[x,y] ) by A6; ::_thesis: verum
end;
consider G being Function of (Funcs ((n + 1),q9)),(Funcs (n,q9)) such that
A11: for x being set st x in Funcs ((n + 1),q9) holds
S2[x,G . x] from FUNCT_2:sch_1(A5);
for x being set st x in Funcs (n,q9) holds
x in rng G
proof
let x be set ; ::_thesis: ( x in Funcs (n,q9) implies x in rng G )
assume A12: x in Funcs (n,q9) ; ::_thesis: x in rng G
consider y being set 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 ; ::_thesis: ( y in q implies g +* (n .--> y) in G " {g} )
assume A14: y in q ; ::_thesis: g +* (n .--> y) in G " {g}
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} by FUNCT_2:def_1;
then dom f = n \/ {n} by A15, A16, FUNCT_4:def_1;
then A18: dom f = 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, XBOOLE_1:1;
then A20: f in Funcs ((n + 1),q) by A18, FUNCT_2:def_2;
then reconsider f = 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;
S2[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 g +* (n .--> y) in G " {g} by A15, A20, A22, FUNCT_1:def_7; ::_thesis: verum
end;
then g +* (n .--> y) in G " {g} by A13;
then consider b being set such that
A23: b in rng G and
A24: [(g +* (n .--> y)),b] in G and
b in {g} by RELAT_1:131;
g +* (n .--> y) in dom G by A24, FUNCT_1:1;
then S2[g +* (n .--> y),G . (g +* (n .--> y))] by A11;
then A25: (g +* (n .--> y)) | n = b by A24, FUNCT_1:1;
A26: dom g = n by FUNCT_2:def_1;
A27: dom (n .--> y) = {n} by FUNCT_2:def_1;
not n in n ;
then n misses {n} by ZFMISC_1:50;
hence x in rng G by A23, A25, A26, A27, FUNCT_4:33; ::_thesis: verum
end;
then Funcs (n,q9) c= rng G by TARSKI:def_3;
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); ::_thesis: ( G " {x} is finite & card (G " {x}) = q )
deffunc H1( set ) -> set = x +* (n .--> $1);
A30: for y being set st y in q holds
H1(y) in G " {x}
proof
let y be set ; ::_thesis: ( y in q implies H1(y) in G " {x} )
assume A31: y in q ; ::_thesis: H1(y) in G " {x}
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} by FUNCT_2:def_1;
then dom f = n \/ {n} by A32, A33, FUNCT_4:def_1;
then A35: dom f = 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, XBOOLE_1:1;
then A37: f in Funcs ((n + 1),q) by A35, FUNCT_2:def_2;
then reconsider f = 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;
S2[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 H1(y) in G " {x} by A32, A37, A39, FUNCT_1:def_7; ::_thesis: verum
end;
consider H being Function of q,(G " {x}) such that
A40: for y being set st y in q holds
H . y = H1(y) from FUNCT_2:sch_2(A30);
A41: for c being set st c in G " {x} holds
ex y being set st
( y in q & H . y = c )
proof
let c be set ; ::_thesis: ( c in G " {x} implies ex y being set st
( y in q & H . y = c ) )
assume A42: c in G " {x} ; ::_thesis: ex y being set st
( y in q & H . y = c )
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; ::_thesis: ( y in q & H . y = c )
G . c in {x} by A42, FUNCT_1:def_7;
then A45: G . c = x by TARSKI:def_1;
n + 1 = 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 n + 1 by NAT_1:45;
thus y in q by FUNCT_2:5, NAT_1:45; ::_thesis: H . y = c
thus H . y = c by A40, A43, A44, A45, A46, A47, FUNCT_2:5; ::_thesis: verum
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 set st x1 in dom H & x2 in dom H & H . x1 = H . x2 holds
x1 = x2
proof
let x1, x2 be set ; ::_thesis: ( x1 in dom H & x2 in dom H & H . x1 = H . x2 implies x1 = x2 )
assume that
A51: x1 in dom H and
A52: x2 in dom H and
A53: H . x1 = H . x2 ; ::_thesis: x1 = x2
A54: H . x2 = x +* (n .--> x2) by A40, A52;
A55: dom (n .--> x1) = {n} by FUNCOP_1:13;
A56: dom (n .--> x2) = {n} by FUNCOP_1:13;
set fx1 = x +* (n .--> x1);
set fx2 = x +* (n .--> x2);
A57: x +* (n .--> x1) = x +* (n .--> x2) 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 (x +* (n .--> x1)) . n = x1 by A55, A58, FUNCT_4:13;
hence x1 = x2 by A56, A57, A59, A60, FUNCT_4:13; ::_thesis: verum
end;
then H is one-to-one by FUNCT_1:def_4;
then q,H .: q are_equipotent by A50, CARD_1:33;
then q, rng H are_equipotent by A50, RELAT_1:113;
hence ( G " {x} is finite & card (G " {x}) = q ) by A49, CARD_1:def_2; ::_thesis: verum
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 ; ::_thesis: ( x is Element of Funcs (n,q9) & y is Element of Funcs (n,q9) & x <> y implies G " {x} misses G " {y} )
assume that
x is Element of Funcs (n,q9) and
y is Element of Funcs (n,q9) and
A62: x <> y ; ::_thesis: G " {x} misses G " {y}
now__::_thesis:_G_"_{x}_misses_G_"_{y}
assume not G " {x} misses G " {y} ; ::_thesis: contradiction
then not (G " {x}) /\ (G " {y}) = {} by XBOOLE_0:def_7;
then consider f being set 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 = 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: S2[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; ::_thesis: verum
end;
hence G " {x} misses G " {y} ; ::_thesis: verum
end;
reconsider X = { (G " {x}) where x is Element of Funcs (n,q9) : verum } as set ;
A67: for y being set st y in union X holds
y in Funcs ((n + 1),q)
proof
let x be set ; ::_thesis: ( x in union X implies x in Funcs ((n + 1),q) )
assume x in union X ; ::_thesis: x in Funcs ((n + 1),q)
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 x in Funcs ((n + 1),q) by A68; ::_thesis: verum
end;
for y being set st y in Funcs ((n + 1),q) holds
y in union X
proof
let x be set ; ::_thesis: ( x in Funcs ((n + 1),q) implies x in union X )
assume x in Funcs ((n + 1),q) ; ::_thesis: x in union X
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 set st
( y in Funcs (n,q9) & S2[f,y] ) by A5, A72;
then G " {(f | n)} in X ;
hence x in union X by A70, A74, TARSKI:def_4; ::_thesis: verum
end;
then A75: union X = Funcs ((n + 1),q) by A67, TARSKI:1;
Funcs ((n + 1),q) is finite by FRAENKEL:6;
then reconsider X = X as finite set by A75, FINSET_1:7;
A76: card X = q |^ n
proof
deffunc H1( set ) -> Element of bool (Funcs ((n + 1),q9)) = G " {$1};
A77: for x being set st x in Funcs (n,q) holds
H1(x) in X ;
consider F being Function of (Funcs (n,q)),X such that
A78: for x being set st x in Funcs (n,q) holds
F . x = H1(x) from FUNCT_2:sch_2(A77);
A79: for c being set st c in X holds
ex x being set st
( x in Funcs (n,q) & c = F . x )
proof
let c be set ; ::_thesis: ( c in X implies ex x being set st
( x in Funcs (n,q) & c = F . x ) )
assume c in X ; ::_thesis: ex x being set st
( x in Funcs (n,q) & c = F . x )
then consider y being Element of Funcs (n,q) such that
A80: c = G " {y} ;
F . y = c by A78, A80;
hence ex x being set st
( x in Funcs (n,q) & c = F . x ) ; ::_thesis: verum
end;
set gg = the Element of Funcs (n,q9);
A81: G " { the Element of Funcs (n,q9)} 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 set st x1 in dom F & x2 in dom F & F . x1 = F . x2 holds
x1 = x2
proof
let x1, x2 be set ; ::_thesis: ( x1 in dom F & x2 in dom F & F . x1 = F . x2 implies x1 = x2 )
assume that
A84: x1 in dom F and
A85: x2 in dom F and
A86: F . x1 = F . x2 ; ::_thesis: x1 = x2
F . x1 = G " {x1} by A78, A84;
then A87: G " {x1} = G " {x2} by A78, A85, A86;
now__::_thesis:_not_x1_<>_x2
assume x1 <> x2 ; ::_thesis: contradiction
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; ::_thesis: verum
end;
hence x1 = x2 ; ::_thesis: verum
end;
then F is one-to-one by FUNCT_1:def_4;
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 card X = q |^ n by A4, A82, CARD_1:5; ::_thesis: verum
end;
for Y being set st Y in X holds
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 ; ::_thesis: ( Y in X implies 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 ) ) ) )
assume Y in X ; ::_thesis: 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 ) ) )
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 ; ::_thesis: ( Z in X & Y <> Z implies ( Y,Z are_equipotent & Y misses Z ) )
assume that
A91: Z in X and
A92: Y <> Z ; ::_thesis: ( Y,Z are_equipotent & Y misses 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__::_thesis:_Y_misses_Z
percases ( x = y or x <> y ) ;
suppose x = y ; ::_thesis: Y misses Z
hence Y misses Z by A88, A92, A93; ::_thesis: verum
end;
suppose x <> y ; ::_thesis: Y misses Z
hence Y misses Z by A61, A88, A93; ::_thesis: verum
end;
end;
end;
hence ( Y,Z are_equipotent & Y misses Z ) by A90, A94, CARD_1:5; ::_thesis: verum
end;
hence 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 ) ) ) by A89, A90; ::_thesis: verum
end;
then ex C being finite set st
( C = union X & card C = q * (card X) ) by GROUP_2:156;
hence S1[n + 1] by A75, A76, NEWTON:6; ::_thesis: verum
end;
for n being Nat holds S1[n] from NAT_1:sch_2(A2, A3);
hence card (Funcs (n,q)) = q |^ n ; ::_thesis: verum
end;
theorem Th5: :: WEDDWITT:5
for f being FinSequence of NAT
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
proof
defpred S1[ Element of NAT ] means for f being FinSequence of NAT st len f = $1 holds
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: S1[ 0 ]
proof
let f be FinSequence of NAT ; ::_thesis: ( len f = 0 implies 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 )
assume len f = 0 ; ::_thesis: 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
then A2: f = <*> NAT ;
let i be Element of NAT ; ::_thesis: ( ( for j being Element of NAT st j in dom f holds
i divides f /. j ) implies i divides Sum f )
assume for j being Element of NAT st j in dom f holds
i divides f /. j ; ::_thesis: i divides Sum f
Sum f = 0 by A2, RVSUM_1:72;
hence i divides Sum f by NAT_D:6; ::_thesis: verum
end;
A3: for k being Element of NAT st S1[k] holds
S1[k + 1]
proof
let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A4: S1[k] ; ::_thesis: S1[k + 1]
let f be FinSequence of NAT ; ::_thesis: ( len f = k + 1 implies 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 )
assume A5: len f = k + 1 ; ::_thesis: 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
let i be Element of NAT ; ::_thesis: ( ( for j being Element of NAT st j in dom f holds
i divides f /. j ) implies i divides Sum f )
assume A6: for j being Element of NAT st j in dom f holds
i divides f /. j ; ::_thesis: i divides Sum f
f <> {} by A5;
then consider q being FinSequence, x being set 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 ; ::_thesis: ( j in dom f1 implies i divides f1 /. j )
assume A9: j in dom f1 ; ::_thesis: i divides f1 /. j
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 i divides f1 /. j by A6, A9, A10; ::_thesis: verum
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 i divides Sum f by A11, A14, NAT_D:8; ::_thesis: verum
end;
A15: for k being Element of NAT holds S1[k] from NAT_1:sch_1(A1, A3);
let f be FinSequence of NAT ; ::_thesis: 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
let i be Element of NAT ; ::_thesis: ( ( for j being Element of NAT st j in dom f holds
i divides f /. j ) implies i divides Sum f )
assume A16: for j being Element of NAT st j in dom f holds
i divides f /. j ; ::_thesis: i divides Sum f
len f = len f ;
hence i divides Sum f by A15, A16; ::_thesis: verum
end;
theorem Th6: :: WEDDWITT:6
for X being finite set
for Y being a_partition of X
for f being FinSequence of Y st f is one-to-one & rng f = Y holds
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 S1[ Element of NAT ] means for X being finite set
for z being a_partition of X st card z = $1 holds
for f being FinSequence of z st f is one-to-one & rng f = z holds
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: S1[ 0 ]
proof
let X be finite set ; ::_thesis: for z being a_partition of X st card z = 0 holds
for f being FinSequence of z st f is one-to-one & rng f = z holds
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
let z be a_partition of X; ::_thesis: ( card z = 0 implies for f being FinSequence of z st f is one-to-one & rng f = z holds
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 )
assume A2: card z = 0 ; ::_thesis: for f being FinSequence of z st f is one-to-one & rng f = z holds
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
let f be FinSequence of z; ::_thesis: ( f is one-to-one & rng f = z implies 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 )
assume that
f is one-to-one and
rng f = z ; ::_thesis: 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
let c be FinSequence of NAT ; ::_thesis: ( len c = len f & ( for i being Element of NAT st i in dom c holds
c . i = card (f . i) ) implies card X = Sum c )
assume that
A3: len c = len f and
for i being Element of NAT st i in dom c holds
c . i = card (f . i) ; ::_thesis: card X = Sum c
A4: z = {} by A2;
A5: X = {} by A2;
c = {} by A3, A4;
hence card X = Sum c by A5, RVSUM_1:72; ::_thesis: verum
end;
A6: for k being Element of NAT st S1[k] holds
S1[k + 1]
proof
let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A7: S1[k] ; ::_thesis: S1[k + 1]
let X be finite set ; ::_thesis: for z being a_partition of X st card z = k + 1 holds
for f being FinSequence of z st f is one-to-one & rng f = z holds
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
let Z be a_partition of X; ::_thesis: ( card Z = k + 1 implies for f being FinSequence of Z st f is one-to-one & rng f = Z holds
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 )
assume A8: card Z = k + 1 ; ::_thesis: for f being FinSequence of Z st f is one-to-one & rng f = Z holds
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
let f be FinSequence of Z; ::_thesis: ( f is one-to-one & rng f = Z implies 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 )
assume that
A9: f is one-to-one and
A10: rng f = Z ; ::_thesis: 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
let c be FinSequence of NAT ; ::_thesis: ( len c = len f & ( for i being Element of NAT st i in dom c holds
c . i = card (f . i) ) implies card X = Sum c )
assume 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) ; ::_thesis: card X = Sum c
A13: len f = k + 1 by A8, A9, A10, FINSEQ_4:62;
A14: Z <> {} by A8;
reconsider Z = Z as non empty set by A8;
reconsider f = f as FinSequence of Z ;
reconsider X = X as non empty finite set by A14, EQREL_1:32;
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 = 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__::_thesis:_Zk_is_a_partition_of_Xk
A20: for a being Subset of Xk st a in Zk holds
( a <> {} & ( for b being Subset of Xk holds
( not b in Zk or a = b or a misses b ) ) )
proof
let a be Subset of Xk; ::_thesis: ( a in Zk implies ( a <> {} & ( for b being Subset of Xk holds
( not b in Zk or a = b or a misses b ) ) ) )
assume A21: a in Zk ; ::_thesis: ( a <> {} & ( for b being Subset of Xk holds
( not b in Zk or a = b or a misses b ) ) )
A22: a in Z by A21;
for b being Subset of Xk holds
( not b in Zk or a = b or a misses b )
proof
let b be Subset of Xk; ::_thesis: ( not b in Zk or a = b or a misses b )
assume A23: b in Zk ; ::_thesis: ( a = b or a misses b )
A24: a in Z by A21;
b in Z by A23;
hence ( a = b or a misses b ) by A24, EQREL_1:def_4; ::_thesis: verum
end;
hence ( a <> {} & ( for b being Subset of Xk holds
( not b in Zk or a = b or a misses b ) ) ) by A22, EQREL_1:def_4; ::_thesis: verum
end;
Zk c= bool (union Zk) by ZFMISC_1:82;
hence Zk is a_partition of Xk by A20, EQREL_1:def_4; ::_thesis: verum
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 ; ::_thesis: ( i in dom ck implies ck . i = card (fk . i) )
assume A26: i in dom ck ; ::_thesis: ck . i = card (fk . i)
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 ck . i = card (fk . i) by A26, A28, FUNCT_1:47; ::_thesis: verum
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 be set ; ::_thesis: ( x in Zk implies x misses fk1 )
assume A31: x in Zk ; ::_thesis: x misses fk1
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__::_thesis:_not_fk_._i_=_fk1
assume A36: fk . i = fk1 ; ::_thesis: contradiction
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, FUNCT_1:def_4; ::_thesis: verum
end;
hence x misses fk1 by A10, A32, A33, A35, EQREL_1:def_4; ::_thesis: verum
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 = 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 card X = Sum c ; ::_thesis: verum
end;
A47: for k being Element of NAT holds S1[k] from NAT_1:sch_1(A1, A6);
let X be finite set ; ::_thesis: for Y being a_partition of X
for f being FinSequence of Y st f is one-to-one & rng f = Y holds
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
let Y be a_partition of X; ::_thesis: for f being FinSequence of Y st f is one-to-one & rng f = Y holds
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
card Y = card Y ;
hence for f being FinSequence of Y st f is one-to-one & rng f = Y holds
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 by A47; ::_thesis: verum
end;
begin
registration
let G be finite Group;
cluster center G -> finite ;
correctness
coherence
center G is finite ;
;
end;
definition
let G be Group;
let a be Element of G;
func Centralizer a -> strict Subgroup of G means :Def1: :: WEDDWITT:def 1
the carrier of it = { b where b is Element of G : a * b = b * a } ;
existence
ex b1 being strict Subgroup of G st the carrier of b1 = { b where b is Element of G : a * b = b * a }
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 { b where b is Element of G : a * b = b * a } by A1;
for x being set st x in { b where b is Element of G : a * b = b * a } holds
x in the carrier of G
proof
let x be set ; ::_thesis: ( x in { b where b is Element of G : a * b = b * a } implies x in the carrier of G )
assume x in { b where b is Element of G : a * b = b * a } ; ::_thesis: x in the carrier of G
then ex g being Element of G st
( x = g & a * g = g * a ) ;
hence x in the carrier of G ; ::_thesis: verum
end;
then A3: { b where b is Element of G : a * b = b * a } is Subset of G by TARSKI:def_3;
A4: for g1, g2 being Element of G st g1 in { b where b is Element of G : a * b = b * a } & g2 in { b where b is Element of G : a * b = b * a } holds
g1 * g2 in { b where b is Element of G : a * b = b * a }
proof
let g1, g2 be Element of G; ::_thesis: ( g1 in { b where b is Element of G : a * b = b * a } & g2 in { b where b is Element of G : a * b = b * a } implies g1 * g2 in { b where b is Element of G : a * b = b * a } )
assume that
A5: g1 in { b where b is Element of G : a * b = b * a } and
A6: g2 in { b where b is Element of G : a * b = b * a } ; ::_thesis: g1 * g2 in { b where b is Element of G : a * b = b * a }
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 g1 * g2 in { b where b is Element of G : a * b = b * a } ; ::_thesis: verum
end;
for g being Element of G st g in { b where b is Element of G : a * b = b * a } holds
g " in { b where b is Element of G : a * b = b * a }
proof
let g be Element of G; ::_thesis: ( g in { b where b is Element of G : a * b = b * a } implies g " in { b where b is Element of G : a * b = b * a } )
assume g in { b where b is Element of G : a * b = b * a } ; ::_thesis: g " in { b where b is Element of G : a * b = b * a }
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 g " in { b where b is Element of G : a * b = b * a } ; ::_thesis: verum
end;
hence ex b1 being strict Subgroup of G st the carrier of b1 = { b where b is Element of G : a * b = b * a } by A2, A3, A4, GROUP_2:52; ::_thesis: verum
end;
uniqueness
for b1, b2 being strict Subgroup of G st the carrier of b1 = { b where b is Element of G : a * b = b * a } & the carrier of b2 = { b where b is Element of G : a * b = b * a } holds
b1 = b2
proof
let H1, H2 be strict Subgroup of G; ::_thesis: ( the carrier of H1 = { b where b is Element of G : a * b = b * a } & the carrier of H2 = { b where b is Element of G : a * b = b * a } implies H1 = H2 )
assume 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 } ; ::_thesis: H1 = H2
for g being Element of G holds
( g in H1 iff g in H2 )
proof
let g be Element of G; ::_thesis: ( g in H1 iff g in H2 )
hereby ::_thesis: ( g in H2 implies g in H1 )
assume g in H1 ; ::_thesis: g in H2
then g in the carrier of H1 by STRUCT_0:def_5;
hence g in H2 by A10, A11, STRUCT_0:def_5; ::_thesis: verum
end;
now__::_thesis:_(_g_in_H2_implies_g_in_H1_)
assume g in H2 ; ::_thesis: g in H1
then g in the carrier of H2 by STRUCT_0:def_5;
hence g in H1 by A10, A11, STRUCT_0:def_5; ::_thesis: verum
end;
hence ( g in H2 implies g in H1 ) ; ::_thesis: verum
end;
hence H1 = H2 by GROUP_2:def_6; ::_thesis: verum
end;
end;
:: deftheorem Def1 defines Centralizer WEDDWITT:def_1_:_
for G being Group
for a being Element of G
for b3 being strict Subgroup of G holds
( b3 = Centralizer a iff the carrier of b3 = { b where b is Element of G : a * b = b * a } );
registration
let G be finite Group;
let a be Element of G;
cluster Centralizer a -> finite strict ;
correctness
coherence
Centralizer a is finite ;
;
end;
theorem Th7: :: WEDDWITT:7
for G being Group
for a being Element of G
for x being set st x in Centralizer a holds
x in G
proof
let G be Group; ::_thesis: for a being Element of G
for x being set st x in Centralizer a holds
x in G
let a be Element of G; ::_thesis: for x being set st x in Centralizer a holds
x in G
let x be set ; ::_thesis: ( x in Centralizer a implies x in G )
assume A1: x in Centralizer a ; ::_thesis: x in G
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, STRUCT_0:def_5;
then ex b being Element of G st
( b = x & a * b = b * a ) ;
hence x in G by STRUCT_0:def_5; ::_thesis: verum
end;
theorem Th8: :: WEDDWITT:8
for G being Group
for a, x being Element of G holds
( a * x = x * a iff x is Element of (Centralizer a) )
proof
let G be Group; ::_thesis: for a, x being Element of G holds
( a * x = x * a iff x is Element of (Centralizer a) )
let a, x be Element of G; ::_thesis: ( a * x = x * a iff x is Element of (Centralizer a) )
A1: the carrier of (Centralizer a) = { b where b is Element of G : a * b = b * a } by Def1;
hereby ::_thesis: ( x is Element of (Centralizer a) implies a * x = x * a )
assume a * x = x * a ; ::_thesis: x is Element of (Centralizer a)
then x in the carrier of (Centralizer a) by A1;
hence x is Element of (Centralizer a) ; ::_thesis: verum
end;
assume x is Element of (Centralizer a) ; ::_thesis: a * x = x * 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 a * x = x * a ; ::_thesis: verum
end;
registration
let G be Group;
let a be Element of G;
cluster con_class a -> non empty ;
correctness
coherence
not con_class a is empty ;
by GROUP_3:83;
end;
definition
let G be Group;
let a be Element of G;
funca -con_map -> Function of the carrier of G,(con_class a) means :Def2: :: WEDDWITT:def 2
for x being Element of G holds it . x = a |^ x;
existence
ex b1 being Function of the carrier of G,(con_class a) st
for x being Element of G holds b1 . x = a |^ x
proof
defpred S1[ Element of G, set ] means $2 = a |^ $1;
A1: for x being Element of G ex y being Element of con_class a st S1[x,y]
proof
let x be Element of G; ::_thesis: ex y being Element of con_class a st S1[x,y]
a |^ x in con_class a by GROUP_3:82;
hence ex y being Element of con_class a st S1[x,y] ; ::_thesis: verum
end;
ex f being Function of the carrier of G,(con_class a) st
for x being Element of G holds S1[x,f . x] from FUNCT_2:sch_3(A1);
hence ex b1 being Function of the carrier of G,(con_class a) st
for x being Element of G holds b1 . x = a |^ x ; ::_thesis: verum
end;
uniqueness
for b1, b2 being Function of the carrier of G,(con_class a) st ( for x being Element of G holds b1 . x = a |^ x ) & ( for x being Element of G holds b2 . x = a |^ x ) holds
b1 = b2
proof
let it1, it2 be Function of the carrier of G,(con_class a); ::_thesis: ( ( for x being Element of G holds it1 . x = a |^ x ) & ( for x being Element of G holds it2 . x = a |^ x ) implies it1 = it2 )
assume 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 ; ::_thesis: it1 = it2
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 set st x in dom it1 holds
it1 . x = it2 . x
proof
let x be set ; ::_thesis: ( x in dom it1 implies it1 . x = it2 . x )
assume x in dom it1 ; ::_thesis: it1 . x = it2 . x
then reconsider y = x as Element of G ;
it1 . y = a |^ y by A2;
hence it1 . x = it2 . x by A3; ::_thesis: verum
end;
hence it1 = it2 by A4, A5, FUNCT_1:2; ::_thesis: verum
end;
end;
:: deftheorem Def2 defines -con_map WEDDWITT:def_2_:_
for G being Group
for a being Element of G
for b3 being Function of the carrier of G,(con_class a) holds
( b3 = a -con_map iff for x being Element of G holds b3 . x = a |^ x );
theorem Th9: :: WEDDWITT:9
for G being finite Group
for a being Element of G
for x being Element of con_class a holds card ((a -con_map) " {x}) = card (Centralizer a)
proof
let G be finite Group; ::_thesis: for a being Element of G
for x being Element of con_class a holds card ((a -con_map) " {x}) = card (Centralizer a)
let a be Element of G; ::_thesis: for x being Element of con_class a holds card ((a -con_map) " {x}) = card (Centralizer a)
let x be Element of con_class a; ::_thesis: card ((a -con_map) " {x}) = card (Centralizer 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 set holds
( g in (a -con_map) " {x} iff g in Cad )
proof
let g be set ; ::_thesis: ( g in (a -con_map) " {x} iff g in Cad )
A3: now__::_thesis:_(_g_in_(a_-con_map)_"_{x}_implies_g_in_Cad_)
assume A4: g in (a -con_map) " {x} ; ::_thesis: g in Cad
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, STRUCT_0:def_5;
reconsider z = z as Element of G ;
y = z * d by A9, GROUP_3:1;
hence g in Cad by A10, GROUP_2:104; ::_thesis: verum
end;
now__::_thesis:_(_g_in_Cad_implies_g_in_(a_-con_map)_"_{x}_)
assume g in Cad ; ::_thesis: g in (a -con_map) " {x}
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, STRUCT_0:def_5;
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; ::_thesis: verum
end;
hence ( g in (a -con_map) " {x} iff g in Cad ) by A3; ::_thesis: verum
end;
hence card ((a -con_map) " {x}) = card (Centralizer a) by A2, TARSKI:1; ::_thesis: verum
end;
theorem Th10: :: WEDDWITT:10
for G being Group
for a being Element of G
for 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; ::_thesis: for a being Element of G
for x, y being Element of con_class a st x <> y holds
(a -con_map) " {x} misses (a -con_map) " {y}
let a be Element of G; ::_thesis: for x, y being Element of con_class a st x <> y holds
(a -con_map) " {x} misses (a -con_map) " {y}
let x, y be Element of con_class a; ::_thesis: ( x <> y implies (a -con_map) " {x} misses (a -con_map) " {y} )
assume A1: x <> y ; ::_thesis: (a -con_map) " {x} misses (a -con_map) " {y}
now__::_thesis:_for_g_being_set_holds_not_g_in_((a_-con_map)_"_{x})_/\_((a_-con_map)_"_{y})
assume ex g being set st g in ((a -con_map) " {x}) /\ ((a -con_map) " {y}) ; ::_thesis: contradiction
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; ::_thesis: verum
end;
then ((a -con_map) " {x}) /\ ((a -con_map) " {y}) = {} by XBOOLE_0:def_1;
hence (a -con_map) " {x} misses (a -con_map) " {y} by XBOOLE_0:def_7; ::_thesis: verum
end;
theorem Th11: :: WEDDWITT:11
for G being Group
for a being Element of G holds { ((a -con_map) " {x}) where x is Element of con_class a : verum } is a_partition of the carrier of G
proof
let G be Group; ::_thesis: for a being Element of G holds { ((a -con_map) " {x}) where x is Element of con_class a : verum } is a_partition of the carrier of G
let a be Element of G; ::_thesis: { ((a -con_map) " {x}) where x is Element of con_class a : verum } is a_partition of the carrier of G
reconsider X = { ((a -con_map) " {x}) where x is Element of con_class a : verum } as set ;
A1: for y being set st y in union X holds
y in the carrier of G
proof
let x be set ; ::_thesis: ( x in union X implies x in the carrier of G )
assume x in union X ; ::_thesis: x in the carrier of G
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 x in the carrier of G by A2; ::_thesis: verum
end;
for y being set st y in the carrier of G holds
y in union X
proof
let x be set ; ::_thesis: ( x in the carrier of G implies x in union X )
assume x in the carrier of G ; ::_thesis: x in union X
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 x in union X by A7, TARSKI:def_4; ::_thesis: verum
end;
then A8: union X = the carrier of G by A1, TARSKI:1;
A9: for A being Subset of G st A in X holds
( A <> {} & ( for B being Subset of G holds
( not B in X or A = B or A misses B ) ) )
proof
let A be Subset of G; ::_thesis: ( A in X implies ( A <> {} & ( for B being Subset of G holds
( not B in X or A = B or A misses B ) ) ) )
assume A in X ; ::_thesis: ( A <> {} & ( for B being Subset of G holds
( not B in X or A = B or A misses B ) ) )
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 holds
( not B in X or A = B or A misses B )
proof
let B be Subset of G; ::_thesis: ( not B in X or A = B or A misses B )
assume B in X ; ::_thesis: ( A = B or A misses B )
then ex y being Element of con_class a st B = (a -con_map) " {y} ;
hence ( A = B or A misses B ) by A10, Th10; ::_thesis: verum
end;
hence ( A <> {} & ( for B being Subset of G holds
( not B in X or A = B or A misses B ) ) ) by A10, A12, A13, FUNCT_1:def_7; ::_thesis: verum
end;
X c= bool (union X) by ZFMISC_1:82;
hence { ((a -con_map) " {x}) where x is Element of con_class a : verum } is a_partition of the carrier of G by A8, A9, EQREL_1:def_4; ::_thesis: verum
end;
theorem Th12: :: WEDDWITT:12
for G being finite Group
for a being Element of G holds card { ((a -con_map) " {x}) where x is Element of con_class a : verum } = card (con_class a)
proof
let G be finite Group; ::_thesis: for a being Element of G holds card { ((a -con_map) " {x}) where x is Element of con_class a : verum } = card (con_class a)
let a be Element of G; ::_thesis: card { ((a -con_map) " {x}) where x is Element of con_class a : verum } = card (con_class a)
reconsider X = { ((a -con_map) " {x}) where x is Element of con_class a : verum } as a_partition of the carrier of G by Th11;
deffunc H1( set ) -> Element of bool the carrier of G = (a -con_map) " {$1};
A1: for x being set st x in con_class a holds
H1(x) in X ;
consider F being Function of (con_class a),X such that
A2: for x being set st x in con_class a holds
F . x = H1(x) from FUNCT_2:sch_2(A1);
for c being set st c in X holds
ex x being set st
( x in con_class a & c = F . x )
proof
let c be set ; ::_thesis: ( c in X implies ex x being set st
( x in con_class a & c = F . x ) )
assume A3: c in X ; ::_thesis: ex x being set st
( x in con_class a & c = F . x )
reconsider c = 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 ex x being set st
( x in con_class a & c = F . x ) ; ::_thesis: verum
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 set st x1 in dom F & x2 in dom F & F . x1 = F . x2 holds
x1 = x2
proof
let x1, x2 be set ; ::_thesis: ( x1 in dom F & x2 in dom F & F . x1 = F . x2 implies x1 = x2 )
assume that
A7: x1 in dom F and
A8: x2 in dom F and
A9: F . x1 = F . x2 ; ::_thesis: x1 = 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__::_thesis:_not_y1_<>_y2
assume y1 <> y2 ; ::_thesis: contradiction
then (a -con_map) " {y1} misses (a -con_map) " {y2} by Th10;
then A12: ((a -con_map) " {y1}) /\ ((a -con_map) " {y2}) = {} by XBOOLE_0:def_7;
consider d being Element of G such that
A13: d = y1 and
A14: a,d are_conjugated by GROUP_3:80;
consider g being Element of G such that
A15: d = a |^ g by A14, GROUP_3:def_7;
(a -con_map) . g = y1 by A13, A15, Def2;
then A16: (a -con_map) . g in {y1} by TARSKI:def_1;
dom (a -con_map) = the carrier of G by FUNCT_2:def_1;
hence contradiction by A9, A10, A11, A12, A16, FUNCT_1:def_7; ::_thesis: verum
end;
hence x1 = x2 ; ::_thesis: verum
end;
then F is one-to-one by FUNCT_1:def_4;
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 card { ((a -con_map) " {x}) where x is Element of con_class a : verum } = card (con_class a) by A5, CARD_1:5; ::_thesis: verum
end;
theorem Th13: :: WEDDWITT:13
for G being finite Group
for a being Element of G holds card G = (card (con_class a)) * (card (Centralizer a))
proof
let G be finite Group; ::_thesis: for a being Element of G holds card G = (card (con_class a)) * (card (Centralizer a))
let a be Element of G; ::_thesis: card G = (card (con_class a)) * (card (Centralizer a))
reconsider X = { ((a -con_map) " {x}) where x is Element of con_class a : verum } 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 ; ::_thesis: ( A in X implies ( A is finite & card A = card (Centralizer a) & ( for B being set st B in X & A <> B holds
A misses B ) ) )
assume A2: A in X ; ::_thesis: ( A is finite & card A = card (Centralizer a) & ( for B being set st B in X & A <> B holds
A misses B ) )
reconsider A = A as Subset of G by A2;
ex x being Element of con_class a st A = (a -con_map) " {x} by A2;
hence ( A is finite & card A = card (Centralizer a) & ( for B being set st B in X & A <> B holds
A misses B ) ) by A2, Th9, EQREL_1:def_4; ::_thesis: verum
end;
reconsider k = card (Centralizer a) as Element of NAT ;
for Y being set st Y in X holds
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 ; ::_thesis: ( Y in X implies 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 ) ) ) )
assume A3: Y in X ; ::_thesis: 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 ) ) )
reconsider Y = 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 ; ::_thesis: ( Z in X & Y <> Z implies ( Y,Z are_equipotent & Y misses Z ) )
assume that
A5: Z in X and
A6: Y <> Z ; ::_thesis: ( Y,Z are_equipotent & Y misses Z )
A7: card Y = card (Centralizer a) by A1, A3;
card Z = card (Centralizer a) by A1, A5;
hence ( Y,Z are_equipotent & Y misses Z ) by A1, A3, A5, A6, A7, CARD_1:5; ::_thesis: verum
end;
hence 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 ) ) ) by A4; ::_thesis: verum
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 card G = (card (con_class a)) * (card (Centralizer a)) ; ::_thesis: verum
end;
definition
let G be Group;
func conjugate_Classes G -> a_partition of the carrier of G equals :: WEDDWITT:def 3
{ (con_class a) where a is Element of G : verum } ;
correctness
coherence
{ (con_class a) where a is Element of G : verum } is a_partition of the carrier of G;
proof
set cG = the carrier of G;
set C = { (con_class a) where a is Element of G : verum } ;
A1: { (con_class a) where a is Element of G : verum } c= bool the carrier of G
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { (con_class a) where a is Element of G : verum } or x in bool the carrier of G )
assume x in { (con_class a) where a is Element of G : verum } ; ::_thesis: x in bool the carrier of G
then ex a being Element of the carrier of G st x = con_class a ;
hence x in bool the carrier of G ; ::_thesis: verum
end;
now__::_thesis:_for_x_being_set_holds_
(_(_x_in_union__{__(con_class_a)_where_a_is_Element_of_G_:_verum__}__implies_x_in_the_carrier_of_G_)_&_(_x_in_the_carrier_of_G_implies_x_in_union__{__(con_class_a)_where_a_is_Element_of_G_:_verum__}__)_)
let x be set ; ::_thesis: ( ( x in union { (con_class a) where a is Element of G : verum } implies x in the carrier of G ) & ( x in the carrier of G implies x in union { (con_class a) where a is Element of G : verum } ) )
hereby ::_thesis: ( x in the carrier of G implies x in union { (con_class a) where a is Element of G : verum } )
assume x in union { (con_class a) where a is Element of G : verum } ; ::_thesis: x in the carrier of G
then consider S being set such that
A2: x in S and
A3: S in { (con_class a) where a is Element of G : verum } by TARSKI:def_4;
ex a being Element of G st S = con_class a by A3;
hence x in the carrier of G by A2; ::_thesis: verum
end;
assume x in the carrier of G ; ::_thesis: x in union { (con_class a) where a is Element of G : verum }
then reconsider x9 = x as Element of the carrier of G ;
reconsider S = con_class x9 as Subset of the carrier of G ;
A4: S in { (con_class a) where a is Element of G : verum } ;
x9 in con_class x9 by GROUP_3:83;
hence x in union { (con_class a) where a is Element of G : verum } by A4, TARSKI:def_4; ::_thesis: verum
end;
then A5: union { (con_class a) where a is Element of G : verum } = the carrier of G by TARSKI:1;
now__::_thesis:_for_A_being_Subset_of_the_carrier_of_G_st_A_in__{__(con_class_a)_where_a_is_Element_of_G_:_verum__}__holds_
(_A_<>_{}_&_(_for_B_being_Subset_of_the_carrier_of_G_st_B_in__{__(con_class_a)_where_a_is_Element_of_G_:_verum__}__&_A_<>_B_holds_
not_A_meets_B_)_)
let A be Subset of the carrier of G; ::_thesis: ( A in { (con_class a) where a is Element of G : verum } implies ( A <> {} & ( for B being Subset of the carrier of G st B in { (con_class a) where a is Element of G : verum } & A <> B holds
not A meets B ) ) )
assume A6: A in { (con_class a) where a is Element of G : verum } ; ::_thesis: ( A <> {} & ( for B being Subset of the carrier of G st B in { (con_class a) where a is Element of G : verum } & A <> B holds
not A meets B ) )
then A7: ex a being Element of the carrier of G st A = con_class a ;
consider a being Element of the carrier of G such that
A8: A = con_class a by A6;
thus A <> {} by A7; ::_thesis: for B being Subset of the carrier of G st B in { (con_class a) where a is Element of G : verum } & A <> B holds
not A meets B
let B be Subset of the carrier of G; ::_thesis: ( B in { (con_class a) where a is Element of G : verum } & A <> B implies not A meets B )
assume B in { (con_class a) where a is Element of G : verum } ; ::_thesis: ( A <> B implies not A meets B )
then consider b being Element of the carrier of G such that
A9: B = con_class b ;
assume A10: A <> B ; ::_thesis: not A meets B
assume A meets B ; ::_thesis: contradiction
then consider x being set such that
A11: x in A and
A12: x in B by XBOOLE_0:3;
reconsider x = x as Element of the carrier of G 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__::_thesis:_for_c_being_set_holds_
(_(_c_in_A_implies_c_in_B_)_&_(_c_in_B_implies_c_in_A_)_)
let c be set ; ::_thesis: ( ( c in A implies c in B ) & ( c in B implies c in A ) )
hereby ::_thesis: ( c in B implies c in A )
assume A15: c in A ; ::_thesis: c in B
then reconsider c9 = c as Element of the carrier of G ;
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; ::_thesis: verum
end;
assume A16: c in B ; ::_thesis: c in A
then reconsider c9 = c as Element of the carrier of G ;
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; ::_thesis: verum
end;
hence contradiction by A10, TARSKI:1; ::_thesis: verum
end;
hence { (con_class a) where a is Element of G : verum } is a_partition of the carrier of G by A1, A5, EQREL_1:def_4; ::_thesis: verum
end;
end;
:: deftheorem defines conjugate_Classes WEDDWITT:def_3_:_
for G being Group holds conjugate_Classes G = { (con_class a) where a is Element of G : verum } ;
theorem :: WEDDWITT:14
for G being finite Group
for f being FinSequence of conjugate_Classes G st f is one-to-one & rng f = conjugate_Classes G holds
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
theorem Th15: :: WEDDWITT:15
for F being finite Field
for V being VectSp of F
for 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; ::_thesis: for V being VectSp of F
for 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
let V be VectSp of F; ::_thesis: for 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
let n, q be Nat; ::_thesis: ( V is finite-dimensional & n = dim V & q = card the carrier of F implies card the carrier of V = q |^ n )
assume that
A1: V is finite-dimensional and
A2: n = dim V and
A3: q = card the carrier of F ; ::_thesis: card the carrier of V = q |^ n
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 = VectSpStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) by A4, VECTSP_7:def_3;
A7: card B = n by A1, A2, A4, VECTSP_9:def_1;
now__::_thesis:_card_the_carrier_of_V_=_q_|^_n
percases ( n = 0 or n <> 0 ) ;
supposeA8: n = 0 ; ::_thesis: card the carrier of V = q |^ n
then (Omega). V = (0). V by A1, A2, VECTSP_9:29;
then VectSpStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult 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 card the carrier of V = q |^ n by A8; ::_thesis: verum
end;
suppose n <> 0 ; ::_thesis: card the carrier of V = q |^ n
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 S1[ 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 n -tuples_on the carrier of F ex y being Element of the carrier of (Lin B) st S1[x,y]
proof
let f be Element of n -tuples_on the carrier of F; ::_thesis: ex y being Element of the carrier of (Lin B) st S1[f,y]
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 H1( set ) -> set = f . (union (Vbf " {$1}));
A14: for x being set st x in B holds
H1(x) in the carrier of F
proof
let x be set ; ::_thesis: ( x in B implies H1(x) in the carrier of F )
assume x in B ; ::_thesis: H1(x) in the carrier of F
then consider i being set 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 H1(x) in the carrier of F by A16; ::_thesis: verum
end;
consider lc being Function of B, the carrier of F such that
A17: for y being set st y in B holds
lc . y = H1(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 by FUNCOP_1:13;
then dom (lc +* (( the carrier of V \ B) --> (0. F))) = (dom lc) \/ ( the carrier of V \ B) by FUNCT_4:def_1;
then dom (lc +* (( the carrier of V \ B) --> (0. F))) = B \/ ( the carrier of V \ B) by FUNCT_2:def_1;
then dom (lc +* (( the carrier of V \ B) --> (0. F))) = B \/ the carrier of V by XBOOLE_1:39;
then A19: dom (lc +* (( the carrier of V \ B) --> (0. F))) = the carrier of V by XBOOLE_1:12;
rng (lc +* (( the carrier of V \ B) --> (0. F))) c= (rng lc) \/ (rng (( the carrier of V \ B) --> (0. F))) by FUNCT_4:17;
then lc +* (( the carrier of V \ B) --> (0. F)) is Function of the carrier of V, the carrier of F by A19, FUNCT_2:2, XBOOLE_1:1;
then A20: lc +* (( the carrier of V \ B) --> (0. F)) 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
(lc +* (( the carrier of V \ B) --> (0. F))) . (Vbf . i) = f . i
proof
let i be set ; ::_thesis: ( i in dom f implies (lc +* (( the carrier of V \ B) --> (0. F))) . (Vbf . i) = f . i )
assume i in dom f ; ::_thesis: (lc +* (( the carrier of V \ B) --> (0. F))) . (Vbf . i) = f . i
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 set 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 (lc +* (( the carrier of V \ B) --> (0. F))) . y = lc . y by A18, FUNCT_4:11;
then (lc +* (( the carrier of V \ B) --> (0. F))) . y = f . (union (Vbf " {y})) by A9, A17;
hence (lc +* (( the carrier of V \ B) --> (0. F))) . (Vbf . i) = f . i by A23, A27, ZFMISC_1:25; ::_thesis: verum
end;
A28: for v being Element of V st not v in B holds
(lc +* (( the carrier of V \ B) --> (0. F))) . v = 0. F
proof
let v be Element of V; ::_thesis: ( not v in B implies (lc +* (( the carrier of V \ B) --> (0. F))) . v = 0. F )
assume not v in B ; ::_thesis: (lc +* (( the carrier of V \ B) --> (0. F))) . v = 0. F
then A29: v in the carrier of V \ B by XBOOLE_0:def_5;
then (lc +* (( the carrier of V \ B) --> (0. F))) . v = (( the carrier of V \ B) --> (0. F)) . v by A18, FUNCT_4:13;
hence (lc +* (( the carrier of V \ B) --> (0. F))) . v = 0. F by A29, FUNCOP_1:7; ::_thesis: verum
end;
then reconsider L = lc +* (( the carrier of V \ B) --> (0. F)) as Linear_Combination of V by A20, VECTSP_6:def_1;
for v being Element of V st v in Carrier L holds
v in B
proof
let v be Element of V; ::_thesis: ( v in Carrier L implies v in B )
assume A30: v in Carrier L ; ::_thesis: v in B
now__::_thesis:_v_in_B
assume not v in B ; ::_thesis: contradiction
then (lc +* (( the carrier of V \ B) --> (0. F))) . v = 0. F by A28;
hence contradiction by A30, VECTSP_6:2; ::_thesis: verum
end;
hence v in B ; ::_thesis: verum
end;
then Carrier L c= B by SUBSET_1:2;
then L is Linear_Combination of B by VECTSP_6:def_4;
hence ex lc being Linear_Combination of B st
for i being set st i in dom f holds
lc . (Vbf . i) = f . i by A21; ::_thesis: verum
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 ex y being Element of the carrier of (Lin B) st S1[f,y] by A6, A31; ::_thesis: verum
end;
consider G being Function of (n -tuples_on the carrier of F), the carrier of (Lin B) such that
A32: for tup being Element of n -tuples_on the carrier of F holds S1[tup,G . tup] from FUNCT_2:sch_3(A13);
A33: dom G = n -tuples_on the carrier of F by FUNCT_2:def_1;
A34: for L being Linear_Combination of B ex nt being Element of n -tuples_on the carrier of F st
for i being set st i in dom nt holds
nt . i = L . (Vbf . i)
proof
let L be Linear_Combination of B; ::_thesis: ex nt being Element of n -tuples_on the carrier of F st
for i being set st i in dom nt holds
nt . i = L . (Vbf . i)
deffunc H1( set ) -> set = L . (Vbf . $1);
A35: for x being set st x in Seg n holds
H1(x) in the carrier of F
proof
let x be set ; ::_thesis: ( x in Seg n implies H1(x) in the carrier of F )
assume x in Seg n ; ::_thesis: H1(x) in the carrier of F
then Vbf . x in rng Vbf by A12, FUNCT_1:3;
then consider vv being Element of V such that
A36: Vbf . x = vv ;
L . vv in the carrier of F ;
hence H1(x) in the carrier of F by A36; ::_thesis: verum
end;
consider f being Function of (Seg n), the carrier of F such that
A37: for x being set st x in Seg n holds
f . x = H1(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 n -tuples_on the carrier of F by FINSEQ_2:92;
hence ex nt being Element of n -tuples_on the carrier of F st
for i being set st i in dom nt holds
nt . i = L . (Vbf . i) by A37, A38; ::_thesis: verum
end;
for c being set st c in the carrier of (Lin B) holds
ex x being set st
( x in n -tuples_on the carrier of F & c = G . x )
proof
let c be set ; ::_thesis: ( c in the carrier of (Lin B) implies ex x being set st
( x in n -tuples_on the carrier of F & c = G . x ) )
assume c in the carrier of (Lin B) ; ::_thesis: ex x being set st
( x in n -tuples_on the carrier of F & c = G . x )
then c in Lin B by STRUCT_0:def_5;
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 n -tuples_on the carrier of F such that
A43: for i being set 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; ::_thesis: l . v = lc . v
now__::_thesis:_l_._v_=_lc_._v
percases ( v in rng Vbf or not v in rng Vbf ) ;
suppose v in rng Vbf ; ::_thesis: l . v = lc . v
then consider x being set 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 l . v = lc . v by A44, A48, A49; ::_thesis: verum
end;
supposeA50: not v in rng Vbf ; ::_thesis: l . v = lc . v
now__::_thesis:_not_v_in_Carrier_l
assume A51: v in Carrier l ; ::_thesis: contradiction
Carrier l c= rng Vbf by A10, VECTSP_6:def_4;
hence contradiction by A50, A51; ::_thesis: verum
end;
then A52: l . v = 0. F by VECTSP_6:2;
now__::_thesis:_not_v_in_Carrier_lc
assume A53: v in Carrier lc ; ::_thesis: contradiction
Carrier lc c= rng Vbf by A10, VECTSP_6:def_4;
hence contradiction by A50, A53; ::_thesis: verum
end;
hence l . v = lc . v by A52, VECTSP_6:2; ::_thesis: verum
end;
end;
end;
hence l . v = lc . v ; ::_thesis: verum
end;
then G . t = Sum (l (#) Vbf) by A45, VECTSP_6:def_7;
hence ex x being set st
( x in n -tuples_on the carrier of F & c = G . x ) by A41, A42; ::_thesis: verum
end;
then A54: rng G = the carrier of (Lin B) by FUNCT_2:10;
for x1, x2 being set st x1 in dom G & x2 in dom G & G . x1 = G . x2 holds
x1 = x2
proof
let x1, x2 be set ; ::_thesis: ( x1 in dom G & x2 in dom G & G . x1 = G . x2 implies x1 = x2 )
assume that
A55: x1 in dom G and
A56: x2 in dom G and
A57: G . x1 = G . x2 ; ::_thesis: x1 = x2
reconsider t1 = x1 as Element of n -tuples_on the carrier of F by A55;
reconsider t2 = x2 as Element of n -tuples_on the carrier of F 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; ::_thesis: L1 . v = L2 . 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 L1 . v = L2 . v by VECTSP_1:27; ::_thesis: verum
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; ::_thesis: ( k in dom t1 implies t1 . k = t2 . k )
assume A68: k in dom t1 ; ::_thesis: t1 . k = t2 . k
t1 . k = L1 . (Vbf . k) by A58, A68;
hence t1 . k = t2 . k by A60, A65, A66, A67, A68; ::_thesis: verum
end;
hence x1 = x2 by A67, FINSEQ_1:13, FINSEQ_2:124; ::_thesis: verum
end;
then G is one-to-one by FUNCT_1:def_4;
then n -tuples_on the carrier of F,G .: (n -tuples_on the carrier of F) are_equipotent by A33, CARD_1:33;
then A69: n -tuples_on the carrier of F, the carrier of (Lin B) 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 (n -tuples_on the carrier of F) = 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 card the carrier of V = q |^ n by A6, A69, CARD_1:5; ::_thesis: verum
end;
end;
end;
hence card the carrier of V = q |^ n ; ::_thesis: verum
end;
definition
let R be Skew-Field;
func center R -> strict Field means :Def4: :: WEDDWITT:def 4
( 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
ex b1 being strict Field st
( the carrier of b1 = { x where x is Element of R : for s being Element of R holds x * s = s * x } & the addF of b1 = the addF of R || the carrier of b1 & the multF of b1 = the multF of R || the carrier of b1 & 0. b1 = 0. R & 1. b1 = 1. R )
proof
set cR = the carrier of R;
set ccs = { x where x is Element of R : for s being Element of R holds x * s = s * x } ;
now__::_thesis:_for_s_being_Element_of_the_carrier_of_R_holds_(0._R)_*_s_=_s_*_(0._R)
let s be Element of the carrier of R; ::_thesis: (0. R) * s = s * (0. R)
thus (0. R) * s = 0. R by VECTSP_1:7
.= s * (0. R) by VECTSP_1:6 ; ::_thesis: verum
end;
then A1: 0. R in { x where x is Element of R : for s being Element of R holds x * s = s * x } ;
then reconsider ccs = { x where x is Element of R : for s being Element of R holds x * s = s * x } as non empty set ;
A2: ccs c= the carrier of R
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in ccs or x in the carrier of R )
assume x in ccs ; ::_thesis: x in the carrier of R
then ex x9 being Element of the carrier of R st
( x9 = x & ( for s being Element of R holds x9 * s = s * x9 ) ) ;
hence x in the carrier of R ; ::_thesis: verum
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= [: the carrier of R, the carrier of R:]
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in [:ccs,ccs:] or x in [: the carrier of R, the carrier of R:] )
assume x in [:ccs,ccs:] ; ::_thesis: x in [: the carrier of R, the carrier of R:]
then ex a, b being set st
( a in ccs & b in ccs & x = [a,b] ) by ZFMISC_1:def_2;
hence x in [: the carrier of R, the carrier of R:] by A2, ZFMISC_1:def_2; ::_thesis: verum
end;
then reconsider acs = the addF of R || ccs as Function of [:ccs,ccs:], the carrier of R by FUNCT_2:32;
rng acs c= ccs
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng acs or y in ccs )
assume y in rng acs ; ::_thesis: y in ccs
then consider x being set such that
A4: x in dom acs and
A5: y = acs . x by FUNCT_1:def_3;
consider a, b being set such that
A6: a in ccs and
A7: b in ccs and
A8: x = [a,b] by A4, ZFMISC_1:def_2;
reconsider a = a, b = b as Element of the carrier of R by A2, A6, A7;
A9: ex a9 being Element of the carrier of R st
( a9 = a & ( for s being Element of R holds a9 * s = s * a9 ) ) by A6;
A10: ex b9 being Element of the carrier of R 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__::_thesis:_for_s_being_Element_of_the_carrier_of_R_holds_(a_+_b)_*_s_=_s_*_(a_+_b)
let s be Element of the carrier of R; ::_thesis: (a + b) * s = s * (a + b)
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 ; ::_thesis: verum
end;
hence y in ccs by A5, A11; ::_thesis: verum
end;
then reconsider acs = acs as BinOp of ccs by FUNCT_2:6;
reconsider mcs = the multF of R || ccs as Function of [:ccs,ccs:], the carrier of R by A3, FUNCT_2:32;
rng mcs c= ccs
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng mcs or y in ccs )
assume y in rng mcs ; ::_thesis: y in ccs
then consider x being set such that
A12: x in dom mcs and
A13: y = mcs . x by FUNCT_1:def_3;
consider a, b being set such that
A14: a in ccs and
A15: b in ccs and
A16: x = [a,b] by A12, ZFMISC_1:def_2;
reconsider a = a, b = b as Element of the carrier of R by A2, A14, A15;
A17: ex a9 being Element of the carrier of R st
( a9 = a & ( for s being Element of R holds a9 * s = s * a9 ) ) by A14;
A18: ex b9 being Element of the carrier of R 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__::_thesis:_for_s_being_Element_of_the_carrier_of_R_holds_(a_*_b)_*_s_=_s_*_(a_*_b)
let s be Element of the carrier of R; ::_thesis: (a * b) * s = s * (a * b)
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 ; ::_thesis: verum
end;
hence y in ccs by A13, A19; ::_thesis: verum
end;
then reconsider mcs = mcs as BinOp of ccs by FUNCT_2:6;
reconsider Zs = 0. R as Element of ccs by A1;
now__::_thesis:_for_s_being_Element_of_the_carrier_of_R_holds_(1__R)_*_s_=_s_*_(1__R)
let s be Element of the carrier of R; ::_thesis: (1_ R) * s = s * (1_ R)
thus (1_ R) * s = s by VECTSP_1:def_8
.= s * (1_ R) by VECTSP_1:def_4 ; ::_thesis: verum
end;
then 1_ R in ccs ;
then reconsider Us = 1_ R as Element of ccs ;
reconsider cs = doubleLoopStr(# ccs,acs,mcs,Us,Zs #) as non empty doubleLoopStr ;
A20: 0. cs = Zs ;
set ccs1 = the carrier of cs;
A21: now__::_thesis:_for_x,_s_being_Element_of_the_carrier_of_R_st_x_in_ccs_holds_
x_*_s_=_s_*_x
let x, s be Element of the carrier of R; ::_thesis: ( x in ccs implies x * s = s * x )
assume x in ccs ; ::_thesis: x * s = s * x
then ex x9 being Element of the carrier of R st
( x9 = x & ( for s being Element of R holds x9 * s = s * x9 ) ) ;
hence x * s = s * x ; ::_thesis: verum
end;
A22: now__::_thesis:_for_a,_b_being_Element_of_the_carrier_of_R
for_c,_d_being_Element_of_the_carrier_of_cs_st_a_=_c_&_b_=_d_holds_
a_*_b_=_c_*_d
let a, b be Element of the carrier of R; ::_thesis: for c, d being Element of the carrier of cs st a = c & b = d holds
a * b = c * d
let c, d be Element of the carrier of cs; ::_thesis: ( a = c & b = d implies a * b = c * d )
assume that
A23: a = c and
A24: b = d ; ::_thesis: a * b = c * d
[c,d] in [:ccs,ccs:] by ZFMISC_1:def_2;
hence a * b = c * d by A23, A24, FUNCT_1:49; ::_thesis: verum
end;
A25: for a, b being Element of the carrier of R
for c, d being Element of the carrier of cs st a = c & b = d holds
a + b = c + d
proof
let a, b be Element of the carrier of R; ::_thesis: for c, d being Element of the carrier of cs st a = c & b = d holds
a + b = c + d
let c, d be Element of the carrier of cs; ::_thesis: ( a = c & b = d implies a + b = c + d )
assume that
A26: a = c and
A27: b = d ; ::_thesis: a + b = c + d
[c,d] in [:ccs,ccs:] by ZFMISC_1:def_2;
hence a + b = c + d by A26, A27, FUNCT_1:49; ::_thesis: verum
end;
A28: cs is Abelian
proof
let x, y be Element of the carrier of cs; :: according to RLVECT_1:def_2 ::_thesis: x + y = y + x
A29: x in the carrier of cs ;
y in the carrier of cs ;
then reconsider x9 = x, y9 = y as Element of the carrier of R by A2, A29;
thus x + y = y9 + x9 by A25
.= y + x by A25 ; ::_thesis: verum
end;
A30: cs is add-associative
proof
let x, y, z be Element of the carrier of cs; :: according to RLVECT_1:def_3 ::_thesis: (x + y) + z = x + (y + z)
A31: x in the carrier of cs ;
A32: y in the carrier of cs ;
z in the carrier of cs ;
then reconsider x9 = x, y9 = y, z9 = z as Element of the carrier of R by A2, A31, A32;
A33: x9 + y9 = x + y by A25;
A34: y9 + z9 = y + z by A25;
thus (x + y) + z = (x9 + y9) + z9 by A25, A33
.= x9 + (y9 + z9) by RLVECT_1:def_3
.= x + (y + z) by A25, A34 ; ::_thesis: verum
end;
A35: cs is right_zeroed
proof
let x be Element of the carrier of cs; :: according to RLVECT_1:def_4 ::_thesis: x + (0. cs) = x
x in the carrier of cs ;
then reconsider x9 = x as Element of the carrier of R by A2;
thus x + (0. cs) = x9 + (0. R) by A25
.= x by RLVECT_1:def_4 ; ::_thesis: verum
end;
A36: cs is right_complementable
proof
let x be Element of the carrier of cs; :: according to ALGSTR_0:def_16 ::_thesis: x is right_complementable
x in the carrier of cs ;
then reconsider x9 = x as Element of the carrier of R by A2;
consider y9 being Element of the carrier of R such that
A37: x9 + y9 = 0. R by ALGSTR_0:def_11;
now__::_thesis:_for_s_being_Element_of_the_carrier_of_R_holds_y9_*_s_=_s_*_y9
let s be Element of the carrier of R; ::_thesis: y9 * s = s * y9
A38: s * x9 = x9 * s by A21;
(0. R) * s = 0. R by VECTSP_1:7
.= s * (0. R) by VECTSP_1:6 ;
then (x9 * s) + (y9 * s) = s * (x9 + y9) by A37, 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 A38, 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;
hence y9 * s = s * y9 by RLVECT_1:4; ::_thesis: verum
end;
then y9 in the carrier of cs ;
then reconsider y = y9 as Element of the carrier of cs ;
x9 + y9 = x + y by A25;
hence ex y being Element of the carrier of cs st x + y = 0. cs by A37; :: according to ALGSTR_0:def_11 ::_thesis: verum
end;
A39: cs is associative
proof
let x, y, z be Element of the carrier of cs; :: according to GROUP_1:def_3 ::_thesis: (x * y) * z = x * (y * z)
A40: x in the carrier of cs ;
A41: y in the carrier of cs ;
z in the carrier of cs ;
then reconsider x9 = x, y9 = y, z9 = z as Element of the carrier of R by A2, A40, A41;
A42: x9 * y9 = x * y by A22;
A43: y9 * z9 = y * z by A22;
thus (x * y) * z = (x9 * y9) * z9 by A22, A42
.= x9 * (y9 * z9) by GROUP_1:def_3
.= x * (y * z) by A22, A43 ; ::_thesis: verum
end;
A44: cs is commutative
proof
let x, y be Element of the carrier of cs; :: according to GROUP_1:def_12 ::_thesis: x * y = y * x
A45: x in the carrier of cs ;
y in the carrier of cs ;
then reconsider x9 = x, y9 = y as Element of the carrier of R by A2, A45;
thus x * y = x9 * y9 by A22
.= y9 * x9 by A21
.= y * x by A22 ; ::_thesis: verum
end;
A46: now__::_thesis:_for_x,_e_being_Element_of_cs_st_e_=_1__R_holds_
(_x_*_e_=_x_&_e_*_x_=_x_)
let x, e be Element of cs; ::_thesis: ( e = 1_ R implies ( x * e = x & e * x = x ) )
assume A47: e = 1_ R ; ::_thesis: ( x * e = x & e * x = x )
A48: [x,e] in [:ccs,ccs:] by ZFMISC_1:87;
x in ccs ;
then reconsider y = x as Element of R by A2;
thus x * e = y * (1_ R) by A47, A48, FUNCT_1:49
.= x by GROUP_1:def_4 ; ::_thesis: e * x = x
hence e * x = x by A44, GROUP_1:def_12; ::_thesis: verum
end;
A49: cs is well-unital
proof
let x be Element of cs; :: according to VECTSP_1:def_6 ::_thesis: ( x * (1. cs) = x & (1. cs) * x = x )
thus ( x * (1. cs) = x & (1. cs) * x = x ) by A46; ::_thesis: verum
end;
A50: 1. cs = 1. R ;
A51: cs is distributive
proof
let x, y, z be Element of the carrier of cs; :: according to VECTSP_1:def_7 ::_thesis: ( x * (y + z) = (x * y) + (x * z) & (y + z) * x = (y * x) + (z * x) )
A52: x in the carrier of cs ;
A53: y in the carrier of cs ;
z in the carrier of cs ;
then reconsider x9 = x, y9 = y, z9 = z as Element of the carrier of R by A2, A52, A53;
A54: y + z = y9 + z9 by A25;
A55: x9 * y9 = x * y by A22;
A56: x9 * z9 = x * z by A22;
A57: y9 * x9 = y * x by A22;
A58: z9 * x9 = z * x by A22;
thus x * (y + z) = x9 * (y9 + z9) by A22, A54
.= (x9 * y9) + (x9 * z9) by VECTSP_1:def_7
.= (x * y) + (x * z) by A25, A55, A56 ; ::_thesis: (y + z) * x = (y * x) + (z * x)
thus (y + z) * x = (y9 + z9) * x9 by A22, A54
.= (y9 * x9) + (z9 * x9) by VECTSP_1:def_7
.= (y * x) + (z * x) by A25, A57, A58 ; ::_thesis: verum
end;
cs is almost_left_invertible
proof
let x be Element of the carrier of cs; :: according to ALGSTR_0:def_39 ::_thesis: ( x = 0. cs or x is left_invertible )
assume A59: x <> 0. cs ; ::_thesis: x is left_invertible
x in the carrier of cs ;
then reconsider x9 = x as Element of the carrier of R by A2;
consider y9 being Element of the carrier of R such that
A60: y9 * x9 = 1. R by A59, VECTSP_1:def_9;
A61: x9 * y9 = 1. R by A60, VECTSP_2:7;
now__::_thesis:_for_s_being_Element_of_the_carrier_of_R_holds_y9_*_s_=_s_*_y9
let s be Element of the carrier of R; ::_thesis: y9 * s = s * y9
(1_ R) * s = s by VECTSP_1:def_8
.= s * (1_ R) by VECTSP_1:def_4 ;
then (x9 * y9) * s = (s * x9) * y9 by A61, GROUP_1:def_3;
then (x9 * y9) * s = (x9 * s) * y9 by A21;
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 A59, VECTSP_2:9;
then ((1_ R) * y9) * s = ((1_ R) * s) * y9 by A59, VECTSP_2:9;
then y9 * s = ((1_ R) * s) * y9 by VECTSP_1:def_8;
hence y9 * s = s * y9 by VECTSP_1:def_8; ::_thesis: verum
end;
then y9 in the carrier of cs ;
then reconsider y = y9 as Element of the carrier of cs ;
take y ; :: according to ALGSTR_0:def_27 ::_thesis: y * x = 1. cs
thus y * x = 1. cs by A22, A60; ::_thesis: verum
end;
then reconsider cs = cs as strict Field by A20, A28, A30, A35, A36, A39, A44, A49, A50, A51, STRUCT_0:def_8;
take cs ; ::_thesis: ( the carrier of cs = { x where x is Element of R : for s being Element of R holds x * s = s * x } & the addF of cs = the addF of R || the carrier of cs & the multF of cs = the multF of R || the carrier of cs & 0. cs = 0. R & 1. cs = 1. R )
thus ( the carrier of cs = { x where x is Element of R : for s being Element of R holds x * s = s * x } & the addF of cs = the addF of R || the carrier of cs & the multF of cs = the multF of R || the carrier of cs & 0. cs = 0. R & 1. cs = 1. R ) ; ::_thesis: verum
end;
uniqueness
for b1, b2 being strict Field st the carrier of b1 = { x where x is Element of R : for s being Element of R holds x * s = s * x } & the addF of b1 = the addF of R || the carrier of b1 & the multF of b1 = the multF of R || the carrier of b1 & 0. b1 = 0. R & 1. b1 = 1. R & the carrier of b2 = { x where x is Element of R : for s being Element of R holds x * s = s * x } & the addF of b2 = the addF of R || the carrier of b2 & the multF of b2 = the multF of R || the carrier of b2 & 0. b2 = 0. R & 1. b2 = 1. R holds
b1 = b2 ;
end;
:: deftheorem Def4 defines center WEDDWITT:def_4_:_
for R being Skew-Field
for b2 being strict Field holds
( b2 = center R iff ( the carrier of b2 = { x where x is Element of R : for s being Element of R holds x * s = s * x } & the addF of b2 = the addF of R || the carrier of b2 & the multF of b2 = the multF of R || the carrier of b2 & 0. b2 = 0. R & 1. b2 = 1. R ) );
theorem Th16: :: WEDDWITT:16
for R being Skew-Field holds the carrier of (center R) c= the carrier of R
proof
let R be Skew-Field; ::_thesis: the carrier of (center R) c= the carrier of R
for x being set st x in the carrier of (center R) holds
x in the carrier of R
proof
let y be set ; ::_thesis: ( y in the carrier of (center R) implies y in the carrier of R )
assume y in the carrier of (center R) ; ::_thesis: y in the carrier of 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 y in the carrier of R ; ::_thesis: verum
end;
hence the carrier of (center R) c= the carrier of R by TARSKI:def_3; ::_thesis: verum
end;
registration
let R be finite Skew-Field;
cluster center R -> finite strict ;
correctness
coherence
center R is finite ;
proof
the carrier of (center R) c= the carrier of R by Th16;
hence center R is finite ; ::_thesis: verum
end;
end;
theorem Th17: :: WEDDWITT:17
for R being Skew-Field
for y being Element of R holds
( y in center R iff for s being Element of R holds y * s = s * y )
proof
let R be Skew-Field; ::_thesis: for y being Element of R holds
( y in center R iff for s being Element of R holds y * s = s * y )
let y be Element of R; ::_thesis: ( y in center R iff for s being Element of R holds y * s = s * y )
hereby ::_thesis: ( ( for s being Element of R holds y * s = s * y ) implies y in center R )
assume y in center R ; ::_thesis: for s being Element of R holds y * s = s * y
then y in the carrier of (center R) by STRUCT_0:def_5;
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 ; ::_thesis: verum
end;
now__::_thesis:_(_(_for_s_being_Element_of_R_holds_y_*_s_=_s_*_y_)_implies_y_in_center_R_)
assume for s being Element of R holds y * s = s * y ; ::_thesis: y in center R
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 by STRUCT_0:def_5; ::_thesis: verum
end;
hence ( ( for s being Element of R holds y * s = s * y ) implies y in center R ) ; ::_thesis: verum
end;
theorem Th18: :: WEDDWITT:18
for R being Skew-Field holds 0. R in center R
proof
let R be Skew-Field; ::_thesis: 0. R in center R
for s being Element of R holds (0. R) * s = s * (0. R)
proof
let s be Element of R; ::_thesis: (0. R) * s = s * (0. R)
(0. R) * s = 0. R by VECTSP_1:7
.= s * (0. R) by VECTSP_1:6 ;
hence (0. R) * s = s * (0. R) ; ::_thesis: verum
end;
hence 0. R in center R by Th17; ::_thesis: verum
end;
theorem Th19: :: WEDDWITT:19
for R being Skew-Field holds 1_ R in center R
proof
let R be Skew-Field; ::_thesis: 1_ R in center R
for s being Element of R holds (1_ R) * s = s * (1_ R)
proof
let s be Element of R; ::_thesis: (1_ R) * s = s * (1_ R)
(1_ R) * s = s by VECTSP_1:def_8
.= s * (1_ R) by VECTSP_1:def_4 ;
hence (1_ R) * s = s * (1_ R) ; ::_thesis: verum
end;
hence 1_ R in center R by Th17; ::_thesis: verum
end;
theorem Th20: :: WEDDWITT:20
for R being finite Skew-Field holds 1 < card the carrier of (center R)
proof
let R be finite Skew-Field; ::_thesis: 1 < card the carrier of (center R)
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) by STRUCT_0:def_5;
for s being Element of R holds (1. R) * s = s * (1. R)
proof
let s be Element of R; ::_thesis: (1. R) * s = s * (1. R)
s * (1. R) = s by VECTSP_1:def_4
.= (1. R) * s by VECTSP_1:def_8 ;
hence (1. R) * s = s * (1. R) ; ::_thesis: verum
end;
then 1. R in center R by Th17;
then 1. R in the carrier of (center R) by STRUCT_0:def_5;
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 1 < card the carrier of (center R) by XXREAL_0:2; ::_thesis: verum
end;
theorem Th21: :: WEDDWITT:21
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; ::_thesis: ( card the carrier of (center R) = card the carrier of R iff R is commutative )
set X = the carrier of R;
set Y = the carrier of (center R);
hereby ::_thesis: ( R is commutative implies card the carrier of (center R) = card the carrier of R )
assume A1: card the carrier of R = card the carrier of (center R) ; ::_thesis: R is commutative
A2: the carrier of (center R) c= the carrier of R by Th16;
card ( the carrier of R \ the carrier of (center R)) = (card the carrier of R) - (card the carrier of R) by A1, Th16, CARD_2:44;
then the carrier of R \ the carrier of (center R) = {} ;
then the carrier of R c= the carrier of (center R) by XBOOLE_1:37;
then A3: the carrier of R = the carrier of (center R) by A2, XBOOLE_0:def_10;
for x, s being Element of the carrier of R holds x * s = s * x
proof
let x be Element of the carrier of R; ::_thesis: for s being Element of the carrier of R holds x * s = s * x
x in center R by A3, STRUCT_0:def_5;
hence for s being Element of the carrier of R holds x * s = s * x by Th17; ::_thesis: verum
end;
hence R is commutative by GROUP_1:def_12; ::_thesis: verum
end;
now__::_thesis:_(_R_is_commutative_implies_card_the_carrier_of_(center_R)_=_card_the_carrier_of_R_)
assume A4: R is commutative ; ::_thesis: card the carrier of (center R) = card the carrier of R
for x being set st x in the carrier of R holds
x in the carrier of (center R)
proof
let x be set ; ::_thesis: ( x in the carrier of R implies x in the carrier of (center R) )
assume A5: x in the carrier of R ; ::_thesis: x in the carrier of (center R)
for x being Element of the carrier of R holds x is Element of the carrier of (center R)
proof
let x be Element of the carrier of R; ::_thesis: x is Element of the carrier of (center R)
for y being Element of the carrier of R holds x * y = y * x by A4, GROUP_1:def_12;
then x in center R by Th17;
hence x is Element of the carrier of (center R) by STRUCT_0:def_5; ::_thesis: verum
end;
then x is Element of the carrier of (center R) by A5;
hence x in the carrier of (center R) ; ::_thesis: verum
end;
then A6: the carrier of R c= the carrier of (center R) by TARSKI:def_3;
the carrier of (center R) c= the carrier of R by Th16;
hence card the carrier of (center R) = card the carrier of R by A6, XBOOLE_0:def_10; ::_thesis: verum
end;
hence ( R is commutative implies card the carrier of (center R) = card the carrier of R ) ; ::_thesis: verum
end;
theorem Th22: :: WEDDWITT:22
for R being Skew-Field holds the carrier of (center R) = the carrier of (center (MultGroup R)) \/ {(0. R)}
proof
let R be Skew-Field; ::_thesis: the carrier of (center R) = the carrier of (center (MultGroup R)) \/ {(0. R)}
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 set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of (center (MultGroup R)) \/ {(0. R)} or x in the carrier of (center R) )
assume A6: x in the carrier of (center (MultGroup R)) \/ {(0. R)} ; ::_thesis: x in the carrier of (center R)
percases ( x in the carrier of (center (MultGroup R)) or x in {(0. R)} ) by A6, XBOOLE_0:def_3;
supposeA7: x in the carrier of (center (MultGroup R)) ; ::_thesis: x in the carrier of (center R)
then reconsider a = x as Element of (MultGroup R) by A1;
A8: a in center (MultGroup R) by A7, STRUCT_0:def_5;
reconsider a1 = a as Element of R by UNIROOTS:19;
now__::_thesis:_for_b_being_Element_of_R_holds_a1_*_b_=_b_*_a1
let b be Element of R; ::_thesis: a1 * b = b * a1
thus a1 * b = b * a1 ::_thesis: verum
proof
percases ( b in the carrier of (MultGroup R) or b in {(0. R)} ) by A3, XBOOLE_0:def_3;
suppose b in the carrier of (MultGroup R) ; ::_thesis: a1 * b = b * a1
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 ; ::_thesis: verum
end;
suppose b in {(0. R)} ; ::_thesis: a1 * b = b * a1
then A9: b = 0. R by TARSKI:def_1;
hence a1 * b = 0. R by VECTSP_1:6
.= b * a1 by A9, VECTSP_1:7 ;
::_thesis: verum
end;
end;
end;
end;
then a1 in center R by Th17;
hence x in the carrier of (center R) by STRUCT_0:def_5; ::_thesis: verum
end;
suppose x in {(0. R)} ; ::_thesis: x in the carrier of (center R)
then x = 0. R by TARSKI:def_1;
then x in center R by Th18;
hence x in the carrier of (center R) by STRUCT_0:def_5; ::_thesis: verum
end;
end;
end;
the carrier of (center R) c= the carrier of (center (MultGroup R)) \/ {(0. R)}
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of (center R) or x in the carrier of (center (MultGroup R)) \/ {(0. R)} )
assume A10: x in the carrier of (center R) ; ::_thesis: x in the carrier of (center (MultGroup R)) \/ {(0. R)}
then reconsider a = x as Element of (center R) ;
reconsider a1 = a as Element of R by A4, A10;
percases ( a1 = 0. R or a1 <> 0. R ) ;
suppose a1 = 0. R ; ::_thesis: x in the carrier of (center (MultGroup R)) \/ {(0. R)}
then a1 in {(0. R)} by TARSKI:def_1;
hence x in the carrier of (center (MultGroup R)) \/ {(0. R)} by XBOOLE_0:def_3; ::_thesis: verum
end;
suppose a1 <> 0. R ; ::_thesis: x in the carrier of (center (MultGroup R)) \/ {(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__::_thesis:_for_b_being_Element_of_(MultGroup_R)_holds_a2_*_b_=_b_*_a2
let b be Element of (MultGroup R); ::_thesis: a2 * b = b * a2
b in the carrier of (MultGroup R) ;
then reconsider b1 = b as Element of R by A2;
A11: x in center R by A10, STRUCT_0:def_5;
thus a2 * b = a1 * b1 by UNIROOTS:16
.= b1 * a1 by A11, Th17
.= b * a2 by UNIROOTS:16 ; ::_thesis: verum
end;
then a1 in center (MultGroup R) by GROUP_5:77;
then a1 in the carrier of (center (MultGroup R)) by STRUCT_0:def_5;
hence x in the carrier of (center (MultGroup R)) \/ {(0. R)} by XBOOLE_0:def_3; ::_thesis: verum
end;
end;
end;
hence the carrier of (center R) = the carrier of (center (MultGroup R)) \/ {(0. R)} by A5, XBOOLE_0:def_10; ::_thesis: verum
end;
definition
let R be Skew-Field;
let s be Element of R;
A1: 1. R = 1_ R ;
func centralizer s -> strict Skew-Field means :Def5: :: WEDDWITT:def 5
( 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
ex b1 being strict Skew-Field st
( the carrier of b1 = { x where x is Element of R : x * s = s * x } & the addF of b1 = the addF of R || the carrier of b1 & the multF of b1 = the multF of R || the carrier of b1 & 0. b1 = 0. R & 1. b1 = 1. R )
proof
set cR = the carrier of R;
set ccs = { x where x is Element of R : x * s = s * x } ;
(0. R) * s = 0. R by VECTSP_1:7
.= s * (0. R) by VECTSP_1:6 ;
then 0. R in { x where x is Element of R : x * s = s * x } ;
then reconsider ccs = { x where x is Element of R : x * s = s * x } as non empty set ;
A2: ccs c= the carrier of R
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in ccs or x in the carrier of R )
assume x in ccs ; ::_thesis: x in the carrier of R
then ex x9 being Element of the carrier of R st
( x9 = x & x9 * s = s * x9 ) ;
hence x in the carrier of R ; ::_thesis: verum
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= [: the carrier of R, the carrier of R:]
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in [:ccs,ccs:] or x in [: the carrier of R, the carrier of R:] )
assume x in [:ccs,ccs:] ; ::_thesis: x in [: the carrier of R, the carrier of R:]
then ex a, b being set st
( a in ccs & b in ccs & x = [a,b] ) by ZFMISC_1:def_2;
hence x in [: the carrier of R, the carrier of R:] by A2, ZFMISC_1:def_2; ::_thesis: verum
end;
then reconsider acs = the addF of R || ccs as Function of [:ccs,ccs:], the carrier of R by FUNCT_2:32;
rng acs c= ccs
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng acs or y in ccs )
assume y in rng acs ; ::_thesis: y in ccs
then consider x being set such that
A4: x in dom acs and
A5: y = acs . x by FUNCT_1:def_3;
consider a, b being set such that
A6: a in ccs and
A7: b in ccs and
A8: x = [a,b] by A4, ZFMISC_1:def_2;
reconsider a = a, b = b as Element of the carrier of R by A2, A6, A7;
A9: ex a9 being Element of the carrier of R st
( a9 = a & a9 * s = s * a9 ) by A6;
A10: ex b9 being Element of the carrier of R 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 y in ccs by A5, A11; ::_thesis: verum
end;
then reconsider acs = acs as BinOp of ccs by FUNCT_2:6;
reconsider mcs = the multF of R || ccs as Function of [:ccs,ccs:], the carrier of R by A3, FUNCT_2:32;
rng mcs c= ccs
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng mcs or y in ccs )
assume y in rng mcs ; ::_thesis: y in ccs
then consider x being set such that
A12: x in dom mcs and
A13: y = mcs . x by FUNCT_1:def_3;
consider a, b being set such that
A14: a in ccs and
A15: b in ccs and
A16: x = [a,b] by A12, ZFMISC_1:def_2;
reconsider a = a, b = b as Element of the carrier of R by A2, A14, A15;
A17: ex a9 being Element of the carrier of R st
( a9 = a & a9 * s = s * a9 ) by A14;
A18: ex b9 being Element of the carrier of R 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 y in ccs by A13, A19; ::_thesis: verum
end;
then reconsider mcs = mcs as BinOp of ccs by FUNCT_2:6;
(0. R) * s = 0. R by VECTSP_1:7
.= s * (0. R) by VECTSP_1:6 ;
then 0. R in ccs ;
then reconsider Zs = 0. R as Element of ccs ;
(1. R) * s = s by VECTSP_1:def_8
.= s * (1. R) by VECTSP_1:def_4 ;
then 1. R in ccs ;
then reconsider Us = 1. R as Element of ccs ;
reconsider cs = doubleLoopStr(# ccs,acs,mcs,Us,Zs #) as non empty doubleLoopStr ;
A20: 0. cs = Zs ;
A21: 1. cs = Us ;
A22: now__::_thesis:_for_x,_e_being_Element_of_cs_st_e_=_1._R_holds_
(_x_*_e_=_x_&_e_*_x_=_x_)
let x, e be Element of cs; ::_thesis: ( e = 1. R implies ( x * e = x & e * x = x ) )
assume A23: e = 1. R ; ::_thesis: ( x * e = x & e * x = x )
A24: [x,e] in [:ccs,ccs:] by ZFMISC_1:87;
A25: [e,x] in [:ccs,ccs:] by ZFMISC_1:87;
x in ccs ;
then reconsider y = x as Element of R by A2;
thus x * e = y * (1. R) by A23, A24, FUNCT_1:49
.= x by A1, GROUP_1:def_4 ; ::_thesis: e * x = x
thus e * x = (1. R) * y by A23, A25, FUNCT_1:49
.= x by A1, GROUP_1:def_4 ; ::_thesis: verum
end;
A26: cs is well-unital
proof
let x be Element of cs; :: according to VECTSP_1:def_6 ::_thesis: ( x * (1. cs) = x & (1. cs) * x = x )
thus ( x * (1. cs) = x & (1. cs) * x = x ) by A22; ::_thesis: verum
end;
A27: 1. cs = 1. R ;
set ccs1 = the carrier of cs;
A28: now__::_thesis:_for_x_being_Element_of_the_carrier_of_R_st_x_in_ccs_holds_
x_*_s_=_s_*_x
let x be Element of the carrier of R; ::_thesis: ( x in ccs implies x * s = s * x )
assume x in ccs ; ::_thesis: x * s = s * x
then ex x9 being Element of the carrier of R st
( x9 = x & x9 * s = s * x9 ) ;
hence x * s = s * x ; ::_thesis: verum
end;
A29: now__::_thesis:_for_a,_b_being_Element_of_the_carrier_of_R
for_c,_d_being_Element_of_the_carrier_of_cs_st_a_=_c_&_b_=_d_holds_
a_*_b_=_c_*_d
let a, b be Element of the carrier of R; ::_thesis: for c, d being Element of the carrier of cs st a = c & b = d holds
a * b = c * d
let c, d be Element of the carrier of cs; ::_thesis: ( a = c & b = d implies a * b = c * d )
assume that
A30: a = c and
A31: b = d ; ::_thesis: a * b = c * d
[c,d] in [:ccs,ccs:] by ZFMISC_1:def_2;
hence a * b = c * d by A30, A31, FUNCT_1:49; ::_thesis: verum
end;
A32: for a, b being Element of the carrier of R
for c, d being Element of the carrier of cs st a = c & b = d holds
a + b = c + d
proof
let a, b be Element of the carrier of R; ::_thesis: for c, d being Element of the carrier of cs st a = c & b = d holds
a + b = c + d
let c, d be Element of the carrier of cs; ::_thesis: ( a = c & b = d implies a + b = c + d )
assume that
A33: a = c and
A34: b = d ; ::_thesis: a + b = c + d
[c,d] in [:ccs,ccs:] by ZFMISC_1:def_2;
hence a + b = c + d by A33, A34, FUNCT_1:49; ::_thesis: verum
end;
A35: cs is Abelian
proof
let x, y be Element of the carrier of cs; :: according to RLVECT_1:def_2 ::_thesis: x + y = y + x
A36: x in the carrier of cs ;
y in the carrier of cs ;
then reconsider x9 = x, y9 = y as Element of the carrier of R by A2, A36;
thus x + y = y9 + x9 by A32
.= y + x by A32 ; ::_thesis: verum
end;
A37: cs is add-associative
proof
let x, y, z be Element of the carrier of cs; :: according to RLVECT_1:def_3 ::_thesis: (x + y) + z = x + (y + z)
A38: x in the carrier of cs ;
A39: y in the carrier of cs ;
z in the carrier of cs ;
then reconsider x9 = x, y9 = y, z9 = z as Element of the carrier of R by A2, A38, A39;
A40: x9 + y9 = x + y by A32;
A41: y9 + z9 = y + z by A32;
thus (x + y) + z = (x9 + y9) + z9 by A32, A40
.= x9 + (y9 + z9) by RLVECT_1:def_3
.= x + (y + z) by A32, A41 ; ::_thesis: verum
end;
A42: cs is right_zeroed
proof
let x be Element of the carrier of cs; :: according to RLVECT_1:def_4 ::_thesis: x + (0. cs) = x
x in the carrier of cs ;
then reconsider x9 = x as Element of the carrier of R by A2;
thus x + (0. cs) = x9 + (0. R) by A32
.= x by RLVECT_1:def_4 ; ::_thesis: verum
end;
A43: cs is right_complementable
proof
let x be Element of the carrier of cs; :: according to ALGSTR_0:def_16 ::_thesis: x is right_complementable
x in the carrier of cs ;
then reconsider x9 = x as Element of the carrier of R by A2;
consider y9 being Element of the carrier of R such that
A44: x9 + y9 = 0. R by ALGSTR_0:def_11;
A45: s * x9 = x9 * s by A28;
(0. R) * s = 0. R by VECTSP_1:7
.= s * (0. R) by VECTSP_1:6 ;
then (x9 * s) + (y9 * s) = s * (x9 + y9) by A44, 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 A45, 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 the carrier of cs ;
then reconsider y = y9 as Element of the carrier of cs ;
x9 + y9 = x + y by A32;
hence ex y being Element of the carrier of cs st x + y = 0. cs by A44; :: according to ALGSTR_0:def_11 ::_thesis: verum
end;
A46: cs is associative
proof
let x, y, z be Element of the carrier of cs; :: according to GROUP_1:def_3 ::_thesis: (x * y) * z = x * (y * z)
A47: x in the carrier of cs ;
A48: y in the carrier of cs ;
z in the carrier of cs ;
then reconsider x9 = x, y9 = y, z9 = z as Element of the carrier of R by A2, A47, A48;
A49: x9 * y9 = x * y by A29;
A50: y9 * z9 = y * z by A29;
thus (x * y) * z = (x9 * y9) * z9 by A29, A49
.= x9 * (y9 * z9) by GROUP_1:def_3
.= x * (y * z) by A29, A50 ; ::_thesis: verum
end;
A51: cs is distributive
proof
let x, y, z be Element of the carrier of cs; :: according to VECTSP_1:def_7 ::_thesis: ( x * (y + z) = (x * y) + (x * z) & (y + z) * x = (y * x) + (z * x) )
A52: x in the carrier of cs ;
A53: y in the carrier of cs ;
z in the carrier of cs ;
then reconsider x9 = x, y9 = y, z9 = z as Element of the carrier of R by A2, A52, A53;
A54: y + z = y9 + z9 by A32;
A55: x9 * y9 = x * y by A29;
A56: x9 * z9 = x * z by A29;
A57: y9 * x9 = y * x by A29;
A58: z9 * x9 = z * x by A29;
thus x * (y + z) = x9 * (y9 + z9) by A29, A54
.= (x9 * y9) + (x9 * z9) by VECTSP_1:def_7
.= (x * y) + (x * z) by A32, A55, A56 ; ::_thesis: (y + z) * x = (y * x) + (z * x)
thus (y + z) * x = (y9 + z9) * x9 by A29, A54
.= (y9 * x9) + (z9 * x9) by VECTSP_1:def_7
.= (y * x) + (z * x) by A32, A57, A58 ; ::_thesis: verum
end;
A59: cs is almost_left_invertible
proof
let x be Element of the carrier of cs; :: according to ALGSTR_0:def_39 ::_thesis: ( x = 0. cs or x is left_invertible )
assume A60: x <> 0. cs ; ::_thesis: x is left_invertible
x in the carrier of cs ;
then reconsider x9 = x as Element of the carrier of R by A2;
consider y9 being Element of the carrier of R such that
A61: y9 * x9 = 1. R by A60, VECTSP_1:def_9;
A62: x9 * y9 = 1. R by A61, VECTSP_2:7;
(1. R) * s = s by VECTSP_1:def_8
.= s * (1. R) by VECTSP_1:def_4 ;
then (x9 * y9) * s = (s * x9) * y9 by A62, GROUP_1:def_3;
then (x9 * y9) * s = (x9 * s) * y9 by A28;
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 A60, VECTSP_2:9;
then ((1_ R) * y9) * s = ((1_ R) * s) * y9 by A60, VECTSP_2:9;
then y9 * s = ((1_ R) * s) * y9 by VECTSP_1:def_8;
then y9 * s = s * y9 by VECTSP_1:def_8;
then y9 in the carrier of cs ;
then reconsider y = y9 as Element of the carrier of cs ;
take y ; :: according to ALGSTR_0:def_27 ::_thesis: y * x = 1. cs
thus y * x = 1. cs by A29, A61; ::_thesis: verum
end;
not cs is degenerated by A20, A27, STRUCT_0:def_8;
hence ex b1 being strict Skew-Field st
( the carrier of b1 = { x where x is Element of R : x * s = s * x } & the addF of b1 = the addF of R || the carrier of b1 & the multF of b1 = the multF of R || the carrier of b1 & 0. b1 = 0. R & 1. b1 = 1. R ) by A20, A21, A26, A35, A37, A42, A43, A46, A51, A59; ::_thesis: verum
end;
uniqueness
for b1, b2 being strict Skew-Field st the carrier of b1 = { x where x is Element of R : x * s = s * x } & the addF of b1 = the addF of R || the carrier of b1 & the multF of b1 = the multF of R || the carrier of b1 & 0. b1 = 0. R & 1. b1 = 1. R & the carrier of b2 = { x where x is Element of R : x * s = s * x } & the addF of b2 = the addF of R || the carrier of b2 & the multF of b2 = the multF of R || the carrier of b2 & 0. b2 = 0. R & 1. b2 = 1. R holds
b1 = b2 ;
end;
:: deftheorem Def5 defines centralizer WEDDWITT:def_5_:_
for R being Skew-Field
for s being Element of R
for b3 being strict Skew-Field holds
( b3 = centralizer s iff ( the carrier of b3 = { x where x is Element of R : x * s = s * x } & the addF of b3 = the addF of R || the carrier of b3 & the multF of b3 = the multF of R || the carrier of b3 & 0. b3 = 0. R & 1. b3 = 1. R ) );
theorem Th23: :: WEDDWITT:23
for R being Skew-Field
for s being Element of R holds the carrier of (centralizer s) c= the carrier of R
proof
let R be Skew-Field; ::_thesis: for s being Element of R holds the carrier of (centralizer s) c= the carrier of R
let s be Element of R; ::_thesis: the carrier of (centralizer s) c= the carrier of R
set cs = centralizer s;
set ccs = the carrier of (centralizer s);
A1: the carrier of (centralizer s) = { x where x is Element of R : x * s = s * x } by Def5;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of (centralizer s) or x in the carrier of R )
assume x in the carrier of (centralizer s) ; ::_thesis: x in the carrier of R
then ex a being Element of R st
( a = x & a * s = s * a ) by A1;
hence x in the carrier of R ; ::_thesis: verum
end;
theorem Th24: :: WEDDWITT:24
for R being Skew-Field
for s, a being Element of R holds
( a in the carrier of (centralizer s) iff a * s = s * a )
proof
let R be Skew-Field; ::_thesis: for s, a being Element of R holds
( a in the carrier of (centralizer s) iff a * s = s * a )
let s, a be Element of R; ::_thesis: ( a in the carrier of (centralizer s) iff a * s = s * a )
set cs = centralizer s;
set ccs = the carrier of (centralizer s);
A1: the carrier of (centralizer s) = { x where x is Element of R : x * s = s * x } by Def5;
hereby ::_thesis: ( a * s = s * a implies a in the carrier of (centralizer s) )
assume a in the carrier of (centralizer s) ; ::_thesis: a * s = s * a
then ex x being Element of R st
( a = x & x * s = s * x ) by A1;
hence a * s = s * a ; ::_thesis: verum
end;
assume a * s = s * a ; ::_thesis: a in the carrier of (centralizer s)
hence a in the carrier of (centralizer s) by A1; ::_thesis: verum
end;
theorem :: WEDDWITT:25
for R being Skew-Field
for s being Element of R holds the carrier of (center R) c= the carrier of (centralizer s)
proof
let R be Skew-Field; ::_thesis: for s being Element of R holds the carrier of (center R) c= the carrier of (centralizer s)
let s be Element of R; ::_thesis: the carrier of (center R) c= the carrier of (centralizer s)
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of (center R) or x in the carrier of (centralizer s) )
assume A1: x in the carrier of (center R) ; ::_thesis: x in the carrier of (centralizer s)
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, STRUCT_0:def_5;
then a * s = s * a by Th17;
hence x in the carrier of (centralizer s) by Th24; ::_thesis: verum
end;
theorem Th26: :: WEDDWITT:26
for R being Skew-Field
for s, a, b being 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; ::_thesis: for s, a, b being 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)
let s, a, b be Element of R; ::_thesis: ( a in the carrier of (center R) & b in the carrier of (centralizer s) implies a * b in the carrier of (centralizer s) )
assume that
A1: a in the carrier of (center R) and
A2: b in the carrier of (centralizer s) ; ::_thesis: a * b in the carrier of (centralizer s)
set cs = centralizer s;
set ccs = the carrier of (centralizer s);
A3: the carrier of (centralizer s) = { x where x is Element of R : x * s = s * x } by Def5;
A4: a in center R by A1, STRUCT_0:def_5;
(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 a * b in the carrier of (centralizer s) by A3; ::_thesis: verum
end;
theorem Th27: :: WEDDWITT:27
for R being Skew-Field
for s being Element of R holds
( 0. R is Element of (centralizer s) & 1_ R is Element of (centralizer s) )
proof
let R be Skew-Field; ::_thesis: for s being Element of R holds
( 0. R is Element of (centralizer s) & 1_ R is Element of (centralizer s) )
let s be Element of R; ::_thesis: ( 0. R is Element of (centralizer s) & 1_ R is Element of (centralizer s) )
A1: 0. R = 0. (centralizer s) by Def5;
1. (centralizer s) = 1_ R by Def5;
hence ( 0. R is Element of (centralizer s) & 1_ R is Element of (centralizer s) ) by A1; ::_thesis: verum
end;
registration
let R be finite Skew-Field;
let s be Element of R;
cluster centralizer s -> finite strict ;
correctness
coherence
centralizer s is finite ;
by Th23, FINSET_1:1;
end;
theorem Th28: :: WEDDWITT:28
for R being finite Skew-Field
for s being Element of R holds 1 < card the carrier of (centralizer s)
proof
let R be finite Skew-Field; ::_thesis: for s being Element of R holds 1 < card the carrier of (centralizer s)
let s be Element of R; ::_thesis: 1 < card the carrier of (centralizer s)
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 1 < card the carrier of (centralizer s) by XXREAL_0:2; ::_thesis: verum
end;
theorem Th29: :: WEDDWITT:29
for R being Skew-Field
for s being Element of R
for 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; ::_thesis: for s being Element of R
for t being Element of (MultGroup R) st t = s holds
the carrier of (centralizer s) = the carrier of (Centralizer t) \/ {(0. R)}
let s be Element of R; ::_thesis: for t being Element of (MultGroup R) st t = s holds
the carrier of (centralizer s) = the carrier of (Centralizer t) \/ {(0. R)}
let t be Element of (MultGroup R); ::_thesis: ( t = s implies the carrier of (centralizer s) = the carrier of (Centralizer t) \/ {(0. R)} )
assume A1: t = s ; ::_thesis: the carrier of (centralizer s) = the carrier of (Centralizer t) \/ {(0. R)}
set ct = Centralizer t;
set cs = centralizer s;
set cct = the carrier of (Centralizer t);
set ccs = the carrier of (centralizer s);
A2: the carrier of (MultGroup R) = NonZero R by UNIROOTS:def_1;
A3: the carrier of (Centralizer t) = { b where b is Element of (MultGroup R) : t * b = b * t } by Def1;
A4: the carrier of (centralizer s) = { x where x is Element of R : x * s = s * x } by Def5;
now__::_thesis:_for_x_being_set_holds_
(_(_x_in_the_carrier_of_(centralizer_s)_implies_x_in_the_carrier_of_(Centralizer_t)_\/_{(0._R)}_)_&_(_x_in_the_carrier_of_(Centralizer_t)_\/_{(0._R)}_implies_x_in_the_carrier_of_(centralizer_s)_)_)
let x be set ; ::_thesis: ( ( x in the carrier of (centralizer s) implies x in the carrier of (Centralizer t) \/ {(0. R)} ) & ( x in the carrier of (Centralizer t) \/ {(0. R)} implies b1 in the carrier of (centralizer s) ) )
hereby ::_thesis: ( x in the carrier of (Centralizer t) \/ {(0. R)} implies b1 in the carrier of (centralizer s) )
assume x in the carrier of (centralizer s) ; ::_thesis: x in the carrier of (Centralizer t) \/ {(0. R)}
then consider c being Element of R such that
A5: c = x and
A6: c * s = s * c by A4;
percases ( c = 0. R or c <> 0. R ) ;
suppose c = 0. R ; ::_thesis: x in the carrier of (Centralizer t) \/ {(0. R)}
then c in {(0. R)} by TARSKI:def_1;
hence x in the carrier of (Centralizer t) \/ {(0. R)} by A5, XBOOLE_0:def_3; ::_thesis: verum
end;
suppose c <> 0. R ; ::_thesis: x in the carrier of (Centralizer t) \/ {(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 the carrier of (Centralizer t) by A3;
hence x in the carrier of (Centralizer t) \/ {(0. R)} by A5, XBOOLE_0:def_3; ::_thesis: verum
end;
end;
end;
assume A7: x in the carrier of (Centralizer t) \/ {(0. R)} ; ::_thesis: b1 in the carrier of (centralizer s)
percases ( x in the carrier of (Centralizer t) or x in {(0. R)} ) by A7, XBOOLE_0:def_3;
suppose x in the carrier of (Centralizer t) ; ::_thesis: b1 in the carrier of (centralizer s)
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 the carrier of (centralizer s) by A4, A8; ::_thesis: verum
end;
suppose x in {(0. R)} ; ::_thesis: b1 in the carrier of (centralizer s)
then A10: x = 0. R by TARSKI:def_1;
(0. R) * s = 0. R by VECTSP_1:7
.= s * (0. R) by VECTSP_1:6 ;
hence x in the carrier of (centralizer s) by A4, A10; ::_thesis: verum
end;
end;
end;
hence the carrier of (centralizer s) = the carrier of (Centralizer t) \/ {(0. R)} by TARSKI:1; ::_thesis: verum
end;
theorem Th30: :: WEDDWITT:30
for R being finite Skew-Field
for s being Element of R
for 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; ::_thesis: for s being Element of R
for t being Element of (MultGroup R) st t = s holds
card (Centralizer t) = (card the carrier of (centralizer s)) - 1
let s be Element of R; ::_thesis: for t being Element of (MultGroup R) st t = s holds
card (Centralizer t) = (card the carrier of (centralizer s)) - 1
let t be Element of (MultGroup R); ::_thesis: ( t = s implies card (Centralizer t) = (card the carrier of (centralizer s)) - 1 )
assume A1: t = s ; ::_thesis: card (Centralizer t) = (card the carrier of (centralizer s)) - 1
set ct = Centralizer t;
set cs = centralizer s;
set cct = the carrier of (Centralizer t);
set ccs = the carrier of (centralizer s);
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 by STRUCT_0:def_5;
then not 0. R in Centralizer t by Th7;
then A2: not 0. R in the carrier of (Centralizer t) by STRUCT_0:def_5;
the carrier of (Centralizer t) \/ {(0. R)} = the carrier of (centralizer s) by A1, Th29;
then card the carrier of (centralizer s) = (card the carrier of (Centralizer t)) + 1 by A2, CARD_2:41;
hence card (Centralizer t) = (card the carrier of (centralizer s)) - 1 ; ::_thesis: verum
end;
begin
definition
let R be Skew-Field;
func VectSp_over_center R -> strict VectSp of center R means :Def6: :: WEDDWITT:def 6
( addLoopStr(# the carrier of it, the addF of it, the ZeroF of it #) = addLoopStr(# the carrier of R, the addF of R, the ZeroF of R #) & the lmult of it = the multF of R | [: the carrier of (center R), the carrier of R:] );
existence
ex b1 being strict VectSp of center R st
( addLoopStr(# the carrier of b1, the addF of b1, the ZeroF of b1 #) = addLoopStr(# the carrier of R, the addF of R, the ZeroF of R #) & the lmult of b1 = the multF of R | [: the carrier of (center R), the carrier of R:] )
proof
set cR = center R;
set ccR = the carrier of (center R);
set ccs = the carrier of R;
set lm = the multF of R | [: the carrier of (center R), the carrier of R:];
A1: the carrier of (center R) 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;
[: the carrier of (center R), the carrier of R:] c= [: the carrier of R, the carrier of R:]
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in [: the carrier of (center R), the carrier of R:] or x in [: the carrier of R, the carrier of R:] )
assume x in [: the carrier of (center R), the carrier of R:] ; ::_thesis: x in [: the carrier of R, the carrier of R:]
then ex x1, x2 being set st
( x1 in the carrier of (center R) & x2 in the carrier of R & x = [x1,x2] ) by ZFMISC_1:def_2;
hence x in [: the carrier of R, the carrier of R:] by A1, ZFMISC_1:def_2; ::_thesis: verum
end;
then A3: dom ( the multF of R | [: the carrier of (center R), the carrier of R:]) = [: the carrier of (center R), the carrier of R:] by A2, RELAT_1:62;
now__::_thesis:_for_x_being_set_st_x_in_[:_the_carrier_of_(center_R),_the_carrier_of_R:]_holds_
(_the_multF_of_R_|_[:_the_carrier_of_(center_R),_the_carrier_of_R:])_._x_in_the_carrier_of_R
let x be set ; ::_thesis: ( x in [: the carrier of (center R), the carrier of R:] implies ( the multF of R | [: the carrier of (center R), the carrier of R:]) . x in the carrier of R )
assume A4: x in [: the carrier of (center R), the carrier of R:] ; ::_thesis: ( the multF of R | [: the carrier of (center R), the carrier of R:]) . x in the carrier of R
then consider x1, x2 being set such that
A5: x1 in the carrier of (center R) and
A6: x2 in the carrier of R and
A7: x = [x1,x2] by ZFMISC_1:def_2;
reconsider x1 = x1 as Element of R by A1, A5;
reconsider x2 = x2 as Element of R by A6;
( the multF of R | [: the carrier of (center R), the carrier of R:]) . x = x1 * x2 by A4, A7, FUNCT_1:49;
hence ( the multF of R | [: the carrier of (center R), the carrier of R:]) . x in the carrier of R ; ::_thesis: verum
end;
then reconsider lm = the multF of R | [: the carrier of (center R), the carrier of R:] as Function of [: the carrier of (center R), the carrier of R:], the carrier of R by A3, FUNCT_2:3;
set Vos = VectSpStr(# the carrier of R, the addF of R,(0. R),lm #);
set cV = the carrier of VectSpStr(# the carrier of R, the addF of R,(0. R),lm #);
A8: ( VectSpStr(# the carrier of R, the addF of R,(0. R),lm #) is vector-distributive & VectSpStr(# the carrier of R, the addF of R,(0. R),lm #) is scalar-distributive & VectSpStr(# the carrier of R, the addF of R,(0. R),lm #) is scalar-associative & VectSpStr(# the carrier of R, the addF of R,(0. R),lm #) is scalar-unital )
proof
A9: the multF of (center R) = the multF of R || the carrier of (center R) by Def4;
A10: the addF of (center R) = the addF of R || the carrier of (center R) by Def4;
thus VectSpStr(# the carrier of R, the addF of R,(0. R),lm #) is vector-distributive ::_thesis: ( VectSpStr(# the carrier of R, the addF of R,(0. R),lm #) is scalar-distributive & VectSpStr(# the carrier of R, the addF of R,(0. R),lm #) is scalar-associative & VectSpStr(# the carrier of R, the addF of R,(0. R),lm #) is scalar-unital )
proof
let x be Element of the carrier of (center R); :: according to VECTSP_1:def_14 ::_thesis: for b1, b2 being Element of the carrier of VectSpStr(# the carrier of R, the addF of R,(0. R),lm #) holds x * (b1 + b2) = (x * b1) + (x * b2)
let v, w be Element of the carrier of VectSpStr(# the carrier of R, the addF of R,(0. R),lm #); ::_thesis: x * (v + w) = (x * v) + (x * w)
x in the carrier of (center R) ;
then reconsider xx = x as Element of R by A1;
reconsider vv = v, ww = w as Element of R ;
A11: [x,w] in [: the carrier of (center R), the carrier of R:] by ZFMISC_1:def_2;
A12: [x,(v + w)] in [: the carrier of (center R), the carrier of R:] by ZFMISC_1:def_2;
A13: [x,v] in [: the carrier of (center R), the carrier of R:] 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 ; ::_thesis: verum
end;
thus VectSpStr(# the carrier of R, the addF of R,(0. R),lm #) is scalar-distributive ::_thesis: ( VectSpStr(# the carrier of R, the addF of R,(0. R),lm #) is scalar-associative & VectSpStr(# the carrier of R, the addF of R,(0. R),lm #) is scalar-unital )
proof
let x, y be Element of the carrier of (center R); :: according to VECTSP_1:def_15 ::_thesis: for b1 being Element of the carrier of VectSpStr(# the carrier of R, the addF of R,(0. R),lm #) holds (x + y) * b1 = (x * b1) + (y * b1)
let v be Element of the carrier of VectSpStr(# the carrier of R, the addF of R,(0. R),lm #); ::_thesis: (x + y) * v = (x * v) + (y * v)
A14: x in the carrier of (center R) ;
y in the carrier of (center R) ;
then reconsider xx = x, yy = y as Element of R by A1, A14;
reconsider vv = v as Element of R ;
A15: [y,v] in [: the carrier of (center R), the carrier of R:] by ZFMISC_1:def_2;
A16: [x,v] in [: the carrier of (center R), the carrier of R:] by ZFMISC_1:def_2;
A17: [(x + y),v] in [: the carrier of (center R), the carrier of R:] by ZFMISC_1:def_2;
A18: [x,y] in [: the carrier of (center R), the carrier of (center R):] by ZFMISC_1:def_2;
thus (x + y) * v = the multF of R . [( the addF of (center R) . [x,y]),vv] by A17, FUNCT_1:49
.= (xx + yy) * vv by A10, A18, 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 A16, FUNCT_1:49
.= (x * v) + (y * v) by A15, FUNCT_1:49 ; ::_thesis: verum
end;
thus VectSpStr(# the carrier of R, the addF of R,(0. R),lm #) is scalar-associative ::_thesis: VectSpStr(# the carrier of R, the addF of R,(0. R),lm #) is scalar-unital
proof
let x, y be Element of the carrier of (center R); :: according to VECTSP_1:def_16 ::_thesis: for b1 being Element of the carrier of VectSpStr(# the carrier of R, the addF of R,(0. R),lm #) holds (x * y) * b1 = x * (y * b1)
let v be Element of the carrier of VectSpStr(# the carrier of R, the addF of R,(0. R),lm #); ::_thesis: (x * y) * v = x * (y * v)
A19: x in the carrier of (center R) ;
y in the carrier of (center R) ;
then reconsider xx = x, yy = y as Element of R by A1, A19;
reconsider vv = v as Element of R ;
A20: [x,(y * v)] in [: the carrier of (center R), the carrier of R:] by ZFMISC_1:def_2;
A21: [y,v] in [: the carrier of (center R), the carrier of R:] by ZFMISC_1:def_2;
A22: [(x * y),v] in [: the carrier of (center R), the carrier of R:] by ZFMISC_1:def_2;
A23: [x,y] in [: the carrier of (center R), the carrier of (center R):] by ZFMISC_1:def_2;
thus (x * y) * v = the multF of R . [( the multF of (center R) . (x,y)),vv] by A22, FUNCT_1:49
.= (xx * yy) * vv by A9, A23, FUNCT_1:49
.= xx * (yy * vv) by GROUP_1:def_3
.= the multF of R . [xx,(lm . (y,v))] by A21, FUNCT_1:49
.= x * (y * v) by A20, FUNCT_1:49 ; ::_thesis: verum
end;
let v be Element of the carrier of VectSpStr(# the carrier of R, the addF of R,(0. R),lm #); :: according to VECTSP_1:def_17 ::_thesis: (1. (center R)) * v = v
reconsider vv = v as Element of R ;
1_ R in center R by Th19;
then 1_ R in the carrier of (center R) by STRUCT_0:def_5;
then A24: [(1_ R),vv] in [: the carrier of (center R), the carrier of R:] by ZFMISC_1:def_2;
thus (1. (center R)) * v = lm . ((1. R),vv) by Def4
.= (1. R) * vv by A24, FUNCT_1:49
.= v by VECTSP_1:def_8 ; ::_thesis: verum
end;
A25: VectSpStr(# the carrier of R, the addF of R,(0. R),lm #) is add-associative
proof
let u, v, w be Element of the carrier of VectSpStr(# the carrier of R, the addF of R,(0. R),lm #); :: according to RLVECT_1:def_3 ::_thesis: (u + v) + w = u + (v + w)
reconsider uu = u, vv = v, ww = w as Element of the carrier of R ;
thus (u + v) + w = (uu + vv) + ww
.= uu + (vv + ww) by RLVECT_1:def_3
.= u + (v + w) ; ::_thesis: verum
end;
A26: VectSpStr(# the carrier of R, the addF of R,(0. R),lm #) is right_zeroed
proof
let v be Element of the carrier of VectSpStr(# the carrier of R, the addF of R,(0. R),lm #); :: according to RLVECT_1:def_4 ::_thesis: v + (0. VectSpStr(# the carrier of R, the addF of R,(0. R),lm #)) = v
reconsider vv = v as Element of the carrier of R ;
thus v + (0. VectSpStr(# the carrier of R, the addF of R,(0. R),lm #)) = vv + (0. R)
.= v by RLVECT_1:def_4 ; ::_thesis: verum
end;
A27: VectSpStr(# the carrier of R, the addF of R,(0. R),lm #) is right_complementable
proof
let v be Element of the carrier of VectSpStr(# the carrier of R, the addF of R,(0. R),lm #); :: according to ALGSTR_0:def_16 ::_thesis: v is right_complementable
reconsider vv = v as Element of the carrier of R ;
consider ww being Element of the carrier of R such that
A28: vv + ww = 0. R by ALGSTR_0:def_11;
reconsider w = ww as Element of the carrier of VectSpStr(# the carrier of R, the addF of R,(0. R),lm #) ;
v + w = 0. VectSpStr(# the carrier of R, the addF of R,(0. R),lm #) by A28;
hence ex w being Element of the carrier of VectSpStr(# the carrier of R, the addF of R,(0. R),lm #) st v + w = 0. VectSpStr(# the carrier of R, the addF of R,(0. R),lm #) ; :: according to ALGSTR_0:def_11 ::_thesis: verum
end;
VectSpStr(# the carrier of R, the addF of R,(0. R),lm #) is Abelian
proof
let v, w be Element of the carrier of VectSpStr(# the carrier of R, the addF of R,(0. R),lm #); :: according to RLVECT_1:def_2 ::_thesis: v + w = w + v
reconsider vv = v, ww = w as Element of the carrier of R ;
thus v + w = ww + vv by RLVECT_1:2
.= w + v ; ::_thesis: verum
end;
hence ex b1 being strict VectSp of center R st
( addLoopStr(# the carrier of b1, the addF of b1, the ZeroF of b1 #) = addLoopStr(# the carrier of R, the addF of R, the ZeroF of R #) & the lmult of b1 = the multF of R | [: the carrier of (center R), the carrier of R:] ) by A8, A25, A26, A27; ::_thesis: verum
end;
uniqueness
for b1, b2 being strict VectSp of center R st addLoopStr(# the carrier of b1, the addF of b1, the ZeroF of b1 #) = addLoopStr(# the carrier of R, the addF of R, the ZeroF of R #) & the lmult of b1 = the multF of R | [: the carrier of (center R), the carrier of R:] & addLoopStr(# the carrier of b2, the addF of b2, the ZeroF of b2 #) = addLoopStr(# the carrier of R, the addF of R, the ZeroF of R #) & the lmult of b2 = the multF of R | [: the carrier of (center R), the carrier of R:] holds
b1 = b2 ;
end;
:: deftheorem Def6 defines VectSp_over_center WEDDWITT:def_6_:_
for R being Skew-Field
for b2 being strict VectSp of center R holds
( b2 = VectSp_over_center R iff ( addLoopStr(# the carrier of b2, the addF of b2, the ZeroF of b2 #) = addLoopStr(# the carrier of R, the addF of R, the ZeroF of R #) & the lmult of b2 = the multF of R | [: the carrier of (center R), the carrier of R:] ) );
theorem Th31: :: WEDDWITT:31
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; ::_thesis: card the carrier of R = (card the carrier of (center R)) |^ (dim (VectSp_over_center R))
set vR = VectSp_over_center R;
A1: addLoopStr(# the carrier of (VectSp_over_center R), the addF of (VectSp_over_center R), the ZeroF of (VectSp_over_center R) #) = addLoopStr(# the carrier of R, the addF of R, the ZeroF of R #) by Def6;
set B = the Basis of VectSp_over_center R;
the Basis of VectSp_over_center R is finite by A1;
then VectSp_over_center R is finite-dimensional by MATRLIN:def_1;
hence card the carrier of R = (card the carrier of (center R)) |^ (dim (VectSp_over_center R)) by A1, Th15; ::_thesis: verum
end;
theorem Th32: :: WEDDWITT:32
for R being finite Skew-Field holds 0 < dim (VectSp_over_center R)
proof
let R be finite Skew-Field; ::_thesis: 0 < dim (VectSp_over_center R)
set q = card the carrier of (center R);
set n = dim (VectSp_over_center R);
set Rs = MultGroup R;
card R = (card the carrier of (center R)) |^ (dim (VectSp_over_center R)) by Th31;
then A1: card (MultGroup R) = ((card the carrier of (center R)) |^ (dim (VectSp_over_center R))) - 1 by UNIROOTS:18;
now__::_thesis:_not_dim_(VectSp_over_center_R)_=_0
assume A2: dim (VectSp_over_center R) = 0 ; ::_thesis: contradiction
(card the carrier of (center R)) |^ (dim (VectSp_over_center R)) = (card the carrier of (center R)) #Z (dim (VectSp_over_center R)) by PREPOWER:36;
then card (MultGroup R) = 1 - 1 by A1, A2, PREPOWER:34;
hence contradiction by GROUP_1:45; ::_thesis: verum
end;
hence 0 < dim (VectSp_over_center R) ; ::_thesis: verum
end;
definition
let R be Skew-Field;
let s be Element of R;
func VectSp_over_center s -> strict VectSp of center R means :Def7: :: WEDDWITT:def 7
( addLoopStr(# the carrier of it, the addF of it, the ZeroF of it #) = addLoopStr(# the carrier of (centralizer s), the addF of (centralizer s), the ZeroF of (centralizer s) #) & the lmult of it = the multF of R | [: the carrier of (center R), the carrier of (centralizer s):] );
existence
ex b1 being strict VectSp of center R st
( addLoopStr(# the carrier of b1, the addF of b1, the ZeroF of b1 #) = addLoopStr(# the carrier of (centralizer s), the addF of (centralizer s), the ZeroF of (centralizer s) #) & the lmult of b1 = the multF of R | [: the carrier of (center R), the carrier of (centralizer s):] )
proof
set cR = center R;
set ccR = the carrier of (center R);
set cs = centralizer s;
set ccs = the carrier of (centralizer s);
set lm = the multF of R | [: the carrier of (center R), the carrier of (centralizer s):];
A1: the carrier of (center R) c= the carrier of R by Th16;
A2: the carrier of (centralizer s) 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;
[: the carrier of (center R), the carrier of (centralizer s):] c= [: the carrier of R, the carrier of R:]
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in [: the carrier of (center R), the carrier of (centralizer s):] or x in [: the carrier of R, the carrier of R:] )
assume x in [: the carrier of (center R), the carrier of (centralizer s):] ; ::_thesis: x in [: the carrier of R, the carrier of R:]
then ex x1, x2 being set st
( x1 in the carrier of (center R) & x2 in the carrier of (centralizer s) & x = [x1,x2] ) by ZFMISC_1:def_2;
hence x in [: the carrier of R, the carrier of R:] by A1, A2, ZFMISC_1:def_2; ::_thesis: verum
end;
then A4: dom ( the multF of R | [: the carrier of (center R), the carrier of (centralizer s):]) = [: the carrier of (center R), the carrier of (centralizer s):] by A3, RELAT_1:62;
now__::_thesis:_for_x_being_set_st_x_in_[:_the_carrier_of_(center_R),_the_carrier_of_(centralizer_s):]_holds_
(_the_multF_of_R_|_[:_the_carrier_of_(center_R),_the_carrier_of_(centralizer_s):])_._x_in_the_carrier_of_(centralizer_s)
let x be set ; ::_thesis: ( x in [: the carrier of (center R), the carrier of (centralizer s):] implies ( the multF of R | [: the carrier of (center R), the carrier of (centralizer s):]) . x in the carrier of (centralizer s) )
assume A5: x in [: the carrier of (center R), the carrier of (centralizer s):] ; ::_thesis: ( the multF of R | [: the carrier of (center R), the carrier of (centralizer s):]) . x in the carrier of (centralizer s)
then consider x1, x2 being set such that
A6: x1 in the carrier of (center R) and
A7: x2 in the carrier of (centralizer s) and
A8: x = [x1,x2] by ZFMISC_1:def_2;
reconsider x1 = x1 as Element of R by A1, A6;
reconsider x2 = x2 as Element of R by A2, A7;
( the multF of R | [: the carrier of (center R), the carrier of (centralizer s):]) . x = x1 * x2 by A5, A8, FUNCT_1:49;
hence ( the multF of R | [: the carrier of (center R), the carrier of (centralizer s):]) . x in the carrier of (centralizer s) by A6, A7, Th26; ::_thesis: verum
end;
then reconsider lm = the multF of R | [: the carrier of (center R), the carrier of (centralizer s):] as Function of [: the carrier of (center R), the carrier of (centralizer s):], the carrier of (centralizer s) by A4, FUNCT_2:3;
set Vos = VectSpStr(# the carrier of (centralizer s), the addF of (centralizer s),(0. (centralizer s)),lm #);
set cV = the carrier of VectSpStr(# the carrier of (centralizer s), the addF of (centralizer s),(0. (centralizer s)),lm #);
set aV = the addF of VectSpStr(# the carrier of (centralizer s), the addF of (centralizer s),(0. (centralizer s)),lm #);
A9: ( VectSpStr(# the carrier of (centralizer s), the addF of (centralizer s),(0. (centralizer s)),lm #) is vector-distributive & VectSpStr(# the carrier of (centralizer s), the addF of (centralizer s),(0. (centralizer s)),lm #) is scalar-distributive & VectSpStr(# the carrier of (centralizer s), the addF of (centralizer s),(0. (centralizer s)),lm #) is scalar-associative & VectSpStr(# the carrier of (centralizer s), the addF of (centralizer s),(0. (centralizer s)),lm #) is scalar-unital )
proof
A10: the multF of (center R) = the multF of R || the carrier of (center R) by Def4;
A11: the addF of (center R) = the addF of R || the carrier of (center R) by Def4;
A12: the addF of (centralizer s) = the addF of R || the carrier of (centralizer s) by Def5;
thus VectSpStr(# the carrier of (centralizer s), the addF of (centralizer s),(0. (centralizer s)),lm #) is vector-distributive ::_thesis: ( VectSpStr(# the carrier of (centralizer s), the addF of (centralizer s),(0. (centralizer s)),lm #) is scalar-distributive & VectSpStr(# the carrier of (centralizer s), the addF of (centralizer s),(0. (centralizer s)),lm #) is scalar-associative & VectSpStr(# the carrier of (centralizer s), the addF of (centralizer s),(0. (centralizer s)),lm #) is scalar-unital )
proof
let x be Element of the carrier of (center R); :: according to VECTSP_1:def_14 ::_thesis: for b1, b2 being Element of the carrier of VectSpStr(# the carrier of (centralizer s), the addF of (centralizer s),(0. (centralizer s)),lm #) holds x * (b1 + b2) = (x * b1) + (x * b2)
let v, w be Element of the carrier of VectSpStr(# the carrier of (centralizer s), the addF of (centralizer s),(0. (centralizer s)),lm #); ::_thesis: x * (v + w) = (x * v) + (x * w)
x in the carrier of (center R) ;
then reconsider xx = x as Element of R by A1;
A13: v in the carrier of (centralizer s) ;
w in the carrier of (centralizer s) ;
then reconsider vv = v, ww = w as Element of R by A2, A13;
A14: [x,w] in [: the carrier of (center R), the carrier of (centralizer s):] by ZFMISC_1:def_2;
A15: [x,(v + w)] in [: the carrier of (center R), the carrier of (centralizer s):] by ZFMISC_1:def_2;
A16: [v,w] in [: the carrier of (centralizer s), the carrier of (centralizer s):] by ZFMISC_1:def_2;
A17: [x,v] in [: the carrier of (center R), the carrier of (centralizer s):] by ZFMISC_1:def_2;
A18: [(x * v),(x * w)] in [: the carrier of (centralizer s), the carrier of (centralizer s):] by ZFMISC_1:def_2;
thus x * (v + w) = the multF of R . [x,( the addF of VectSpStr(# the carrier of (centralizer s), the addF of (centralizer s),(0. (centralizer s)),lm #) . [v,w])] by A15, FUNCT_1:49
.= xx * (vv + ww) by A12, A16, 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 A17, FUNCT_1:49
.= the addF of R . [(x * v),(x * w)] by A14, FUNCT_1:49
.= (x * v) + (x * w) by A12, A18, FUNCT_1:49 ; ::_thesis: verum
end;
thus VectSpStr(# the carrier of (centralizer s), the addF of (centralizer s),(0. (centralizer s)),lm #) is scalar-distributive ::_thesis: ( VectSpStr(# the carrier of (centralizer s), the addF of (centralizer s),(0. (centralizer s)),lm #) is scalar-associative & VectSpStr(# the carrier of (centralizer s), the addF of (centralizer s),(0. (centralizer s)),lm #) is scalar-unital )
proof
let x, y be Element of the carrier of (center R); :: according to VECTSP_1:def_15 ::_thesis: for b1 being Element of the carrier of VectSpStr(# the carrier of (centralizer s), the addF of (centralizer s),(0. (centralizer s)),lm #) holds (x + y) * b1 = (x * b1) + (y * b1)
let v be Element of the carrier of VectSpStr(# the carrier of (centralizer s), the addF of (centralizer s),(0. (centralizer s)),lm #); ::_thesis: (x + y) * v = (x * v) + (y * v)
A19: x in the carrier of (center R) ;
y in the carrier of (center R) ;
then reconsider xx = x, yy = y as Element of R by A1, A19;
v in the carrier of (centralizer s) ;
then reconsider vv = v as Element of R by A2;
A20: [y,v] in [: the carrier of (center R), the carrier of (centralizer s):] by ZFMISC_1:def_2;
A21: [x,v] in [: the carrier of (center R), the carrier of (centralizer s):] by ZFMISC_1:def_2;
A22: [(x + y),v] in [: the carrier of (center R), the carrier of (centralizer s):] by ZFMISC_1:def_2;
A23: [x,y] in [: the carrier of (center R), the carrier of (center R):] by ZFMISC_1:def_2;
A24: [(x * v),(y * v)] in [: the carrier of (centralizer s), the carrier of (centralizer s):] by ZFMISC_1:def_2;
thus (x + y) * v = the multF of R . [( the addF of (center R) . [x,y]),vv] by A22, FUNCT_1:49
.= (xx + yy) * vv by A11, A23, 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 A21, FUNCT_1:49
.= the addF of R . [(x * v),(lm . (y,v))] by A20, FUNCT_1:49
.= (x * v) + (y * v) by A12, A24, FUNCT_1:49 ; ::_thesis: verum
end;
thus VectSpStr(# the carrier of (centralizer s), the addF of (centralizer s),(0. (centralizer s)),lm #) is scalar-associative ::_thesis: VectSpStr(# the carrier of (centralizer s), the addF of (centralizer s),(0. (centralizer s)),lm #) is scalar-unital
proof
let x, y be Element of the carrier of (center R); :: according to VECTSP_1:def_16 ::_thesis: for b1 being Element of the carrier of VectSpStr(# the carrier of (centralizer s), the addF of (centralizer s),(0. (centralizer s)),lm #) holds (x * y) * b1 = x * (y * b1)
let v be Element of the carrier of VectSpStr(# the carrier of (centralizer s), the addF of (centralizer s),(0. (centralizer s)),lm #); ::_thesis: (x * y) * v = x * (y * v)
A25: x in the carrier of (center R) ;
y in the carrier of (center R) ;
then reconsider xx = x, yy = y as Element of R by A1, A25;
v in the carrier of (centralizer s) ;
then reconsider vv = v as Element of R by A2;
A26: [x,(y * v)] in [: the carrier of (center R), the carrier of (centralizer s):] by ZFMISC_1:def_2;
A27: [y,v] in [: the carrier of (center R), the carrier of (centralizer s):] by ZFMISC_1:def_2;
A28: [(x * y),v] in [: the carrier of (center R), the carrier of (centralizer s):] by ZFMISC_1:def_2;
A29: [x,y] in [: the carrier of (center R), the carrier of (center R):] by ZFMISC_1:def_2;
thus (x * y) * v = the multF of R . [( the multF of (center R) . (x,y)),vv] by A28, FUNCT_1:49
.= (xx * yy) * vv by A10, A29, FUNCT_1:49
.= xx * (yy * vv) by GROUP_1:def_3
.= the multF of R . [xx,(lm . (y,v))] by A27, FUNCT_1:49
.= x * (y * v) by A26, FUNCT_1:49 ; ::_thesis: verum
end;
let v be Element of the carrier of VectSpStr(# the carrier of (centralizer s), the addF of (centralizer s),(0. (centralizer s)),lm #); :: according to VECTSP_1:def_17 ::_thesis: (1. (center R)) * v = v
v in the carrier of (centralizer s) ;
then reconsider vv = v as Element of R by A2;
1_ R in center R by Th19;
then 1_ R in the carrier of (center R) by STRUCT_0:def_5;
then A30: [(1_ R),vv] in [: the carrier of (center R), the carrier of (centralizer s):] by ZFMISC_1:def_2;
thus (1. (center R)) * v = lm . ((1. R),vv) by Def4
.= (1. R) * vv by A30, FUNCT_1:49
.= v by VECTSP_1:def_8 ; ::_thesis: verum
end;
A31: VectSpStr(# the carrier of (centralizer s), the addF of (centralizer s),(0. (centralizer s)),lm #) is add-associative
proof
let u, v, w be Element of the carrier of VectSpStr(# the carrier of (centralizer s), the addF of (centralizer s),(0. (centralizer s)),lm #); :: according to RLVECT_1:def_3 ::_thesis: (u + v) + w = u + (v + w)
reconsider uu = u, vv = v, ww = w as Element of the carrier of (centralizer s) ;
thus (u + v) + w = (uu + vv) + ww
.= uu + (vv + ww) by RLVECT_1:def_3
.= u + (v + w) ; ::_thesis: verum
end;
A32: VectSpStr(# the carrier of (centralizer s), the addF of (centralizer s),(0. (centralizer s)),lm #) is right_zeroed
proof
let v be Element of the carrier of VectSpStr(# the carrier of (centralizer s), the addF of (centralizer s),(0. (centralizer s)),lm #); :: according to RLVECT_1:def_4 ::_thesis: v + (0. VectSpStr(# the carrier of (centralizer s), the addF of (centralizer s),(0. (centralizer s)),lm #)) = v
reconsider vv = v as Element of the carrier of (centralizer s) ;
thus v + (0. VectSpStr(# the carrier of (centralizer s), the addF of (centralizer s),(0. (centralizer s)),lm #)) = vv + (0. (centralizer s))
.= v by RLVECT_1:def_4 ; ::_thesis: verum
end;
A33: VectSpStr(# the carrier of (centralizer s), the addF of (centralizer s),(0. (centralizer s)),lm #) is right_complementable
proof
let v be Element of the carrier of VectSpStr(# the carrier of (centralizer s), the addF of (centralizer s),(0. (centralizer s)),lm #); :: according to ALGSTR_0:def_16 ::_thesis: v is right_complementable
reconsider vv = v as Element of the carrier of (centralizer s) ;
consider ww being Element of the carrier of (centralizer s) such that
A34: vv + ww = 0. (centralizer s) by ALGSTR_0:def_11;
reconsider w = ww as Element of the carrier of VectSpStr(# the carrier of (centralizer s), the addF of (centralizer s),(0. (centralizer s)),lm #) ;
v + w = 0. VectSpStr(# the carrier of (centralizer s), the addF of (centralizer s),(0. (centralizer s)),lm #) by A34;
hence ex w being Element of the carrier of VectSpStr(# the carrier of (centralizer s), the addF of (centralizer s),(0. (centralizer s)),lm #) st v + w = 0. VectSpStr(# the carrier of (centralizer s), the addF of (centralizer s),(0. (centralizer s)),lm #) ; :: according to ALGSTR_0:def_11 ::_thesis: verum
end;
VectSpStr(# the carrier of (centralizer s), the addF of (centralizer s),(0. (centralizer s)),lm #) is Abelian
proof
let v, w be Element of the carrier of VectSpStr(# the carrier of (centralizer s), the addF of (centralizer s),(0. (centralizer s)),lm #); :: according to RLVECT_1:def_2 ::_thesis: v + w = w + v
reconsider vv = v, ww = w as Element of the carrier of (centralizer s) ;
thus v + w = ww + vv by RLVECT_1:2
.= w + v ; ::_thesis: verum
end;
hence ex b1 being strict VectSp of center R st
( addLoopStr(# the carrier of b1, the addF of b1, the ZeroF of b1 #) = addLoopStr(# the carrier of (centralizer s), the addF of (centralizer s), the ZeroF of (centralizer s) #) & the lmult of b1 = the multF of R | [: the carrier of (center R), the carrier of (centralizer s):] ) by A9, A31, A32, A33; ::_thesis: verum
end;
uniqueness
for b1, b2 being strict VectSp of center R st addLoopStr(# the carrier of b1, the addF of b1, the ZeroF of b1 #) = addLoopStr(# the carrier of (centralizer s), the addF of (centralizer s), the ZeroF of (centralizer s) #) & the lmult of b1 = the multF of R | [: the carrier of (center R), the carrier of (centralizer s):] & addLoopStr(# the carrier of b2, the addF of b2, the ZeroF of b2 #) = addLoopStr(# the carrier of (centralizer s), the addF of (centralizer s), the ZeroF of (centralizer s) #) & the lmult of b2 = the multF of R | [: the carrier of (center R), the carrier of (centralizer s):] holds
b1 = b2 ;
end;
:: deftheorem Def7 defines VectSp_over_center WEDDWITT:def_7_:_
for R being Skew-Field
for s being Element of R
for b3 being strict VectSp of center R holds
( b3 = VectSp_over_center s iff ( addLoopStr(# the carrier of b3, the addF of b3, the ZeroF of b3 #) = addLoopStr(# the carrier of (centralizer s), the addF of (centralizer s), the ZeroF of (centralizer s) #) & the lmult of b3 = the multF of R | [: the carrier of (center R), the carrier of (centralizer s):] ) );
theorem Th33: :: WEDDWITT:33
for R being finite Skew-Field
for 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; ::_thesis: for s being Element of R holds card the carrier of (centralizer s) = (card the carrier of (center R)) |^ (dim (VectSp_over_center s))
let s be Element of R; ::_thesis: card the carrier of (centralizer s) = (card the carrier of (center R)) |^ (dim (VectSp_over_center s))
set vR = VectSp_over_center s;
A1: addLoopStr(# the carrier of (VectSp_over_center s), the addF of (VectSp_over_center s), the ZeroF of (VectSp_over_center s) #) = addLoopStr(# the carrier of (centralizer s), the addF of (centralizer s), the ZeroF of (centralizer s) #) by Def7;
set B = the Basis of VectSp_over_center s;
the Basis of VectSp_over_center s is finite by A1;
then VectSp_over_center s is finite-dimensional by MATRLIN:def_1;
hence card the carrier of (centralizer s) = (card the carrier of (center R)) |^ (dim (VectSp_over_center s)) by A1, Th15; ::_thesis: verum
end;
theorem Th34: :: WEDDWITT:34
for R being finite Skew-Field
for s being Element of R holds 0 < dim (VectSp_over_center s)
proof
let R be finite Skew-Field; ::_thesis: for s being Element of R holds 0 < dim (VectSp_over_center s)
let s be Element of R; ::_thesis: 0 < dim (VectSp_over_center s)
set q = card the carrier of (center R);
set ns = dim (VectSp_over_center s);
now__::_thesis:_not_dim_(VectSp_over_center_s)_=_0
assume A1: dim (VectSp_over_center s) = 0 ; ::_thesis: contradiction
(card the carrier of (center R)) |^ (dim (VectSp_over_center s)) = (card the carrier of (center R)) #Z (dim (VectSp_over_center s)) by PREPOWER:36;
then (card the carrier of (center R)) |^ (dim (VectSp_over_center s)) = 1 by A1, PREPOWER:34;
then card the carrier of (centralizer s) = 1 by Th33;
hence contradiction by Th28; ::_thesis: verum
end;
hence 0 < dim (VectSp_over_center s) ; ::_thesis: verum
end;
theorem Th35: :: WEDDWITT:35
for R being finite Skew-Field
for 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; ::_thesis: for 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
let r be Element of R; ::_thesis: ( r is Element of (MultGroup R) implies ((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 )
assume A1: r is Element of (MultGroup R) ; ::_thesis: ((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
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 = (card the carrier of (center R)) |^ (dim (VectSp_over_center R)) by Th31;
then card (MultGroup R) = ((card the carrier of (center R)) |^ (dim (VectSp_over_center R))) - 1 by UNIROOTS:18;
then ((card the carrier of (center R)) |^ (dim (VectSp_over_center R))) - 1 = (card (con_class s)) * (card (Centralizer s)) by Th13;
then card (Centralizer s) divides ((card the carrier of (center R)) |^ (dim (VectSp_over_center R))) - 1 by INT_1:def_3;
then (card the carrier of (centralizer r)) - 1 divides ((card the carrier of (center R)) |^ (dim (VectSp_over_center R))) - 1 by Th30;
hence ((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 by Th33; ::_thesis: verum
end;
theorem Th36: :: WEDDWITT:36
for R being finite Skew-Field
for 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; ::_thesis: for s being Element of R st s is Element of (MultGroup R) holds
dim (VectSp_over_center s) divides dim (VectSp_over_center R)
let s be Element of R; ::_thesis: ( s is Element of (MultGroup R) implies dim (VectSp_over_center s) divides dim (VectSp_over_center R) )
assume A1: s is Element of (MultGroup R) ; ::_thesis: dim (VectSp_over_center s) divides dim (VectSp_over_center R)
set n = dim (VectSp_over_center R);
set ns = dim (VectSp_over_center s);
set q = card the carrier of (center R);
A2: dim (VectSp_over_center R) in NAT by ORDINAL1:def_12;
A3: dim (VectSp_over_center s) in NAT by ORDINAL1:def_12;
A4: 0 < dim (VectSp_over_center s) by Th34;
A5: 1 < card the carrier of (center R) by Th20;
0 < (card the carrier of (center R)) |^ (dim (VectSp_over_center s)) by PREPOWER:6;
then 0 + 1 < ((card the carrier of (center R)) |^ (dim (VectSp_over_center s))) + 1 by XREAL_1:8;
then A6: 1 <= (card the carrier of (center R)) |^ (dim (VectSp_over_center s)) by NAT_1:13;
0 < (card the carrier of (center R)) |^ (dim (VectSp_over_center R)) by PREPOWER:6;
then 0 + 1 < ((card the carrier of (center R)) |^ (dim (VectSp_over_center R))) + 1 by XREAL_1:8;
then 1 <= (card the carrier of (center R)) |^ (dim (VectSp_over_center R)) by NAT_1:13;
then A7: ((card the carrier of (center R)) |^ (dim (VectSp_over_center R))) - 1 = ((card the carrier of (center R)) |^ (dim (VectSp_over_center R))) -' 1 by XREAL_1:233;
((card the carrier of (center R)) |^ (dim (VectSp_over_center s))) - 1 = ((card the carrier of (center R)) |^ (dim (VectSp_over_center s))) -' 1 by A6, XREAL_1:233;
hence dim (VectSp_over_center s) divides dim (VectSp_over_center R) by A1, A2, A3, A4, A5, A7, Th3, Th35; ::_thesis: verum
end;
theorem Th37: :: WEDDWITT:37
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; ::_thesis: card the carrier of (center (MultGroup R)) = (card the carrier of (center R)) - 1
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 card the carrier of (center (MultGroup R)) = (card the carrier of (center R)) - 1 ; ::_thesis: verum
end;
begin
theorem :: WEDDWITT:38
for R being finite Skew-Field holds R is commutative
proof
let R be finite Skew-Field; ::_thesis: R is commutative
assume A1: not R is commutative ; ::_thesis: contradiction
set Z = center R;
set cZ = the carrier of (center R);
set q = card the carrier of (center R);
set vR = VectSp_over_center R;
set n = dim (VectSp_over_center R);
set Rs = MultGroup R;
set cR = the carrier of R;
set cRs = the carrier of (MultGroup R);
set cZs = the carrier of (center (MultGroup R));
A2: card R = (card the carrier of (center R)) |^ (dim (VectSp_over_center R)) by Th31;
then A3: card (MultGroup R) = ((card the carrier of (center R)) |^ (dim (VectSp_over_center R))) - 1 by UNIROOTS:18;
A4: 1 < card the carrier of (center R) by Th20;
A5: 1 + (- 1) < (card the carrier of (center R)) + (- 1) by Th20, XREAL_1:8;
then reconsider natq1 = (card the carrier of (center R)) - 1 as Element of NAT by INT_1:3;
0 + 1 < (dim (VectSp_over_center R)) + 1 by Th32, XREAL_1:8;
then A6: 1 <= dim (VectSp_over_center R) by NAT_1:13;
now__::_thesis:_not_dim_(VectSp_over_center_R)_=_1
assume A7: dim (VectSp_over_center R) = 1 ; ::_thesis: contradiction
card the carrier of R = (card the carrier of (center R)) #Z (dim (VectSp_over_center R)) by A2, PREPOWER:36;
then card the carrier of R = card the carrier of (center R) by A7, PREPOWER:35;
hence contradiction by A1, Th21; ::_thesis: verum
end;
then A8: 1 < dim (VectSp_over_center R) by A6, XXREAL_0:1;
set A = { X where X is Subset of the carrier of (MultGroup R) : ( X in conjugate_Classes (MultGroup R) & card X = 1 ) } ;
set B = (conjugate_Classes (MultGroup R)) \ { X where X is Subset of the carrier of (MultGroup R) : ( X in conjugate_Classes (MultGroup R) & card X = 1 ) } ;
for x being set st x in { X where X is Subset of the carrier of (MultGroup R) : ( X in conjugate_Classes (MultGroup R) & card X = 1 ) } holds
x in conjugate_Classes (MultGroup R)
proof
let x be set ; ::_thesis: ( x in { X where X is Subset of the carrier of (MultGroup R) : ( X in conjugate_Classes (MultGroup R) & card X = 1 ) } implies x in conjugate_Classes (MultGroup R) )
assume x in { X where X is Subset of the carrier of (MultGroup R) : ( X in conjugate_Classes (MultGroup R) & card X = 1 ) } ; ::_thesis: x in conjugate_Classes (MultGroup R)
then ex y being Subset of the carrier of (MultGroup R) st
( x = y & y in conjugate_Classes (MultGroup R) & card y = 1 ) ;
hence x in conjugate_Classes (MultGroup R) ; ::_thesis: verum
end;
then A9: { X where X is Subset of the carrier of (MultGroup R) : ( X in conjugate_Classes (MultGroup R) & card X = 1 ) } c= conjugate_Classes (MultGroup R) by TARSKI:def_3;
then A10: conjugate_Classes (MultGroup R) = { X where X is Subset of the carrier of (MultGroup R) : ( X in conjugate_Classes (MultGroup R) & card X = 1 ) } \/ ((conjugate_Classes (MultGroup R)) \ { X where X is Subset of the carrier of (MultGroup R) : ( X in conjugate_Classes (MultGroup R) & card X = 1 ) } ) by XBOOLE_1:45;
consider f being Function such that
A11: dom f = the carrier of (center (MultGroup R)) and
A12: for x being set st x in the carrier of (center (MultGroup R)) holds
f . x = {x} from FUNCT_1:sch_3();
A13: f is one-to-one
proof
let x1, x2 be set ; :: according to FUNCT_1:def_4 ::_thesis: ( not x1 in dom f or not x2 in dom f or not f . x1 = f . x2 or x1 = x2 )
assume that
A14: x1 in dom f and
A15: x2 in dom f and
A16: f . x1 = f . x2 ; ::_thesis: x1 = x2
A17: f . x1 = {x1} by A11, A12, A14;
f . x2 = {x2} by A11, A12, A15;
hence x1 = x2 by A16, A17, ZFMISC_1:3; ::_thesis: verum
end;
now__::_thesis:_for_x_being_set_holds_
(_(_x_in_rng_f_implies_x_in__{__X_where_X_is_Subset_of_the_carrier_of_(MultGroup_R)_:_(_X_in_conjugate_Classes_(MultGroup_R)_&_card_X_=_1_)__}__)_&_(_x_in__{__X_where_X_is_Subset_of_the_carrier_of_(MultGroup_R)_:_(_X_in_conjugate_Classes_(MultGroup_R)_&_card_X_=_1_)__}__implies_x_in_rng_f_)_)
let x be set ; ::_thesis: ( ( x in rng f implies x in { X where X is Subset of the carrier of (MultGroup R) : ( X in conjugate_Classes (MultGroup R) & card X = 1 ) } ) & ( x in { X where X is Subset of the carrier of (MultGroup R) : ( X in conjugate_Classes (MultGroup R) & card X = 1 ) } implies x in rng f ) )
hereby ::_thesis: ( x in { X where X is Subset of the carrier of (MultGroup R) : ( X in conjugate_Classes (MultGroup R) & card X = 1 ) } implies x in rng f )
assume x in rng f ; ::_thesis: x in { X where X is Subset of the carrier of (MultGroup R) : ( X in conjugate_Classes (MultGroup R) & card X = 1 ) }
then consider xx being set such that
A18: xx in dom f and
A19: x = f . xx by FUNCT_1:def_3;
A20: x = {xx} by A11, A12, A18, A19;
A21: the carrier of (center (MultGroup R)) c= the carrier of (MultGroup R) by GROUP_2:def_5;
then reconsider X = x as Subset of the carrier of (MultGroup R) by A11, A18, A20, ZFMISC_1:31;
reconsider xx = xx as Element of (MultGroup R) by A11, A18, A21;
xx in center (MultGroup R) by A11, A18, STRUCT_0:def_5;
then con_class xx = {xx} by GROUP_5:81;
then A22: X in conjugate_Classes (MultGroup R) by A20;
card X = 1 by A20, CARD_1:30;
hence x in { X where X is Subset of the carrier of (MultGroup R) : ( X in conjugate_Classes (MultGroup R) & card X = 1 ) } by A22; ::_thesis: verum
end;
assume x in { X where X is Subset of the carrier of (MultGroup R) : ( X in conjugate_Classes (MultGroup R) & card X = 1 ) } ; ::_thesis: x in rng f
then consider X being Subset of the carrier of (MultGroup R) such that
A23: x = X and
A24: X in conjugate_Classes (MultGroup R) and
A25: card X = 1 ;
consider a being Element of the carrier of (MultGroup R) such that
A26: con_class a = X by A24;
A27: a in con_class a by GROUP_3:83;
consider xx being set such that
A28: X = {xx} by A25, CARD_2:42;
A29: a = xx by A26, A27, A28, TARSKI:def_1;
then a in center (MultGroup R) by A26, A28, GROUP_5:81;
then A30: a in the carrier of (center (MultGroup R)) by STRUCT_0:def_5;
then f . a = {a} by A12;
hence x in rng f by A11, A23, A28, A29, A30, FUNCT_1:3; ::_thesis: verum
end;
then rng f = { X where X is Subset of the carrier of (MultGroup R) : ( X in conjugate_Classes (MultGroup R) & card X = 1 ) } by TARSKI:1;
then A31: { X where X is Subset of the carrier of (MultGroup R) : ( X in conjugate_Classes (MultGroup R) & card X = 1 ) } , the carrier of (center (MultGroup R)) are_equipotent by A11, A13, WELLORD2:def_4;
card the carrier of (center (MultGroup R)) = natq1 by Th37;
then A32: card { X where X is Subset of the carrier of (MultGroup R) : ( X in conjugate_Classes (MultGroup R) & card X = 1 ) } = natq1 by A31, CARD_1:5;
consider f1 being FinSequence such that
A33: rng f1 = { X where X is Subset of the carrier of (MultGroup R) : ( X in conjugate_Classes (MultGroup R) & card X = 1 ) } and
A34: f1 is one-to-one by A9, FINSEQ_4:58;
consider f2 being FinSequence such that
A35: rng f2 = (conjugate_Classes (MultGroup R)) \ { X where X is Subset of the carrier of (MultGroup R) : ( X in conjugate_Classes (MultGroup R) & card X = 1 ) } and
A36: f2 is one-to-one by FINSEQ_4:58;
set f = f1 ^ f2;
A37: rng (f1 ^ f2) = conjugate_Classes (MultGroup R) by A10, A33, A35, FINSEQ_1:31;
now__::_thesis:_for_x_being_set_holds_not_x_in__{__X_where_X_is_Subset_of_the_carrier_of_(MultGroup_R)_:_(_X_in_conjugate_Classes_(MultGroup_R)_&_card_X_=_1_)__}__/\_((conjugate_Classes_(MultGroup_R))_\__{__X_where_X_is_Subset_of_the_carrier_of_(MultGroup_R)_:_(_X_in_conjugate_Classes_(MultGroup_R)_&_card_X_=_1_)__}__)
given x being set such that A38: x in { X where X is Subset of the carrier of (MultGroup R) : ( X in conjugate_Classes (MultGroup R) & card X = 1 ) } /\ ((conjugate_Classes (MultGroup R)) \ { X where X is Subset of the carrier of (MultGroup R) : ( X in conjugate_Classes (MultGroup R) & card X = 1 ) } ) ; ::_thesis: contradiction
A39: x in { X where X is Subset of the carrier of (MultGroup R) : ( X in conjugate_Classes (MultGroup R) & card X = 1 ) } by A38, XBOOLE_0:def_4;
x in (conjugate_Classes (MultGroup R)) \ { X where X is Subset of the carrier of (MultGroup R) : ( X in conjugate_Classes (MultGroup R) & card X = 1 ) } by A38, XBOOLE_0:def_4;
hence contradiction by A39, XBOOLE_0:def_5; ::_thesis: verum
end;
then { X where X is Subset of the carrier of (MultGroup R) : ( X in conjugate_Classes (MultGroup R) & card X = 1 ) } /\ ((conjugate_Classes (MultGroup R)) \ { X where X is Subset of the carrier of (MultGroup R) : ( X in conjugate_Classes (MultGroup R) & card X = 1 ) } ) = {} by XBOOLE_0:def_1;
then rng f1 misses rng f2 by A33, A35, XBOOLE_0:def_7;
then A40: f1 ^ f2 is one-to-one FinSequence of conjugate_Classes (MultGroup R) by A34, A36, A37, FINSEQ_1:def_4, FINSEQ_3:91;
deffunc H1( set ) -> set = card (f1 . $1);
consider p1 being FinSequence such that
A41: ( len p1 = len f1 & ( for i being Nat st i in dom p1 holds
p1 . i = H1(i) ) ) from FINSEQ_1:sch_2();
for x being set st x in rng p1 holds
x in NAT
proof
let x be set ; ::_thesis: ( x in rng p1 implies x in NAT )
assume x in rng p1 ; ::_thesis: x in NAT
then consider i being Nat such that
A42: i in dom p1 and
A43: p1 . i = x by FINSEQ_2:10;
A44: x = card (f1 . i) by A41, A42, A43;
i in dom f1 by A41, A42, FINSEQ_3:29;
then f1 . i in { X where X is Subset of the carrier of (MultGroup R) : ( X in conjugate_Classes (MultGroup R) & card X = 1 ) } by A33, FUNCT_1:3;
then ex X being Subset of the carrier of (MultGroup R) st
( f1 . i = X & X in conjugate_Classes (MultGroup R) & card X = 1 ) ;
hence x in NAT by A44; ::_thesis: verum
end;
then rng p1 c= NAT by TARSKI:def_3;
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 ; ::_thesis: ( i in dom c1 implies c1 . i = 1 )
assume A47: i in dom c1 ; ::_thesis: c1 . i = 1
i in dom f1 by A41, A47, FINSEQ_3:29;
then f1 . i in { X where X is Subset of the carrier of (MultGroup R) : ( X in conjugate_Classes (MultGroup R) & card X = 1 ) } by A33, FUNCT_1:3;
then ex X being Subset of the carrier of (MultGroup R) st
( f1 . i = X & X in conjugate_Classes (MultGroup R) & card X = 1 ) ;
hence c1 . i = 1 by A41, A47; ::_thesis: verum
end;
for x being set st x in rng c1 holds
x in {1}
proof
let x be set ; ::_thesis: ( x in rng c1 implies x in {1} )
assume x in rng c1 ; ::_thesis: x in {1}
then ex i being Nat st
( i in dom c1 & x = c1 . i ) by FINSEQ_2:10;
then x = 1 by A46;
hence x in {1} by TARSKI:def_1; ::_thesis: verum
end;
then A48: rng c1 c= {1} by TARSKI:def_3;
for x being set st x in {1} holds
x in rng c1
proof
let x be set ; ::_thesis: ( x in {1} implies x in rng c1 )
assume A49: x in {1} ; ::_thesis: x in rng c1
A50: Seg (len c1) = dom c1 by FINSEQ_1:def_3;
then c1 . (len c1) = 1 by A5, A45, A46, FINSEQ_1:3;
then c1 . (len c1) = x by A49, TARSKI:def_1;
hence x in rng c1 by A5, A45, A50, FINSEQ_1:3, FUNCT_1:3; ::_thesis: verum
end;
then {1} c= rng c1 by TARSKI:def_3;
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 H2( set ) -> set = card (f2 . $1);
consider p2 being FinSequence such that
A52: ( len p2 = len f2 & ( for i being Nat st i in dom p2 holds
p2 . i = H2(i) ) ) from FINSEQ_1:sch_2();
for x being set st x in rng p2 holds
x in NAT
proof
let x be set ; ::_thesis: ( x in rng p2 implies x in NAT )
assume x in rng p2 ; ::_thesis: x in NAT
then consider i being Nat such that
A53: i in dom p2 and
A54: p2 . i = x by FINSEQ_2:10;
A55: x = card (f2 . i) by A52, A53, A54;
i in dom f2 by A52, A53, FINSEQ_3:29;
then f2 . i in (conjugate_Classes (MultGroup R)) \ { X where X is Subset of the carrier of (MultGroup R) : ( X in conjugate_Classes (MultGroup R) & card X = 1 ) } by A35, FUNCT_1:3;
then f2 . i in conjugate_Classes (MultGroup R) by XBOOLE_0:def_5;
then consider a being Element of the carrier of (MultGroup R) such that
A56: con_class a = f2 . i ;
card (con_class a) is Element of NAT ;
hence x in NAT by A55, A56; ::_thesis: verum
end;
then rng p2 c= NAT by TARSKI:def_3;
then reconsider c2 = p2 as FinSequence of NAT by FINSEQ_1:def_4;
set c = c1 ^ c2;
reconsider c = c1 ^ c2 as FinSequence of NAT ;
len c = (len f1) + (len f2) by A41, A52, FINSEQ_1:22;
then A57: len c = len (f1 ^ f2) by FINSEQ_1:22;
for i being Element of NAT st i in dom c holds
c . i = card ((f1 ^ f2) . i)
proof
let i be Element of NAT ; ::_thesis: ( i in dom c implies c . i = card ((f1 ^ f2) . i) )
assume A58: i in dom c ; ::_thesis: c . i = card ((f1 ^ f2) . i)
now__::_thesis:_c_._i_=_card_((f1_^_f2)_._i)
percases ( i in dom c1 or ex j being Nat st
( j in dom c2 & i = (len c1) + j ) ) by A58, FINSEQ_1:25;
supposeA59: i in dom c1 ; ::_thesis: c . i = card ((f1 ^ f2) . i)
then A60: i in dom f1 by A41, FINSEQ_3:29;
c . i = c1 . i by A59, FINSEQ_1:def_7
.= card (f1 . i) by A41, A59
.= card ((f1 ^ f2) . i) by A60, FINSEQ_1:def_7 ;
hence c . i = card ((f1 ^ f2) . i) ; ::_thesis: verum
end;
suppose ex j being Nat st
( j in dom c2 & i = (len c1) + j ) ; ::_thesis: c . i = card ((f1 ^ f2) . i)
then consider j being Nat such that
A61: j in dom c2 and
A62: i = (len c1) + j ;
A63: j in dom f2 by A52, A61, FINSEQ_3:29;
c . i = c2 . j by A61, A62, FINSEQ_1:def_7
.= card (f2 . j) by A52, A61
.= card ((f1 ^ f2) . i) by A41, A62, A63, FINSEQ_1:def_7 ;
hence c . i = card ((f1 ^ f2) . i) ; ::_thesis: verum
end;
end;
end;
hence c . i = card ((f1 ^ f2) . i) ; ::_thesis: verum
end;
then card (MultGroup R) = Sum c by A37, A40, A57, Th6;
then A64: ((card the carrier of (center R)) |^ (dim (VectSp_over_center R))) - 1 = (Sum c2) + ((card the carrier of (center R)) - 1) by A3, A51, RVSUM_1:75;
reconsider q = card the carrier of (center R) as non empty Element of NAT ;
reconsider n = dim (VectSp_over_center R) as non empty Element of NAT by Th32, ORDINAL1:def_12;
q in COMPLEX by XCMPLX_0:def_2;
then reconsider qc = q as Element of F_Complex by COMPLFLD:def_1;
set pnq = eval ((cyclotomic_poly n),qc);
reconsider pnq = eval ((cyclotomic_poly n),qc) as Integer by UNIROOTS:52;
reconsider abspnq = abs 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 abs ((q |^ n) - 1) by INT_2:16;
then A65: abspnq divides qn1 by ABSVALUE:def_1;
for i being Element of NAT st i in dom c2 holds
abspnq divides c2 /. i
proof
let i be Element of NAT ; ::_thesis: ( i in dom c2 implies abspnq divides c2 /. i )
assume A66: i in dom c2 ; ::_thesis: abspnq divides c2 /. i
c2 . i = card (f2 . i) by A52, A66;
then A67: c2 /. i = card (f2 . i) by A66, PARTFUN1:def_6;
A68: i in dom f2 by A52, A66, FINSEQ_3:29;
then f2 . i in (conjugate_Classes (MultGroup R)) \ { X where X is Subset of the carrier of (MultGroup R) : ( X in conjugate_Classes (MultGroup R) & card X = 1 ) } by A35, FUNCT_1:3;
then f2 . i in conjugate_Classes (MultGroup R) by XBOOLE_0:def_5;
then consider a being Element of the carrier of (MultGroup R) such that
A69: con_class a = f2 . i ;
reconsider a = a as Element of (MultGroup R) ;
reconsider s = a as Element of R by UNIROOTS:19;
set ns = dim (VectSp_over_center s);
set ca = card (con_class a);
set oa = card (Centralizer a);
A70: card (MultGroup R) = ((card (con_class a)) * (card (Centralizer a))) + 0 by Th13;
then A71: (card (MultGroup R)) div (card (Centralizer a)) = card (con_class a) by NAT_D:def_1;
A72: qn1 div (card (Centralizer a)) = card (con_class a) by A3, A70, NAT_D:def_1;
q |^ (dim (VectSp_over_center s)) <> 0 by PREPOWER:5;
then (q |^ (dim (VectSp_over_center s))) + 1 > 0 + 1 by XREAL_1:8;
then q |^ (dim (VectSp_over_center s)) >= 1 by NAT_1:13;
then (q |^ (dim (VectSp_over_center s))) + (- 1) >= 1 + (- 1) by XREAL_1:7;
then reconsider qns1 = (q |^ (dim (VectSp_over_center s))) - 1 as Element of NAT by INT_1:3;
A73: card (Centralizer a) = (card the carrier of (centralizer s)) - 1 by Th30
.= qns1 by Th33 ;
reconsider ns = dim (VectSp_over_center s) as non empty Element of NAT by Th34, ORDINAL1:def_12;
A74: ns <= n by Th36, NAT_D:7;
now__::_thesis:_not_ns_=_n
assume ns = n ; ::_thesis: contradiction
then A75: card (f2 . i) = 1 by A3, A69, A71, A73, NAT_2:3;
A76: f2 . i in (conjugate_Classes (MultGroup R)) \ { X where X is Subset of the carrier of (MultGroup R) : ( X in conjugate_Classes (MultGroup R) & card X = 1 ) } by A35, A68, FUNCT_1:3;
then A77: f2 . i in conjugate_Classes (MultGroup R) by XBOOLE_0:def_5;
not f2 . i in { X where X is Subset of the carrier of (MultGroup R) : ( X in conjugate_Classes (MultGroup R) & card X = 1 ) } by A76, XBOOLE_0:def_5;
hence contradiction by A75, A77; ::_thesis: verum
end;
then ns < n by A74, XXREAL_0:1;
then pnq divides qn1 div qns1 by Th36, UNIROOTS:59;
then abspnq divides abs (qn1 div qns1) by INT_2:16;
hence abspnq divides c2 /. i by A67, A69, A72, A73, ABSVALUE:def_1; ::_thesis: verum
end;
then abspnq divides natq1 by A64, A65, Th5, NAT_D:10;
hence contradiction by A4, A5, A8, NAT_D:7, UNIROOTS:60; ::_thesis: verum
end;
theorem :: WEDDWITT:39
for R being Skew-Field holds 1. (center R) = 1. R by Def4;
theorem :: WEDDWITT:40
for R being Skew-Field
for s being Element of R holds 1. (centralizer s) = 1. R by Def5;