weddwitt.miz



    begin

    theorem :: WEDDWITT:1

    

     Th1: for a be Element of NAT , q be Real st 1 < q & (q |^ a) = 1 holds a = 0

    proof

      let a be Element of NAT , q be Real such that

       A1: 1 < q and

       A2: (q |^ a) = 1 and

       A3: a <> 0 ;

      a < (1 + 1) by A1, A2, PREPOWER: 13;

      then a <= ( 0 + 1) by NAT_1: 13;

      then a = 1 by A3, NAT_1: 8;

      then (q #Z a) = q by PREPOWER: 35;

      hence contradiction by A1, A2, PREPOWER: 36;

    end;

    theorem :: WEDDWITT:2

    

     Th2: for a,k,r be Nat, x be Real st 1 < x & 0 < k holds (x |^ ((a * k) + r)) = ((x |^ a) * (x |^ ((a * (k -' 1)) + r)))

    proof

      let a,k,r be Nat, x be Real such that

       A1: 1 < x and

       A2: 0 < k;

      set xNak = (x |^ ((a * k) + r));

      ( 0 + 1) <= k by A2, NAT_1: 13;

      then k = ((k -' 1) + 1) by XREAL_1: 235;

      then xNak = (x #Z (a + ((a * (k -' 1)) + r))) by PREPOWER: 36;

      then xNak = ((x #Z a) * (x #Z ((a * (k -' 1)) + r))) by A1, PREPOWER: 44;

      then xNak = ((x |^ a) * (x #Z ((a * (k -' 1)) + r))) by PREPOWER: 36;

      hence thesis by PREPOWER: 36;

    end;

    theorem :: WEDDWITT:3

    

     Th3: for q,a,b be Element of NAT st 0 < a & 1 < q & ((q |^ a) -' 1) divides ((q |^ b) -' 1) holds a divides b

    proof

      let q,a,b be Element of NAT such that

       A1: 0 < a and

       A2: 1 < q and

       A3: ((q |^ a) -' 1) divides ((q |^ b) -' 1);

      set r = (b mod a);

      set qNa = (q |^ a);

      set qNr = (q |^ r);

      defpred P[ Nat] means (qNa -' 1) divides ((q |^ ((a * $1) + r)) -' 1);

      

       A4: b = ((a * (b div a)) + r) by A1, NAT_D: 2;

      then

       A5: ex k be Nat st P[k] by A3;

      consider k be Nat such that

       A6: P[k] and

       A7: for n be Nat st P[n] holds k <= n from NAT_1:sch 5( A5);

      now

        per cases ;

          suppose

           A8: k = 0 ;

           A9:

          now

            assume

             A10: 0 <> (qNr -' 1);

            r < a by A1, NAT_D: 1;

            then

            consider m be Nat such that

             A11: a = (r + m) by NAT_1: 10;

            

             A12: m <> 0 by A1, A11, NAT_D: 1;

            

             A13: (q |^ (r + m)) = (q #Z (r + m)) by PREPOWER: 36;

            

             A14: (q #Z (r + m)) = ((q #Z r) * (q #Z m)) by A2, PREPOWER: 44;

            

             A15: (q #Z r) = (q |^ r) by PREPOWER: 36;

            

             A16: (q #Z m) = (q |^ m) by PREPOWER: 36;

            

             A17: (q |^ m) >= 1 by A2, PREPOWER: 11;

            m in NAT by ORDINAL1:def 12;

            then (q |^ m) <> 1 by A2, A12, Th1;

            then (q |^ m) > 1 by A17, XXREAL_0: 1;

            then

             A18: qNr < qNa by A2, A11, A13, A14, A15, A16, PREPOWER: 39, XREAL_1: 155;

            then ( 0 + 1) <= qNa by NAT_1: 13;

            then (qNa -' 1) = (qNa - 1) by XREAL_1: 233;

            then

             A19: (qNa -' 1) = (qNa + ( - 1));

            ( 0 + 1) <= qNr by A10, NAT_2: 8;

            then (qNr -' 1) = (qNr - 1) by XREAL_1: 233;

            then (qNr -' 1) = (qNr + ( - 1));

            then (qNr -' 1) < (qNa -' 1) by A18, A19, XREAL_1: 8;

            hence contradiction by A6, A8, A10, NAT_D: 7;

          end;

           0 < qNr by A2, PREPOWER: 6;

          then ( 0 + 1) <= qNr by NAT_1: 13;

          then ((qNr - 1) + 1) = 1 by A9, XREAL_1: 233;

          then r = 0 by A2, Th1;

          hence thesis by A4, NAT_D: 3;

        end;

          suppose

           A20: k <> 0 ;

          then

          consider j be Nat such that

           A21: k = (j + 1) by NAT_1: 6;

          

           A22: (k - 1) = j by A21;

          ( 0 + 1) <= k by A20, NAT_1: 13;

          then

           A23: (k -' 1) = j by A22, XREAL_1: 233;

          set qNaj = (q |^ ((a * j) + r));

          set qNak = (q |^ ((a * k) + r));

          set qNak1 = (q |^ ((a * (k -' 1)) + r));

          

           A24: not (qNa -' 1) divides (qNaj -' 1) by A7, A21, XREAL_1: 29;

          (qNa -' 1) divides ( - (qNa -' 1)) by INT_2: 10;

          then

           A25: (qNa -' 1) divides ((qNak -' 1) + ( - (qNa -' 1))) by A6, WSIERP_1: 4;

          

           A26: 0 < qNak by A2, PREPOWER: 6;

          

           A27: 0 < qNa by A2, PREPOWER: 6;

          ( 0 + 1) <= qNak by A26, NAT_1: 13;

          then

           A28: (qNak -' 1) = (qNak - 1) by XREAL_1: 233;

          

           A29: ( 0 + 1) <= qNa by A27, NAT_1: 13;

          ((qNak - 1) - (qNa - 1)) = (qNak - qNa);

          then ((qNak - 1) - (qNa - 1)) = ((qNa * qNak1) - (qNa * 1)) by A2, A20, Th2;

          then

           A30: ((qNak -' 1) - (qNa -' 1)) = (qNa * (qNak1 - 1)) by A28, A29, XREAL_1: 233;

           0 < qNak1 by A2, PREPOWER: 6;

          then ( 0 + 1) <= qNak1 by NAT_1: 13;

          then

           A31: ((qNak -' 1) - (qNa -' 1)) = (qNa * (qNak1 -' 1)) by A30, XREAL_1: 233;

           0 < qNa by A2, PREPOWER: 6;

          then ( 0 + 1) <= qNa by NAT_1: 13;

          then ((qNa -' 1) + 1) = qNa by XREAL_1: 235;

          then ((qNa -' 1),qNa) are_coprime by PEPIN: 1;

          hence thesis by A23, A24, A25, A31, INT_2: 25;

        end;

      end;

      hence thesis;

    end;

    theorem :: WEDDWITT:4

    

     Th4: for n,q be Nat st 0 < q holds ( card ( Funcs (n,q))) = (q |^ n)

    proof

      let n,q be Nat such that

       A1: 0 < q;

      reconsider q as Element of NAT by ORDINAL1:def 12;

      defpred P[ Nat] means ( card ( Funcs ($1,q))) = (q |^ $1);

      ( Funcs ( {} ,q)) = { {} } by FUNCT_5: 57;

      

      then ( card ( Funcs ( 0 ,q))) = 1 by CARD_1: 30

      .= (q #Z 0 ) by PREPOWER: 34

      .= (q |^ 0 ) by PREPOWER: 36;

      then

       A2: P[ 0 ];

      

       A3: for n be Nat st P[n] holds P[(n + 1)]

      proof

        let n be Nat such that

         A4: P[n];

        reconsider n as Element of NAT by ORDINAL1:def 12;

        reconsider q9 = q as non empty set by A1;

        defpred R[ object, object] means ex x be Function of (n + 1), q st $1 = x & $2 = (x | n);

        

         A5: for x be object st x in ( Funcs ((n + 1),q9)) holds ex y be object st y in ( Funcs (n,q9)) & R[x, y]

        proof

          let x be object;

          assume x in ( Funcs ((n + 1),q9));

          then

          consider f be Function such that

           A6: x = f and

           A7: ( dom f) = (n + 1) and

           A8: ( rng f) c= q9 by FUNCT_2:def 2;

          reconsider f as Function of (n + 1), q9 by A7, A8, FUNCT_2: 2;

           not n in n;

          then

           A9: n misses {n} by ZFMISC_1: 50;

          (( Segm (n + 1)) /\ n) = ((( Segm n) \/ {n}) /\ n) by AFINSQ_1: 2;

          then ((n + 1) /\ n) = ((n /\ n) \/ ( {n} /\ n)) by XBOOLE_1: 23;

          then ((n + 1) /\ n) = (n \/ {} ) by A9, XBOOLE_0:def 7;

          then

           A10: ( dom (f | n)) = n by A7, RELAT_1: 61;

          ( rng (f | n)) c= q9;

          then (f | n) in ( Funcs (n,q9)) by A10, FUNCT_2:def 2;

          hence thesis by A6;

        end;

        consider G be Function of ( Funcs ((n + 1),q9)), ( Funcs (n,q9)) such that

         A11: for x be object st x in ( Funcs ((n + 1),q9)) holds R[x, (G . x)] from FUNCT_2:sch 1( A5);

        for x be object st x in ( Funcs (n,q9)) holds x in ( rng G)

        proof

          let x be object such that

           A12: x in ( Funcs (n,q9));

          consider y be object such that

           A13: y in q9 by XBOOLE_0:def 1;

          reconsider g = x as Element of ( Funcs (n,q9)) by A12;

          set fx = (g +* (n .--> y));

          for y be set st y in q holds (g +* (n .--> y)) in (G " {g})

          proof

            let y be set such that

             A14: y in q;

            consider f be Function such that

             A15: f = (g +* (n .--> y));

            

             A16: ( dom g) = n by FUNCT_2:def 1;

            

             A17: ( dom (n .--> y)) = {n};

            then ( dom f) = (( Segm n) \/ {n}) by A15, A16, FUNCT_4:def 1;

            then

             A18: ( dom f) = ( Segm (n + 1)) by AFINSQ_1: 2;

            ( rng (n .--> y)) = {y} by FUNCOP_1: 8;

            then

             A19: ( rng f) c= (( rng g) \/ {y}) by A15, FUNCT_4: 17;

             {y} c= q by A14, ZFMISC_1: 31;

            then (( rng g) \/ {y}) c= q by XBOOLE_1: 8;

            then ( rng f) c= q by A19;

            then

             A20: f in ( Funcs ((n + 1),q)) by A18, FUNCT_2:def 2;

            then

            reconsider f as Function of (n + 1), q by FUNCT_2: 66;

             not n in n;

            then n misses {n} by ZFMISC_1: 50;

            then

             A21: (f | n) = g by A15, A16, A17, FUNCT_4: 33;

             R[f, (G . f)] by A11, A20;

            then

             A22: (G . f) in {x} by A21, TARSKI:def 1;

            ( dom G) = ( Funcs ((n + 1),q)) by FUNCT_2:def 1;

            hence thesis by A15, A20, A22, FUNCT_1:def 7;

          end;

          then (g +* (n .--> y)) in (G " {g}) by A13;

          then

          consider b be object such that

           A23: b in ( rng G) and

           A24: [fx, b] in G and b in {g} by RELAT_1: 131;

          fx in ( dom G) by A24, FUNCT_1: 1;

          then R[fx, (G . fx)] by A11;

          then

           A25: (fx | n) = b by A24, FUNCT_1: 1;

          

           A26: ( dom g) = n by FUNCT_2:def 1;

          

           A27: ( dom (n .--> y)) = {n};

           not n in n;

          then n misses {n} by ZFMISC_1: 50;

          hence thesis by A23, A25, A26, A27, FUNCT_4: 33;

        end;

        then ( Funcs (n,q9)) c= ( rng G);

        then

         A28: ( rng G) = ( Funcs (n,q9)) by XBOOLE_0:def 10;

        

         A29: for x be Element of ( Funcs (n,q9)) holds (G " {x}) is finite & ( card (G " {x})) = q

        proof

          let x be Element of ( Funcs (n,q9));

          deffunc HH( object) = (x +* (n .--> $1));

          

           A30: for y be object st y in q holds HH(y) in (G " {x})

          proof

            let y be object such that

             A31: y in q;

            consider f be Function such that

             A32: f = (x +* (n .--> y));

            

             A33: ( dom x) = n by FUNCT_2:def 1;

            

             A34: ( dom (n .--> y)) = {n};

            then ( dom f) = (( Segm n) \/ {n}) by A32, A33, FUNCT_4:def 1;

            then

             A35: ( dom f) = ( Segm (n + 1)) by AFINSQ_1: 2;

            ( rng (n .--> y)) = {y} by FUNCOP_1: 8;

            then

             A36: ( rng f) c= (( rng x) \/ {y}) by A32, FUNCT_4: 17;

             {y} c= q by A31, ZFMISC_1: 31;

            then (( rng x) \/ {y}) c= q by XBOOLE_1: 8;

            then ( rng f) c= q by A36;

            then

             A37: f in ( Funcs ((n + 1),q)) by A35, FUNCT_2:def 2;

            then

            reconsider f as Function of (n + 1), q by FUNCT_2: 66;

             not n in n;

            then n misses {n} by ZFMISC_1: 50;

            then

             A38: (f | n) = x by A32, A33, A34, FUNCT_4: 33;

             R[f, (G . f)] by A11, A37;

            then

             A39: (G . f) in {x} by A38, TARSKI:def 1;

            ( dom G) = ( Funcs ((n + 1),q)) by FUNCT_2:def 1;

            hence thesis by A32, A37, A39, FUNCT_1:def 7;

          end;

          consider H be Function of q, (G " {x}) such that

           A40: for y be object st y in q holds (H . y) = HH(y) from FUNCT_2:sch 2( A30);

          

           A41: for c be object st c in (G " {x}) holds ex y be object st y in q & (H . y) = c

          proof

            let c be object;

            assume

             A42: c in (G " {x});

            then

            consider f be Function of (n + 1), q9 such that

             A43: c = f and

             A44: (G . c) = (f | n) by A11;

            take y = (f . n);

            (G . c) in {x} by A42, FUNCT_1:def 7;

            then

             A45: (G . c) = x by TARSKI:def 1;

            ( Segm (n + 1)) = (( Segm n) \/ {n}) by AFINSQ_1: 2;

            then ( dom f) = (n \/ {n}) by FUNCT_2:def 1;

            then

             A46: f = ((f | n) +* (n .--> (f . n))) by FUNCT_7: 14;

            

             A47: n in ( Segm (n + 1)) by NAT_1: 45;

            hence y in q by FUNCT_2: 5;

            thus thesis by A40, A43, A44, A45, A46, A47, FUNCT_2: 5;

          end;

           {x} c= ( rng G) by A28, ZFMISC_1: 31;

          then

           A48: (G " {x}) <> {} by RELAT_1: 139;

          

           A49: ( rng H) = (G " {x}) by A41, FUNCT_2: 10;

          

           A50: ( dom H) = q by A48, FUNCT_2:def 1;

          for x1,x2 be object st x1 in ( dom H) & x2 in ( dom H) & (H . x1) = (H . x2) holds x1 = x2

          proof

            let x1,x2 be object such that

             A51: x1 in ( dom H) and

             A52: x2 in ( dom H) and

             A53: (H . x1) = (H . x2);

            

             A54: (H . x2) = (x +* (n .--> x2)) by A40, A52;

            

             A55: ( dom (n .--> x1)) = {n};

            

             A56: ( dom (n .--> x2)) = {n};

            set fx1 = (x +* (n .--> x1));

            set fx2 = (x +* (n .--> x2));

            

             A57: fx1 = fx2 by A40, A51, A53, A54;

            

             A58: ((n .--> x1) . n) = x1 by FUNCOP_1: 72;

            

             A59: ((n .--> x2) . n) = x2 by FUNCOP_1: 72;

            

             A60: n in {n} by TARSKI:def 1;

            then (fx1 . n) = x1 by A55, A58, FUNCT_4: 13;

            hence thesis by A56, A57, A59, A60, FUNCT_4: 13;

          end;

          then H is one-to-one;

          then (q,(H .: q)) are_equipotent by A50, CARD_1: 33;

          then (q,( rng H)) are_equipotent by A50, RELAT_1: 113;

          hence thesis by A49, CARD_1:def 2;

        end;

        

         A61: for x,y be set st x is Element of ( Funcs (n,q9)) & y is Element of ( Funcs (n,q9)) & x <> y holds (G " {x}) misses (G " {y})

        proof

          let x,y be set such that x is Element of ( Funcs (n,q9)) and y is Element of ( Funcs (n,q9)) and

           A62: x <> y;

          now

            assume not (G " {x}) misses (G " {y});

            then not ((G " {x}) /\ (G " {y})) = {} by XBOOLE_0:def 7;

            then

            consider f be object such that

             A63: f in ((G " {x}) /\ (G " {y})) by XBOOLE_0:def 1;

            f in (G " {x}) by A63, XBOOLE_0:def 4;

            then

             A64: (G . f) in {x} by FUNCT_1:def 7;

            reconsider f as Function of (n + 1), q by A63, FUNCT_2: 66;

            f in ( Funcs ((n + 1),q)) by A1, FUNCT_2: 8;

            then

             A65: R[f, (G . f)] by A11;

            then

             A66: (f | n) = x by A64, TARSKI:def 1;

            f in (G " {y}) by A63, XBOOLE_0:def 4;

            then (G . f) in {y} by FUNCT_1:def 7;

            hence contradiction by A62, A65, A66, TARSKI:def 1;

          end;

          hence thesis;

        end;

        reconsider X = the set of all (G " {x}) where x be Element of ( Funcs (n,q9)) as set;

        

         A67: for y be object holds y in ( union X) implies y in ( Funcs ((n + 1),q))

        proof

          let x be object;

          assume x in ( union X);

          then

          consider Y be set such that

           A68: x in Y and

           A69: Y in X by TARSKI:def 4;

          ex z be Element of ( Funcs (n,q)) st ((G " {z}) = Y) by A69;

          hence thesis by A68;

        end;

        for y be object holds y in ( Funcs ((n + 1),q)) implies y in ( union X)

        proof

          let x be object;

          assume x in ( Funcs ((n + 1),q));

          then

          consider f be 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 be object st (y in ( Funcs (n,q9))) & R[f, y] by A5, A72;

          then (G " {(f | n)}) in X;

          hence thesis by A70, A74, TARSKI:def 4;

        end;

        then

         A75: ( union X) = ( Funcs ((n + 1),q)) by A67, TARSKI: 2;

        ( Funcs ((n + 1),q)) is finite by FRAENKEL: 6;

        then

        reconsider X as finite set by A75, FINSET_1: 7;

        

         A76: ( card X) = (q |^ n)

        proof

          deffunc FF( object) = (G " {$1});

          

           A77: for x be object st x in ( Funcs (n,q)) holds FF(x) in X;

          consider F be Function of ( Funcs (n,q)), X such that

           A78: for x be object st x in ( Funcs (n,q)) holds (F . x) = FF(x) from FUNCT_2:sch 2( A77);

          

           A79: for c be object st c in X holds ex x be object st x in ( Funcs (n,q)) & c = (F . x)

          proof

            let c be object;

            assume c in X;

            then

            consider y be Element of ( Funcs (n,q)) such that

             A80: c = (G " {y});

            (F . y) = c by A78, A80;

            hence thesis;

          end;

          set gg = the Element of ( Funcs (n,q9));

          

           A81: (G " {gg}) in X;

          

           A82: ( rng F) = X by A79, FUNCT_2: 10;

          

           A83: ( dom F) = ( Funcs (n,q)) by A81, FUNCT_2:def 1;

          for x1,x2 be object st x1 in ( dom F) & x2 in ( dom F) & (F . x1) = (F . x2) holds x1 = x2

          proof

            let x1,x2 be object such that

             A84: x1 in ( dom F) and

             A85: x2 in ( dom F) and

             A86: (F . x1) = (F . x2);

            (F . x1) = (G " {x1}) by A78, A84;

            then

             A87: (G " {x1}) = (G " {x2}) by A78, A85, A86;

            now

              assume x1 <> x2;

              then (G " {x1}) misses (G " {x2}) by A61, A84, A85;

              then ((G " {x1}) /\ (G " {x1})) = {} by A87, XBOOLE_0:def 7;

              hence contradiction by A29, A84, CARD_1: 27;

            end;

            hence thesis;

          end;

          then F is one-to-one;

          then (( Funcs (n,q)),(F .: ( Funcs (n,q)))) are_equipotent by A83, CARD_1: 33;

          then (( Funcs (n,q)),( rng F)) are_equipotent by A83, RELAT_1: 113;

          hence thesis by A4, A82, CARD_1: 5;

        end;

        for Y be set st Y in X holds ex B be finite set st B = Y & ( card B) = q & for Z be set st Z in X & Y <> Z holds (Y,Z) are_equipotent & Y misses Z

        proof

          let Y be set;

          assume Y in X;

          then

          consider x be 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 be set st Z in X & Y <> Z holds (Y,Z) are_equipotent & Y misses Z

          proof

            let Z be set such that

             A91: Z in X and

             A92: Y <> Z;

            consider y be Element of ( Funcs (n,q9)) such that

             A93: Z = (G " {y}) by A91;

            

             A94: ( card Z) = q by A29, A93;

            now

              per cases ;

                suppose x = y;

                hence Y misses Z by A88, A92, A93;

              end;

                suppose x <> y;

                hence Y misses Z by A61, A88, A93;

              end;

            end;

            hence thesis by A90, A94, CARD_1: 5;

          end;

          hence thesis by A89, A90;

        end;

        then ex C be finite set st C = ( union X) & ( card C) = (q * ( card X)) by GROUP_2: 156;

        hence thesis by A75, A76, NEWTON: 6;

      end;

      for n be Nat holds P[n] from NAT_1:sch 2( A2, A3);

      hence thesis;

    end;

    theorem :: WEDDWITT:5

    

     Th5: for f be FinSequence of NAT , i be Element of NAT st for j be Element of NAT st j in ( dom f) holds i divides (f /. j) holds i divides ( Sum f)

    proof

      defpred P[ Nat] means for f be FinSequence of NAT st ( len f) = $1 holds for i be Element of NAT st for j be Element of NAT st j in ( dom f) holds i divides (f /. j) holds i divides ( Sum f);

      

       A1: P[ 0 ]

      proof

        let f be FinSequence of NAT ;

        assume ( len f) = 0 ;

        then

         A2: f = ( <*> NAT );

        let i be Element of NAT such that for j be Element of NAT st j in ( dom f) holds i divides (f /. j);

        ( Sum f) = 0 by A2, RVSUM_1: 72;

        hence thesis by NAT_D: 6;

      end;

      

       A3: for k be Nat st P[k] holds P[(k + 1)]

      proof

        let k be Nat such that

         A4: P[k];

        let f be FinSequence of NAT such that

         A5: ( len f) = (k + 1);

        let i be Element of NAT such that

         A6: for j be Element of NAT st j in ( dom f) holds i divides (f /. j);

        f <> {} by A5;

        then

        consider q be FinSequence, x be object such that

         A7: f = (q ^ <*x*>) by FINSEQ_1: 46;

        reconsider f1 = q as FinSequence of NAT by A7, FINSEQ_1: 36;

        reconsider f2 = <*x*> as FinSequence of NAT by A7, FINSEQ_1: 36;

        (k + 1) = (( len f1) + ( len f2)) by A5, A7, FINSEQ_1: 22;

        then

         A8: (k + 1) = (( len f1) + 1) by FINSEQ_1: 39;

        for j be Element of NAT st j in ( dom f1) holds i divides (f1 /. j)

        proof

          let j be Element of NAT such that

           A9: j in ( dom f1);

          

           A10: ( dom f1) c= ( dom f) by A7, FINSEQ_1: 26;

          

          then (f /. j) = (f . j) by A9, PARTFUN1:def 6

          .= (f1 . j) by A7, A9, FINSEQ_1:def 7

          .= (f1 /. j) by A9, PARTFUN1:def 6;

          hence thesis by A6, A9, A10;

        end;

        then

         A11: i divides ( Sum f1) by A4, A8;

        ( rng f2) c= NAT by FINSEQ_1:def 4;

        then {x} c= NAT by FINSEQ_1: 38;

        then

        reconsider m = x as Element of NAT by ZFMISC_1: 31;

        

         A12: (f . ( len f)) = m by A5, A7, A8, FINSEQ_1: 42;

        ( len f) in ( Seg ( len f)) by A5, FINSEQ_1: 3;

        then

         A13: ( len f) in ( dom f) by FINSEQ_1:def 3;

        then (f /. ( len f)) = (f . ( len f)) by PARTFUN1:def 6;

        then

         A14: i divides m by A6, A12, A13;

        ( Sum f) = (( Sum f1) + m) by A7, RVSUM_1: 74;

        hence thesis by A11, A14, NAT_D: 8;

      end;

      

       A15: for k be Nat holds P[k] from NAT_1:sch 2( A1, A3);

      let f be FinSequence of NAT , i be Element of NAT such that

       A16: for j be Element of NAT st j in ( dom f) holds i divides (f /. j);

      ( len f) = ( len f);

      hence thesis by A15, A16;

    end;

    theorem :: WEDDWITT:6

    

     Th6: for X be finite set, Y be a_partition of X, f be FinSequence of Y st f is one-to-one & ( rng f) = Y holds for c be FinSequence of NAT st ( len c) = ( len f) & for i be Element of NAT st i in ( dom c) holds (c . i) = ( card (f . i)) holds ( card X) = ( Sum c)

    proof

      defpred P[ Nat] means for X be finite set, z be a_partition of X st ( card z) = $1 holds for f be FinSequence of z st f is one-to-one & ( rng f) = z holds for c be FinSequence of NAT st ( len c) = ( len f) & for i be Element of NAT st i in ( dom c) holds (c . i) = ( card (f . i)) holds ( card X) = ( Sum c);

      

       A1: P[ 0 ]

      proof

        let X be finite set;

        let z be a_partition of X such that

         A2: ( card z) = 0 ;

        let f be FinSequence of z such that f is one-to-one and ( rng f) = z;

        let c be FinSequence of NAT such that

         A3: ( len c) = ( len f) and for i be Element of NAT st i in ( dom c) holds (c . i) = ( card (f . i));

        

         A4: z = {} by A2;

        

         A5: X = {} by A2;

        c = {} by A3, A4;

        hence thesis by A5, RVSUM_1: 72;

      end;

      

       A6: for k be Nat st P[k] holds P[(k + 1)]

      proof

        let k be Nat;

        assume

         A7: P[k];

        let X be finite set;

        let Z be a_partition of X such that

         A8: ( card Z) = (k + 1);

        let f be FinSequence of Z such that

         A9: f is one-to-one and

         A10: ( rng f) = Z;

        let c be FinSequence of NAT such that

         A11: ( len c) = ( len f) and

         A12: for i be Element of NAT st i in ( dom c) holds (c . i) = ( card (f . i));

        

         A13: ( len f) = (k + 1) by A8, A9, A10, FINSEQ_4: 62;

        

         A14: Z <> {} by A8;

        reconsider Z as non empty set by A8;

        reconsider f as FinSequence of Z;

        reconsider X as non empty finite set by A14;

        reconsider fk = (f | ( Seg k)) as FinSequence of Z by FINSEQ_1: 18;

        

         A15: ( len fk) = k by A13, FINSEQ_3: 53;

        

         A16: f = (fk ^ <*(f . (k + 1))*>) by A13, FINSEQ_3: 55;

        reconsider Zk = ( rng fk) as finite set;

        reconsider fk as FinSequence of Zk by FINSEQ_1:def 4;

        

         A17: fk is one-to-one by A9, FUNCT_1: 52;

        then

         A18: ( card Zk) = k by A15, FINSEQ_4: 62;

        reconsider Xk = ( union Zk) as finite set;

         A19:

        now

          

           A20: for a be Subset of Xk st a in Zk holds a <> {} & for b be Subset of Xk st b in Zk holds a = b or a misses b

          proof

            let a be Subset of Xk such that

             A21: a in Zk;

            

             A22: a in Z by A21;

            for b be Subset of Xk st b in Zk holds a = b or a misses b

            proof

              let b be Subset of Xk such that

               A23: b in Zk;

              

               A24: a in Z by A21;

              b in Z by A23;

              hence thesis by A24, EQREL_1:def 4;

            end;

            hence thesis by A22;

          end;

          Zk c= ( bool ( union Zk)) by ZFMISC_1: 82;

          hence Zk is a_partition of Xk by A20, EQREL_1:def 4;

        end;

        reconsider ck = (c | ( Seg k)) as FinSequence of NAT by FINSEQ_1: 18;

        

         A25: ( len ck) = ( len fk) by A11, A13, A15, FINSEQ_3: 53;

        for i be Element of NAT st i in ( dom ck) holds (ck . i) = ( card (fk . i))

        proof

          let i be Element of NAT ;

          assume

           A26: i in ( dom ck);

          

           A27: k <= (k + 1) by NAT_1: 11;

          then ( dom ck) = ( Seg k) by A11, A13, FINSEQ_1: 17;

          then

           A28: ( dom ck) = ( dom fk) by A13, A27, FINSEQ_1: 17;

          

           A29: ( dom ck) c= ( dom c) by RELAT_1: 60;

          (ck . i) = (c . i) by A26, FUNCT_1: 47;

          then (ck . i) = ( card (f . i)) by A12, A26, A29;

          hence thesis by A26, A28, FUNCT_1: 47;

        end;

        then

         A30: ( card Xk) = ( Sum ck) by A7, A17, A18, A19, A25;

        reconsider fk1 = (f . (k + 1)) as set;

        for x be set st x in Zk holds x misses fk1

        proof

          let x be set such that

           A31: x in Zk;

          

           A32: x in Z by A31;

          ( dom f) = ( Seg ( len f)) by FINSEQ_1:def 3;

          then

           A33: fk1 in ( rng f) by A13, FINSEQ_1: 4, FUNCT_1: 3;

          consider i be Nat such that

           A34: i in ( dom fk) and

           A35: (fk . i) = x by A31, FINSEQ_2: 10;

          now

            assume

             A36: (fk . i) = fk1;

            

             A37: ( dom fk) = ( Seg k) by A15, FINSEQ_1:def 3;

            

             A38: i in ( Seg k) by A15, A34, FINSEQ_1:def 3;

            i <= k by A34, A37, FINSEQ_1: 1;

            then

             A39: i < (k + 1) by NAT_1: 13;

            

             A40: ( dom f) = ( Seg (k + 1)) by A13, FINSEQ_1:def 3;

            k <= (k + 1) by NAT_1: 12;

            then

             A41: ( Seg k) c= ( Seg (k + 1)) by FINSEQ_1: 5;

            

             A42: (k + 1) in ( dom f) by A40, FINSEQ_1: 4;

            (fk . i) = (f . i) by A34, FUNCT_1: 47;

            hence contradiction by A9, A36, A38, A39, A40, A41, A42;

          end;

          hence thesis by A10, A32, A33, A35, EQREL_1:def 4;

        end;

        then

         A43: fk1 misses Xk by ZFMISC_1: 80;

        ( dom f) = ( Seg ( len f)) by FINSEQ_1:def 3;

        then fk1 in ( rng f) by A13, FINSEQ_1: 4, FUNCT_1: 3;

        then

        reconsider fk1 as finite set;

        

         A44: Z = (( rng fk) \/ ( rng <*fk1*>)) by A10, A16, FINSEQ_1: 31

        .= (Zk \/ {fk1}) by FINSEQ_1: 39;

        

         A45: X = ( union Z) by EQREL_1:def 4

        .= (( union Zk) \/ ( union {fk1})) by A44, ZFMISC_1: 78

        .= (Xk \/ fk1) by ZFMISC_1: 25;

        (k + 1) in ( Seg (k + 1)) by FINSEQ_1: 4;

        then

         A46: (k + 1) in ( dom c) by A11, A13, FINSEQ_1:def 3;

        ( rng ck) c= REAL ;

        then

        reconsider ckc = ck as FinSequence of REAL by FINSEQ_1:def 4;

        ( card X) = (( Sum ck) + ( card fk1)) by A30, A43, A45, CARD_2: 40

        .= (( Sum ck) + (c . (k + 1))) by A12, A46

        .= ( Sum (ckc ^ <*(c . (k + 1))*>)) by RVSUM_1: 74

        .= ( Sum c) by A11, A13, FINSEQ_3: 55;

        hence thesis;

      end;

      

       A47: for k be Nat holds P[k] from NAT_1:sch 2( A1, A6);

      let X be finite set, Y be a_partition of X;

      ( card Y) = ( card Y);

      hence thesis by A47;

    end;

    begin

    registration

      let G be finite Group;

      cluster ( center G) -> finite;

      correctness ;

    end

    definition

      let G be Group, a be Element of G;

      :: WEDDWITT:def1

      func Centralizer a -> strict Subgroup of G means

      : Def1: the carrier of it = { b where b be Element of G : (a * b) = (b * a) };

      existence

      proof

        set Car = { b where b be Element of G : (a * b) = (b * a) };

        

         A1: (a * ( 1_ G)) = a by GROUP_1:def 4;

        (( 1_ G) * a) = a by GROUP_1:def 4;

        then

         A2: ( 1_ G) in Car by A1;

        for x be object st x in Car holds x in the carrier of G

        proof

          let x be object;

          assume x in Car;

          then ex g be Element of G st (x = g) & ((a * g) = (g * a));

          hence thesis;

        end;

        then

         A3: Car is Subset of G by TARSKI:def 3;

        

         A4: for g1,g2 be Element of G st g1 in Car & g2 in Car holds (g1 * g2) in Car

        proof

          let g1,g2 be Element of G such that

           A5: g1 in Car and

           A6: g2 in Car;

          

           A7: ex z1 be Element of G st (z1 = g1) & ((z1 * a) = (a * z1)) by A5;

          

           A8: ex z2 be Element of G st (z2 = g2) & ((z2 * a) = (a * z2)) by A6;

          (a * (g1 * g2)) = ((g1 * a) * g2) by A7, GROUP_1:def 3

          .= (g1 * (g2 * a)) by A8, GROUP_1:def 3

          .= ((g1 * g2) * a) by GROUP_1:def 3;

          hence thesis;

        end;

        for g be Element of G st g in Car holds (g " ) in Car

        proof

          let g be Element of G;

          assume g in Car;

          then

           A9: ex z1 be Element of G st (z1 = g) & ((z1 * a) = (a * z1));

          ((g " ) * (g * a)) = a by GROUP_3: 1;

          then ((g " ) * ((a * g) * (g " ))) = (a * (g " )) by A9, GROUP_1:def 3;

          then ((g " ) * a) = (a * (g " )) by GROUP_3: 1;

          hence thesis;

        end;

        hence thesis by A2, A3, A4, GROUP_2: 52;

      end;

      uniqueness

      proof

        let H1,H2 be strict Subgroup of G such that

         A10: the carrier of H1 = { b where b be Element of G : (a * b) = (b * a) } and

         A11: the carrier of H2 = { b where b be Element of G : (a * b) = (b * a) };

        for g be Element of G holds g in H1 iff g in H2 by A10, A11;

        hence thesis;

      end;

    end

    registration

      let G be finite Group;

      let a be Element of G;

      cluster ( Centralizer a) -> finite;

      correctness ;

    end

    theorem :: WEDDWITT:7

    

     Th7: for G be Group, a be Element of G, x be set st x in ( Centralizer a) holds x in G

    proof

      let G be Group, a be Element of G, x be set;

      assume

       A1: x in ( Centralizer a);

      the carrier of ( Centralizer a) = { b where b be Element of G : (a * b) = (b * a) } by Def1;

      then x in { b where b be Element of G : (a * b) = (b * a) } by A1;

      then ex b be Element of G st b = x & (a * b) = (b * a);

      hence thesis;

    end;

    theorem :: WEDDWITT:8

    

     Th8: for G be Group, a,x be Element of G holds (a * x) = (x * a) iff x is Element of ( Centralizer a)

    proof

      let G be Group, a,x be Element of G;

      

       A1: the carrier of ( Centralizer a) = { b where b be Element of G : (a * b) = (b * a) } by Def1;

      hereby

        assume (a * x) = (x * a);

        then x in the carrier of ( Centralizer a) by A1;

        hence x is Element of ( Centralizer a);

      end;

      assume x is Element of ( Centralizer a);

      then x in the carrier of ( Centralizer a);

      then ex b be Element of G st b = x & (a * b) = (b * a) by A1;

      hence thesis;

    end;

    registration

      let G be Group, a be Element of G;

      cluster ( con_class a) -> non empty;

      correctness by GROUP_3: 83;

    end

    definition

      let G be Group, a be Element of G;

      :: WEDDWITT:def2

      func a -con_map -> Function of the carrier of G, ( con_class a) means

      : Def2: for x be Element of G holds (it . x) = (a |^ x);

      existence

      proof

        defpred P[ Element of G, set] means $2 = (a |^ $1);

        

         A1: for x be Element of G holds ex y be Element of ( con_class a) st P[x, y]

        proof

          let x be Element of G;

          (a |^ x) in ( con_class a) by GROUP_3: 82;

          hence thesis;

        end;

        ex f be Function of the carrier of G, ( con_class a) st for x be Element of G holds P[x, (f . x)] from FUNCT_2:sch 3( A1);

        hence thesis;

      end;

      uniqueness

      proof

        let it1,it2 be Function of the carrier of G, ( con_class a) such that

         A2: for x be Element of G holds (it1 . x) = (a |^ x) and

         A3: for x be Element of G holds (it2 . x) = (a |^ x);

        

         A4: ( dom it1) = the carrier of G by FUNCT_2:def 1;

        

         A5: ( dom it2) = the carrier of G by FUNCT_2:def 1;

        for x be object st x in ( dom it1) holds (it1 . x) = (it2 . x)

        proof

          let x be object;

          assume x in ( dom it1);

          then

          reconsider y = x as Element of G;

          (it1 . y) = (a |^ y) by A2;

          hence thesis by A3;

        end;

        hence thesis by A4, A5;

      end;

    end

    theorem :: WEDDWITT:9

    

     Th9: for G be finite Group, a be Element of G, x be Element of ( con_class a) holds ( card ((a -con_map ) " {x})) = ( card ( Centralizer a))

    proof

      let G be finite Group, a be Element of G, x be Element of ( con_class a);

      ex b be Element of G st (b = x) & ((a,b) are_conjugated ) by GROUP_3: 80;

      then

      consider d be 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 be 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 be object holds g in ((a -con_map ) " {x}) iff g in Cad

      proof

        let g be object;

         A3:

        now

          assume

           A4: g in ((a -con_map ) " {x});

          then ((a -con_map ) . g) in {x} by FUNCT_1:def 7;

          then

           A5: ((a -con_map ) . g) = x by TARSKI:def 1;

          reconsider y = g as Element of G by A4;

          

           A6: ((a -con_map ) . g) = (a |^ y) by Def2;

          

           A7: (y * (((d " ) * a) * d)) = ((y * ((d " ) * a)) * d) by GROUP_1:def 3

          .= (((y * (d " )) * a) * d) by GROUP_1:def 3;

          (y * (((y " ) * a) * y)) = ((y * ((y " ) * a)) * y) by GROUP_1:def 3

          .= (a * y) by GROUP_3: 1;

          then ((((y * (d " )) * a) * d) * (d " )) = (a * (y * (d " ))) by A1, A5, A6, A7, GROUP_1:def 3;

          then ((y * (d " )) * a) = (a * (y * (d " ))) by GROUP_3: 1;

          then (y * (d " )) is Element of ( Centralizer a) by Th8;

          then

          consider z be Element of G such that

           A8: z in the carrier of ( Centralizer a) and

           A9: (y * (d " )) = z;

          

           A10: z in ( Centralizer a) by A8;

          reconsider z as Element of G;

          y = (z * d) by A9, GROUP_3: 1;

          hence g in Cad by A10, GROUP_2: 104;

        end;

        now

          assume g in Cad;

          then

          consider z be Element of G such that

           A11: g = (z * d) and

           A12: z in ( Centralizer a) by GROUP_2: 104;

          reconsider y = g as Element of G by A11;

          (y * (d " )) = z by A11, GROUP_3: 1;

          then (y * (d " )) in ( carr ( Centralizer a)) by A12;

          then ((y * (d " )) * a) = (a * (y * (d " ))) by Th8;

          then (((y * (d " )) * a) * d) = (a * ((y * (d " )) * d)) by GROUP_1:def 3;

          then (((y * (d " )) * a) * d) = (a * y) by GROUP_3: 1;

          then ((y * (d " )) * (a * d)) = (a * y) by GROUP_1:def 3;

          then ((y " ) * ((y * (d " )) * (a * d))) = (((y " ) * a) * y) by GROUP_1:def 3;

          then (((y " ) * (y * (d " ))) * (a * d)) = (((y " ) * a) * y) by GROUP_1:def 3;

          then ((d " ) * (a * d)) = (((y " ) * a) * y) by GROUP_3: 1;

          then x = (a |^ y) by A1, GROUP_1:def 3;

          then ((a -con_map ) . y) = x by Def2;

          then

           A13: ((a -con_map ) . y) in {x} by TARSKI:def 1;

          ( dom (a -con_map )) = the carrier of G by FUNCT_2:def 1;

          hence g in ((a -con_map ) " {x}) by A13, FUNCT_1:def 7;

        end;

        hence thesis by A3;

      end;

      hence thesis by A2, TARSKI: 2;

    end;

    theorem :: WEDDWITT:10

    

     Th10: for G be Group, a be Element of G, x,y be Element of ( con_class a) st x <> y holds ((a -con_map ) " {x}) misses ((a -con_map ) " {y})

    proof

      let G be Group, a be Element of G, x,y be Element of ( con_class a) such that

       A1: x <> y;

      now

        assume ex g be object st g in (((a -con_map ) " {x}) /\ ((a -con_map ) " {y}));

        then

        consider g be set such that

         A2: g in (((a -con_map ) " {x}) /\ ((a -con_map ) " {y}));

        

         A3: g in ((a -con_map ) " {x}) by A2, XBOOLE_0:def 4;

        

         A4: g in ((a -con_map ) " {y}) by A2, XBOOLE_0:def 4;

        ((a -con_map ) . g) in {x} by A3, FUNCT_1:def 7;

        then

         A5: ((a -con_map ) . g) = x by TARSKI:def 1;

        ((a -con_map ) . g) in {y} by A4, FUNCT_1:def 7;

        hence contradiction by A1, A5, TARSKI:def 1;

      end;

      then (((a -con_map ) " {x}) /\ ((a -con_map ) " {y})) = {} by XBOOLE_0:def 1;

      hence thesis by XBOOLE_0:def 7;

    end;

    theorem :: WEDDWITT:11

    

     Th11: for G be Group, a be Element of G holds the set of all ((a -con_map ) " {x}) where x be Element of ( con_class a) is a_partition of the carrier of G

    proof

      let G be Group, a be Element of G;

      reconsider X = the set of all ((a -con_map ) " {x}) where x be Element of ( con_class a) as set;

      

       A1: for y be object holds y in ( union X) implies y in the carrier of G

      proof

        let x be object;

        assume x in ( union X);

        then

        consider Y be set such that

         A2: x in Y and

         A3: Y in X by TARSKI:def 4;

        ex z be Element of ( con_class a) st (((a -con_map ) " {z}) = Y) by A3;

        hence thesis by A2;

      end;

      for y be object holds y in the carrier of G implies y in ( union X)

      proof

        let x be object;

        assume x in the carrier of G;

        then

        reconsider y = x as Element of G;

        consider z be Element of G such that

         A4: z in ( con_class a) and

         A5: z = (a |^ y) by GROUP_3: 82;

        ((a -con_map ) . y) = z by A5, Def2;

        then

         A6: ((a -con_map ) . y) in {z} by TARSKI:def 1;

        ( dom (a -con_map )) = the carrier of G by FUNCT_2:def 1;

        then

         A7: y in ((a -con_map ) " {z}) by A6, FUNCT_1:def 7;

        ((a -con_map ) " {z}) in X by A4;

        hence thesis by A7, TARSKI:def 4;

      end;

      then

       A8: ( union X) = the carrier of G by A1, TARSKI: 2;

      

       A9: for A be Subset of G st A in X holds A <> {} & for B be Subset of G st B in X holds A = B or A misses B

      proof

        let A be Subset of G;

        assume A in X;

        then

        consider x be Element of ( con_class a) such that

         A10: A = ((a -con_map ) " {x});

        (a,x) are_conjugated by GROUP_3: 81;

        then

        consider g be 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 be Subset of G st B in X holds A = B or A misses B

        proof

          let B be Subset of G;

          assume B in X;

          then ex y be Element of ( con_class a) st (B = ((a -con_map ) " {y}));

          hence thesis by A10, Th10;

        end;

        hence thesis by A10, A12, A13, FUNCT_1:def 7;

      end;

      X c= ( bool ( union X)) by ZFMISC_1: 82;

      hence thesis by A8, A9, EQREL_1:def 4;

    end;

    theorem :: WEDDWITT:12

    

     Th12: for G be finite Group, a be Element of G holds ( card the set of all ((a -con_map ) " {x}) where x be Element of ( con_class a)) = ( card ( con_class a))

    proof

      let G be finite Group, a be Element of G;

      reconsider X = the set of all ((a -con_map ) " {x}) where x be Element of ( con_class a) as a_partition of the carrier of G by Th11;

      deffunc FF( object) = ((a -con_map ) " {$1});

      

       A1: for x be object st x in ( con_class a) holds FF(x) in X;

      consider F be Function of ( con_class a), X such that

       A2: for x be object st x in ( con_class a) holds (F . x) = FF(x) from FUNCT_2:sch 2( A1);

      for c be object st c in X holds ex x be object st x in ( con_class a) & c = (F . x)

      proof

        let c be object such that

         A3: c in X;

        reconsider c as Subset of G by A3;

        consider y be Element of ( con_class a) such that

         A4: c = ((a -con_map ) " {y}) by A3;

        (F . y) = c by A2, A4;

        hence thesis;

      end;

      then

       A5: ( rng F) = X by FUNCT_2: 10;

      

       A6: ( dom F) = ( con_class a) by FUNCT_2:def 1;

      for x1,x2 be object st x1 in ( dom F) & x2 in ( dom F) & (F . x1) = (F . x2) holds x1 = x2

      proof

        let x1,x2 be object such that

         A7: x1 in ( dom F) and

         A8: x2 in ( dom F) and

         A9: (F . x1) = (F . x2);

        reconsider y1 = x1 as Element of ( con_class a) by A7;

        reconsider y2 = x2 as Element of ( con_class a) by A8;

        

         A10: ((a -con_map ) " {y1}) = (F . y1) by A2;

        

         A11: ((a -con_map ) " {y2}) = (F . y2) by A2;

        now

          assume y1 <> y2;

          then ((a -con_map ) " {y1}) misses ((a -con_map ) " {y2}) by Th10;

          then (((a -con_map ) " {y1}) /\ ((a -con_map ) " {y2})) = {} by XBOOLE_0:def 7;

          hence contradiction by A9, A10, A11;

        end;

        hence thesis;

      end;

      then F is one-to-one;

      then (( con_class a),(F .: ( con_class a))) are_equipotent by A6, CARD_1: 33;

      then (( con_class a),( rng F)) are_equipotent by A6, RELAT_1: 113;

      hence thesis by A5, CARD_1: 5;

    end;

    theorem :: WEDDWITT:13

    

     Th13: for G be finite Group, a be Element of G holds ( card G) = (( card ( con_class a)) * ( card ( Centralizer a)))

    proof

      let G be finite Group, a be Element of G;

      reconsider X = the set of all ((a -con_map ) " {x}) where x be Element of ( con_class a) as a_partition of the carrier of G by Th11;

      

       A1: for A be set st A in X holds A is finite & ( card A) = ( card ( Centralizer a)) & for B be set st B in X & A <> B holds A misses B

      proof

        let A be set such that

         A2: A in X;

        reconsider A as Subset of G by A2;

        ex x be Element of ( con_class a) st (A = ((a -con_map ) " {x})) by A2;

        hence thesis by A2, Th9, EQREL_1:def 4;

      end;

      reconsider k = ( card ( Centralizer a)) as Element of NAT ;

      for Y be set st Y in X holds ex B be finite set st B = Y & ( card B) = k & for Z be set st Z in X & Y <> Z holds (Y,Z) are_equipotent & Y misses Z

      proof

        let Y be set such that

         A3: Y in X;

        reconsider Y as finite set by A3;

        

         A4: ( card Y) = ( card ( Centralizer a)) by A1, A3;

        for Z be set st Z in X & Y <> Z holds (Y,Z) are_equipotent & Y misses Z

        proof

          let Z be set such that

           A5: Z in X and

           A6: Y <> Z;

          

           A7: ( card Y) = ( card ( Centralizer a)) by A1, A3;

          ( card Z) = ( card ( Centralizer a)) by A1, A5;

          hence thesis by A1, A3, A5, A6, A7, CARD_1: 5;

        end;

        hence thesis by A4;

      end;

      then

      consider C be finite set such that

       A8: C = ( union X) and

       A9: ( card C) = (( card X) * k) by GROUP_2: 156;

      ( card G) = ( card C) by A8, EQREL_1:def 4

      .= (( card ( con_class a)) * ( card ( Centralizer a))) by A9, Th12;

      hence thesis;

    end;

    definition

      let G be Group;

      :: WEDDWITT:def3

      func conjugate_Classes G -> a_partition of the carrier of G equals the set of all ( con_class a) where a be Element of G;

      correctness

      proof

        set cG = the carrier of G;

        set C = the set of all ( con_class a) where a be Element of G;

        

         A1: C c= ( bool cG)

        proof

          let x be object;

          assume x in C;

          then ex a be Element of cG st x = ( con_class a);

          hence thesis;

        end;

        now

          let x be object;

          hereby

            assume x in ( union C);

            then

            consider S be set such that

             A2: x in S and

             A3: S in C by TARSKI:def 4;

            ex a be Element of G st S = ( con_class a) by A3;

            hence x in cG by A2;

          end;

          assume x in cG;

          then

          reconsider x9 = x as Element of cG;

          reconsider S = ( con_class x9) as Subset of cG;

          

           A4: S in C;

          x9 in ( con_class x9) by GROUP_3: 83;

          hence x in ( union C) by A4, TARSKI:def 4;

        end;

        then

         A5: ( union C) = cG by TARSKI: 2;

        now

          let A be Subset of cG;

          assume

           A6: A in C;

          then

           A7: ex a be Element of cG st A = ( con_class a);

          consider a be Element of cG such that

           A8: A = ( con_class a) by A6;

          thus A <> {} by A7;

          let B be Subset of cG;

          assume B in C;

          then

          consider b be Element of cG such that

           A9: B = ( con_class b);

          assume

           A10: A <> B;

          assume A meets B;

          then

          consider x be object such that

           A11: x in A and

           A12: x in B by XBOOLE_0: 3;

          reconsider x as Element of cG by A11;

          

           A13: (x,a) are_conjugated by A8, A11, GROUP_3: 81;

          (x,b) are_conjugated by A9, A12, GROUP_3: 81;

          then

           A14: (a,b) are_conjugated by A13, GROUP_3: 77;

          now

            let c be object;

            hereby

              assume

               A15: c in A;

              then

              reconsider c9 = c as Element of cG;

              (c9,a) are_conjugated by A8, A15, GROUP_3: 81;

              then (c9,b) are_conjugated by A14, GROUP_3: 77;

              hence c in B by A9, GROUP_3: 81;

            end;

            assume

             A16: c in B;

            then

            reconsider c9 = c as Element of cG;

            (c9,b) are_conjugated by A9, A16, GROUP_3: 81;

            then (c9,a) are_conjugated by A14, GROUP_3: 77;

            hence c in A by A8, GROUP_3: 81;

          end;

          hence contradiction by A10, TARSKI: 2;

        end;

        hence thesis by A1, A5, EQREL_1:def 4;

      end;

    end

    theorem :: WEDDWITT:14

    for G be finite Group, f be FinSequence of ( conjugate_Classes G) st f is one-to-one & ( rng f) = ( conjugate_Classes G) holds for c be FinSequence of NAT st ( len c) = ( len f) & for i be Element of NAT st i in ( dom c) holds (c . i) = ( card (f . i)) holds ( card G) = ( Sum c) by Th6;

    begin

    theorem :: WEDDWITT:15

    

     Th15: for F be finite Field, V be VectSp of F, n,q be Nat st V is finite-dimensional & n = ( dim V) & q = ( card the carrier of F) holds ( card the carrier of V) = (q |^ n)

    proof

      let F be finite Field, V be VectSp of F, n,q be Nat such that

       A1: V is finite-dimensional and

       A2: n = ( dim V) and

       A3: q = ( card the carrier of F);

      consider B be finite Subset of V such that

       A4: B is Basis of V by A1, MATRLIN:def 1;

      

       A5: B is linearly-independent by A4, VECTSP_7:def 3;

      

       A6: ( Lin B) = the ModuleStr of V by A4, VECTSP_7:def 3;

      

       A7: ( card B) = n by A1, A2, A4, VECTSP_9:def 1;

      now

        per cases ;

          suppose

           A8: n = 0 ;

          then ( (Omega). V) = ( (0). V) by A1, A2, VECTSP_9: 29;

          then the ModuleStr of V = ( (0). V) by VECTSP_4:def 4;

          then the carrier of V = {( 0. V)} by VECTSP_4:def 3;

          

          then ( card the carrier of V) = 1 by CARD_1: 30

          .= (q #Z 0 ) by PREPOWER: 34

          .= (q |^ 0 ) by PREPOWER: 36;

          hence thesis by A8;

        end;

          suppose n <> 0 ;

          then

           A9: B <> 0 by A7;

          consider bf be FinSequence such that

           A10: ( rng bf) = B and

           A11: bf is one-to-one by FINSEQ_4: 58;

          ( len bf) = n by A7, A10, A11, FINSEQ_4: 62;

          then

           A12: ( Seg n) = ( dom bf) by FINSEQ_1:def 3;

          reconsider Vbf = bf as FinSequence of the carrier of V by A10, FINSEQ_1:def 4;

          set cLinB = the carrier of ( Lin B);

          set ntocF = (n -tuples_on the carrier of F);

          defpred P[ Function, set] means ex lc be Linear_Combination of B st (for i be set st i in ( dom $1) holds (lc . (Vbf . i)) = ($1 . i)) & $2 = ( Sum (lc (#) Vbf));

          

           A13: for x be Element of ntocF holds ex y be Element of cLinB st P[x, y]

          proof

            let f be Element of ntocF;

            ex lc be Linear_Combination of B st for i be set st i in ( dom f) holds (lc . (Vbf . i)) = (f . i)

            proof

              deffunc LC( object) = (f . ( union (Vbf " {$1})));

              

               A14: for x be object st x in B holds LC(x) in the carrier of F

              proof

                let x be object;

                assume x in B;

                then

                consider i be object such that

                 A15: (Vbf " {x}) = {i} by A10, A11, FUNCT_1: 74;

                

                 A16: ( union (Vbf " {x})) = i by A15, ZFMISC_1: 25;

                i in (Vbf " {x}) by A15, TARSKI:def 1;

                then i in ( dom Vbf) by FUNCT_1:def 7;

                then i in ( dom f) by A12, FINSEQ_2: 124;

                then (f . i) in ( rng f) by FUNCT_1: 3;

                hence thesis by A16;

              end;

              consider lc be Function of B, the carrier of F such that

               A17: for y be object st y in B holds (lc . y) = LC(y) from FUNCT_2:sch 2( A14);

              set ll = (lc +* ((the carrier of V \ B) --> ( 0. F)));

              

               A18: ( dom ((the carrier of V \ B) --> ( 0. F))) = (the carrier of V \ B);

              then ( dom ll) = (( dom lc) \/ (the carrier of V \ B)) by FUNCT_4:def 1;

              then ( dom ll) = (B \/ (the carrier of V \ B)) by FUNCT_2:def 1;

              then ( dom ll) = (B \/ the carrier of V) by XBOOLE_1: 39;

              then

               A19: ( dom ll) = the carrier of V by XBOOLE_1: 12;

              ( rng ll) c= (( rng lc) \/ ( rng ((the carrier of V \ B) --> ( 0. F)))) by FUNCT_4: 17;

              then ll is Function of the carrier of V, the carrier of F by A19, FUNCT_2: 2, XBOOLE_1: 1;

              then

               A20: ll is Element of ( Funcs (the carrier of V,the carrier of F)) by FUNCT_2: 8;

              

               A21: for i be set st i in ( dom f) holds (ll . (Vbf . i)) = (f . i)

              proof

                let i be set;

                assume i in ( dom f);

                then

                 A22: i in ( dom Vbf) by A12, FINSEQ_2: 124;

                then (Vbf . i) in B by A10, FUNCT_1: 3;

                then

                consider y be Element of B such that

                 A23: y = (Vbf . i);

                

                 A24: (Vbf . i) in {y} by A23, TARSKI:def 1;

                consider ee be object such that

                 A25: (Vbf " {y}) c= {ee} by A11, FUNCT_1: 89;

                

                 A26: i in (Vbf " {y}) by A22, A24, FUNCT_1:def 7;

                then {i} c= {ee} by A25, ZFMISC_1: 31;

                then i = ee by ZFMISC_1: 18;

                then

                 A27: (Vbf " {y}) = {i} by A25, A26, ZFMISC_1: 33;

                 not y in (the carrier of V \ B) by A9, XBOOLE_0:def 5;

                then (ll . y) = (lc . y) by A18, FUNCT_4: 11;

                then (ll . y) = (f . ( union (Vbf " {y}))) by A9, A17;

                hence thesis by A23, A27, ZFMISC_1: 25;

              end;

              

               A28: for v be Element of V st not v in B holds (ll . v) = ( 0. F)

              proof

                let v be Element of V;

                assume not v in B;

                then

                 A29: v in (the carrier of V \ B) by XBOOLE_0:def 5;

                then (ll . v) = (((the carrier of V \ B) --> ( 0. F)) . v) by A18, FUNCT_4: 13;

                hence thesis by A29, FUNCOP_1: 7;

              end;

              then

              reconsider L = ll as Linear_Combination of V by A20, VECTSP_6:def 1;

              for v be Element of V holds v in ( Carrier L) implies v in B

              proof

                let v be Element of V;

                assume

                 A30: v in ( Carrier L);

                now

                  assume not v in B;

                  then (ll . v) = ( 0. F) by A28;

                  hence contradiction by A30, VECTSP_6: 2;

                end;

                hence thesis;

              end;

              then ( Carrier L) c= B;

              then L is Linear_Combination of B by VECTSP_6:def 4;

              hence thesis by A21;

            end;

            then

            consider lc be Linear_Combination of B such that

             A31: for i be set st i in ( dom f) holds (lc . (Vbf . i)) = (f . i);

            ex y be Element of V st y = ( Sum (lc (#) Vbf));

            hence thesis by A6, A31;

          end;

          consider G be Function of ntocF, cLinB such that

           A32: for tup be Element of ntocF holds P[tup, (G . tup)] from FUNCT_2:sch 3( A13);

          

           A33: ( dom G) = ntocF by FUNCT_2:def 1;

          

           A34: for L be Linear_Combination of B holds ex nt be Element of ntocF st for i be object st i in ( dom nt) holds (nt . i) = (L . (Vbf . i))

          proof

            let L be Linear_Combination of B;

            deffunc F( object) = (L . (Vbf . $1));

            

             A35: for x be object st x in ( Seg n) holds F(x) in the carrier of F

            proof

              let x be object;

              assume x in ( Seg n);

              then (Vbf . x) in ( rng Vbf) by A12, FUNCT_1: 3;

              then

              consider vv be Element of V such that

               A36: (Vbf . x) = vv;

              (L . vv) in the carrier of F;

              hence thesis by A36;

            end;

            consider f be Function of ( Seg n), the carrier of F such that

             A37: for x be object st x in ( Seg n) holds (f . x) = F(x) from FUNCT_2:sch 2( A35);

            

             A38: ( dom f) = ( Seg n) by FUNCT_2:def 1;

            

             A39: ( rng f) c= the carrier of F;

            

             A40: n is Element of NAT by ORDINAL1:def 12;

            f is FinSequence-like by A38, FINSEQ_1:def 2;

            then

            reconsider ff = f as FinSequence of the carrier of F by A39, FINSEQ_1:def 4;

            ( len ff) = n by A38, A40, FINSEQ_1:def 3;

            then ff is Element of ntocF by FINSEQ_2: 92;

            hence thesis by A37, A38;

          end;

          for c be object st c in cLinB holds ex x be object st x in ntocF & c = (G . x)

          proof

            let c be object;

            assume c in cLinB;

            then c in ( Lin B);

            then

            consider l be 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 be Element of ntocF such that

             A43: for i be object st i in ( dom t) holds (t . i) = (l . (Vbf . i)) by A34;

            consider lc be Linear_Combination of B such that

             A44: for i be set st i in ( dom t) holds (lc . (Vbf . i)) = (t . i) and

             A45: (G . t) = ( Sum (lc (#) Vbf)) by A32;

            for v be Element of V holds (l . v) = (lc . v)

            proof

              let v be Element of V;

              now

                per cases ;

                  suppose v in ( rng Vbf);

                  then

                  consider x be object such that

                   A46: [x, v] in Vbf by XTUPLE_0:def 13;

                  

                   A47: x in ( dom Vbf) by A46, FUNCT_1: 1;

                  

                   A48: (Vbf . x) = v by A46, FUNCT_1: 1;

                  

                   A49: x in ( dom t) by A12, A47, FINSEQ_2: 124;

                  then (l . (Vbf . x)) = (t . x) by A43;

                  hence thesis by A44, A48, A49;

                end;

                  suppose

                   A50: not v in ( rng Vbf);

                  now

                    assume

                     A51: v in ( Carrier l);

                    ( Carrier l) c= ( rng Vbf) by A10, VECTSP_6:def 4;

                    hence contradiction by A50, A51;

                  end;

                  then

                   A52: (l . v) = ( 0. F) by VECTSP_6: 2;

                  now

                    assume

                     A53: v in ( Carrier lc);

                    ( Carrier lc) c= ( rng Vbf) by A10, VECTSP_6:def 4;

                    hence contradiction by A50, A53;

                  end;

                  hence thesis by A52, VECTSP_6: 2;

                end;

              end;

              hence thesis;

            end;

            then (G . t) = ( Sum (l (#) Vbf)) by A45, VECTSP_6:def 7;

            hence thesis by A41, A42;

          end;

          then

           A54: ( rng G) = cLinB by FUNCT_2: 10;

          for x1,x2 be object st x1 in ( dom G) & x2 in ( dom G) & (G . x1) = (G . x2) holds x1 = x2

          proof

            let x1,x2 be object such that

             A55: x1 in ( dom G) and

             A56: x2 in ( dom G) and

             A57: (G . x1) = (G . x2);

            reconsider t1 = x1 as Element of ntocF by A55;

            reconsider t2 = x2 as Element of ntocF by A56;

            consider L1 be Linear_Combination of B such that

             A58: for i be set st i in ( dom t1) holds (L1 . (Vbf . i)) = (t1 . i) and

             A59: (G . t1) = ( Sum (L1 (#) Vbf)) by A32;

            consider L2 be Linear_Combination of B such that

             A60: for i be 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 be Element of V holds (L1 . v) = (L2 . v)

            proof

              let v be Element of V;

              reconsider LL = (L1 - L2) as Linear_Combination of B by VECTSP_6: 42;

              (LL . v) = ( 0. F) by A64, VECTSP_6: 2;

              then ( 0. F) = ((L1 . v) - (L2 . v)) by VECTSP_6: 40;

              hence thesis by VECTSP_1: 27;

            end;

            then

             A65: L1 = L2 by VECTSP_6:def 7;

            

             A66: ( dom t1) = ( Seg n) by FINSEQ_2: 124;

            

             A67: ( dom t2) = ( Seg n) by FINSEQ_2: 124;

            for k be Nat st k in ( dom t1) holds (t1 . k) = (t2 . k)

            proof

              let k be Nat such that

               A68: k in ( dom t1);

              (t1 . k) = (L1 . (Vbf . k)) by A58, A68;

              hence thesis by A60, A65, A66, A67, A68;

            end;

            hence thesis by A67, FINSEQ_1: 13, FINSEQ_2: 124;

          end;

          then G is one-to-one;

          then (ntocF,(G .: ntocF)) are_equipotent by A33, CARD_1: 33;

          then

           A69: (ntocF,cLinB) are_equipotent by A33, A54, RELAT_1: 113;

          

           A70: ( card ( Seg n)) = ( card n) by FINSEQ_1: 55;

          

           A71: ( card q) = ( card the carrier of F) by A3;

          ( card ntocF) = ( card ( Funcs (( Seg n),the carrier of F))) by FINSEQ_2: 93

          .= ( card ( Funcs (n,q))) by A70, A71, FUNCT_5: 61

          .= (q |^ n) by A3, Th4;

          hence thesis by A6, A69, CARD_1: 5;

        end;

      end;

      hence thesis;

    end;

    definition

      let R be Skew-Field;

      :: WEDDWITT:def4

      func center R -> strict Field means

      : Def4: the carrier of it = { x where x be Element of R : for s be Element of R holds (x * s) = (s * x) } & the addF of it = (the addF of R || the carrier of it ) & the multF of it = (the multF of R || the carrier of it ) & ( 0. it ) = ( 0. R) & ( 1. it ) = ( 1. R);

      existence

      proof

        set cR = the carrier of R;

        set ccs = { x where x be Element of R : for s be Element of R holds (x * s) = (s * x) };

        for s be Element of cR holds (( 0. R) * s) = (s * ( 0. R));

        then

         A1: ( 0. R) in ccs;

        then

        reconsider ccs as non empty set;

        

         A2: ccs c= cR

        proof

          let x be object;

          assume x in ccs;

          then ex x9 be Element of cR st x9 = x & for s be Element of R holds (x9 * s) = (s * x9);

          hence thesis;

        end;

        set acs = (the addF of R || ccs);

        set mcs = (the multF of R || ccs);

        set Zs = ( 0. R);

        set Us = ( 1_ R);

        

         A3: [:ccs, ccs:] c= [:cR, cR:]

        proof

          let x be object;

          assume x in [:ccs, ccs:];

          then ex a,b be object st (a in ccs) & (b in ccs) & (x = [a, b]) by ZFMISC_1:def 2;

          hence thesis by A2, ZFMISC_1:def 2;

        end;

        then

        reconsider acs as Function of [:ccs, ccs:], cR by FUNCT_2: 32;

        ( rng acs) c= ccs

        proof

          let y be object;

          assume y in ( rng acs);

          then

          consider x be object such that

           A4: x in ( dom acs) and

           A5: y = (acs . x) by FUNCT_1:def 3;

          consider a,b be object such that

           A6: a in ccs and

           A7: b in ccs and

           A8: x = [a, b] by A4, ZFMISC_1:def 2;

          reconsider a, b as Element of cR by A2, A6, A7;

          

           A9: ex a9 be Element of cR st a9 = a & for s be Element of R holds (a9 * s) = (s * a9) by A6;

          

           A10: ex b9 be Element of cR st b9 = b & for s be Element of R holds (b9 * s) = (s * b9) by A7;

           [a, b] in [:ccs, ccs:] by A6, A7, ZFMISC_1:def 2;

          then

           A11: (a + b) = (acs . x) by A8, FUNCT_1: 49;

          now

            let s be Element of cR;

            

            thus ((a + b) * s) = ((a * s) + (b * s)) by VECTSP_1:def 3

            .= ((s * a) + (b * s)) by A9

            .= ((s * a) + (s * b)) by A10

            .= (s * (a + b)) by VECTSP_1:def 2;

          end;

          hence thesis by A5, A11;

        end;

        then

        reconsider acs as BinOp of ccs by FUNCT_2: 6;

        reconsider mcs as Function of [:ccs, ccs:], cR by A3, FUNCT_2: 32;

        ( rng mcs) c= ccs

        proof

          let y be object;

          assume y in ( rng mcs);

          then

          consider x be object such that

           A12: x in ( dom mcs) and

           A13: y = (mcs . x) by FUNCT_1:def 3;

          consider a,b be object such that

           A14: a in ccs and

           A15: b in ccs and

           A16: x = [a, b] by A12, ZFMISC_1:def 2;

          reconsider a, b as Element of cR by A2, A14, A15;

          

           A17: ex a9 be Element of cR st a9 = a & for s be Element of R holds (a9 * s) = (s * a9) by A14;

          

           A18: ex b9 be Element of cR st b9 = b & for s be Element of R holds (b9 * s) = (s * b9) by A15;

           [a, b] in [:ccs, ccs:] by A14, A15, ZFMISC_1:def 2;

          then

           A19: (a * b) = (mcs . x) by A16, FUNCT_1: 49;

          now

            let s be Element of cR;

            

            thus ((a * b) * s) = (a * (b * s)) by GROUP_1:def 3

            .= (a * (s * b)) by A18

            .= ((a * s) * b) by GROUP_1:def 3

            .= ((s * a) * b) by A17

            .= (s * (a * b)) by GROUP_1:def 3;

          end;

          hence thesis by A13, A19;

        end;

        then

        reconsider mcs as BinOp of ccs by FUNCT_2: 6;

        reconsider Zs as Element of ccs by A1;

        for s be Element of cR holds (( 1_ R) * s) = (s * ( 1_ R));

        then Us in ccs;

        then

        reconsider Us as Element of ccs;

        reconsider cs = doubleLoopStr (# ccs, acs, mcs, Us, Zs #) as non empty doubleLoopStr;

        set ccs1 = the carrier of cs;

         A20:

        now

          let x,s be Element of cR;

          assume x in ccs;

          then ex x9 be Element of cR st x9 = x & for s be Element of R holds (x9 * s) = (s * x9);

          hence (x * s) = (s * x);

        end;

         A21:

        now

          let a,b be Element of cR, c,d be Element of ccs1 such that

           A22: a = c and

           A23: b = d;

           [c, d] in [:ccs, ccs:] by ZFMISC_1:def 2;

          hence (a * b) = (c * d) by A22, A23, FUNCT_1: 49;

        end;

        

         A24: for a,b be Element of cR, c,d be Element of ccs1 st a = c & b = d holds (a + b) = (c + d)

        proof

          let a,b be Element of cR, c,d be Element of ccs1 such that

           A25: a = c and

           A26: b = d;

           [c, d] in [:ccs, ccs:] by ZFMISC_1:def 2;

          hence thesis by A25, A26, FUNCT_1: 49;

        end;

        

         A27: cs is Abelian

        proof

          let x,y be Element of ccs1;

          reconsider x9 = x, y9 = y as Element of cR by A2;

          

          thus (x + y) = (y9 + x9) by A24

          .= (y + x) by A24;

        end;

        

         A28: cs is add-associative

        proof

          let x,y,z be Element of ccs1;

          reconsider x9 = x, y9 = y, z9 = z as Element of cR by A2;

          

           A29: (x9 + y9) = (x + y) by A24;

          

           A30: (y9 + z9) = (y + z) by A24;

          

          thus ((x + y) + z) = ((x9 + y9) + z9) by A24, A29

          .= (x9 + (y9 + z9)) by RLVECT_1:def 3

          .= (x + (y + z)) by A24, A30;

        end;

        

         A31: cs is right_zeroed

        proof

          let x be Element of ccs1;

          reconsider x9 = x as Element of cR by A2;

          

          thus (x + ( 0. cs)) = (x9 + ( 0. R)) by A24

          .= x by RLVECT_1:def 4;

        end;

        

         A32: cs is right_complementable

        proof

          let x be Element of ccs1;

          reconsider x9 = x as Element of cR by A2;

          consider y9 be Element of cR such that

           A33: (x9 + y9) = ( 0. R) by ALGSTR_0:def 11;

          now

            let s be Element of cR;

            

             A34: (s * x9) = (x9 * s) by A20;

            (( 0. R) * s) = (s * ( 0. R));

            then ((x9 * s) + (y9 * s)) = (s * (x9 + y9)) by A33, 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 A34, 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;

          end;

          then y9 in ccs1;

          then

          reconsider y = y9 as Element of ccs1;

          (x9 + y9) = (x + y) by A24;

          hence ex y be Element of ccs1 st (x + y) = ( 0. cs) by A33;

        end;

        

         A35: cs is associative

        proof

          let x,y,z be Element of ccs1;

          reconsider x9 = x, y9 = y, z9 = z as Element of cR by A2;

          

           A36: (x9 * y9) = (x * y) by A21;

          

           A37: (y9 * z9) = (y * z) by A21;

          

          thus ((x * y) * z) = ((x9 * y9) * z9) by A21, A36

          .= (x9 * (y9 * z9)) by GROUP_1:def 3

          .= (x * (y * z)) by A21, A37;

        end;

        

         A38: cs is commutative

        proof

          let x,y be Element of ccs1;

          reconsider x9 = x, y9 = y as Element of cR by A2;

          

          thus (x * y) = (x9 * y9) by A21

          .= (y9 * x9) by A20

          .= (y * x) by A21;

        end;

         A39:

        now

          let x,e be Element of cs;

          assume

           A40: e = ( 1_ R);

          

           A41: [x, e] in [:ccs, ccs:] by ZFMISC_1: 87;

          reconsider y = x as Element of R by A2;

          

          thus (x * e) = (y * ( 1_ R)) by A40, A41, FUNCT_1: 49

          .= x;

          hence (e * x) = x by A38;

        end;

        

         A42: cs is well-unital by A39;

        

         A43: cs is distributive

        proof

          let x,y,z be Element of ccs1;

          reconsider x9 = x, y9 = y, z9 = z as Element of cR by A2;

          

           A44: (y + z) = (y9 + z9) by A24;

          

           A45: (x9 * y9) = (x * y) by A21;

          

           A46: (x9 * z9) = (x * z) by A21;

          

           A47: (y9 * x9) = (y * x) by A21;

          

           A48: (z9 * x9) = (z * x) by A21;

          

          thus (x * (y + z)) = (x9 * (y9 + z9)) by A21, A44

          .= ((x9 * y9) + (x9 * z9)) by VECTSP_1:def 7

          .= ((x * y) + (x * z)) by A24, A45, A46;

          

          thus ((y + z) * x) = ((y9 + z9) * x9) by A21, A44

          .= ((y9 * x9) + (z9 * x9)) by VECTSP_1:def 7

          .= ((y * x) + (z * x)) by A24, A47, A48;

        end;

        cs is almost_left_invertible

        proof

          let x be Element of ccs1 such that

           A49: x <> ( 0. cs);

          reconsider x9 = x as Element of cR by A2;

          consider y9 be Element of cR such that

           A50: (y9 * x9) = ( 1. R) by A49, VECTSP_1:def 9;

          

           A51: (x9 * y9) = ( 1. R) by A50, VECTSP_2: 7;

          now

            let s be Element of cR;

            (( 1_ R) * s) = s

            .= (s * ( 1_ R));

            then ((x9 * y9) * s) = ((s * x9) * y9) by A51, GROUP_1:def 3;

            then ((x9 * y9) * s) = ((x9 * s) * y9) by A20;

            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 A49, VECTSP_2: 9;

            then ((( 1_ R) * y9) * s) = ((( 1_ R) * s) * y9) by A49, VECTSP_2: 9;

            then (y9 * s) = ((( 1_ R) * s) * y9);

            hence (y9 * s) = (s * y9);

          end;

          then y9 in ccs1;

          then

          reconsider y = y9 as Element of ccs1;

          take y;

          thus thesis by A21, A50;

        end;

        then

        reconsider cs as strict Field by A27, A28, A31, A32, A35, A38, A42, A43, STRUCT_0:def 8;

        take cs;

        thus thesis;

      end;

      uniqueness ;

    end

    theorem :: WEDDWITT:16

    

     Th16: for R be Skew-Field holds the carrier of ( center R) c= the carrier of R

    proof

      let R be Skew-Field;

      for x be object st x in the carrier of ( center R) holds x in the carrier of R

      proof

        let y be object;

        assume y in the carrier of ( center R);

        then y in { x where x be Element of R : for s be Element of R holds (x * s) = (s * x) } by Def4;

        then ex x be Element of R st (x = y) & (for s be Element of R holds (x * s) = (s * x));

        hence thesis;

      end;

      hence thesis;

    end;

    registration

      let R be finite Skew-Field;

      cluster ( center R) -> finite;

      correctness

      proof

        the carrier of ( center R) c= the carrier of R by Th16;

        hence thesis;

      end;

    end

    theorem :: WEDDWITT:17

    

     Th17: for R be Skew-Field, y be Element of R holds y in ( center R) iff for s be Element of R holds (y * s) = (s * y)

    proof

      let R be Skew-Field, y be Element of R;

      hereby

        assume y in ( center R);

        then y in the carrier of ( center R);

        then y in { x where x be Element of R : for s be Element of R holds (x * s) = (s * x) } by Def4;

        then ex x be Element of R st (x = y) & (for s be Element of R holds (x * s) = (s * x));

        hence for s be Element of R holds (y * s) = (s * y);

      end;

      now

        assume for s be Element of R holds (y * s) = (s * y);

        then y in { x where x be Element of R : for s be Element of R holds (x * s) = (s * x) };

        then y is Element of ( center R) by Def4;

        hence y in ( center R);

      end;

      hence thesis;

    end;

    theorem :: WEDDWITT:18

    

     Th18: for R be Skew-Field holds ( 0. R) in ( center R)

    proof

      let R be Skew-Field;

      for s be Element of R holds (( 0. R) * s) = (s * ( 0. R));

      hence thesis by Th17;

    end;

    theorem :: WEDDWITT:19

    

     Th19: for R be Skew-Field holds ( 1_ R) in ( center R)

    proof

      let R be Skew-Field;

      for s be Element of R holds (( 1_ R) * s) = (s * ( 1_ R));

      hence thesis by Th17;

    end;

    theorem :: WEDDWITT:20

    

     Th20: for R be finite Skew-Field holds 1 < ( card the carrier of ( center R))

    proof

      let R be finite Skew-Field;

      

       A1: ( card {( 0. R), ( 1. R)}) = 2 by CARD_2: 57;

      ( 0. R) in ( center R) by Th18;

      then

       A2: ( 0. R) in the carrier of ( center R);

      for s be Element of R holds (( 1. R) * s) = (s * ( 1. R));

      then ( 1. R) in ( center R) by Th17;

      then ( 1. R) in the carrier of ( center R);

      then {( 0. R), ( 1. R)} c= the carrier of ( center R) by A2, ZFMISC_1: 32;

      then 2 <= ( card the carrier of ( center R)) by A1, NAT_1: 43;

      hence thesis by XXREAL_0: 2;

    end;

    theorem :: WEDDWITT:21

    

     Th21: for R be finite Skew-Field holds ( card the carrier of ( center R)) = ( card the carrier of R) iff R is commutative

    proof

      let R be finite Skew-Field;

      set X = the carrier of R;

      set Y = the carrier of ( center R);

      hereby

        assume

         A1: ( card X) = ( card Y);

        

         A2: Y c= X by Th16;

        ( card (X \ Y)) = (( card X) - ( card X)) by A1, Th16, CARD_2: 44;

        then (X \ Y) = {} ;

        then X c= Y by XBOOLE_1: 37;

        then

         A3: X = Y by A2, XBOOLE_0:def 10;

        for x be Element of X holds for s be Element of X holds (x * s) = (s * x) by A3, STRUCT_0:def 5, Th17;

        hence R is commutative;

      end;

      now

        assume

         A4: R is commutative;

        for x be object st x in X holds x in Y

        proof

          let x be object such that

           A5: x in X;

          for x be Element of X holds x is Element of Y

          proof

            let x be Element of X;

            for y be Element of X holds (x * y) = (y * x) by A4;

            then x in ( center R) by Th17;

            hence thesis;

          end;

          then x is Element of Y by A5;

          hence thesis;

        end;

        then

         A6: X c= Y;

        Y c= X by Th16;

        hence ( card Y) = ( card X) by A6, XBOOLE_0:def 10;

      end;

      hence thesis;

    end;

    theorem :: WEDDWITT:22

    

     Th22: for R be Skew-Field holds the carrier of ( center R) = (the carrier of ( center ( MultGroup R)) \/ {( 0. R)})

    proof

      let R be Skew-Field;

      

       A1: the carrier of ( center ( MultGroup R)) c= the carrier of ( MultGroup R) by GROUP_2:def 5;

      

       A2: the carrier of ( MultGroup R) = ( NonZero R) by UNIROOTS:def 1;

      

       A3: (the carrier of ( MultGroup R) \/ {( 0. R)}) = the carrier of R by UNIROOTS: 15;

      

       A4: the carrier of ( center R) c= the carrier of R by Th16;

      

       A5: (the carrier of ( center ( MultGroup R)) \/ {( 0. R)}) c= the carrier of ( center R)

      proof

        let x be object;

        assume

         A6: x in (the carrier of ( center ( MultGroup R)) \/ {( 0. R)});

        per cases by A6, XBOOLE_0:def 3;

          suppose

           A7: x in the carrier of ( center ( MultGroup R));

          then

          reconsider a = x as Element of ( MultGroup R) by A1;

          

           A8: a in ( center ( MultGroup R)) by A7;

          reconsider a1 = a as Element of R by UNIROOTS: 19;

          now

            let b be Element of R;

            thus (a1 * b) = (b * a1)

            proof

              per cases by A3, XBOOLE_0:def 3;

                suppose b in the carrier of ( MultGroup R);

                then

                reconsider b1 = b as Element of ( MultGroup R);

                

                thus (a1 * b) = (a * b1) by UNIROOTS: 16

                .= (b1 * a) by A8, GROUP_5: 77

                .= (b * a1) by UNIROOTS: 16;

              end;

                suppose b in {( 0. R)};

                then

                 A9: b = ( 0. R) by TARSKI:def 1;

                

                hence (a1 * b) = ( 0. R)

                .= (b * a1) by A9;

              end;

            end;

          end;

          then a1 in ( center R) by Th17;

          hence thesis;

        end;

          suppose x in {( 0. R)};

          then x = ( 0. R) by TARSKI:def 1;

          then x in ( center R) by Th18;

          hence thesis;

        end;

      end;

      the carrier of ( center R) c= (the carrier of ( center ( MultGroup R)) \/ {( 0. R)})

      proof

        let x be object;

        assume

         A10: x in the carrier of ( center R);

        then

        reconsider a = x as Element of ( center R);

        reconsider a1 = a as Element of R by A4;

        per cases ;

          suppose a1 = ( 0. R);

          then a1 in {( 0. R)} by TARSKI:def 1;

          hence thesis by XBOOLE_0:def 3;

        end;

          suppose a1 <> ( 0. R);

          then not a1 in {( 0. R)} by TARSKI:def 1;

          then

          reconsider a2 = a1 as Element of ( MultGroup R) by A2, XBOOLE_0:def 5;

          now

            let b be Element of ( MultGroup R);

            b in the carrier of ( MultGroup R);

            then

            reconsider b1 = b as Element of R by A2;

            

             A11: x in ( center R) by A10;

            

            thus (a2 * b) = (a1 * b1) by UNIROOTS: 16

            .= (b1 * a1) by A11, Th17

            .= (b * a2) by UNIROOTS: 16;

          end;

          then a1 in ( center ( MultGroup R)) by GROUP_5: 77;

          then a1 in the carrier of ( center ( MultGroup R));

          hence thesis by XBOOLE_0:def 3;

        end;

      end;

      hence thesis by A5, XBOOLE_0:def 10;

    end;

    definition

      let R be Skew-Field, s be Element of R;

      :: WEDDWITT:def5

      func centralizer s -> strict Skew-Field means

      : Def5: the carrier of it = { x where x be Element of R : (x * s) = (s * x) } & the addF of it = (the addF of R || the carrier of it ) & the multF of it = (the multF of R || the carrier of it ) & ( 0. it ) = ( 0. R) & ( 1. it ) = ( 1. R);

      existence

      proof

        set cR = the carrier of R;

        set ccs = { x where x be Element of R : (x * s) = (s * x) };

        (( 0. R) * s) = (s * ( 0. R));

        then ( 0. R) in ccs;

        then

        reconsider ccs as non empty set;

        

         A2: ccs c= cR

        proof

          let x be object;

          assume x in ccs;

          then ex x9 be Element of cR st x9 = x & (x9 * s) = (s * x9);

          hence thesis;

        end;

        set acs = (the addF of R || ccs);

        set mcs = (the multF of R || ccs);

        set Zs = ( 0. R);

        set Us = ( 1. R);

        

         A3: [:ccs, ccs:] c= [:cR, cR:]

        proof

          let x be object;

          assume x in [:ccs, ccs:];

          then ex a,b be object st (a in ccs) & (b in ccs) & (x = [a, b]) by ZFMISC_1:def 2;

          hence thesis by A2, ZFMISC_1:def 2;

        end;

        then

        reconsider acs as Function of [:ccs, ccs:], cR by FUNCT_2: 32;

        ( rng acs) c= ccs

        proof

          let y be object;

          assume y in ( rng acs);

          then

          consider x be object such that

           A4: x in ( dom acs) and

           A5: y = (acs . x) by FUNCT_1:def 3;

          consider a,b be object such that

           A6: a in ccs and

           A7: b in ccs and

           A8: x = [a, b] by A4, ZFMISC_1:def 2;

          reconsider a, b as Element of cR by A2, A6, A7;

          

           A9: ex a9 be Element of cR st a9 = a & (a9 * s) = (s * a9) by A6;

          

           A10: ex b9 be Element of cR st b9 = b & (b9 * s) = (s * b9) by A7;

           [a, b] in [:ccs, ccs:] by A6, A7, ZFMISC_1:def 2;

          then

           A11: (a + b) = (acs . x) by A8, FUNCT_1: 49;

          ((a + b) * s) = ((s * a) + (s * b)) by A9, A10, VECTSP_1:def 3

          .= (s * (a + b)) by VECTSP_1:def 2;

          hence thesis by A5, A11;

        end;

        then

        reconsider acs as BinOp of ccs by FUNCT_2: 6;

        reconsider mcs as Function of [:ccs, ccs:], cR by A3, FUNCT_2: 32;

        ( rng mcs) c= ccs

        proof

          let y be object;

          assume y in ( rng mcs);

          then

          consider x be object such that

           A12: x in ( dom mcs) and

           A13: y = (mcs . x) by FUNCT_1:def 3;

          consider a,b be object such that

           A14: a in ccs and

           A15: b in ccs and

           A16: x = [a, b] by A12, ZFMISC_1:def 2;

          reconsider a, b as Element of cR by A2, A14, A15;

          

           A17: ex a9 be Element of cR st a9 = a & (a9 * s) = (s * a9) by A14;

          

           A18: ex b9 be Element of cR st b9 = b & (b9 * s) = (s * b9) by A15;

           [a, b] in [:ccs, ccs:] by A14, A15, ZFMISC_1:def 2;

          then

           A19: (a * b) = (mcs . x) by A16, FUNCT_1: 49;

          ((a * b) * s) = (a * (s * b)) by A18, GROUP_1:def 3

          .= ((a * s) * b) by GROUP_1:def 3

          .= (s * (a * b)) by A17, GROUP_1:def 3;

          hence thesis by A13, A19;

        end;

        then

        reconsider mcs as BinOp of ccs by FUNCT_2: 6;

        (( 0. R) * s) = (s * ( 0. R));

        then Zs in ccs;

        then

        reconsider Zs as Element of ccs;

        (( 1. R) * s) = s

        .= (s * ( 1. R));

        then Us in ccs;

        then

        reconsider Us as Element of ccs;

        reconsider cs = doubleLoopStr (# ccs, acs, mcs, Us, Zs #) as non empty doubleLoopStr;

         A20:

        now

          let x,e be Element of cs;

          assume

           A21: e = ( 1. R);

          

           A22: [x, e] in [:ccs, ccs:] by ZFMISC_1: 87;

          

           A23: [e, x] in [:ccs, ccs:] by ZFMISC_1: 87;

          reconsider y = x as Element of R by A2;

          

          thus (x * e) = (y * ( 1. R)) by A21, A22, FUNCT_1: 49

          .= x;

          

          thus (e * x) = (( 1. R) * y) by A21, A23, FUNCT_1: 49

          .= x;

        end;

        

         A24: cs is well-unital by A20;

        set ccs1 = the carrier of cs;

         A25:

        now

          let x be Element of cR;

          assume x in ccs;

          then ex x9 be Element of cR st x9 = x & (x9 * s) = (s * x9);

          hence (x * s) = (s * x);

        end;

         A26:

        now

          let a,b be Element of cR, c,d be Element of ccs1 such that

           A27: a = c and

           A28: b = d;

           [c, d] in [:ccs, ccs:] by ZFMISC_1:def 2;

          hence (a * b) = (c * d) by A27, A28, FUNCT_1: 49;

        end;

        

         A29: for a,b be Element of cR, c,d be Element of ccs1 st a = c & b = d holds (a + b) = (c + d)

        proof

          let a,b be Element of cR, c,d be Element of ccs1 such that

           A30: a = c and

           A31: b = d;

           [c, d] in [:ccs, ccs:] by ZFMISC_1:def 2;

          hence thesis by A30, A31, FUNCT_1: 49;

        end;

        

         A32: cs is Abelian

        proof

          let x,y be Element of ccs1;

          reconsider x9 = x, y9 = y as Element of cR by A2;

          

          thus (x + y) = (y9 + x9) by A29

          .= (y + x) by A29;

        end;

        

         A33: cs is add-associative

        proof

          let x,y,z be Element of ccs1;

          reconsider x9 = x, y9 = y, z9 = z as Element of cR by A2;

          

           A34: (x9 + y9) = (x + y) by A29;

          

           A35: (y9 + z9) = (y + z) by A29;

          

          thus ((x + y) + z) = ((x9 + y9) + z9) by A29, A34

          .= (x9 + (y9 + z9)) by RLVECT_1:def 3

          .= (x + (y + z)) by A29, A35;

        end;

        

         A36: cs is right_zeroed

        proof

          let x be Element of ccs1;

          reconsider x9 = x as Element of cR by A2;

          

          thus (x + ( 0. cs)) = (x9 + ( 0. R)) by A29

          .= x by RLVECT_1:def 4;

        end;

        

         A37: cs is right_complementable

        proof

          let x be Element of ccs1;

          reconsider x9 = x as Element of cR by A2;

          consider y9 be Element of cR such that

           A38: (x9 + y9) = ( 0. R) by ALGSTR_0:def 11;

          

           A39: (s * x9) = (x9 * s) by A25;

          (( 0. R) * s) = (s * ( 0. R));

          then ((x9 * s) + (y9 * s)) = (s * (x9 + y9)) by A38, VECTSP_1:def 3;

          then ((x9 * s) + (y9 * s)) = ((s * x9) + (s * y9)) by VECTSP_1:def 2;

          then ((( - (x9 * s)) + (x9 * s)) + (y9 * s)) = (( - (s * x9)) + ((s * x9) + (s * y9))) by A39, RLVECT_1:def 3;

          then (( 0. R) + (y9 * s)) = (( - (s * x9)) + ((s * x9) + (s * y9))) by RLVECT_1: 5;

          then (y9 * s) = (( - (s * x9)) + ((s * x9) + (s * y9))) by RLVECT_1: 4;

          then (y9 * s) = ((( - (s * x9)) + (s * x9)) + (s * y9)) by RLVECT_1:def 3;

          then (y9 * s) = (( 0. R) + (s * y9)) by RLVECT_1: 5;

          then (y9 * s) = (s * y9) by RLVECT_1: 4;

          then y9 in ccs1;

          then

          reconsider y = y9 as Element of ccs1;

          (x9 + y9) = (x + y) by A29;

          hence ex y be Element of ccs1 st (x + y) = ( 0. cs) by A38;

        end;

        

         A40: cs is associative

        proof

          let x,y,z be Element of ccs1;

          reconsider x9 = x, y9 = y, z9 = z as Element of cR by A2;

          

           A41: (x9 * y9) = (x * y) by A26;

          

           A42: (y9 * z9) = (y * z) by A26;

          

          thus ((x * y) * z) = ((x9 * y9) * z9) by A26, A41

          .= (x9 * (y9 * z9)) by GROUP_1:def 3

          .= (x * (y * z)) by A26, A42;

        end;

        

         A43: cs is distributive

        proof

          let x,y,z be Element of ccs1;

          reconsider x9 = x, y9 = y, z9 = z as Element of cR by A2;

          

           A44: (y + z) = (y9 + z9) by A29;

          

           A45: (x9 * y9) = (x * y) by A26;

          

           A46: (x9 * z9) = (x * z) by A26;

          

           A47: (y9 * x9) = (y * x) by A26;

          

           A48: (z9 * x9) = (z * x) by A26;

          

          thus (x * (y + z)) = (x9 * (y9 + z9)) by A26, A44

          .= ((x9 * y9) + (x9 * z9)) by VECTSP_1:def 7

          .= ((x * y) + (x * z)) by A29, A45, A46;

          

          thus ((y + z) * x) = ((y9 + z9) * x9) by A26, A44

          .= ((y9 * x9) + (z9 * x9)) by VECTSP_1:def 7

          .= ((y * x) + (z * x)) by A29, A47, A48;

        end;

        

         A49: cs is almost_left_invertible

        proof

          let x be Element of ccs1 such that

           A50: x <> ( 0. cs);

          reconsider x9 = x as Element of cR by A2;

          consider y9 be Element of cR such that

           A51: (y9 * x9) = ( 1. R) by A50, VECTSP_1:def 9;

          

           A52: (x9 * y9) = ( 1. R) by A51, VECTSP_2: 7;

          (( 1. R) * s) = s

          .= (s * ( 1. R));

          then ((x9 * y9) * s) = ((s * x9) * y9) by A52, GROUP_1:def 3;

          then ((x9 * y9) * s) = ((x9 * s) * y9) by A25;

          then (((x9 " ) * (x9 * y9)) * s) = ((x9 " ) * ((x9 * s) * y9)) by GROUP_1:def 3;

          then (((x9 " ) * (x9 * y9)) * s) = (((x9 " ) * (x9 * s)) * y9) by GROUP_1:def 3;

          then ((((x9 " ) * x9) * y9) * s) = (((x9 " ) * (x9 * s)) * y9) by GROUP_1:def 3;

          then ((((x9 " ) * x9) * y9) * s) = ((((x9 " ) * x9) * s) * y9) by GROUP_1:def 3;

          then ((( 1_ R) * y9) * s) = ((((x9 " ) * x9) * s) * y9) by A50, VECTSP_2: 9;

          then ((( 1_ R) * y9) * s) = ((( 1_ R) * s) * y9) by A50, VECTSP_2: 9;

          then (y9 * s) = ((( 1_ R) * s) * y9);

          then (y9 * s) = (s * y9);

          then y9 in ccs1;

          then

          reconsider y = y9 as Element of ccs1;

          take y;

          thus thesis by A26, A51;

        end;

        cs is non degenerated;

        hence thesis by A24, A32, A33, A36, A37, A40, A43, A49;

      end;

      uniqueness ;

    end

    theorem :: WEDDWITT:23

    

     Th23: for R be Skew-Field, s be Element of R holds the carrier of ( centralizer s) c= the carrier of R

    proof

      let R be Skew-Field, s be Element of R;

      set cs = ( centralizer s);

      set ccs = the carrier of cs;

      

       A1: ccs = { x where x be Element of R : (x * s) = (s * x) } by Def5;

      let x be object;

      assume x in the carrier of ( centralizer s);

      then ex a be Element of R st a = x & (a * s) = (s * a) by A1;

      hence thesis;

    end;

    theorem :: WEDDWITT:24

    

     Th24: for R be Skew-Field, s,a be Element of R holds a in the carrier of ( centralizer s) iff (a * s) = (s * a)

    proof

      let R be Skew-Field, s,a be Element of R;

      set cs = ( centralizer s);

      set ccs = the carrier of cs;

      

       A1: ccs = { x where x be Element of R : (x * s) = (s * x) } by Def5;

      hereby

        assume a in the carrier of ( centralizer s);

        then ex x be Element of R st a = x & (x * s) = (s * x) by A1;

        hence (a * s) = (s * a);

      end;

      assume (a * s) = (s * a);

      hence thesis by A1;

    end;

    theorem :: WEDDWITT:25

    for R be Skew-Field, s be Element of R holds the carrier of ( center R) c= the carrier of ( centralizer s)

    proof

      let R be Skew-Field, s be Element of R;

      let x be object;

      assume

       A1: x in the carrier of ( center R);

      the carrier of ( center R) c= the carrier of R by Th16;

      then

      reconsider a = x as Element of R by A1;

      a in ( center R) by A1;

      then (a * s) = (s * a) by Th17;

      hence thesis by Th24;

    end;

    theorem :: WEDDWITT:26

    

     Th26: for R be Skew-Field, s,a,b be Element of R st a in the carrier of ( center R) & b in the carrier of ( centralizer s) holds (a * b) in the carrier of ( centralizer s)

    proof

      let R be Skew-Field, s,a,b be Element of R such that

       A1: a in the carrier of ( center R) and

       A2: b in the carrier of ( centralizer s);

      set cs = ( centralizer s);

      set ccs = the carrier of cs;

      

       A3: ccs = { x where x be Element of R : (x * s) = (s * x) } by Def5;

      

       A4: a in ( center R) by A1;

      ((a * b) * s) = (a * (b * s)) by GROUP_1:def 3

      .= ((b * s) * a) by A4, Th17

      .= ((s * b) * a) by A2, Th24

      .= (s * (b * a)) by GROUP_1:def 3

      .= (s * (a * b)) by A4, Th17;

      hence thesis by A3;

    end;

    theorem :: WEDDWITT:27

    

     Th27: for R be Skew-Field, s be Element of R holds ( 0. R) is Element of ( centralizer s) & ( 1_ R) is Element of ( centralizer s)

    proof

      let R be Skew-Field, s be Element of R;

      

       A1: ( 0. R) = ( 0. ( centralizer s)) by Def5;

      ( 1. ( centralizer s)) = ( 1_ R) by Def5;

      hence thesis by A1;

    end;

    registration

      let R be finite Skew-Field;

      let s be Element of R;

      cluster ( centralizer s) -> finite;

      correctness by Th23, FINSET_1: 1;

    end

    theorem :: WEDDWITT:28

    

     Th28: for R be finite Skew-Field, s be Element of R holds 1 < ( card the carrier of ( centralizer s))

    proof

      let R be finite Skew-Field, s be Element of R;

      

       A1: ( card {( 0. R), ( 1. R)}) = 2 by CARD_2: 57;

      

       A2: ( 0. R) is Element of ( centralizer s) by Th27;

      ( 1_ R) is Element of ( centralizer s) by Th27;

      then {( 0. R), ( 1_ R)} c= the carrier of ( centralizer s) by A2, ZFMISC_1: 32;

      then 2 <= ( card the carrier of ( centralizer s)) by A1, NAT_1: 43;

      hence thesis by XXREAL_0: 2;

    end;

    theorem :: WEDDWITT:29

    

     Th29: for R be Skew-Field, s be Element of R, t be Element of ( MultGroup R) st t = s holds the carrier of ( centralizer s) = (the carrier of ( Centralizer t) \/ {( 0. R)})

    proof

      let R be Skew-Field, s be Element of R, t be Element of ( MultGroup R) such that

       A1: t = s;

      set ct = ( Centralizer t), cs = ( centralizer s);

      set cct = the carrier of ct, ccs = the carrier of cs;

      

       A2: the carrier of ( MultGroup R) = ( NonZero R) by UNIROOTS:def 1;

      

       A3: cct = { b where b be Element of ( MultGroup R) : (t * b) = (b * t) } by Def1;

      

       A4: ccs = { x where x be Element of R : (x * s) = (s * x) } by Def5;

      now

        let x be object;

        hereby

          assume x in ccs;

          then

          consider c be Element of R such that

           A5: c = x and

           A6: (c * s) = (s * c) by A4;

          per cases ;

            suppose c = ( 0. R);

            then c in {( 0. R)} by TARSKI:def 1;

            hence x in (cct \/ {( 0. R)}) by A5, XBOOLE_0:def 3;

          end;

            suppose c <> ( 0. R);

            then not c in {( 0. R)} by TARSKI:def 1;

            then

            reconsider c1 = c as Element of ( MultGroup R) by A2, XBOOLE_0:def 5;

            (t * c1) = (s * c) by A1, UNIROOTS: 16

            .= (c1 * t) by A1, A6, UNIROOTS: 16;

            then c in cct by A3;

            hence x in (cct \/ {( 0. R)}) by A5, XBOOLE_0:def 3;

          end;

        end;

        assume

         A7: x in (cct \/ {( 0. R)});

        per cases by A7, XBOOLE_0:def 3;

          suppose x in cct;

          then

          consider b be Element of ( MultGroup R) such that

           A8: x = b and

           A9: (t * b) = (b * t) by A3;

          reconsider b1 = b as Element of R by UNIROOTS: 19;

          (b1 * s) = (t * b) by A1, A9, UNIROOTS: 16

          .= (s * b1) by A1, UNIROOTS: 16;

          hence x in ccs by A4, A8;

        end;

          suppose x in {( 0. R)};

          then

           A10: x = ( 0. R) by TARSKI:def 1;

          (( 0. R) * s) = (s * ( 0. R));

          hence x in ccs by A4, A10;

        end;

      end;

      hence thesis by TARSKI: 2;

    end;

    theorem :: WEDDWITT:30

    

     Th30: for R be finite Skew-Field, s be Element of R, t be Element of ( MultGroup R) st t = s holds ( card ( Centralizer t)) = (( card the carrier of ( centralizer s)) - 1)

    proof

      let R be finite Skew-Field, s be Element of R, t be Element of ( MultGroup R) such that

       A1: t = s;

      set ct = ( Centralizer t), cs = ( centralizer s);

      set cct = the carrier of ct, ccs = the carrier of cs;

      the carrier of ( MultGroup R) = ( NonZero R) by UNIROOTS:def 1;

      then not ( 0. R) in the carrier of ( MultGroup R) by ZFMISC_1: 56;

      then not ( 0. R) in ( MultGroup R);

      then not ( 0. R) in ct by Th7;

      then

       A2: not ( 0. R) in cct;

      (cct \/ {( 0. R)}) = ccs by A1, Th29;

      then ( card ccs) = (( card cct) + 1) by A2, CARD_2: 41;

      hence thesis;

    end;

    begin

    definition

      let R be Skew-Field;

      :: WEDDWITT:def6

      func VectSp_over_center R -> strict VectSp of ( center R) means

      : Def6: the addLoopStr of it = the addLoopStr of R & the lmult of it = (the multF of R | [:the carrier of ( center R), the carrier of R:]);

      existence

      proof

        set cR = ( center R);

        set ccR = the carrier of cR;

        set ccs = the carrier of R;

        set lm = (the multF of R | [:ccR, ccs:]);

        

         A1: ccR c= the carrier of R by Th16;

        

         A2: ( dom the multF of R) = [:the carrier of R, the carrier of R:] by FUNCT_2:def 1;

         [:ccR, ccs:] c= [:the carrier of R, the carrier of R:]

        proof

          let x be object;

          assume x in [:ccR, ccs:];

          then ex x1,x2 be object st (x1 in ccR) & (x2 in ccs) & (x = [x1, x2]) by ZFMISC_1:def 2;

          hence thesis by A1, ZFMISC_1:def 2;

        end;

        then

         A3: ( dom lm) = [:ccR, ccs:] by A2, RELAT_1: 62;

        now

          let x be object;

          assume

           A4: x in [:ccR, ccs:];

          then

          consider x1,x2 be object such that

           A5: x1 in ccR and

           A6: x2 in ccs and

           A7: x = [x1, x2] by ZFMISC_1:def 2;

          reconsider x1 as Element of R by A1, A5;

          reconsider x2 as Element of R by A6;

          (lm . x) = (x1 * x2) by A4, A7, FUNCT_1: 49;

          hence (lm . x) in ccs;

        end;

        then

        reconsider lm as Function of [:ccR, ccs:], ccs by A3, FUNCT_2: 3;

        set Vos = ModuleStr (# ccs, the addF of R, ( 0. R), lm #);

        set cV = the carrier of Vos;

        

         A8: Vos is vector-distributive scalar-distributive scalar-associative scalar-unital

        proof

          

           A9: the multF of cR = (the multF of R || ccR) by Def4;

          

           A10: the addF of cR = (the addF of R || ccR) by Def4;

          thus Vos is vector-distributive

          proof

            let x be Element of ccR, v,w be Element of cV;

            reconsider xx = x as Element of R by A1;

            reconsider vv = v, ww = w as Element of R;

            

             A11: [x, w] in [:ccR, ccs:] by ZFMISC_1:def 2;

            

             A12: [x, (v + w)] in [:ccR, ccs:] by ZFMISC_1:def 2;

            

             A13: [x, v] in [:ccR, ccs:] by ZFMISC_1:def 2;

            

            thus (x * (v + w)) = (xx * (vv + ww)) by A12, FUNCT_1: 49

            .= ((xx * vv) + (xx * ww)) by VECTSP_1:def 2

            .= (the addF of R . [(x * v), (the multF of R . [xx, ww])]) by A13, FUNCT_1: 49

            .= ((x * v) + (x * w)) by A11, FUNCT_1: 49;

          end;

          thus Vos is scalar-distributive

          proof

            let x,y be Element of ccR, v be Element of cV;

            reconsider xx = x, yy = y as Element of R by A1;

            reconsider vv = v as Element of R;

            

             A14: [y, v] in [:ccR, ccs:] by ZFMISC_1:def 2;

            

             A15: [x, v] in [:ccR, ccs:] by ZFMISC_1:def 2;

            

             A16: [(x + y), v] in [:ccR, ccs:] by ZFMISC_1:def 2;

            

             A17: [x, y] in [:ccR, ccR:] by ZFMISC_1:def 2;

            

            thus ((x + y) * v) = (the multF of R . [(the addF of cR . [x, y]), vv]) by A16, FUNCT_1: 49

            .= ((xx + yy) * vv) by A10, A17, FUNCT_1: 49

            .= ((xx * vv) + (yy * vv)) by VECTSP_1:def 3

            .= (the addF of R . [(x * v), (the multF of R . [yy, vv])]) by A15, FUNCT_1: 49

            .= ((x * v) + (y * v)) by A14, FUNCT_1: 49;

          end;

          thus Vos is scalar-associative

          proof

            let x,y be Element of ccR, v be Element of cV;

            reconsider xx = x, yy = y as Element of R by A1;

            reconsider vv = v as Element of R;

            

             A18: [x, (y * v)] in [:ccR, ccs:] by ZFMISC_1:def 2;

            

             A19: [y, v] in [:ccR, ccs:] by ZFMISC_1:def 2;

            

             A20: [(x * y), v] in [:ccR, ccs:] by ZFMISC_1:def 2;

            

             A21: [x, y] in [:ccR, ccR:] by ZFMISC_1:def 2;

            

            thus ((x * y) * v) = (the multF of R . [(the multF of cR . (x,y)), vv]) by A20, FUNCT_1: 49

            .= ((xx * yy) * vv) by A9, A21, FUNCT_1: 49

            .= (xx * (yy * vv)) by GROUP_1:def 3

            .= (the multF of R . [xx, (lm . (y,v))]) by A19, FUNCT_1: 49

            .= (x * (y * v)) by A18, FUNCT_1: 49;

          end;

          let v be Element of cV;

          reconsider vv = v as Element of R;

          ( 1_ R) in ( center R) by Th19;

          then ( 1_ R) in ccR;

          then

           A22: [( 1_ R), vv] in [:ccR, ccs:] by ZFMISC_1:def 2;

          

          thus (( 1. cR) * v) = (lm . (( 1. R),vv)) by Def4

          .= (( 1. R) * vv) by A22, FUNCT_1: 49

          .= v;

        end;

        

         A23: Vos is add-associative

        proof

          let u,v,w be Element of cV;

          reconsider uu = u, vv = v, ww = w as Element of ccs;

          

          thus ((u + v) + w) = ((uu + vv) + ww)

          .= (uu + (vv + ww)) by RLVECT_1:def 3

          .= (u + (v + w));

        end;

        

         A24: Vos is right_zeroed

        proof

          let v be Element of cV;

          reconsider vv = v as Element of ccs;

          

          thus (v + ( 0. Vos)) = (vv + ( 0. R))

          .= v by RLVECT_1:def 4;

        end;

        

         A25: Vos is right_complementable

        proof

          let v be Element of cV;

          reconsider vv = v as Element of ccs;

          consider ww be Element of ccs such that

           A26: (vv + ww) = ( 0. R) by ALGSTR_0:def 11;

          reconsider w = ww as Element of cV;

          (v + w) = ( 0. Vos) by A26;

          hence ex w be Element of cV st (v + w) = ( 0. Vos);

        end;

        Vos is Abelian

        proof

          let v,w be Element of cV;

          reconsider vv = v, ww = w as Element of ccs;

          

          thus (v + w) = (ww + vv) by RLVECT_1: 2

          .= (w + v);

        end;

        hence thesis by A8, A23, A24, A25;

      end;

      uniqueness ;

    end

    theorem :: WEDDWITT:31

    

     Th31: for R be finite Skew-Field holds ( card the carrier of R) = (( card the carrier of ( center R)) |^ ( dim ( VectSp_over_center R)))

    proof

      let R be finite Skew-Field;

      set vR = ( VectSp_over_center R);

      

       A1: the addLoopStr of vR = the addLoopStr of R by Def6;

      set B = the Basis of vR;

      B is finite by A1;

      then vR is finite-dimensional by MATRLIN:def 1;

      hence thesis by A1, Th15;

    end;

    theorem :: WEDDWITT:32

    

     Th32: for R be finite Skew-Field holds 0 < ( dim ( VectSp_over_center R))

    proof

      let R be finite Skew-Field;

      set q = ( card the carrier of ( center R));

      set n = ( dim ( VectSp_over_center R));

      set Rs = ( MultGroup R);

      ( card R) = (q |^ n) by Th31;

      then

       A1: ( card Rs) = ((q |^ n) - 1) by UNIROOTS: 18;

      now

        assume

         A2: n = 0 ;

        (q |^ n) = (q #Z n) by PREPOWER: 36;

        then ( card Rs) = (1 - 1) by A1, A2, PREPOWER: 34;

        hence contradiction by GROUP_1: 45;

      end;

      hence thesis;

    end;

    definition

      let R be Skew-Field, s be Element of R;

      :: WEDDWITT:def7

      func VectSp_over_center s -> strict VectSp of ( center R) means

      : Def7: the addLoopStr of it = the addLoopStr of ( centralizer s) & the lmult of it = (the multF of R | [:the carrier of ( center R), the carrier of ( centralizer s):]);

      existence

      proof

        set cR = ( center R);

        set ccR = the carrier of cR;

        set cs = ( centralizer s);

        set ccs = the carrier of cs;

        set lm = (the multF of R | [:ccR, ccs:]);

        

         A1: ccR c= the carrier of R by Th16;

        

         A2: ccs c= the carrier of R by Th23;

        

         A3: ( dom the multF of R) = [:the carrier of R, the carrier of R:] by FUNCT_2:def 1;

         [:ccR, ccs:] c= [:the carrier of R, the carrier of R:]

        proof

          let x be object;

          assume x in [:ccR, ccs:];

          then ex x1,x2 be object st (x1 in ccR) & (x2 in ccs) & (x = [x1, x2]) by ZFMISC_1:def 2;

          hence thesis by A1, A2, ZFMISC_1:def 2;

        end;

        then

         A4: ( dom lm) = [:ccR, ccs:] by A3, RELAT_1: 62;

        now

          let x be object;

          assume

           A5: x in [:ccR, ccs:];

          then

          consider x1,x2 be object such that

           A6: x1 in ccR and

           A7: x2 in ccs and

           A8: x = [x1, x2] by ZFMISC_1:def 2;

          reconsider x1 as Element of R by A1, A6;

          reconsider x2 as Element of R by A2, A7;

          (lm . x) = (x1 * x2) by A5, A8, FUNCT_1: 49;

          hence (lm . x) in ccs by A6, A7, Th26;

        end;

        then

        reconsider lm as Function of [:ccR, ccs:], ccs by A4, FUNCT_2: 3;

        set Vos = ModuleStr (# the carrier of ( centralizer s), the addF of ( centralizer s), ( 0. ( centralizer s)), lm #);

        set cV = the carrier of Vos;

        set aV = the addF of Vos;

        

         A9: Vos is vector-distributive scalar-distributive scalar-associative scalar-unital

        proof

          

           A10: the multF of cR = (the multF of R || ccR) by Def4;

          

           A11: the addF of cR = (the addF of R || ccR) by Def4;

          

           A12: the addF of cs = (the addF of R || ccs) by Def5;

          thus Vos is vector-distributive

          proof

            let x be Element of ccR, v,w be Element of cV;

            reconsider xx = x as Element of R by A1;

            reconsider vv = v, ww = w as Element of R by A2;

            

             A13: [x, w] in [:ccR, ccs:] by ZFMISC_1:def 2;

            

             A14: [x, (v + w)] in [:ccR, ccs:] by ZFMISC_1:def 2;

            

             A15: [v, w] in [:ccs, ccs:] by ZFMISC_1:def 2;

            

             A16: [x, v] in [:ccR, ccs:] by ZFMISC_1:def 2;

            

             A17: [(x * v), (x * w)] in [:ccs, ccs:] by ZFMISC_1:def 2;

            

            thus (x * (v + w)) = (the multF of R . [x, (aV . [v, w])]) by A14, FUNCT_1: 49

            .= (xx * (vv + ww)) by A12, A15, FUNCT_1: 49

            .= ((xx * vv) + (xx * ww)) by VECTSP_1:def 2

            .= (the addF of R . [(x * v), (the multF of R . [xx, ww])]) by A16, FUNCT_1: 49

            .= (the addF of R . [(x * v), (x * w)]) by A13, FUNCT_1: 49

            .= ((x * v) + (x * w)) by A12, A17, FUNCT_1: 49;

          end;

          thus Vos is scalar-distributive

          proof

            let x,y be Element of ccR, v be Element of cV;

            reconsider xx = x, yy = y as Element of R by A1;

            reconsider vv = v as Element of R by A2;

            

             A18: [y, v] in [:ccR, ccs:] by ZFMISC_1:def 2;

            

             A19: [x, v] in [:ccR, ccs:] by ZFMISC_1:def 2;

            

             A20: [(x + y), v] in [:ccR, ccs:] by ZFMISC_1:def 2;

            

             A21: [x, y] in [:ccR, ccR:] by ZFMISC_1:def 2;

            

             A22: [(x * v), (y * v)] in [:ccs, ccs:] by ZFMISC_1:def 2;

            

            thus ((x + y) * v) = (the multF of R . [(the addF of cR . [x, y]), vv]) by A20, FUNCT_1: 49

            .= ((xx + yy) * vv) by A11, A21, FUNCT_1: 49

            .= ((xx * vv) + (yy * vv)) by VECTSP_1:def 3

            .= (the addF of R . [(x * v), (the multF of R . [yy, vv])]) by A19, FUNCT_1: 49

            .= (the addF of R . [(x * v), (lm . (y,v))]) by A18, FUNCT_1: 49

            .= ((x * v) + (y * v)) by A12, A22, FUNCT_1: 49;

          end;

          thus Vos is scalar-associative

          proof

            let x,y be Element of ccR, v be Element of cV;

            reconsider xx = x, yy = y as Element of R by A1;

            reconsider vv = v as Element of R by A2;

            

             A23: [x, (y * v)] in [:ccR, ccs:] by ZFMISC_1:def 2;

            

             A24: [y, v] in [:ccR, ccs:] by ZFMISC_1:def 2;

            

             A25: [(x * y), v] in [:ccR, ccs:] by ZFMISC_1:def 2;

            

             A26: [x, y] in [:ccR, ccR:] by ZFMISC_1:def 2;

            

            thus ((x * y) * v) = (the multF of R . [(the multF of cR . (x,y)), vv]) by A25, FUNCT_1: 49

            .= ((xx * yy) * vv) by A10, A26, FUNCT_1: 49

            .= (xx * (yy * vv)) by GROUP_1:def 3

            .= (the multF of R . [xx, (lm . (y,v))]) by A24, FUNCT_1: 49

            .= (x * (y * v)) by A23, FUNCT_1: 49;

          end;

          let v be Element of cV;

          reconsider vv = v as Element of R by A2;

          ( 1_ R) in ( center R) by Th19;

          then ( 1_ R) in ccR;

          then

           A27: [( 1_ R), vv] in [:ccR, ccs:] by ZFMISC_1:def 2;

          

          thus (( 1. cR) * v) = (lm . (( 1. R),vv)) by Def4

          .= (( 1. R) * vv) by A27, FUNCT_1: 49

          .= v;

        end;

        

         A28: Vos is add-associative

        proof

          let u,v,w be Element of cV;

          reconsider uu = u, vv = v, ww = w as Element of ccs;

          

          thus ((u + v) + w) = ((uu + vv) + ww)

          .= (uu + (vv + ww)) by RLVECT_1:def 3

          .= (u + (v + w));

        end;

        

         A29: Vos is right_zeroed

        proof

          let v be Element of cV;

          reconsider vv = v as Element of ccs;

          

          thus (v + ( 0. Vos)) = (vv + ( 0. cs))

          .= v by RLVECT_1:def 4;

        end;

        

         A30: Vos is right_complementable

        proof

          let v be Element of cV;

          reconsider vv = v as Element of ccs;

          consider ww be Element of ccs such that

           A31: (vv + ww) = ( 0. cs) by ALGSTR_0:def 11;

          reconsider w = ww as Element of cV;

          (v + w) = ( 0. Vos) by A31;

          hence ex w be Element of cV st (v + w) = ( 0. Vos);

        end;

        Vos is Abelian

        proof

          let v,w be Element of cV;

          reconsider vv = v, ww = w as Element of ccs;

          

          thus (v + w) = (ww + vv) by RLVECT_1: 2

          .= (w + v);

        end;

        hence thesis by A9, A28, A29, A30;

      end;

      uniqueness ;

    end

    theorem :: WEDDWITT:33

    

     Th33: for R be finite Skew-Field, s be Element of R holds ( card the carrier of ( centralizer s)) = (( card the carrier of ( center R)) |^ ( dim ( VectSp_over_center s)))

    proof

      let R be finite Skew-Field, s be Element of R;

      set vR = ( VectSp_over_center s);

      

       A1: the addLoopStr of vR = the addLoopStr of ( centralizer s) by Def7;

      set B = the Basis of vR;

      B is finite by A1;

      then vR is finite-dimensional by MATRLIN:def 1;

      hence thesis by A1, Th15;

    end;

    theorem :: WEDDWITT:34

    

     Th34: for R be finite Skew-Field, s be Element of R holds 0 < ( dim ( VectSp_over_center s))

    proof

      let R be finite Skew-Field, s be Element of R;

      set q = ( card the carrier of ( center R));

      set ns = ( dim ( VectSp_over_center s));

      now

        assume

         A1: ns = 0 ;

        (q |^ ns) = (q #Z ns) by PREPOWER: 36;

        then (q |^ ns) = 1 by A1, PREPOWER: 34;

        then ( card the carrier of ( centralizer s)) = 1 by Th33;

        hence contradiction by Th28;

      end;

      hence thesis;

    end;

    theorem :: WEDDWITT:35

    

     Th35: for R be finite Skew-Field, r be Element of R st r is Element of ( MultGroup R) holds ((( card the carrier of ( center R)) |^ ( dim ( VectSp_over_center r))) - 1) divides ((( card the carrier of ( center R)) |^ ( dim ( VectSp_over_center R))) - 1)

    proof

      let R be finite Skew-Field, r be Element of R such that

       A1: r is Element of ( MultGroup R);

      set G = ( MultGroup R);

      set q = ( card the carrier of ( center R));

      set qr = ( card the carrier of ( centralizer r));

      set n = ( dim ( VectSp_over_center R));

      reconsider s = r as Element of ( MultGroup R) by A1;

      ( card R) = (q |^ n) by Th31;

      then ( card G) = ((q |^ n) - 1) by UNIROOTS: 18;

      then ((q |^ n) - 1) = (( card ( con_class s)) * ( card ( Centralizer s))) by Th13;

      then ( card ( Centralizer s)) divides ((q |^ n) - 1) by INT_1:def 3;

      then (qr - 1) divides ((q |^ n) - 1) by Th30;

      hence thesis by Th33;

    end;

    theorem :: WEDDWITT:36

    

     Th36: for R be finite Skew-Field, s be Element of R st s is Element of ( MultGroup R) holds ( dim ( VectSp_over_center s)) divides ( dim ( VectSp_over_center R))

    proof

      let R be finite Skew-Field, s be Element of R such that

       A1: s is Element of ( MultGroup R);

      set n = ( dim ( VectSp_over_center R));

      set ns = ( dim ( VectSp_over_center s));

      set q = ( card the carrier of ( center R));

      

       A2: n in NAT by ORDINAL1:def 12;

      

       A3: ns in NAT by ORDINAL1:def 12;

      

       A4: 0 < ns by Th34;

      

       A5: 1 < q by Th20;

       0 < (q |^ ns) by PREPOWER: 6;

      then ( 0 + 1) < ((q |^ ns) + 1) by XREAL_1: 8;

      then

       A6: 1 <= (q |^ ns) by NAT_1: 13;

       0 < (q |^ n) by PREPOWER: 6;

      then ( 0 + 1) < ((q |^ n) + 1) by XREAL_1: 8;

      then 1 <= (q |^ n) by NAT_1: 13;

      then

       A7: ((q |^ n) - 1) = ((q |^ n) -' 1) by XREAL_1: 233;

      ((q |^ ns) - 1) = ((q |^ ns) -' 1) by A6, XREAL_1: 233;

      hence thesis by A1, A2, A3, A4, A5, A7, Th3, Th35;

    end;

    theorem :: WEDDWITT:37

    

     Th37: for R be finite Skew-Field holds ( card the carrier of ( center ( MultGroup R))) = (( card the carrier of ( center R)) - 1)

    proof

      let R be finite Skew-Field;

      

       A1: the carrier of ( MultGroup R) = ( NonZero R) by UNIROOTS:def 1;

      the carrier of ( center ( MultGroup R)) c= the carrier of ( MultGroup R) by GROUP_2:def 5;

      then

       A2: not ( 0. R) in the carrier of ( center ( MultGroup R)) by A1, ZFMISC_1: 56;

      the carrier of ( center R) = (the carrier of ( center ( MultGroup R)) \/ {( 0. R)}) by Th22;

      then ( card the carrier of ( center R)) = (( card the carrier of ( center ( MultGroup R))) + 1) by A2, CARD_2: 41;

      hence thesis;

    end;

    begin

    ::$Notion-Name

    theorem :: WEDDWITT:38

    for R be finite Skew-Field holds R is commutative

    proof

      let R be finite Skew-Field such that

       A1: not R is commutative;

      set Z = ( center R);

      set cZ = the carrier of Z;

      set q = ( card cZ);

      set vR = ( VectSp_over_center R);

      set n = ( dim vR);

      set Rs = ( MultGroup R);

      set cR = the carrier of R;

      set cRs = the carrier of Rs;

      set cZs = the carrier of ( center Rs);

      

       A2: ( card R) = (q |^ n) by Th31;

      then

       A3: ( card Rs) = ((q |^ n) - 1) by UNIROOTS: 18;

      

       A4: 1 < q by Th20;

      

       A5: (1 + ( - 1)) < (q + ( - 1)) by Th20, XREAL_1: 8;

      then

      reconsider natq1 = (q - 1) as Element of NAT by INT_1: 3;

      ( 0 + 1) < (n + 1) by Th32, XREAL_1: 8;

      then

       A6: 1 <= n by NAT_1: 13;

      n <> 1 by A2, A1, Th21;

      then

       A8: 1 < n by A6, XXREAL_0: 1;

      set A = { X where X be Subset of cRs : X in ( conjugate_Classes Rs) & ( card X) = 1 };

      set B = (( conjugate_Classes Rs) \ A);

      for x be object st x in A holds x in ( conjugate_Classes Rs)

      proof

        let x be object;

        assume x in A;

        then ex y be Subset of cRs st x = y & y in ( conjugate_Classes Rs) & ( card y) = 1;

        hence thesis;

      end;

      then

       A9: A c= ( conjugate_Classes Rs);

      then

       A10: ( conjugate_Classes Rs) = (A \/ B) by XBOOLE_1: 45;

      consider f be Function such that

       A11: ( dom f) = cZs and

       A12: for x be object st x in cZs holds (f . x) = {x} from FUNCT_1:sch 3;

      

       A13: f is one-to-one

      proof

        let x1,x2 be object;

        assume that

         A14: x1 in ( dom f) and

         A15: x2 in ( dom f) and

         A16: (f . x1) = (f . x2);

        

         A17: (f . x1) = {x1} by A11, A12, A14;

        (f . x2) = {x2} by A11, A12, A15;

        hence thesis by A16, A17, ZFMISC_1: 3;

      end;

      now

        let x be object;

        hereby

          assume x in ( rng f);

          then

          consider xx be object such that

           A18: xx in ( dom f) and

           A19: x = (f . xx) by FUNCT_1:def 3;

          

           A20: x = {xx} by A11, A12, A18, A19;

          

           A21: cZs c= cRs by GROUP_2:def 5;

          then

          reconsider X = x as Subset of cRs by A11, A18, A20, ZFMISC_1: 31;

          reconsider xx as Element of Rs by A11, A18, A21;

          xx in ( center Rs) by A11, A18;

          then ( con_class xx) = {xx} by GROUP_5: 81;

          then

           A22: X in ( conjugate_Classes Rs) by A20;

          ( card X) = 1 by A20, CARD_1: 30;

          hence x in A by A22;

        end;

        assume x in A;

        then

        consider X be Subset of cRs such that

         A23: x = X and

         A24: X in ( conjugate_Classes Rs) and

         A25: ( card X) = 1;

        consider a be Element of cRs such that

         A26: ( con_class a) = X by A24;

        

         A27: a in ( con_class a) by GROUP_3: 83;

        consider xx be object such that

         A28: X = {xx} by A25, CARD_2: 42;

        

         A29: a = xx by A26, A27, A28, TARSKI:def 1;

        then a in ( center Rs) by A26, A28, GROUP_5: 81;

        then

         A30: a in cZs;

        then (f . a) = {a} by A12;

        hence x in ( rng f) by A11, A23, A28, A29, A30, FUNCT_1: 3;

      end;

      then ( rng f) = A by TARSKI: 2;

      then

       A31: (A,cZs) are_equipotent by A11, A13, WELLORD2:def 4;

      ( card cZs) = natq1 by Th37;

      then

       A32: ( card A) = natq1 by A31, CARD_1: 5;

      consider f1 be FinSequence such that

       A33: ( rng f1) = A and

       A34: f1 is one-to-one by A9, FINSEQ_4: 58;

      consider f2 be FinSequence such that

       A35: ( rng f2) = B and

       A36: f2 is one-to-one by FINSEQ_4: 58;

      set f = (f1 ^ f2);

      

       A37: ( rng f) = ( conjugate_Classes Rs) by A10, A33, A35, FINSEQ_1: 31;

      now

        given x be object such that

         A38: x in (A /\ B);

        

         A39: x in A by A38, XBOOLE_0:def 4;

        x in B by A38, XBOOLE_0:def 4;

        hence contradiction by A39, XBOOLE_0:def 5;

      end;

      then (A /\ B) = {} by XBOOLE_0:def 1;

      then ( rng f1) misses ( rng f2) by A33, A35, XBOOLE_0:def 7;

      then

       A40: f is one-to-one FinSequence of ( conjugate_Classes Rs) by A34, A36, A37, FINSEQ_1:def 4, FINSEQ_3: 91;

      deffunc F( set) = ( card (f1 . $1));

      consider p1 be FinSequence such that

       A41: ( len p1) = ( len f1) & for i be Nat st i in ( dom p1) holds (p1 . i) = F(i) from FINSEQ_1:sch 2;

      for x be object st x in ( rng p1) holds x in NAT

      proof

        let x be object;

        assume x in ( rng p1);

        then

        consider i be Nat such that

         A42: i in ( dom p1) and

         A43: (p1 . i) = x by FINSEQ_2: 10;

        

         A44: x = ( card (f1 . i)) by A41, A42, A43;

        i in ( dom f1) by A41, A42, FINSEQ_3: 29;

        then (f1 . i) in A by A33, FUNCT_1: 3;

        then ex X be Subset of cRs st ((f1 . i) = X) & (X in ( conjugate_Classes Rs)) & (( card X) = 1);

        hence thesis by A44;

      end;

      then ( rng p1) c= NAT ;

      then

      reconsider c1 = p1 as FinSequence of NAT by FINSEQ_1:def 4;

      

       A45: ( len c1) = natq1 by A32, A33, A34, A41, FINSEQ_4: 62;

      

       A46: for i be Element of NAT st i in ( dom c1) holds (c1 . i) = 1

      proof

        let i be Element of NAT such that

         A47: i in ( dom c1);

        i in ( dom f1) by A41, A47, FINSEQ_3: 29;

        then (f1 . i) in A by A33, FUNCT_1: 3;

        then ex X be Subset of cRs st (f1 . i) = X & X in ( conjugate_Classes Rs) & ( card X) = 1;

        hence thesis by A41, A47;

      end;

      for x be object st x in ( rng c1) holds x in {1}

      proof

        let x be object;

        assume x in ( rng c1);

        then ex i be Nat st (i in ( dom c1)) & (x = (c1 . i)) by FINSEQ_2: 10;

        then x = 1 by A46;

        hence thesis by TARSKI:def 1;

      end;

      then

       A48: ( rng c1) c= {1};

      for x be object st x in {1} holds x in ( rng c1)

      proof

        let x be object such that

         A49: x in {1};

        

         A50: ( Seg ( len c1)) = ( dom c1) by FINSEQ_1:def 3;

        then (c1 . ( len c1)) = 1 by A5, A45, A46, FINSEQ_1: 3;

        then (c1 . ( len c1)) = x by A49, TARSKI:def 1;

        hence thesis by A5, A45, A50, FINSEQ_1: 3, FUNCT_1: 3;

      end;

      then {1} c= ( rng c1);

      then ( rng c1) = {1} by A48, XBOOLE_0:def 10;

      then c1 = (( dom c1) --> 1) by FUNCOP_1: 9;

      then c1 = (( Seg ( len c1)) --> 1) by FINSEQ_1:def 3;

      then c1 = (( len c1) |-> 1) by FINSEQ_2:def 2;

      then ( Sum c1) = (( len c1) * 1) by RVSUM_1: 80;

      then

       A51: ( Sum c1) = natq1 by A32, A33, A34, A41, FINSEQ_4: 62;

      deffunc P2( set) = ( card (f2 . $1));

      consider p2 be FinSequence such that

       A52: ( len p2) = ( len f2) & for i be Nat st i in ( dom p2) holds (p2 . i) = P2(i) from FINSEQ_1:sch 2;

      for x be object st x in ( rng p2) holds x in NAT

      proof

        let x be object;

        assume x in ( rng p2);

        then

        consider i be Nat such that

         A53: i in ( dom p2) and

         A54: (p2 . i) = x by FINSEQ_2: 10;

        

         A55: x = ( card (f2 . i)) by A52, A53, A54;

        i in ( dom f2) by A52, A53, FINSEQ_3: 29;

        then (f2 . i) in (( conjugate_Classes Rs) \ A) by A35, FUNCT_1: 3;

        then (f2 . i) in ( conjugate_Classes Rs) by XBOOLE_0:def 5;

        then

        consider a be Element of cRs such that

         A56: ( con_class a) = (f2 . i);

        ( card ( con_class a)) is Element of NAT ;

        hence thesis by A55, A56;

      end;

      then ( rng p2) c= NAT ;

      then

      reconsider c2 = p2 as FinSequence of NAT by FINSEQ_1:def 4;

      set c = (c1 ^ c2);

      reconsider c as FinSequence of NAT ;

      ( len c) = (( len f1) + ( len f2)) by A41, A52, FINSEQ_1: 22;

      then

       A57: ( len c) = ( len f) by FINSEQ_1: 22;

      for i be Element of NAT st i in ( dom c) holds (c . i) = ( card (f . i))

      proof

        let i be Element of NAT such that

         A58: i in ( dom c);

        now

          per cases by A58, FINSEQ_1: 25;

            suppose

             A59: i in ( dom c1);

            then

             A60: i in ( dom f1) by A41, FINSEQ_3: 29;

            (c . i) = (c1 . i) by A59, FINSEQ_1:def 7

            .= ( card (f1 . i)) by A41, A59

            .= ( card (f . i)) by A60, FINSEQ_1:def 7;

            hence thesis;

          end;

            suppose ex j be Nat st j in ( dom c2) & i = (( len c1) + j);

            then

            consider j be Nat such that

             A61: j in ( dom c2) and

             A62: i = (( len c1) + j);

            

             A63: j in ( dom f2) by A52, A61, FINSEQ_3: 29;

            (c . i) = (c2 . j) by A61, A62, FINSEQ_1:def 7

            .= ( card (f2 . j)) by A52, A61

            .= ( card (f . i)) by A41, A62, A63, FINSEQ_1:def 7;

            hence thesis;

          end;

        end;

        hence thesis;

      end;

      then ( card Rs) = ( Sum c) by A37, A40, A57, Th6;

      then

       A64: ((q |^ n) - 1) = (( Sum c2) + (q - 1)) by A3, A51, RVSUM_1: 75;

      reconsider q as non zero Element of NAT ;

      reconsider n as non zero Element of NAT by Th32, ORDINAL1:def 12;

      q in COMPLEX by XCMPLX_0:def 2;

      then

      reconsider qc = q as Element of F_Complex by COMPLFLD:def 1;

      set pnq = ( eval (( cyclotomic_poly n),qc));

      reconsider pnq as Integer by UNIROOTS: 52;

      reconsider abspnq = |.pnq.| as Element of NAT ;

      (q |^ n) <> 0 by PREPOWER: 5;

      then ((q |^ n) + 1) > ( 0 + 1) by XREAL_1: 8;

      then (q |^ n) >= 1 by NAT_1: 13;

      then ((q |^ n) + ( - 1)) >= (1 + ( - 1)) by XREAL_1: 7;

      then

      reconsider qn1 = ((q |^ n) - 1) as Element of NAT by INT_1: 3;

      pnq divides ((q |^ n) - 1) by UNIROOTS: 58;

      then abspnq divides |.((q |^ n) - 1).| by INT_2: 16;

      then

       A65: abspnq divides qn1 by ABSVALUE:def 1;

      for i be Element of NAT st i in ( dom c2) holds abspnq divides (c2 /. i)

      proof

        let i be Element of NAT such that

         A66: i in ( dom c2);

        (c2 . i) = ( card (f2 . i)) by A52, A66;

        then

         A67: (c2 /. i) = ( card (f2 . i)) by A66, PARTFUN1:def 6;

        

         A68: i in ( dom f2) by A52, A66, FINSEQ_3: 29;

        then (f2 . i) in (( conjugate_Classes Rs) \ A) by A35, FUNCT_1: 3;

        then (f2 . i) in ( conjugate_Classes Rs) by XBOOLE_0:def 5;

        then

        consider a be Element of cRs such that

         A69: ( con_class a) = (f2 . i);

        reconsider a as Element of Rs;

        reconsider s = a as Element of R by UNIROOTS: 19;

        set ns = ( dim ( VectSp_over_center s));

        set ca = ( card ( con_class a));

        set oa = ( card ( Centralizer a));

        

         A70: ( card Rs) = ((ca * oa) + 0 ) by Th13;

        then

         A71: (( card Rs) div oa) = ca by NAT_D:def 1;

        

         A72: (qn1 div oa) = ca by A3, A70, NAT_D:def 1;

        (q |^ ns) <> 0 by PREPOWER: 5;

        then ((q |^ ns) + 1) > ( 0 + 1) by XREAL_1: 8;

        then (q |^ ns) >= 1 by NAT_1: 13;

        then ((q |^ ns) + ( - 1)) >= (1 + ( - 1)) by XREAL_1: 7;

        then

        reconsider qns1 = ((q |^ ns) - 1) as Element of NAT by INT_1: 3;

        

         A73: oa = (( card the carrier of ( centralizer s)) - 1) by Th30

        .= qns1 by Th33;

        reconsider ns as non zero Element of NAT by Th34, ORDINAL1:def 12;

        

         A74: ns <= n by Th36, NAT_D: 7;

        now

          assume ns = n;

          then

           A75: ( card (f2 . i)) = 1 by A3, A69, A71, A73, NAT_2: 3;

          

           A76: (f2 . i) in B by A35, A68, FUNCT_1: 3;

          then

           A77: (f2 . i) in ( conjugate_Classes Rs) by XBOOLE_0:def 5;

           not (f2 . i) in A by A76, XBOOLE_0:def 5;

          hence contradiction by A75, A77;

        end;

        then ns < n by A74, XXREAL_0: 1;

        then pnq divides (qn1 qua Integer div qns1) by Th36, UNIROOTS: 59;

        then abspnq divides |.(qn1 div qns1).| by INT_2: 16;

        hence thesis by A67, A69, A72, A73, ABSVALUE:def 1;

      end;

      then abspnq divides natq1 by A64, A65, Th5, NAT_D: 10;

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

    end;

    theorem :: WEDDWITT:39

    for R be Skew-Field holds ( 1. ( center R)) = ( 1. R) by Def4;

    theorem :: WEDDWITT:40

    for R be Skew-Field, s be Element of R holds ( 1. ( centralizer s)) = ( 1. R) by Def5;