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