field_6.miz



    begin

    theorem :: FIELD_6:1

    

     degen: for R be Ring holds R is degenerated iff the carrier of R = {( 0. R)}

    proof

      let L be Ring;

      now

        assume

         AS: L is degenerated;

        

         B: {( 0. L)} c= the carrier of L;

        now

          let o be object;

          assume o in the carrier of L;

          then

          reconsider a = o as Element of L;

          a = (a * ( 1. L))

          .= ( 0. L) by AS;

          hence o in {( 0. L)} by TARSKI:def 1;

        end;

        hence the carrier of L = {( 0. L)} by B, TARSKI: 2;

      end;

      hence thesis;

    end;

    registration

      let F be Field;

      cluster ( {( 0. F)} -Ideal ) -> maximal;

      coherence

      proof

        set I = ( {( 0. F)} -Ideal );

        I = {( 0. F)} by IDEAL_1: 47;

        then not (( 1. F) in I) by TARSKI:def 1;

        then

         A: I is proper by IDEAL_1: 19;

        for J be Ideal of F st I c= J holds J = I or J is non proper

        proof

          let J be Ideal of F;

          per cases by IDEAL_1: 22;

            suppose J = {( 0. F)};

            hence thesis by IDEAL_1: 47;

          end;

            suppose J = the carrier of F;

            then J = ( [#] F);

            hence thesis;

          end;

        end;

        hence thesis by A, RING_1:def 3, RING_1:def 4;

      end;

    end

    registration

      let R be non degenerated non almost_left_invertible comRing;

      cluster ( {( 0. R)} -Ideal ) -> non maximal;

      coherence

      proof

        set I = ( {( 0. R)} -Ideal );

        consider J be Ideal of R such that

         H: J <> {( 0. R)} & J <> the carrier of R by IDEAL_1: 22;

        

         A: I c= J

        proof

          now

            let o be object;

            assume o in I;

            then o in {( 0. R)} by IDEAL_1: 47;

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

            hence o in J by IDEAL_1: 2;

          end;

          hence thesis;

        end;

        

         B: J is proper by H, SUBSET_1:def 6;

        J <> I by H, IDEAL_1: 47;

        hence thesis by A, B, RING_1:def 3;

      end;

    end

    definition

      let R be Ring;

      :: FIELD_6:def1

      attr R is field-containing means

      : deffc: ex F be Field st F is Subring of R;

    end

    registration

      cluster field-containing for Ring;

      existence

      proof

        ex R be Ring st R is field-containing

        proof

          set F = the Field;

          take F;

          F is Subfield of F by FIELD_4: 1;

          then F is Subring of F by FIELD_5: 12;

          hence thesis;

        end;

        hence thesis;

      end;

    end

    definition

      let R be field-containing Ring;

      :: FIELD_6:def2

      mode Subfield of R -> Field means

      : defsubfr: it is Subring of R;

      existence by deffc;

    end

    theorem :: FIELD_6:2

    

     thLC: for R be non degenerated Ring holds for p be non zero Polynomial of R holds (p . ( deg p)) = ( LC p)

    proof

      let R be non degenerated Ring, p be non zero Polynomial of R;

      ( deg p) = (( len p) - 1) by HURWITZ:def 2;

      

      hence (p . ( deg p)) = (p . (( len p) -' 1)) by XREAL_0:def 2

      .= ( LC p) by RATFUNC1:def 6;

    end;

    registration

      let R be non degenerated Ring;

      let p be non zero Polynomial of R;

      cluster ( LM p) -> non zero;

      coherence

      proof

        ( len ( LM p)) = ( len p) by POLYNOM4: 15;

        then ( LM p) <> ( 0_. R) by POLYNOM4: 5, POLYNOM4: 3;

        hence thesis by UPROOTS:def 5;

      end;

    end

    theorem :: FIELD_6:3

    

     thdegLM: for R be Ring, p be Polynomial of R holds ( deg ( LM p)) = ( deg p)

    proof

      let R be Ring, p be Polynomial of R;

      

      thus ( deg ( LM p)) = (( len ( LM p)) - 1) by HURWITZ:def 2

      .= (( len p) - 1) by POLYNOM4: 15

      .= ( deg p) by HURWITZ:def 2;

    end;

    theorem :: FIELD_6:4

    

     thdegLC: for R be Ring, p be Polynomial of R holds ( LC ( LM p)) = ( LC p)

    proof

      let R be Ring, p be Polynomial of R;

      

      thus ( LC ( LM p)) = (( LM p) . (( len ( LM p)) -' 1)) by RATFUNC1:def 6

      .= (( LM p) . (( len p) -' 1)) by POLYNOM4: 15

      .= (p . (( len p) -' 1)) by POLYNOM4:def 1

      .= ( LC p) by RATFUNC1:def 6;

    end;

    theorem :: FIELD_6:5

    

     thdLM: for R be non degenerated Ring holds for p be non zero Polynomial of R holds ( deg (p - ( LM p))) < ( deg p)

    proof

      let R be non degenerated Ring, p be non zero Polynomial of R;

      per cases ;

        suppose (p - ( LM p)) = ( 0_. R);

        hence thesis by HURWITZ: 20;

      end;

        suppose (p - ( LM p)) <> ( 0_. R);

        then

        reconsider q = (p - ( LM p)) as non zero Polynomial of R by UPROOTS:def 5;

         A:

        now

          assume ( deg q) = ( deg p);

          

          then ( LC q) = (q . ( deg p)) by thLC

          .= ((p . ( deg p)) - (( LM p) . ( deg p))) by POLYNOM3: 27

          .= ((p . ( deg p)) - (( LM p) . ( deg ( LM p)))) by thdegLM

          .= ((p . ( deg p)) - ( LC ( LM p))) by thLC

          .= ((p . ( deg p)) - ( LC p)) by thdegLC

          .= (( LC p) - ( LC p)) by thLC

          .= ( 0. R) by RLVECT_1: 15;

          hence contradiction;

        end;

        now

          assume

           B0: ( deg q) > ( deg p);

          then ( deg q) >= (( deg p) + 1) by INT_1: 7;

          then

           B1: ( deg q) >= ((( len p) - 1) + 1) by HURWITZ:def 2;

          p <> ( 0_. R);

          then ( len p) <> 0 by POLYNOM4: 5;

          then (( len p) + 1) > ( 0 + 1) by XREAL_1: 6;

          then

           D: ( len p) >= 1 by NAT_1: 13;

          ( deg q) <> (( len p) - 1) by B0, HURWITZ:def 2;

          then ( deg q) <> (( len p) -' 1) by D, XREAL_0:def 2;

          then

           B2: (( LM p) . ( deg q)) = ( 0. R) by POLYNOM4:def 1;

          ( LC q) = (q . ( deg q)) by thLC

          .= ((p . ( deg q)) - (( LM p) . ( deg q))) by POLYNOM3: 27

          .= (( 0. R) - ( 0. R)) by ALGSEQ_1: 8, B1, B2;

          hence contradiction;

        end;

        hence thesis by A, XXREAL_0: 1;

      end;

    end;

    theorem :: FIELD_6:6

    

     thE1: for R be Ring holds for p be Polynomial of R holds for i be Nat holds (( <%( 0. R), ( 1. R)%> *' p) . (i + 1)) = (p . i)

    proof

      let R be Ring, p be Polynomial of R;

      let i be Nat;

      set q = <%( 0. R), ( 1. R)%>;

      consider r be FinSequence of the carrier of R such that

       A: ( len r) = ((i + 1) + 1) & (( <%( 0. R), ( 1. R)%> *' p) . (i + 1)) = ( Sum r) & for k be Element of NAT st k in ( dom r) holds (r . k) = ((q . (k -' 1)) * (p . (((i + 1) + 1) -' k))) by POLYNOM3:def 9;

      

       B: ( dom r) = ( Seg (i + 2)) by A, FINSEQ_1:def 3;

      

       C: ( Seg 2) c= ( dom r) by B, FINSEQ_1: 5, NAT_1: 11;

      

       D: 2 in ( dom r) by C, FINSEQ_1: 3;

      

       H2: (2 - 2) <= ((i + 2) - 2) by NAT_1: 11, XREAL_1: 9;

      

       H3: 0 <= (2 - 1);

      

       E: (r /. 2) = (r . 2) by D, PARTFUN1:def 6

      .= ((q . (2 -' 1)) * (p . (((i + 1) + 1) -' 2))) by D, A

      .= ((q . 1) * (p . (((i + 1) + 1) -' 2))) by H3, XREAL_0:def 2

      .= ((q . 1) * (p . i)) by H2, XREAL_0:def 2

      .= (( 1. R) * (p . i)) by POLYNOM5: 38;

       F:

      now

        let k be Element of NAT ;

        assume

         F: k in ( dom r) & k <> 2;

        per cases by XXREAL_0: 1;

          suppose k < 2;

          then (k + 1) <= 2 by INT_1: 7;

          then

           F4: ((k + 1) - 1) <= (2 - 1) by XREAL_1: 9;

          

           F5: 1 <= k by F, B, FINSEQ_1: 1;

          then

           F3: k = 1 by F4, XXREAL_0: 1;

          

           F2: (k -' 1) = (k - 1) by F5, XREAL_0:def 2;

          

          thus (r /. k) = (r . k) by F, PARTFUN1:def 6

          .= ((q . (k -' 1)) * (p . (((i + 1) + 1) -' k))) by A, F

          .= (( 0. R) * (p . (((i + 1) + 1) -' k))) by F3, F2, POLYNOM5: 38

          .= ( 0. R);

        end;

          suppose

           F4: k > 2;

          then (2 + 1) <= k by INT_1: 7;

          then

           F3: ((2 + 1) - 1) <= (k - 1) by XREAL_1: 9;

          

           F2: (k - 1) = (k -' 1) by F4, XREAL_0:def 2;

          

          thus (r /. k) = (r . k) by F, PARTFUN1:def 6

          .= ((q . (k -' 1)) * (p . (((i + 1) + 1) -' k))) by A, F

          .= (( 0. R) * (p . (((i + 1) + 1) -' k))) by F2, F3, POLYNOM5: 38

          .= ( 0. R);

        end;

      end;

      thus (( <%( 0. R), ( 1. R)%> *' p) . (i + 1)) = (p . i) by E, A, D, F, POLYNOM2: 3;

    end;

    theorem :: FIELD_6:7

    

     thE2: for R be Ring holds for p be Polynomial of R holds (( <%( 0. R), ( 1. R)%> *' p) . 0 ) = ( 0. R)

    proof

      let R be Ring, p be Polynomial of R;

      set q = <%( 0. R), ( 1. R)%>;

      consider r be FinSequence of the carrier of R such that

       A: ( len r) = ( 0 + 1) & (( <%( 0. R), ( 1. R)%> *' p) . 0 ) = ( Sum r) & for k be Element of NAT st k in ( dom r) holds (r . k) = ((q . (k -' 1)) * (p . (( 0 + 1) -' k))) by POLYNOM3:def 9;

      ( dom r) = {1} by FINSEQ_1: 2, A, FINSEQ_1:def 3;

      then 1 in ( dom r) by TARSKI:def 1;

      

      then

       C: (r . 1) = ((q . (1 -' 1)) * (p . (( 0 + 1) -' 1))) by A

      .= ((q . 0 ) * (p . (1 -' 1))) by NAT_2: 8

      .= ((q . 0 ) * (p . 0 )) by NAT_2: 8

      .= (( 0. R) * (p . 0 )) by POLYNOM5: 38;

      r = <*(r . 1)*> by A, FINSEQ_1: 40;

      hence thesis by A, C, RLVECT_1: 44;

    end;

    theorem :: FIELD_6:8

    for R be domRing holds for p be non zero Polynomial of R holds ( deg ( <%( 0. R), ( 1. R)%> *' p)) = (( deg p) + 1)

    proof

      let R be domRing, p be non zero Polynomial of R;

      

       B: ( len <%( 0. R), ( 1. R)%>) = 2 by POLYNOM5: 40;

      then

       A: <%( 0. R), ( 1. R)%> <> ( 0_. R) by POLYNOM4: 3;

      

       C: ( deg <%( 0. R), ( 1. R)%>) = (2 - 1) by B, HURWITZ:def 2;

      thus ( deg ( <%( 0. R), ( 1. R)%> *' p)) = (( deg p) + 1) by C, A, HURWITZ: 23;

    end;

    

     help1: for R be domRing, n be Element of NAT holds (( <%( 0. R), ( 1. R)%> `^ n) . n) = ( 1. R)

    proof

      let R be domRing, n be Element of NAT ;

      ( <%( 0. R), ( 1. R)%> `^ n) = ( anpoly (( 1. R),n)) by FIELD_1: 12;

      hence thesis by POLYDIFF: 24;

    end;

    

     help2: for R be domRing, n,i be Element of NAT st i <> n holds (( <%( 0. R), ( 1. R)%> `^ n) . i) = ( 0. R)

    proof

      let R be domRing, n,i be Element of NAT ;

      assume

       AS: i <> n;

      ( <%( 0. R), ( 1. R)%> `^ n) = ( anpoly (( 1. R),n)) by FIELD_1: 12;

      hence (( <%( 0. R), ( 1. R)%> `^ n) . i) = ( 0. R) by AS, POLYDIFF: 25;

    end;

    

     help3a: for R be domRing holds for n be Element of NAT st n <> 0 holds for a be Element of R holds ( eval (( <%( 0. R), ( 1. R)%> `^ n),a)) = (a |^ n)

    proof

      let R be domRing;

      let n be Element of NAT ;

      assume

       A: n <> 0 ;

      let a be Element of R;

      ( <%( 0. R), ( 1. R)%> `^ n) = ( anpoly (( 1. R),n)) by FIELD_1: 12;

      

      hence ( eval (( <%( 0. R), ( 1. R)%> `^ n),a)) = (( 1. R) * (a |^ n)) by A, FIELD_1: 6

      .= (a |^ n);

    end;

    theorem :: FIELD_6:9

    for R be comRing, p be Polynomial of R holds for a be Element of R holds ( eval (( <%( 0. R), ( 1. R)%> *' p),a)) = (a * ( eval (p,a)))

    proof

      let R be comRing, p be Polynomial of R;

      let a be Element of R;

      per cases ;

        suppose R is degenerated;

        then

         A: the carrier of R = {( 0. R)} by degen;

        

        hence ( eval (( <%( 0. R), ( 1. R)%> *' p),a)) = ( 0. R) by TARSKI:def 1

        .= (a * ( eval (p,a))) by A, TARSKI:def 1;

      end;

        suppose R is non degenerated;

        

        hence ( eval (( <%( 0. R), ( 1. R)%> *' p),a)) = (( eval ( <%( 0. R), ( 1. R)%>,a)) * ( eval (p,a))) by POLYNOM4: 24

        .= ((( 0. R) + (( 1. R) * a)) * ( eval (p,a))) by POLYNOM5: 44

        .= (a * ( eval (p,a)));

      end;

    end;

    

     ThR1: for R be Ring holds R is Subring of R by LIOUVIL2: 18;

    theorem :: FIELD_6:10

    

     FIELD427: for R be Ring, S be RingExtension of R holds for p be Element of the carrier of ( Polynom-Ring R), a be Element of R, b be Element of S st b = a holds ( Ext_eval (p,b)) = ( eval (p,a))

    proof

      let R be Ring, S be RingExtension of R;

      let p be Element of the carrier of ( Polynom-Ring R);

      let a be Element of R, b be Element of S;

      assume

       A1: b = a;

      

       A2: R is Subring of S by FIELD_4:def 1;

      then

       A3: the carrier of R c= the carrier of S by C0SP1:def 3;

      ( Ext_eval (p,( In (a,S)))) = ( In (( eval (p,a)),S)) by A2, ALGNUM_1: 12

      .= ( eval (p,a)) by A3, SUBSET_1:def 8;

      hence thesis by A1;

    end;

    theorem :: FIELD_6:11

    

     lemma7: for F be Field, p be Element of the carrier of ( Polynom-Ring F) holds for E be FieldExtension of F, K be E -extending FieldExtension of F holds for a be Element of E, b be Element of K st a = b holds ( Ext_eval (p,a)) = ( Ext_eval (p,b))

    proof

      let F be Field, p be Element of the carrier of ( Polynom-Ring F);

      let E be FieldExtension of F, U be E -extending FieldExtension of F;

      let a be Element of E, b be Element of U;

      assume

       AS2: a = b;

      

       H1: E is Subring of U by FIELD_4:def 1;

      then

       H2: the carrier of E c= the carrier of U by C0SP1:def 3;

      F is Subring of E by FIELD_4:def 1;

      then

       H4: the carrier of F c= the carrier of E by C0SP1:def 3;

      consider Fp be FinSequence of E such that

       A: ( Ext_eval (p,a)) = ( Sum Fp) & ( len Fp) = ( len p) & for n be Element of NAT st n in ( dom Fp) holds (Fp . n) = (( In ((p . (n -' 1)),E)) * (( power E) . (a,(n -' 1)))) by ALGNUM_1:def 1;

      consider Fq be FinSequence of U such that

       B: ( Ext_eval (p,b)) = ( Sum Fq) & ( len Fq) = ( len p) & for n be Element of NAT st n in ( dom Fq) holds (Fq . n) = (( In ((p . (n -' 1)),U)) * (( power U) . (b,(n -' 1)))) by ALGNUM_1:def 1;

       C:

      now

        let n be Element of NAT ;

        

        thus (( power U) . (b,(n -' 1))) = (( power U) . (( In (b,U)),(n -' 1)))

        .= ( In ((( power E) . (a,(n -' 1))),U)) by AS2, H1, ALGNUM_1: 7

        .= (( power E) . (a,(n -' 1))) by H2, SUBSET_1:def 8;

      end;

      

       D: ( dom Fp) = ( Seg ( len Fq)) by A, B, FINSEQ_1:def 3

      .= ( dom Fq) by FINSEQ_1:def 3;

       E:

      now

        let n be Element of NAT ;

        (p . (n -' 1)) in U by H2, H4;

        

        hence ( In ((p . (n -' 1)),U)) = (p . (n -' 1)) by SUBSET_1:def 8

        .= ( In ((p . (n -' 1)),E)) by H4, SUBSET_1:def 8;

      end;

      

       H: for n be Element of NAT holds [( In ((p . (n -' 1)),E)), (( power E) . (a,(n -' 1)))] in [:the carrier of E, the carrier of E:] by ZFMISC_1:def 2;

      now

        let n be Nat;

        assume

         F: n in ( dom Fq);

        

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

        

        thus (Fq . n) = (( In ((p . (n -' 1)),U)) * (( power U) . (b,(n -' 1)))) by B, F

        .= (the multF of U . (( In ((p . (n -' 1)),U)),(( power E) . (a,(n -' 1))))) by C, G

        .= (the multF of U . (( In ((p . (n -' 1)),E)),(( power E) . (a,(n -' 1))))) by E, G

        .= ((the multF of U || the carrier of E) . (( In ((p . (n -' 1)),E)),(( power E) . (a,(n -' 1))))) by G, H, FUNCT_1: 49

        .= (( In ((p . (n -' 1)),E)) * (( power E) . (a,(n -' 1)))) by H1, C0SP1:def 3

        .= (Fp . n) by A, D, F;

      end;

      then Fp = Fq by D;

      hence thesis by H1, A, B, FIELD_4: 2;

    end;

    registration

      let L be non empty ZeroStr, a,b be Element of L;

      let f be the carrier of L -valued Function;

      let x,y be object;

      cluster (f +* ((x,y) --> (a,b))) -> the carrier of L -valued;

      coherence

      proof

        set g = (f +* ((x,y) --> (a,b)));

        

         I: ( dom ((x,y) --> (a,b))) = {x, y} by FUNCT_2:def 1;

        then

         H: ( dom g) = (( dom f) \/ {x, y}) by FUNCT_4:def 1;

        now

          let o be object;

          assume o in ( rng g);

          then

          consider z be object such that

           A: z in ( dom g) & (g . z) = o by FUNCT_1:def 3;

          per cases ;

            suppose

             B: z in {x, y};

            per cases by TARSKI:def 2;

              suppose z = x;

              then

               G: (g . z) = (((x,y) --> (a,b)) . x) by B, I, FUNCT_4: 13;

              per cases ;

                suppose x <> y;

                then (g . z) = a by G, FUNCT_4: 63;

                hence o in the carrier of L by A;

              end;

                suppose x = y;

                then (g . z) = b by G, FUNCT_4: 63;

                hence o in the carrier of L by A;

              end;

            end;

              suppose z = y;

              

              then (g . z) = (((x,y) --> (a,b)) . y) by B, I, FUNCT_4: 13

              .= b by FUNCT_4: 63;

              hence o in the carrier of L by A;

            end;

          end;

            suppose

             D: not z in {x, y};

            then not z in ( dom ((x,y) --> (a,b)));

            then

             C: (g . z) = (f . z) by FUNCT_4: 11;

            z in ( dom f) by D, A, H, XBOOLE_0:def 3;

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

            hence o in the carrier of L by A, C;

          end;

        end;

        then ( rng g) c= the carrier of L;

        hence thesis by RELAT_1:def 19;

      end;

    end

    registration

      let L be non empty ZeroStr, a,b be Element of L;

      let f be finite-Support sequence of L;

      let x,y be object;

      cluster (f +* ((x,y) --> (a,b))) -> finite-Support;

      coherence

      proof

        let g be sequence of L such that

         A1: g = (f +* ((x,y) --> (a,b)));

        

         H0: ( dom ((x,y) --> (a,b))) = {x, y} by FUNCT_4: 62;

        then

         H1: ( dom g) = (( dom f) \/ {x, y}) by A1, FUNCT_4:def 1;

        

         A2: ( Support f) is finite by POLYNOM1:def 5;

        now

          let o be object;

          assume o in ( Support g);

          then

           B0: o in ( dom g) & (g . o) <> ( 0. L) by POLYNOM1:def 3;

          per cases ;

            suppose

             B1: not o in {x, y};

            then

             B2: (g . o) = (f . o) by A1, H0, FUNCT_4: 11;

            o in ( dom f) by B0, B1, H1, XBOOLE_0:def 3;

            then o in ( Support f) by B2, B0, POLYNOM1:def 3;

            hence o in (( Support f) \/ {x, y}) by XBOOLE_0:def 3;

          end;

            suppose o in {x, y};

            hence o in (( Support f) \/ {x, y}) by XBOOLE_0:def 3;

          end;

        end;

        then ( Support g) c= (( Support f) \/ {x, y});

        hence thesis by A2, POLYNOM1:def 5;

      end;

    end

    begin

    theorem :: FIELD_6:12

    

     RE: for R1,R2 be strict Ring st R1 is Subring of R2 & R2 is Subring of R1 holds R1 = R2

    proof

      let K1,K2 be strict Ring;

      assume

       A1: K1 is Subring of K2 & K2 is Subring of K1;

      

       A2: the carrier of K1 c= the carrier of K2 & the carrier of K2 c= the carrier of K1 by A1, C0SP1:def 3;

      then

       A3: the carrier of K1 = the carrier of K2 by XBOOLE_0:def 10;

      

       A4: the addF of K2 = (the addF of K2 || the carrier of K1) by A3

      .= the addF of K1 by A1, C0SP1:def 3;

      

       A5: the multF of K2 = (the multF of K2 || the carrier of K1) by A3

      .= the multF of K1 by A1, C0SP1:def 3;

      ( 1. K1) = ( 1. K2) & ( 0. K1) = ( 0. K2) by A1, C0SP1:def 3;

      hence thesis by A4, A5, A2, XBOOLE_0:def 10;

    end;

    theorem :: FIELD_6:13

    

     Th6: for S be Ring, R1,R2 be Subring of S holds R1 is Subring of R2 iff the carrier of R1 c= the carrier of R2

    proof

      let K be Ring, SK1,SK2 be Subring of K;

      set C1 = the carrier of SK1;

      set C2 = the carrier of SK2;

      set ADD = the addF of K;

      set MULT = the multF of K;

      thus SK1 is Subring of SK2 implies C1 c= C2 by C0SP1:def 3;

      assume

       A1: C1 c= C2;

      then

       A2: [:C1, C1:] c= [:C2, C2:] by ZFMISC_1: 96;

      the addF of SK2 = (ADD || C2) by C0SP1:def 3;

      

      then

       A3: (the addF of SK2 || C1) = (ADD || C1) by A2, FUNCT_1: 51

      .= the addF of SK1 by C0SP1:def 3;

      the multF of SK2 = (MULT || C2) by C0SP1:def 3;

      

      then

       A4: (the multF of SK2 || C1) = (MULT || C1) by A2, FUNCT_1: 51

      .= the multF of SK1 by C0SP1:def 3;

      ( 1. SK1) = ( 1. K) & ( 0. SK1) = ( 0. K) by C0SP1:def 3;

      then ( 1. SK1) = ( 1. SK2) & ( 0. SK1) = ( 0. SK2) by C0SP1:def 3;

      hence thesis by A1, A3, A4, C0SP1:def 3;

    end;

    theorem :: FIELD_6:14

    

     RE1: for S be Ring, R1,R2 be strict Subring of S holds R1 = R2 iff the carrier of R1 = the carrier of R2

    proof

      let K be Ring;

      let SK1,SK2 be strict Subring of K;

      thus SK1 = SK2 implies the carrier of SK1 = the carrier of SK2;

      assume

       A1: the carrier of SK1 = the carrier of SK2;

      then

       A2: SK2 is strict Subring of SK1 by Th6;

      SK1 is strict Subring of SK2 by A1, Th6;

      hence thesis by A2, RE;

    end;

    theorem :: FIELD_6:15

    

     Th17: for S be Ring, R be Subring of S holds for x,y be Element of S, x1,y1 be Element of R st x = x1 & y = y1 holds (x + y) = (x1 + y1)

    proof

      let R be Ring, S be Subring of R;

      let x,y be Element of R, x1,y1 be Element of S;

      set C1 = the carrier of S;

      the addF of S = (the addF of R || C1) by C0SP1:def 3;

      hence thesis by FUNCT_1: 49, ZFMISC_1: 87;

    end;

    theorem :: FIELD_6:16

    

     Th18: for S be Ring, R be Subring of S holds for x,y be Element of S, x1,y1 be Element of R st x = x1 & y = y1 holds (x * y) = (x1 * y1)

    proof

      let R be Ring, S be Subring of R;

      let x,y be Element of R, x1,y1 be Element of S;

      set C1 = the carrier of S;

      the multF of S = (the multF of R || C1) by C0SP1:def 3;

      hence thesis by FUNCT_1: 49, ZFMISC_1: 87;

    end;

    theorem :: FIELD_6:17

    

     Th19: for S be Ring, R be Subring of S holds for x be Element of S, x1 be Element of R st x = x1 holds ( - x) = ( - x1)

    proof

      let R be Ring, S be Subring of R;

      let x be Element of R, x1 be Element of S;

      set C = the carrier of R, C1 = the carrier of S, a = ( - x1);

      assume

       A1: x = x1;

      C1 c= C by C0SP1:def 3;

      then

      reconsider g = a as Element of R;

      (x + g) = (x1 + a) by A1, Th17

      .= ( 0. S) by VECTSP_1: 19

      .= ( 0. R) by C0SP1:def 3;

      hence thesis by VECTSP_1: 16;

    end;

    theorem :: FIELD_6:18

    

     Th19f: for E be Field, F be Subfield of E holds for x be non zero Element of E, x1 be Element of F st x = x1 holds (x " ) = (x1 " )

    proof

      let R be Field, S be Subfield of R;

      let x be non zero Element of R, x1 be Element of S;

      set C = the carrier of R, C1 = the carrier of S, a = (x1 " );

      assume

       A1: x = x1;

      

       A2: x <> ( 0. R);

      then

       A3: x1 <> ( 0. S) by A1, EC_PF_1:def 1;

      C1 c= C by EC_PF_1:def 1;

      then

      reconsider g = a as Element of R;

      R is FieldExtension of S by FIELD_4: 7;

      then S is Subring of R by FIELD_4:def 1;

      

      then (g * x) = (a * x1) by A1, Th18

      .= ( 1. S) by A3, VECTSP_1:def 10

      .= ( 1. R) by EC_PF_1:def 1;

      hence thesis by A2, VECTSP_1:def 10;

    end;

    theorem :: FIELD_6:19

    

     pr5: for S be Ring, R be Subring of S holds for x be Element of S, x1 be Element of R holds for n be Element of NAT st x = x1 holds (x |^ n) = (x1 |^ n)

    proof

      let S be Ring, R be Subring of S;

      let x be Element of S, x1 be Element of R;

      let n be Element of NAT ;

      assume

       AS: x = x1;

      defpred P[ Nat] means for x be Element of S, x1 be Element of R st x = x1 holds (x |^ $1) = (x1 |^ $1);

      now

        let x be Element of S, x1 be Element of R;

        assume x = x1;

        

        thus (x |^ 0 ) = ( 1_ S) by BINOM: 8

        .= ( 1_ R) by C0SP1:def 3

        .= (x1 |^ 0 ) by BINOM: 8;

      end;

      then

       IA: P[ 0 ];

      

       A: the multF of R = (the multF of S || the carrier of R) by C0SP1:def 3;

       IS:

      now

        let k be Nat;

        assume

         IV: P[k];

        now

          let x be Element of S, x1 be Element of R;

          assume

           AS: x = x1;

          then

           C: (x |^ k) = (x1 |^ k) by IV;

          

           B: [(x1 |^ k), x1] in [:the carrier of R, the carrier of R:] by ZFMISC_1:def 2;

          

          thus (x |^ (k + 1)) = ((x |^ k) * (x |^ 1)) by BINOM: 10

          .= ((x |^ k) * x) by BINOM: 8

          .= ((x1 |^ k) * x1) by AS, A, B, C, FUNCT_1: 49

          .= ((x1 |^ k) * (x1 |^ 1)) by BINOM: 8

          .= (x1 |^ (k + 1)) by BINOM: 10;

        end;

        hence P[(k + 1)];

      end;

      for k be Nat holds P[k] from NAT_1:sch 2( IA, IS);

      hence thesis by AS;

    end;

    theorem :: FIELD_6:20

    

     pr20: for S be Ring, R be Subring of S holds for x1,x2 be Element of S, y1,y2 be Element of R st x1 = y1 & x2 = y2 holds <%x1, x2%> = <%y1, y2%>

    proof

      let S be Ring, R be Subring of S;

      let x1,x2 be Element of S, y1,y2 be Element of R;

      assume

       AS: x1 = y1 & x2 = y2;

      set p = <%x1, x2%>, q = <%y1, y2%>;

      now

        let n be Element of NAT ;

        per cases ;

          suppose

           A: n is trivial;

          per cases by A, NAT_2:def 1;

            suppose

             B: n = 0 ;

            

            hence (p . n) = y1 by AS, POLYNOM5: 38

            .= (q . n) by B, POLYNOM5: 38;

          end;

            suppose

             B: n = 1;

            

            hence (p . n) = y2 by AS, POLYNOM5: 38

            .= (q . n) by B, POLYNOM5: 38;

          end;

        end;

          suppose

           A: n is non trivial;

          

          hence (p . n) = ( 0. S) by NAT_2: 29, POLYNOM5: 38

          .= ( 0. R) by C0SP1:def 3

          .= (q . n) by A, NAT_2: 29, POLYNOM5: 38;

        end;

      end;

      hence thesis;

    end;

    theorem :: FIELD_6:21

    

     helpp: for R be comRing, S be comRingExtension of R holds for x1,x2 be Element of S, y1,y2 be Element of R holds for n be Element of NAT st x1 = y1 & x2 = y2 holds ( <%x1, x2%> `^ n) = ( <%y1, y2%> `^ n)

    proof

      let R be comRing, S be comRingExtension of R;

      let x1,x2 be Element of S, y1,y2 be Element of R;

      let n be Element of NAT ;

      assume

       A: x1 = y1 & x2 = y2;

      defpred P[ Nat] means ( <%x1, x2%> `^ $1) = ( <%y1, y2%> `^ $1);

      ( <%x1, x2%> `^ 0 ) = ( 1_. S) by POLYNOM5: 15

      .= ( 1_. R) by FIELD_4: 14

      .= ( <%y1, y2%> `^ 0 ) by POLYNOM5: 15;

      then

       IA: P[ 0 ];

      reconsider qS = <%x1, x2%> as Element of the carrier of ( Polynom-Ring S) by POLYNOM3:def 10;

      reconsider qR = <%y1, y2%> as Element of the carrier of ( Polynom-Ring R) by POLYNOM3:def 10;

      R is Subring of S by FIELD_4:def 1;

      then

       E: <%x1, x2%> = <%y1, y2%> by A, pr20;

       IS:

      now

        let k be Nat;

        assume

         IV: P[k];

        

         B: ( <%x1, x2%> `^ (k + 1)) = (( power ( Polynom-Ring S)) . ( <%x1, x2%>,(k + 1))) by POLYNOM5:def 3

        .= ((( power ( Polynom-Ring S)) . (qS,k)) * qS) by GROUP_1:def 7;

        

         C: ( <%y1, y2%> `^ (k + 1)) = (( power ( Polynom-Ring R)) . ( <%y1, y2%>,(k + 1))) by POLYNOM5:def 3

        .= ((( power ( Polynom-Ring R)) . (qR,k)) * qR) by GROUP_1:def 7;

        

         D: (( power ( Polynom-Ring R)) . (qR,k)) = ( <%x1, x2%> `^ k) by IV, POLYNOM5:def 3

        .= (( power ( Polynom-Ring S)) . (qS,k)) by POLYNOM5:def 3;

        reconsider u = (( power ( Polynom-Ring R)) . (qR,k)) as Polynomial of R by POLYNOM3:def 10;

        reconsider v = (( power ( Polynom-Ring S)) . (qS,k)) as Polynomial of S by POLYNOM3:def 10;

        ((( power ( Polynom-Ring R)) . (qR,k)) * qR) = (u *' <%y1, y2%>) by POLYNOM3:def 10

        .= (v *' <%x1, x2%>) by D, E, FIELD_4: 17

        .= ((( power ( Polynom-Ring S)) . (qS,k)) * qS) by POLYNOM3:def 10;

        hence P[(k + 1)] by B, C;

      end;

      for k be Nat holds P[k] from NAT_1:sch 2( IA, IS);

      hence thesis;

    end;

    theorem :: FIELD_6:22

    

     help3: for R be domRing, S be domRingExtension of R holds for n be non zero Element of NAT holds for a be Element of S holds ( Ext_eval (( <%( 0. R), ( 1. R)%> `^ n),a)) = (a |^ n)

    proof

      let R be domRing, S be domRingExtension of R;

      let n be non zero Element of NAT ;

      let a be Element of S;

      reconsider q = ( <%( 0. S), ( 1. S)%> `^ n) as Element of the carrier of ( Polynom-Ring S) by POLYNOM3:def 10;

      reconsider p = ( <%( 0. R), ( 1. R)%> `^ n) as Element of the carrier of ( Polynom-Ring R) by POLYNOM3:def 10;

      R is Subring of S by FIELD_4:def 1;

      then ( 0. R) = ( 0. S) & ( 1. R) = ( 1. S) by C0SP1:def 3;

      then ( <%( 0. R), ( 1. R)%> `^ n) = ( <%( 0. S), ( 1. S)%> `^ n) by helpp;

      

      then ( Ext_eval (p,a)) = ( eval (q,a)) by FIELD_4: 26

      .= (a |^ n) by help3a;

      hence thesis;

    end;

    

     Th28: for L be non empty ZeroStr, a be Element of L holds ((a | L) . 0 ) = a & for n be Nat st n <> 0 holds ((a | L) . n) = ( 0. L)

    proof

      let L be non empty ZeroStr, a be Element of L;

      

       A: (a | L) = (( 0_. L) +* ( 0 ,a)) by RING_4:def 5;

       0 in ( dom ( 0_. L));

      hence ((a | L) . 0 ) = a by A, FUNCT_7: 31;

      let n be Nat;

      assume n <> 0 ;

      

      hence ((a | L) . n) = (( 0_. L) . n) by A, FUNCT_7: 32

      .= ( 0. L) by ORDINAL1:def 12, FUNCOP_1: 7;

    end;

    theorem :: FIELD_6:23

    

     constpol: for R be Ring, S be RingExtension of R holds for a be Element of R, b be Element of S st a = b holds (a | R) = (b | S)

    proof

      let F be Ring, E be RingExtension of F;

      let a be Element of F, b be Element of E;

      assume

       AS: a = b;

      set ap = (a | F), bp = (b | E);

      

       X: F is Subring of E by FIELD_4:def 1;

      now

        let n be Element of NAT ;

        per cases ;

          suppose

           A: n = 0 ;

          

          hence (ap . n) = b by AS, Th28

          .= (bp . n) by A, Th28;

        end;

          suppose

           A: n <> 0 ;

          

          hence (ap . n) = ( 0. F) by Th28

          .= ( 0. E) by X, C0SP1:def 3

          .= (bp . n) by A, Th28;

        end;

      end;

      hence thesis;

    end;

    theorem :: FIELD_6:24

    

     pr0: for F be Field, E be FieldExtension of F holds for p be Element of the carrier of ( Polynom-Ring F) holds for q be Element of the carrier of ( Polynom-Ring E) st p = q holds ( NormPolynomial p) = ( NormPolynomial q)

    proof

      let F be Field, E be FieldExtension of F;

      let p be Element of the carrier of ( Polynom-Ring F);

      let q be Element of the carrier of ( Polynom-Ring E);

      assume

       AS: p = q;

      set np = ( NormPolynomial p), nq = ( NormPolynomial q);

      

       B1: F is Subfield of E by FIELD_4: 7;

      

       B: F is Subring of E by FIELD_4:def 1;

      per cases ;

        suppose q is zero;

        then

         B: q = ( 0_. E) by UPROOTS:def 5;

        

        then

         A: nq = ( 0_. E) by RING_4: 22

        .= ( 0_. F) by FIELD_4: 12;

        p = ( 0_. F) by AS, B, FIELD_4: 12;

        hence thesis by A, RING_4: 22;

      end;

        suppose q is non zero;

        then ( LC q) is non zero;

        then

         A1: (q . (( len q) -' 1)) is non zero by RATFUNC1:def 6;

        (( len p) - 1) = ( deg p) by HURWITZ:def 2

        .= ( deg q) by AS, FIELD_4: 20

        .= (( len q) - 1) by HURWITZ:def 2;

        then

         A: ((p . (( len p) -' 1)) " ) = ((q . (( len q) -' 1)) " ) by AS, A1, B1, Th19f;

        now

          let n be Element of NAT ;

          

          thus (np . n) = ((p . n) / (p . (( len p) -' 1))) by POLYNOM5:def 11

          .= ((q . n) / (q . (( len q) -' 1))) by B, A, AS, Th18

          .= (nq . n) by POLYNOM5:def 11;

        end;

        hence thesis;

      end;

    end;

    theorem :: FIELD_6:25

    

     pr1: for F be Field, E be FieldExtension of F holds for p be Element of the carrier of ( Polynom-Ring F) holds for a be Element of E holds ( Ext_eval (p,a)) = ( 0. E) iff ( Ext_eval (( NormPolynomial p),a)) = ( 0. E)

    proof

      let F be Field, E be FieldExtension of F;

      let p be Element of the carrier of ( Polynom-Ring F);

      let a be Element of E;

      the carrier of ( Polynom-Ring F) c= the carrier of ( Polynom-Ring E) by FIELD_4: 10;

      then

      reconsider q = p as Element of the carrier of ( Polynom-Ring E);

      reconsider qa = q as Polynomial of E;

      reconsider ra = ( rpoly (1,a)) as Element of the carrier of ( Polynom-Ring E) by POLYNOM3:def 10;

       A:

      now

        assume ( Ext_eval (p,a)) = ( 0. E);

        then ( eval (qa,a)) = ( 0. E) by FIELD_4: 26;

        then ra divides ( NormPolynomial qa) by RING_4: 26, RING_5: 11;

        then ( eval (( NormPolynomial q),a)) = ( 0. E) by RING_5: 11;

        hence ( Ext_eval (( NormPolynomial p),a)) = ( 0. E) by pr0, FIELD_4: 26;

      end;

      now

        assume ( Ext_eval (( NormPolynomial p),a)) = ( 0. E);

        then ( eval (( NormPolynomial q),a)) = ( 0. E) by pr0, FIELD_4: 26;

        then ra divides ( NormPolynomial qa) by RING_5: 11;

        then ( eval (qa,a)) = ( 0. E) by RING_5: 11, RING_4: 26;

        hence ( Ext_eval (p,a)) = ( 0. E) by FIELD_4: 26;

      end;

      hence thesis by A;

    end;

    theorem :: FIELD_6:26

    

     exevalminus: for R be Ring, S be RingExtension of R holds for a be Element of S, p be Polynomial of R holds ( Ext_eval (( - p),a)) = ( - ( Ext_eval (p,a)))

    proof

      let R be Ring, S be RingExtension of R;

      let a be Element of S, p be Polynomial of R;

      consider G be FinSequence of S such that

       A: ( Ext_eval (p,a)) = ( Sum G) & ( len G) = ( len p) & for n be Element of NAT st n in ( dom G) holds (G . n) = (( In ((p . (n -' 1)),S)) * (( power S) . (a,(n -' 1)))) by ALGNUM_1:def 1;

      consider H be FinSequence of S such that

       B: ( Ext_eval (( - p),a)) = ( Sum H) & ( len H) = ( len ( - p)) & for n be Element of NAT st n in ( dom H) holds (H . n) = (( In ((( - p) . (n -' 1)),S)) * (( power S) . (a,(n -' 1)))) by ALGNUM_1:def 1;

      

       K: R is Subring of S by FIELD_4:def 1;

      then

       H: the carrier of R c= the carrier of S by C0SP1:def 3;

      

       C: ( len G) = ( len H) by A, B, POLYNOM4: 8;

      now

        let n be Nat, b be Element of S;

        assume

         D1: n in ( dom H) & b = (G . n);

        

         D2: ( dom H) = ( Seg ( len G)) by C, FINSEQ_1:def 3

        .= ( dom G) by FINSEQ_1:def 3;

        reconsider pn1 = (p . (n -' 1)), mpn1 = ( - (p . (n -' 1))) as Element of S by H;

        

        thus (H . n) = (( In ((( - p) . (n -' 1)),S)) * (( power S) . (a,(n -' 1)))) by B, D1

        .= (( In (( - (p . (n -' 1))),S)) * (( power S) . (a,(n -' 1)))) by BHSP_1: 44

        .= (mpn1 * (( power S) . (a,(n -' 1))))

        .= (( - pn1) * (( power S) . (a,(n -' 1)))) by K, Th19

        .= ( - (( In ((p . (n -' 1)),S)) * (( power S) . (a,(n -' 1))))) by VECTSP_1: 9

        .= ( - b) by D1, D2, A;

      end;

      hence thesis by A, B, POLYNOM4: 8, RLVECT_1: 40;

    end;

    theorem :: FIELD_6:27

    

     exevalminus2: for R be Ring, S be RingExtension of R holds for a be Element of S, p,q be Polynomial of R holds ( Ext_eval ((p - q),a)) = (( Ext_eval (p,a)) - ( Ext_eval (q,a)))

    proof

      let R be Ring, S be RingExtension of R;

      let a be Element of S, p,q be Polynomial of R;

      R is Subring of S by FIELD_4:def 1;

      

      hence ( Ext_eval ((p - q),a)) = (( Ext_eval (p,a)) + ( Ext_eval (( - q),a))) by ALGNUM_1: 15

      .= (( Ext_eval (p,a)) - ( Ext_eval (q,a))) by exevalminus;

    end;

    theorem :: FIELD_6:28

    

     exevalconst: for R be Ring, S be RingExtension of R holds for a be Element of S, p be constant Polynomial of R holds ( Ext_eval (p,a)) = ( LC p)

    proof

      let R be Ring, S be RingExtension of R;

      let a be Element of S, p be constant Polynomial of R;

      

       A: R is Subring of S by FIELD_4:def 1;

      per cases ;

        suppose

         A0: p = ( 0_. R);

        

        hence ( Ext_eval (p,a)) = ( 0. S) by ALGNUM_1: 13

        .= (p . (( len p) -' 1)) by A0, A, C0SP1:def 3

        .= ( LC p) by RATFUNC1:def 6;

      end;

        suppose

         A0: p <> ( 0_. R);

        the carrier of R c= the carrier of S by A, C0SP1:def 3;

        then

        reconsider p0 = (p . 0 ) as Element of S;

        consider F be FinSequence of S such that

         A1: ( Ext_eval (p,a)) = ( Sum F) and

         A2: ( len F) = ( len p) and

         A3: for n be Element of NAT st n in ( dom F) holds (F . n) = (( In ((p . (n -' 1)),S)) * (( power S) . (a,(n -' 1)))) by ALGNUM_1:def 1;

        reconsider degp = ( deg p) as Element of NAT by A0, FIELD_1: 1;

        

         A7: degp = 0 by RATFUNC1:def 2;

        

         A6: ( deg p) = (( len p) - 1) by HURWITZ:def 2;

        

        then

         A4: (F . 1) = (( In ((p . (1 -' 1)),S)) * (( power S) . (a,(1 -' 1)))) by A7, A2, A3, FINSEQ_3: 25

        .= (( In ((p . 0 ),S)) * (( power S) . (a,(1 -' 1)))) by XREAL_1: 232

        .= (p0 * (( power S) . (a, 0 ))) by XREAL_1: 232

        .= (p0 * ( 1_ S)) by GROUP_1:def 7

        .= p0;

        ( Sum F) = ( Sum <*p0*>) by A6, A7, A2, FINSEQ_1: 40, A4

        .= (p . (1 - 1)) by RLVECT_1: 44

        .= (p . (1 -' 1)) by XREAL_0:def 2

        .= ( LC p) by A6, A7, RATFUNC1:def 6;

        hence thesis by A1;

      end;

    end;

    theorem :: FIELD_6:29

    

     exevalLM: for R be non degenerated Ring, S be RingExtension of R holds for a,b be Element of S, p be non zero Polynomial of R st b = ( LC p) holds ( Ext_eval (( Leading-Monomial p),a)) = (b * (a |^ ( deg p)))

    proof

      let R be non degenerated Ring, S be RingExtension of R;

      let a,b be Element of S, p be non zero Polynomial of R;

      assume

       AS: b = ( LC p);

      

       H0: R is Subring of S by FIELD_4:def 1;

      

       H2: (p . (( len p) -' 1)) = ( LC p) by RATFUNC1:def 6;

      ( deg p) = (( len p) - 1) by HURWITZ:def 2;

      then

       H3: (( len p) -' 1) = ( deg p) by XREAL_0:def 2;

      

      thus ( Ext_eval (( Leading-Monomial p),a)) = (( In ((p . (( len p) -' 1)),S)) * (( power S) . (a,(( len p) -' 1)))) by H0, ALGNUM_1: 17

      .= (b * (a |^ ( deg p))) by AS, H2, H3, BINOM:def 2;

    end;

    begin

    definition

      let R be Ring, S be RingExtension of R;

      let T be Subset of S;

      :: FIELD_6:def3

      func carrierRA (T) -> non empty Subset of S equals { x where x be Element of S : for U be Subring of S st R is Subring of U & T is Subset of U holds x in U };

      coherence

      proof

        set M = { x where x be Element of S : for U be Subring of S st R is Subring of U & T is Subset of U holds x in U };

        now

          let U be Subring of S;

          assume R is Subring of U & T is Subset of U;

          ( 1. U) = ( 1. S) by C0SP1:def 3;

          hence ( 1. S) in U;

        end;

        then

         A: ( 1. S) in M;

        now

          let o be object;

          assume o in M;

          then

          consider x be Element of S such that

           H: o = x & for U be Subring of S st R is Subring of U & T is Subset of U holds x in U;

          thus o in the carrier of S by H;

        end;

        hence thesis by TARSKI:def 3, A;

      end;

    end

    definition

      let R be Ring, S be RingExtension of R;

      let T be Subset of S;

      :: FIELD_6:def4

      func RingAdjunction (R,T) -> strict doubleLoopStr means

      : dRA: the carrier of it = ( carrierRA T) & the addF of it = (the addF of S || ( carrierRA T)) & the multF of it = (the multF of S || ( carrierRA T)) & the OneF of it = ( 1. S) & the ZeroF of it = ( 0. S);

      existence

      proof

        set C = ( carrierRA T);

        set f = the addF of S;

        C is Preserv of f

        proof

          now

            let x be set;

            assume x in [:C, C:];

            then

            consider x1,x2 be object such that

             A1: x1 in C and

             A2: x2 in C and

             A3: x = [x1, x2] by ZFMISC_1:def 2;

            consider y1 be Element of S such that

             A4: x1 = y1 and

             A5: for U be Subring of S st R is Subring of U & T is Subset of U holds y1 in U by A1;

            consider y2 be Element of S such that

             A6: x2 = y2 and

             A7: for U be Subring of S st R is Subring of U & T is Subset of U holds y2 in U by A2;

            now

              let U be Subring of S;

              assume R is Subring of U & T is Subset of U;

              then y1 in U & y2 in U by A5, A7;

              then

              reconsider a1 = y1, a2 = y2 as Element of U;

              the addF of U = (f || the carrier of U) by C0SP1:def 3;

              then (the addF of U . (a1,a2)) = (f . (a1,a2)) by RING_3: 1;

              hence (f . (y1,y2)) in U;

            end;

            hence (f . x) in C by A3, A4, A6;

          end;

          hence thesis by REALSET1:def 1;

        end;

        then

        reconsider C as Preserv of the addF of S;

        set f = the multF of S;

        C is Preserv of f

        proof

          now

            let x be set;

            assume x in [:C, C:];

            then

            consider x1,x2 be object such that

             A1: x1 in C and

             A2: x2 in C and

             A3: x = [x1, x2] by ZFMISC_1:def 2;

            consider y1 be Element of S such that

             A4: x1 = y1 and

             A5: for U be Subring of S st R is Subring of U & T is Subset of U holds y1 in U by A1;

            consider y2 be Element of S such that

             A6: x2 = y2 and

             A7: for U be Subring of S st R is Subring of U & T is Subset of U holds y2 in U by A2;

            now

              let U be Subring of S;

              assume R is Subring of U & T is Subset of U;

              then y1 in U & y2 in U by A5, A7;

              then

              reconsider a1 = y1, a2 = y2 as Element of U;

              the multF of U = (f || the carrier of U) by C0SP1:def 3;

              then (the multF of U . (a1,a2)) = (f . (a1,a2)) by RING_3: 1;

              hence (f . (y1,y2)) in U;

            end;

            hence (f . x) in C by A3, A4, A6;

          end;

          hence thesis by REALSET1:def 1;

        end;

        then

        reconsider D = C as Preserv of the multF of S;

        reconsider m = (the multF of S || D) as BinOp of C;

        set o = ( 1. S), z = ( 0. S);

        ex x be Element of S st x = o & for U be Subring of S st R is Subring of U & T is Subset of U holds x in U

        proof

          take o;

          now

            let U be Subring of S;

            assume T is Subset of U;

            ( 1. U) = ( 1. S) by C0SP1:def 3;

            hence o in U;

          end;

          hence thesis;

        end;

        then o in C;

        then

        reconsider o as Element of C;

        ex x be Element of S st x = z & for U be Subring of S st R is Subring of U & T is Subset of U holds x in U

        proof

          take z;

          now

            let U be Subring of S;

            assume R is Subring of U & T is Subset of U;

            ( 0. U) = ( 0. S) by C0SP1:def 3;

            hence z in U;

          end;

          hence thesis;

        end;

        then z in C;

        then

        reconsider z as Element of C;

        take doubleLoopStr (# C, (the addF of S || C), m, o, z #);

        thus thesis;

      end;

      uniqueness ;

    end

    notation

      let R be Ring, S be RingExtension of R;

      let T be Subset of S;

      synonym RAdj (R,T) for RingAdjunction (R,T);

    end

    registration

      let R be Ring, S be RingExtension of R;

      let T be Subset of S;

      cluster ( RAdj (R,T)) -> non empty;

      coherence

      proof

        the carrier of ( RAdj (R,T)) = ( carrierRA T) by dRA;

        hence thesis;

      end;

    end

    registration

      let R be non degenerated Ring, S be RingExtension of R;

      let T be Subset of S;

      cluster ( RAdj (R,T)) -> non degenerated;

      coherence

      proof

        set RA = ( RAdj (R,T));

        ( 0. RA) = ( 0. S) & ( 1. RA) = ( 1. S) by dRA;

        hence ( 0. RA) <> ( 1. RA);

      end;

    end

    

     Lm10: for R be Ring, S be RingExtension of R, T be Subset of S holds for x be Element of ( RAdj (R,T)) holds x is Element of S

    proof

      let R be Ring, S be RingExtension of R, T be Subset of S;

      let x be Element of ( RAdj (R,T));

      

       A1: the carrier of ( RAdj (R,T)) = ( carrierRA T) by dRA;

      x in the carrier of ( RAdj (R,T));

      hence thesis by A1;

    end;

    

     Lm11: for R be Ring, S be RingExtension of R, T be Subset of S holds for a,b be Element of S holds for x,y be Element of ( RAdj (R,T)) st a = x & b = y holds (a + b) = (x + y)

    proof

      let R be Ring, S be RingExtension of R, T be Subset of S;

      let a,b be Element of S;

      let x,y be Element of ( RAdj (R,T)) such that

       A1: a = x & b = y;

      the carrier of ( RAdj (R,T)) = ( carrierRA T) by dRA;

      

      hence (a + b) = ((the addF of S || ( carrierRA T)) . (x,y)) by A1, RING_3: 1

      .= (x + y) by dRA;

    end;

    

     Lm12: for R be Ring, S be RingExtension of R, T be Subset of S holds for a,b be Element of S holds for x,y be Element of ( RAdj (R,T)) st a = x & b = y holds (a * b) = (x * y)

    proof

      let R be Ring, S be RingExtension of R, T be Subset of S;

      let a,b be Element of S;

      let x,y be Element of ( RAdj (R,T)) such that

       A1: a = x & b = y;

      the carrier of ( RAdj (R,T)) = ( carrierRA T) by dRA;

      

      hence (a * b) = ((the multF of S || ( carrierRA T)) . (x,y)) by A1, RING_3: 1

      .= (x * y) by dRA;

    end;

    registration

      let R be Ring, S be RingExtension of R;

      let T be Subset of S;

      cluster ( RAdj (R,T)) -> Abelian add-associative right_zeroed right_complementable;

      coherence

      proof

        set P = ( RAdj (R,T));

        

         A1: ( 0. P) = ( 0. S) by dRA;

        

         A2: the carrier of ( RAdj (R,T)) = ( carrierRA T) by dRA;

        hereby

          let x,y be Element of P;

          reconsider a = x, b = y as Element of S by Lm10;

          

          thus (x + y) = (a + b) by Lm11

          .= (y + x) by Lm11;

        end;

        hereby

          let x,y,z be Element of P;

          reconsider a = x, b = y, c = z as Element of S by Lm10;

          

           A3: (y + z) = (b + c) by Lm11;

          (x + y) = (a + b) by Lm11;

          

          hence ((x + y) + z) = ((a + b) + c) by Lm11

          .= (a + (b + c)) by RLVECT_1:def 3

          .= (x + (y + z)) by A3, Lm11;

        end;

        hereby

          let x be Element of P;

          reconsider a = x as Element of S by Lm10;

          

          thus (x + ( 0. P)) = (a + ( 0. S)) by A1, Lm11

          .= x;

        end;

        let x be Element of P;

        reconsider a = x as Element of S by Lm10;

        x in ( carrierRA T) by A2;

        then

        consider x1 be Element of S such that

         A4: x = x1 and

         A5: for U be Subring of S st R is Subring of U & T is Subset of U holds x1 in U;

        now

          let U be Subring of S;

          assume R is Subring of U & T is Subset of U;

          then x1 in U by A5;

          then

          reconsider t = x1 as Element of U;

          ( - t) = ( - x1) by Th19;

          hence ( - x1) in U;

        end;

        then ( - x1) in ( carrierRA T);

        then

        reconsider y = ( - x1) as Element of P by dRA;

        take y;

        

        thus (x + y) = (a + ( - x1)) by Lm11

        .= ( 0. P) by A1, A4, RLVECT_1: 5;

      end;

    end

    registration

      let R be comRing, S be comRingExtension of R;

      let T be Subset of S;

      cluster ( RAdj (R,T)) -> commutative;

      coherence

      proof

        now

          let x,y be Element of ( RAdj (R,T));

          reconsider a = x, b = y as Element of S by Lm10;

          

          thus (x * y) = (a * b) by Lm12

          .= (b * a) by GROUP_1:def 12

          .= (y * x) by Lm12;

        end;

        hence thesis;

      end;

    end

    registration

      let R be Ring, S be RingExtension of R;

      let T be Subset of S;

      cluster ( RAdj (R,T)) -> associative well-unital distributive;

      coherence

      proof

        set P = ( RAdj (R,T));

        

         A1: ( 1. P) = ( 1. S) by dRA;

        now

          let x,y,z be Element of P;

          reconsider a = x, b = y, c = z as Element of S by Lm10;

          

           A3: (y * z) = (b * c) by Lm12;

          (x * y) = (a * b) by Lm12;

          

          hence ((x * y) * z) = ((a * b) * c) by Lm12

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

          .= (x * (y * z)) by A3, Lm12;

        end;

        hence P is associative;

        now

          let x be Element of P;

          reconsider a = x as Element of S by Lm10;

          

          thus (x * ( 1. P)) = (a * ( 1. S)) by A1, Lm12

          .= x;

          

          thus (( 1. P) * x) = (( 1. S) * a) by A1, Lm12

          .= x;

        end;

        hence P is well-unital;

        now

          let x,y,z be Element of P;

          reconsider a = x, b = y, c = z as Element of S by Lm10;

          

           A4: (a * b) = (x * y) & (a * c) = (x * z) by Lm12;

          

           A6: (b * a) = (y * x) & (c * a) = (z * x) by Lm12;

          

           A5: (y + z) = (b + c) by Lm11;

          

          hence (x * (y + z)) = (a * (b + c)) by Lm12

          .= ((a * b) + (a * c)) by VECTSP_1:def 7

          .= ((x * y) + (x * z)) by A4, Lm11;

          

          thus ((y + z) * x) = ((b + c) * a) by A5, Lm12

          .= ((b * a) + (c * a)) by VECTSP_1:def 7

          .= ((y * x) + (z * x)) by A6, Lm11;

        end;

        hence thesis;

      end;

    end

    theorem :: FIELD_6:30

    

     RAt: for R be Ring, S be RingExtension of R holds for T be Subset of S holds T is Subset of ( RAdj (R,T))

    proof

      let R be Ring, S be RingExtension of R;

      let T be Subset of S;

      set P = ( RAdj (R,T));

      now

        let o be object;

        assume

         A: o in T;

        then

        reconsider a = o as Element of S;

        for U be Subring of S st R is Subring of U & T is Subset of U holds o in U by A;

        then a in ( carrierRA T);

        hence o in the carrier of P by dRA;

      end;

      hence thesis by TARSKI:def 3;

    end;

    theorem :: FIELD_6:31

    

     RAsub: for R be Ring, S be RingExtension of R holds for T be Subset of S holds R is Subring of ( RAdj (R,T))

    proof

      let R be Ring, S be RingExtension of R;

      let T be Subset of S;

      set P = ( RAdj (R,T));

      

       X: R is Subring of S by FIELD_4:def 1;

      

       A: ( 1. P) = ( 1. S) by dRA

      .= ( 1. R) by X, C0SP1:def 3;

      

       B: ( 0. P) = ( 0. S) by dRA

      .= ( 0. R) by X, C0SP1:def 3;

      

       C: the carrier of R c= the carrier of P

      proof

        now

          let o be object;

          assume

           C1: o in the carrier of R;

          the carrier of R c= the carrier of S by X, C0SP1:def 3;

          then

          reconsider a = o as Element of S by C1;

          now

            let U be Subring of S;

            assume R is Subring of U & T is Subset of U;

            then the carrier of R c= the carrier of U by C0SP1:def 3;

            hence o in U by C1;

          end;

          then a in ( carrierRA T);

          hence o in the carrier of P by dRA;

        end;

        hence thesis;

      end;

      then

       Y: [:the carrier of R, the carrier of R:] c= [:the carrier of P, the carrier of P:] by ZFMISC_1: 96;

      

       D: (the addF of P || the carrier of R) = ((the addF of S || ( carrierRA T)) || the carrier of R) by dRA

      .= ((the addF of S || the carrier of P) || the carrier of R) by dRA

      .= (the addF of S || the carrier of R) by Y, FUNCT_1: 51

      .= the addF of R by X, C0SP1:def 3;

      (the multF of P || the carrier of R) = ((the multF of S || ( carrierRA T)) || the carrier of R) by dRA

      .= ((the multF of S || the carrier of P) || the carrier of R) by dRA

      .= (the multF of S || the carrier of R) by Y, FUNCT_1: 51

      .= the multF of R by X, C0SP1:def 3;

      hence thesis by A, B, C, D, C0SP1:def 3;

    end;

    theorem :: FIELD_6:32

    

     RAsub2: for R be Ring, S be RingExtension of R, T be Subset of S holds for U be Subring of S st R is Subring of U & T is Subset of U holds ( RAdj (R,T)) is Subring of U

    proof

      let R be Ring, S be RingExtension of R;

      let T be Subset of S;

      let U be Subring of S;

      assume

       AS: R is Subring of U & T is Subset of U;

      set P = ( RAdj (R,T));

      

       A: ( 1. P) = ( 1. S) by dRA

      .= ( 1. U) by C0SP1:def 3;

      

       B: ( 0. P) = ( 0. S) by dRA

      .= ( 0. U) by C0SP1:def 3;

      

       C: the carrier of P c= the carrier of U

      proof

        now

          let o be object;

          assume o in the carrier of P;

          then o in ( carrierRA T) by dRA;

          then

          consider x be Element of S such that

           C2: x = o & for U be Subring of S st R is Subring of U & T is Subset of U holds x in U;

          x in U by C2, AS;

          hence o in the carrier of U by C2;

        end;

        hence thesis;

      end;

      then

       Y: [:the carrier of P, the carrier of P:] c= [:the carrier of U, the carrier of U:] by ZFMISC_1: 96;

      

       D: (the addF of U || the carrier of P) = ((the addF of S || the carrier of U) || the carrier of P) by C0SP1:def 3

      .= (the addF of S || the carrier of P) by Y, FUNCT_1: 51

      .= (the addF of S || ( carrierRA T)) by dRA

      .= the addF of P by dRA;

      (the multF of U || the carrier of P) = ((the multF of S || the carrier of U) || the carrier of P) by C0SP1:def 3

      .= (the multF of S || the carrier of P) by Y, FUNCT_1: 51

      .= (the multF of S || ( carrierRA T)) by dRA

      .= the multF of P by dRA;

      hence thesis by A, B, C, D, C0SP1:def 3;

    end;

    theorem :: FIELD_6:33

    for R be strict Ring, S be RingExtension of R, T be Subset of S holds ( RAdj (R,T)) = R iff T is Subset of R

    proof

      let R be strict Ring, S be RingExtension of R;

      let T be Subset of S;

      set P = ( RAdj (R,T));

      

       X: R is Subring of R & R is Subring of S by FIELD_4:def 1, LIOUVIL2: 18;

       Z:

      now

        let o be object;

        assume

         C1: o in the carrier of R;

        the carrier of R c= the carrier of S by X, C0SP1:def 3;

        then

        reconsider a = o as Element of S by C1;

        now

          let U be Subring of S;

          assume R is Subring of U & T is Subset of U;

          then the carrier of R c= the carrier of U by C0SP1:def 3;

          hence o in U by C1;

        end;

        then a in ( carrierRA T);

        hence o in the carrier of P by dRA;

      end;

      now

        assume

         B0: T is Subset of R;

         B5:

        now

          let o be object;

          assume o in the carrier of P;

          then o in ( carrierRA T) by dRA;

          then

          consider x be Element of S such that

           B1: x = o & for U be Subring of S st R is Subring of U & T is Subset of U holds x in U;

          x in R by X, B0, B1;

          hence o in the carrier of R by B1;

        end;

        then

         B1: the carrier of R = the carrier of P by Z, TARSKI: 2;

        

         B2: ( 1. P) = ( 1. S) by dRA

        .= ( 1. R) by X, C0SP1:def 3;

        

         B3: ( 0. P) = ( 0. S) by dRA

        .= ( 0. R) by X, C0SP1:def 3;

        

         B4: the addF of P = (the addF of S || ( carrierRA T)) by dRA

        .= (the addF of S || the carrier of R) by B1, dRA

        .= the addF of R by X, C0SP1:def 3;

        the multF of P = (the multF of S || ( carrierRA T)) by dRA

        .= (the multF of S || the carrier of R) by B1, dRA

        .= the multF of R by X, C0SP1:def 3;

        hence ( RAdj (R,T)) = R by Z, TARSKI: 2, B5, B2, B3, B4;

      end;

      hence thesis by RAt;

    end;

    definition

      let R be Ring, S be RingExtension of R;

      let T be Subset of S;

      :: original: RAdj

      redefine

      func RAdj (R,T) -> strict Subring of S ;

      coherence

      proof

        R is Subring of S & S is Subring of S by LIOUVIL2: 18, FIELD_4:def 1;

        hence thesis by RAsub2;

      end;

    end

    registration

      let R be Ring, S be RingExtension of R;

      let T be Subset of S;

      cluster ( RAdj (R,T)) -> R -extending;

      coherence

      proof

        R is Subring of ( RAdj (R,T)) by RAsub;

        hence thesis by FIELD_4:def 1;

      end;

    end

    registration

      let F be Field, R be RingExtension of F;

      let T be Subset of R;

      cluster ( RAdj (F,T)) -> field-containing;

      coherence

      proof

        ex E be Field st E is Subring of ( RAdj (F,T))

        proof

          take F;

          thus thesis by RAsub;

        end;

        hence thesis;

      end;

    end

    theorem :: FIELD_6:34

    for F be Field, R be RingExtension of F holds for T be Subset of R holds F is Subfield of ( RAdj (F,T))

    proof

      let F be Field, R be RingExtension of F, T be Subset of R;

      F is Subring of ( RAdj (F,T)) by RAsub;

      hence thesis by defsubfr;

    end;

    definition

      let F be Field, E be FieldExtension of F;

      let T be Subset of E;

      :: FIELD_6:def5

      func carrierFA (T) -> non empty Subset of E equals { x where x be Element of E : for U be Subfield of E st F is Subfield of U & T is Subset of U holds x in U };

      coherence

      proof

        set M = { x where x be Element of E : for U be Subfield of E st F is Subfield of U & T is Subset of U holds x in U };

        now

          let U be Subfield of E;

          assume F is Subfield of U & T is Subset of U;

          ( 1. U) = ( 1. E) by EC_PF_1:def 1;

          hence ( 1. E) in U;

        end;

        then

         A: ( 1. E) in M;

        now

          let o be object;

          assume o in M;

          then

          consider x be Element of E such that

           H: o = x & for U be Subfield of E st F is Subfield of U & T is Subset of U holds x in U;

          thus o in the carrier of E by H;

        end;

        hence thesis by TARSKI:def 3, A;

      end;

    end

    definition

      let F be Field, E be FieldExtension of F;

      let T be Subset of E;

      :: FIELD_6:def6

      func FieldAdjunction (F,T) -> strict doubleLoopStr means

      : dFA: the carrier of it = ( carrierFA T) & the addF of it = (the addF of E || ( carrierFA T)) & the multF of it = (the multF of E || ( carrierFA T)) & the OneF of it = ( 1. E) & the ZeroF of it = ( 0. E);

      existence

      proof

        set C = ( carrierFA T);

        set f = the addF of E;

        C is Preserv of f

        proof

          now

            let x be set;

            assume x in [:C, C:];

            then

            consider x1,x2 be object such that

             A1: x1 in C and

             A2: x2 in C and

             A3: x = [x1, x2] by ZFMISC_1:def 2;

            consider y1 be Element of E such that

             A4: x1 = y1 and

             A5: for U be Subfield of E st F is Subfield of U & T is Subset of U holds y1 in U by A1;

            consider y2 be Element of E such that

             A6: x2 = y2 and

             A7: for U be Subfield of E st F is Subfield of U & T is Subset of U holds y2 in U by A2;

            now

              let U be Subfield of E;

              assume F is Subfield of U & T is Subset of U;

              then y1 in U & y2 in U by A5, A7;

              then

              reconsider a1 = y1, a2 = y2 as Element of U;

              the addF of U = (f || the carrier of U) by EC_PF_1:def 1;

              then (the addF of U . (a1,a2)) = (f . (a1,a2)) by RING_3: 1;

              hence (f . (y1,y2)) in U;

            end;

            hence (f . x) in C by A3, A4, A6;

          end;

          hence thesis by REALSET1:def 1;

        end;

        then

        reconsider C as Preserv of the addF of E;

        set f = the multF of E;

        C is Preserv of f

        proof

          now

            let x be set;

            assume x in [:C, C:];

            then

            consider x1,x2 be object such that

             A1: x1 in C and

             A2: x2 in C and

             A3: x = [x1, x2] by ZFMISC_1:def 2;

            consider y1 be Element of E such that

             A4: x1 = y1 and

             A5: for U be Subfield of E st F is Subfield of U & T is Subset of U holds y1 in U by A1;

            consider y2 be Element of E such that

             A6: x2 = y2 and

             A7: for U be Subfield of E st F is Subfield of U & T is Subset of U holds y2 in U by A2;

            now

              let U be Subfield of E;

              assume F is Subfield of U & T is Subset of U;

              then y1 in U & y2 in U by A5, A7;

              then

              reconsider a1 = y1, a2 = y2 as Element of U;

              the multF of U = (f || the carrier of U) by EC_PF_1:def 1;

              then (the multF of U . (a1,a2)) = (f . (a1,a2)) by RING_3: 1;

              hence (f . (y1,y2)) in U;

            end;

            hence (f . x) in C by A3, A4, A6;

          end;

          hence thesis by REALSET1:def 1;

        end;

        then

        reconsider D = C as Preserv of the multF of E;

        reconsider m = (the multF of E || D) as BinOp of C;

        set o = ( 1. E), z = ( 0. E);

        ex x be Element of E st x = o & for U be Subfield of E st F is Subfield of U & T is Subset of U holds x in U

        proof

          take o;

          now

            let U be Subfield of E;

            assume T is Subset of U;

            ( 1. U) = ( 1. E) by EC_PF_1:def 1;

            hence o in U;

          end;

          hence thesis;

        end;

        then o in C;

        then

        reconsider o as Element of C;

        ex x be Element of E st x = z & for U be Subfield of E st F is Subfield of U & T is Subset of U holds x in U

        proof

          take z;

          now

            let U be Subfield of E;

            assume F is Subfield of U & T is Subset of U;

            ( 0. U) = ( 0. E) by EC_PF_1:def 1;

            hence z in U;

          end;

          hence thesis;

        end;

        then z in C;

        then

        reconsider z as Element of C;

        take doubleLoopStr (# C, (the addF of E || C), m, o, z #);

        thus thesis;

      end;

      uniqueness ;

    end

    notation

      let F be Field, E be FieldExtension of F;

      let T be Subset of E;

      synonym FAdj (F,T) for FieldAdjunction (F,T);

    end

    registration

      let F be Field, E be FieldExtension of F;

      let T be Subset of E;

      cluster ( FAdj (F,T)) -> non degenerated;

      coherence

      proof

        set FA = ( FAdj (F,T));

        ( 0. FA) = ( 0. E) & ( 1. FA) = ( 1. E) by dFA;

        hence ( 0. FA) <> ( 1. FA);

      end;

    end

    

     Lm10f: for R be Field, S be FieldExtension of R, T be Subset of S holds for x be Element of ( FAdj (R,T)) holds x is Element of S

    proof

      let R be Field, S be FieldExtension of R, T be Subset of S;

      let x be Element of ( FAdj (R,T));

      

       A1: the carrier of ( FAdj (R,T)) = ( carrierFA T) by dFA;

      x in the carrier of ( FAdj (R,T));

      hence thesis by A1;

    end;

    

     Lm11f: for R be Field, S be FieldExtension of R, T be Subset of S holds for a,b be Element of S holds for x,y be Element of ( FAdj (R,T)) st a = x & b = y holds (a + b) = (x + y)

    proof

      let R be Field, S be FieldExtension of R, T be Subset of S;

      let a,b be Element of S;

      let x,y be Element of ( FAdj (R,T)) such that

       A1: a = x & b = y;

      the carrier of ( FAdj (R,T)) = ( carrierFA T) by dFA;

      

      hence (a + b) = ((the addF of S || ( carrierFA T)) . (x,y)) by A1, RING_3: 1

      .= (x + y) by dFA;

    end;

    

     Lm12f: for R be Field, S be FieldExtension of R, T be Subset of S holds for a,b be Element of S holds for x,y be Element of ( FAdj (R,T)) st a = x & b = y holds (a * b) = (x * y)

    proof

      let R be Field, S be FieldExtension of R, T be Subset of S;

      let a,b be Element of S;

      let x,y be Element of ( FAdj (R,T)) such that

       A1: a = x & b = y;

      the carrier of ( FAdj (R,T)) = ( carrierFA T) by dFA;

      

      hence (a * b) = ((the multF of S || ( carrierFA T)) . (x,y)) by A1, RING_3: 1

      .= (x * y) by dFA;

    end;

    registration

      let F be Field, E be FieldExtension of F;

      let T be Subset of E;

      cluster ( FAdj (F,T)) -> Abelian add-associative right_zeroed right_complementable;

      coherence

      proof

        set P = ( FAdj (F,T));

        

         A1: ( 0. P) = ( 0. E) by dFA;

        

         A2: the carrier of ( FAdj (F,T)) = ( carrierFA T) by dFA;

        hereby

          let x,y be Element of P;

          reconsider a = x, b = y as Element of E by Lm10f;

          

          thus (x + y) = (a + b) by Lm11f

          .= (y + x) by Lm11f;

        end;

        hereby

          let x,y,z be Element of P;

          reconsider a = x, b = y, c = z as Element of E by Lm10f;

          

           A3: (y + z) = (b + c) by Lm11f;

          (x + y) = (a + b) by Lm11f;

          

          hence ((x + y) + z) = ((a + b) + c) by Lm11f

          .= (a + (b + c)) by RLVECT_1:def 3

          .= (x + (y + z)) by A3, Lm11f;

        end;

        hereby

          let x be Element of P;

          reconsider a = x as Element of E by Lm10f;

          

          thus (x + ( 0. P)) = (a + ( 0. E)) by A1, Lm11f

          .= x;

        end;

        let x be Element of P;

        reconsider a = x as Element of E by Lm10f;

        x in ( carrierFA T) by A2;

        then

        consider x1 be Element of E such that

         A4: x = x1 and

         A5: for U be Subfield of E st F is Subfield of U & T is Subset of U holds x1 in U;

        now

          let U be Subfield of E;

          assume F is Subfield of U & T is Subset of U;

          then x1 in U by A5;

          then

          reconsider t = x1 as Element of U;

          ( - t) = ( - x1) by GAUSSINT: 19;

          hence ( - x1) in U;

        end;

        then ( - x1) in ( carrierFA T);

        then

        reconsider y = ( - x1) as Element of P by dFA;

        take y;

        

        thus (x + y) = (a + ( - x1)) by Lm11f

        .= ( 0. P) by A1, A4, RLVECT_1: 5;

      end;

    end

    registration

      let F be Field, E be FieldExtension of F;

      let T be Subset of E;

      cluster ( FieldAdjunction (F,T)) -> commutative associative well-unital distributive almost_left_invertible;

      coherence

      proof

        set P = ( FAdj (F,T));

        

         A1: ( 1. P) = ( 1. E) by dFA;

        

         A2: ( 0. P) = ( 0. E) by dFA;

        now

          let x,y be Element of P;

          reconsider a = x, b = y as Element of E by Lm10f;

          

          thus (x * y) = (a * b) by Lm12f

          .= (b * a) by GROUP_1:def 12

          .= (y * x) by Lm12f;

        end;

        hence P is commutative;

        now

          let x,y,z be Element of P;

          reconsider a = x, b = y, c = z as Element of E by Lm10f;

          

           A3: (y * z) = (b * c) by Lm12f;

          (x * y) = (a * b) by Lm12f;

          

          hence ((x * y) * z) = ((a * b) * c) by Lm12f

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

          .= (x * (y * z)) by A3, Lm12f;

        end;

        hence P is associative;

        now

          let x be Element of P;

          reconsider a = x as Element of E by Lm10f;

          

          thus (x * ( 1. P)) = (a * ( 1. E)) by A1, Lm12f

          .= x;

          

          thus (( 1. P) * x) = (( 1. E) * a) by A1, Lm12f

          .= x;

        end;

        hence P is well-unital;

        now

          let x,y,z be Element of P;

          reconsider a = x, b = y, c = z as Element of E by Lm10f;

          

           A4: (a * b) = (x * y) & (a * c) = (x * z) by Lm12f;

          

           A6: (b * a) = (y * x) & (c * a) = (z * x) by Lm12f;

          

           A5: (y + z) = (b + c) by Lm11f;

          

          hence (x * (y + z)) = (a * (b + c)) by Lm12f

          .= ((a * b) + (a * c)) by VECTSP_1:def 7

          .= ((x * y) + (x * z)) by A4, Lm11f;

          

          thus ((y + z) * x) = ((b + c) * a) by A5, Lm12f

          .= ((b * a) + (c * a)) by VECTSP_1:def 7

          .= ((y * x) + (z * x)) by A6, Lm11f;

        end;

        hence P is distributive;

        now

          let x be Element of P such that

           A5: x <> ( 0. P);

          reconsider a = x as Element of E by Lm10f;

          the carrier of P = ( carrierFA T) by dFA;

          then x in ( carrierFA T);

          then

          consider x1 be Element of E such that

           A6: x = x1 and

           A7: for U be Subfield of E st F is Subfield of U & T is Subset of U holds x1 in U;

          now

            let U be Subfield of E;

            assume F is Subfield of U & T is Subset of U;

            then x1 in U by A7;

            then

            reconsider t = x1 as Element of U;

            (t " ) = (x1 " ) by A5, A6, A2, GAUSSINT: 21;

            hence (x1 " ) in U;

          end;

          then (x1 " ) in ( carrierFA T);

          then

          reconsider y = (x1 " ) as Element of P by dFA;

          take y;

          

          thus (y * x) = ((x1 " ) * a) by Lm12f

          .= ( 1. P) by A1, A2, A5, A6, VECTSP_1:def 10;

        end;

        hence thesis;

      end;

    end

    theorem :: FIELD_6:35

    

     FAt: for F be Field, E be FieldExtension of F holds for T be Subset of E holds T is Subset of ( FAdj (F,T))

    proof

      let R be Field, S be FieldExtension of R;

      let T be Subset of S;

      set P = ( FAdj (R,T));

      now

        let o be object;

        assume

         A: o in T;

        then

        reconsider a = o as Element of S;

        for U be Subfield of S st R is Subfield of U & T is Subset of U holds o in U by A;

        then a in ( carrierFA T);

        hence o in the carrier of P by dFA;

      end;

      hence thesis by TARSKI:def 3;

    end;

    theorem :: FIELD_6:36

    

     FAsub: for F be Field, E be FieldExtension of F holds for T be Subset of E holds F is Subfield of ( FAdj (F,T))

    proof

      let R be Field, S be FieldExtension of R;

      let T be Subset of S;

      set P = ( FAdj (R,T));

      

       X: R is Subring of S by FIELD_4:def 1;

      

       A: ( 1. P) = ( 1. S) by dFA

      .= ( 1. R) by X, C0SP1:def 3;

      

       B: ( 0. P) = ( 0. S) by dFA

      .= ( 0. R) by X, C0SP1:def 3;

      

       C: the carrier of R c= the carrier of P

      proof

        now

          let o be object;

          assume

           C1: o in the carrier of R;

          the carrier of R c= the carrier of S by X, C0SP1:def 3;

          then

          reconsider a = o as Element of S by C1;

          now

            let U be Subfield of S;

            assume R is Subfield of U & T is Subset of U;

            then the carrier of R c= the carrier of U by EC_PF_1:def 1;

            hence o in U by C1;

          end;

          then a in ( carrierFA T);

          hence o in the carrier of P by dFA;

        end;

        hence thesis;

      end;

      then

       Y: [:the carrier of R, the carrier of R:] c= [:the carrier of P, the carrier of P:] by ZFMISC_1: 96;

      

       D: (the addF of P || the carrier of R) = ((the addF of S || ( carrierFA T)) || the carrier of R) by dFA

      .= ((the addF of S || the carrier of P) || the carrier of R) by dFA

      .= (the addF of S || the carrier of R) by Y, FUNCT_1: 51

      .= the addF of R by X, C0SP1:def 3;

      (the multF of P || the carrier of R) = ((the multF of S || ( carrierFA T)) || the carrier of R) by dFA

      .= ((the multF of S || the carrier of P) || the carrier of R) by dFA

      .= (the multF of S || the carrier of R) by Y, FUNCT_1: 51

      .= the multF of R by X, C0SP1:def 3;

      hence thesis by A, B, C, D, EC_PF_1:def 1;

    end;

    theorem :: FIELD_6:37

    

     FAsub2: for F be Field, E be FieldExtension of F, T be Subset of E holds for U be Subfield of E st F is Subfield of U & T is Subset of U holds ( FAdj (F,T)) is Subfield of U

    proof

      let R be Field, S be FieldExtension of R;

      let T be Subset of S;

      let U be Subfield of S;

      assume

       AS: R is Subfield of U & T is Subset of U;

      set P = ( FAdj (R,T));

      

       A: ( 1. P) = ( 1. S) by dFA

      .= ( 1. U) by EC_PF_1:def 1;

      

       B: ( 0. P) = ( 0. S) by dFA

      .= ( 0. U) by EC_PF_1:def 1;

      

       C: the carrier of P c= the carrier of U

      proof

        now

          let o be object;

          assume o in the carrier of P;

          then o in ( carrierFA T) by dFA;

          then

          consider x be Element of S such that

           C2: x = o & for U be Subfield of S st R is Subfield of U & T is Subset of U holds x in U;

          x in U by C2, AS;

          hence o in the carrier of U by C2;

        end;

        hence thesis;

      end;

      then

       Y: [:the carrier of P, the carrier of P:] c= [:the carrier of U, the carrier of U:] by ZFMISC_1: 96;

      

       D: (the addF of U || the carrier of P) = ((the addF of S || the carrier of U) || the carrier of P) by EC_PF_1:def 1

      .= (the addF of S || the carrier of P) by Y, FUNCT_1: 51

      .= (the addF of S || ( carrierFA T)) by dFA

      .= the addF of P by dFA;

      (the multF of U || the carrier of P) = ((the multF of S || the carrier of U) || the carrier of P) by EC_PF_1:def 1

      .= (the multF of S || the carrier of P) by Y, FUNCT_1: 51

      .= (the multF of S || ( carrierFA T)) by dFA

      .= the multF of P by dFA;

      hence thesis by A, B, C, D, EC_PF_1:def 1;

    end;

    theorem :: FIELD_6:38

    for F be strict Field, E be FieldExtension of F, T be Subset of E holds ( FAdj (F,T)) = F iff T is Subset of F

    proof

      let R be strict Field, S be FieldExtension of R;

      let T be Subset of S;

      set P = ( FAdj (R,T));

      

       X: R is Subring of R & R is Subring of S by FIELD_4:def 1, LIOUVIL2: 18;

      

       X1: R is Subfield of R & R is Subfield of S by FIELD_4: 7, FIELD_4: 1;

       Z:

      now

        let o be object;

        assume

         C1: o in the carrier of R;

        the carrier of R c= the carrier of S by X, C0SP1:def 3;

        then

        reconsider a = o as Element of S by C1;

        now

          let U be Subfield of S;

          assume R is Subfield of U & T is Subset of U;

          then the carrier of R c= the carrier of U by EC_PF_1:def 1;

          hence o in U by C1;

        end;

        then a in ( carrierFA T);

        hence o in the carrier of P by dFA;

      end;

      now

        assume

         B0: T is Subset of R;

         B5:

        now

          let o be object;

          assume o in the carrier of P;

          then o in ( carrierFA T) by dFA;

          then

          consider x be Element of S such that

           B1: x = o & for U be Subfield of S st R is Subfield of U & T is Subset of U holds x in U;

          x in R by X1, B0, B1;

          hence o in the carrier of R by B1;

        end;

        then

         B1: the carrier of R = the carrier of P by Z, TARSKI: 2;

        

         B2: ( 1. P) = ( 1. S) by dFA

        .= ( 1. R) by X, C0SP1:def 3;

        

         B3: ( 0. P) = ( 0. S) by dFA

        .= ( 0. R) by X, C0SP1:def 3;

        

         B4: the addF of P = (the addF of S || ( carrierFA T)) by dFA

        .= (the addF of S || the carrier of R) by B1, dFA

        .= the addF of R by X, C0SP1:def 3;

        the multF of P = (the multF of S || ( carrierFA T)) by dFA

        .= (the multF of S || the carrier of R) by B1, dFA

        .= the multF of R by X, C0SP1:def 3;

        hence ( FAdj (R,T)) = R by Z, TARSKI: 2, B5, B2, B3, B4;

      end;

      hence thesis by FAt;

    end;

    definition

      let F be Field, E be FieldExtension of F;

      let T be Subset of E;

      :: original: FAdj

      redefine

      func FAdj (F,T) -> strict Subfield of E ;

      coherence

      proof

        

         A: F is Subfield of E by FIELD_4: 7;

        E is Subfield of E by FIELD_4: 1;

        hence thesis by A, FAsub2;

      end;

    end

    registration

      let F be Field, E be FieldExtension of F;

      let T be Subset of E;

      cluster ( FAdj (F,T)) -> F -extending;

      coherence

      proof

        F is Subfield of ( FAdj (F,T)) by FAsub;

        then F is Subring of ( FAdj (F,T)) by RING_3: 43;

        hence thesis by FIELD_4:def 1;

      end;

    end

    theorem :: FIELD_6:39

    

     RF: for F be Field, E be FieldExtension of F, T be Subset of E holds ( RAdj (F,T)) is Subring of ( FAdj (F,T))

    proof

      let F be Field, E be FieldExtension of F;

      let T be Subset of E;

      set Pf = ( FAdj (F,T)), Pr = ( RAdj (F,T));

      

       A: ( 1. Pr) = ( 1. E) by dRA

      .= ( 1. Pf) by dFA;

      

       B: ( 0. Pr) = ( 0. E) by dRA

      .= ( 0. Pf) by dFA;

      now

        let o be object;

        assume o in the carrier of Pr;

        then o in ( carrierRA T) by dRA;

        then

        consider x be Element of E such that

         B1: x = o & for U be Subring of E st F is Subring of U & T is Subset of U holds x in U;

        now

          let U be Subfield of E;

          assume F is Subfield of U & T is Subset of U;

          then F is Subring of U & U is Subring of E & T is Subset of U by RING_3: 43;

          hence x in U by B1;

        end;

        then x in ( carrierFA T);

        hence o in the carrier of Pf by B1, dFA;

      end;

      then

       C: the carrier of Pr c= the carrier of Pf;

      then

       Y: [:the carrier of Pr, the carrier of Pr:] c= [:the carrier of Pf, the carrier of Pf:] by ZFMISC_1: 96;

      

       D: (the addF of Pf || the carrier of Pr) = ((the addF of E || ( carrierFA T)) || the carrier of Pr) by dFA

      .= ((the addF of E || the carrier of Pf) || the carrier of Pr) by dFA

      .= (the addF of E || the carrier of Pr) by Y, FUNCT_1: 51

      .= (the addF of E || ( carrierRA T)) by dRA

      .= the addF of Pr by dRA;

      (the multF of Pf || the carrier of Pr) = ((the multF of E || ( carrierFA T)) || the carrier of Pr) by dFA

      .= ((the multF of E || the carrier of Pf) || the carrier of Pr) by dFA

      .= (the multF of E || the carrier of Pr) by Y, FUNCT_1: 51

      .= (the multF of E || ( carrierRA T)) by dRA

      .= the multF of Pr by dRA;

      hence thesis by A, B, C, D, C0SP1:def 3;

    end;

    theorem :: FIELD_6:40

    

     RF2: for F be Field, E be FieldExtension of F, T be Subset of E holds ( RAdj (F,T)) = ( FAdj (F,T)) iff ( RAdj (F,T)) is Field

    proof

      let F be Field, E be FieldExtension of F;

      let T be Subset of E;

      set Pf = ( FAdj (F,T)), Pr = ( RAdj (F,T));

      now

        assume Pr is Field;

        then

        reconsider Prf = Pr as Field;

        F is Subring of Prf by RAsub;

        then

         A: F is Subfield of Prf by FIELD_5: 13;

        

         B: Prf is Subfield of E by FIELD_5: 13;

        T is Subset of Prf by RAt;

        then Pf is Subfield of Prf by A, B, FAsub2;

        then

         C: Pf is Subring of Prf by FIELD_5: 12;

        Pr is Subring of Pf by RF;

        hence Pf = Pr by C, RE;

      end;

      hence thesis;

    end;

    

     lcsub1: for F be Field, E be FieldExtension of F holds for a be Element of E holds for n be Element of NAT holds (a |^ n) in the carrier of ( FAdj (F, {a}))

    proof

      let F be Field, E be FieldExtension of F;

      let a be Element of E;

      let n be Element of NAT ;

      defpred P[ Nat] means (a |^ $1) in the carrier of ( FAdj (F, {a}));

      set K = ( FAdj (F, {a}));

      

       H: {a} is Subset of K by FAt;

      a in {a} by TARSKI:def 1;

      then

      reconsider a1 = a as Element of K by H;

      (a |^ 0 ) = ( 1_ E) by BINOM: 8

      .= ( 1. K) by dFA;

      then

       IA: P[ 0 ];

       IS:

      now

        let k be Nat;

        assume P[k];

        then

        reconsider ak = (a |^ k) as Element of K;

        ( carrierFA {a}) = the carrier of K by dFA;

        then

         I: [ak, a1] in [:( carrierFA {a}), ( carrierFA {a}):] by ZFMISC_1:def 2;

        (a |^ (k + 1)) = ((a |^ k) * (a |^ 1)) by BINOM: 10

        .= (the multF of E . (ak,a1)) by BINOM: 8

        .= ((the multF of E || ( carrierFA {a})) . (ak,a1)) by I, FUNCT_1: 49

        .= (ak * a1) by dFA;

        hence P[(k + 1)];

      end;

      for k be Nat holds P[k] from NAT_1:sch 2( IA, IS);

      hence thesis;

    end;

    begin

    registration

      let R be non degenerated comRing, S be comRingExtension of R;

      let a be Element of S;

      cluster ( hom_Ext_eval (a,R)) -> additive multiplicative unity-preserving;

      coherence

      proof

        set F = R, E = S;

        

         X: F is Subring of E by FIELD_4:def 1;

        set g = ( hom_Ext_eval (a,F));

        now

          let x,y be Element of ( Polynom-Ring F);

          reconsider p = x, q = y as Polynomial of F by POLYNOM3:def 10;

          

          thus (g . (x + y)) = (g . (p + q)) by POLYNOM3:def 10

          .= ( Ext_eval ((p + q),a)) by ALGNUM_1:def 11

          .= (( Ext_eval (p,a)) + ( Ext_eval (q,a))) by X, ALGNUM_1: 15

          .= ((g . x) + ( Ext_eval (q,a))) by ALGNUM_1:def 11

          .= ((g . x) + (g . y)) by ALGNUM_1:def 11;

        end;

        hence g is additive;

        now

          let x,y be Element of ( Polynom-Ring F);

          reconsider p = x, q = y as Polynomial of F by POLYNOM3:def 10;

          

          thus (g . (x * y)) = (g . (p *' q)) by POLYNOM3:def 10

          .= ( Ext_eval ((p *' q),a)) by ALGNUM_1:def 11

          .= (( Ext_eval (p,a)) * ( Ext_eval (q,a))) by X, ALGNUM_1: 20

          .= ((g . x) * ( Ext_eval (q,a))) by ALGNUM_1:def 11

          .= ((g . x) * (g . y)) by ALGNUM_1:def 11;

        end;

        hence g is multiplicative;

        (g . ( 1_ ( Polynom-Ring F))) = (g . ( 1_. F)) by POLYNOM3: 37

        .= ( Ext_eval (( 1_. F),a)) by ALGNUM_1:def 11

        .= ( 1_ E) by X, ALGNUM_1: 14;

        hence g is unity-preserving;

      end;

    end

    registration

      let R be non degenerated comRing;

      cluster -> ( Polynom-Ring R) -homomorphic for comRingExtension of R;

      coherence

      proof

        let S be comRingExtension of R;

        set a = the Element of S;

        ( hom_Ext_eval (a,R)) is additive multiplicative unity-preserving;

        hence thesis by RING_2:def 4;

      end;

    end

    registration

      let F be Field;

      cluster ( Polynom-Ring F) -homomorphic for FieldExtension of F;

      existence

      proof

        set E = the FieldExtension of F;

        set a = the Element of E;

        take E;

        thus thesis;

      end;

    end

    definition

      let F be Field, E be FieldExtension of F;

      let a be Element of E;

      :: FIELD_6:def7

      attr a is F -algebraic means ( ker ( hom_Ext_eval (a,F))) <> {( 0. ( Polynom-Ring F))};

    end

    notation

      let F be Field, E be FieldExtension of F;

      let a be Element of E;

      antonym a is F -transcendental for a is F -algebraic;

    end

    theorem :: FIELD_6:41

    

     alg0: for R be Ring, S be RingExtension of R holds for a be Element of S holds ( Ann_Poly (a,R)) = ( ker ( hom_Ext_eval (a,R)))

    proof

      let F be Ring, E be RingExtension of F;

      let a be Element of E;

      set g = ( hom_Ext_eval (a,F));

       A:

      now

        let o be object;

        assume o in ( Ann_Poly (a,F));

        then

        consider p be Polynomial of F such that

         A1: o = p & ( Ext_eval (p,a)) = ( 0. E);

        

         A2: (g . p) = ( 0. E) by A1, ALGNUM_1:def 11;

        reconsider b = p as Element of ( Polynom-Ring F) by POLYNOM3:def 10;

        b in { x where x be Element of ( Polynom-Ring F) : (g . x) = ( 0. E) } by A2;

        hence o in ( ker ( hom_Ext_eval (a,F))) by A1, VECTSP10:def 9;

      end;

      now

        let o be object;

        assume o in ( ker ( hom_Ext_eval (a,F)));

        then o in { x where x be Element of ( Polynom-Ring F) : (g . x) = ( 0. E) } by VECTSP10:def 9;

        then

        consider b be Element of ( Polynom-Ring F) such that

         A1: o = b & (g . b) = ( 0. E);

        reconsider p = b as Polynomial of F by POLYNOM3:def 10;

        ( Ext_eval (p,a)) = ( 0. E) by A1, ALGNUM_1:def 11;

        hence o in ( Ann_Poly (a,F)) by A1;

      end;

      hence thesis by A, TARSKI: 2;

    end;

    theorem :: FIELD_6:42

    

     alg1: for F be Field, E be FieldExtension of F holds for a be Element of E holds a is F -algebraic iff a is_integral_over F

    proof

      let F be Field, E be FieldExtension of F;

      let a be Element of E;

      set g = ( hom_Ext_eval (a,F));

       A:

      now

        assume a is_integral_over F;

        then

        consider p be Polynomial of F such that

         A1: ( LC p) = ( 1. F) & ( Ext_eval (p,a)) = ( 0. E);

        (( 0_. F) . (( len ( 0_. F)) -' 1)) = ( 0. F);

        then p <> ( 0_. F) by A1, RATFUNC1:def 6;

        then

         A3: p <> ( 0. ( Polynom-Ring F)) by POLYNOM3:def 10;

        reconsider b = p as Element of ( Polynom-Ring F) by POLYNOM3:def 10;

        (g . p) = ( 0. E) by A1, ALGNUM_1:def 11;

        then b in { x where x be Element of ( Polynom-Ring F) : (g . x) = ( 0. E) };

        then b in ( ker g) by VECTSP10:def 9;

        hence a is F -algebraic by A3, TARSKI:def 1;

      end;

      now

        assume

         A0: a is F -algebraic;

        now

          assume

           AS: not ex p be Element of the carrier of ( Polynom-Ring F) st p in ( ker g) & p <> ( 0. ( Polynom-Ring F));

          for x be object holds x in ( ker g) iff x = ( 0. ( Polynom-Ring F))

          proof

            let x be object;

            now

              assume

               A2: x = ( 0. ( Polynom-Ring F));

              then (g . x) = ( 0. E) by RING_2: 6;

              then x in { v where v be Element of ( Polynom-Ring F) : (g . v) = ( 0. E) } by A2;

              hence x in ( ker g) by VECTSP10:def 9;

            end;

            hence thesis by AS;

          end;

          hence contradiction by A0, TARSKI:def 1;

        end;

        then

        consider p be Element of the carrier of ( Polynom-Ring F) such that

         A1: p in ( ker g) & p <> ( 0. ( Polynom-Ring F));

        p <> ( 0_. F) by A1, POLYNOM3:def 10;

        then

        reconsider p as non zero Element of the carrier of ( Polynom-Ring F) by UPROOTS:def 5;

        set q = ( NormPolynomial p);

        

         A2: ( LC q) = ( 1. F) by RATFUNC1:def 7;

        ( ker g) = { v where v be Element of ( Polynom-Ring F) : (g . v) = ( 0. E) } by VECTSP10:def 9;

        then

        consider v be Element of the carrier of ( Polynom-Ring F) such that

         A3: v = p & (g . v) = ( 0. E) by A1;

        ( Ext_eval (p,a)) = ( 0. E) by A3, ALGNUM_1:def 11;

        then ( Ext_eval (q,a)) = ( 0. E) by pr1;

        hence a is_integral_over F by A2;

      end;

      hence thesis by A;

    end;

    theorem :: FIELD_6:43

    

     alg00: for F be Field, E be FieldExtension of F holds for a be Element of E holds a is F -algebraic iff ex p be non zero Polynomial of F st ( Ext_eval (p,a)) = ( 0. E)

    proof

      let F be Field, E be FieldExtension of F;

      let a be Element of E;

      set g = ( hom_Ext_eval (a,F));

       A:

      now

        assume a is F -algebraic;

        then a is_integral_over F by alg1;

        then

        consider p be Polynomial of F such that

         A1: ( LC p) = ( 1. F) & ( Ext_eval (p,a)) = ( 0. E);

        ( LC ( 0_. F)) = (( 0_. F) . (( len ( 0_. F)) -' 1)) by RATFUNC1:def 6

        .= ( 0. F);

        then p is non zero by A1, UPROOTS:def 5;

        hence ex p be non zero Polynomial of F st ( Ext_eval (p,a)) = ( 0. E) by A1;

      end;

      now

        assume ex p be non zero Polynomial of F st ( Ext_eval (p,a)) = ( 0. E);

        then

        consider p be non zero Polynomial of F such that

         A1: ( Ext_eval (p,a)) = ( 0. E);

        

         A2: (g . p) = ( 0. E) by A1, ALGNUM_1:def 11;

        reconsider b = p as Element of ( Polynom-Ring F) by POLYNOM3:def 10;

        p <> ( 0_. F);

        then b is non zero by POLYNOM3:def 10;

        then

        reconsider b as non zero Element of ( Polynom-Ring F);

        b in { x where x be Element of ( Polynom-Ring F) : (g . x) = ( 0. E) } by A2;

        then b in ( ker g) by VECTSP10:def 9;

        hence a is F -algebraic by TARSKI:def 1;

      end;

      hence thesis by A;

    end;

    registration

      let F be Field, E be FieldExtension of F;

      cluster F -algebraic for Element of E;

      existence

      proof

        set a = ( 1. F);

        F is Subring of E by FIELD_4:def 1;

        then ( In (a,E)) is_integral_over F by ALGNUM_1: 23;

        hence thesis by alg1;

      end;

    end

    

     lemphi1: for F be Field, E be FieldExtension of F holds for a be Element of E holds ( rng ( hom_Ext_eval (a,F))) = the set of all ( Ext_eval (p,a)) where p be Polynomial of F

    proof

      let F be Field, E be FieldExtension of F;

      let a be Element of E;

      set g = ( hom_Ext_eval (a,F));

       A:

      now

        let x be object;

        assume x in ( rng g);

        then

        consider p be object such that

         A1: p in ( dom g) & x = (g . p) by FUNCT_1:def 3;

        reconsider p as Element of the carrier of ( Polynom-Ring F) by A1;

        reconsider p as Polynomial of F;

        x = ( Ext_eval (p,a)) by A1, ALGNUM_1:def 11;

        hence x in the set of all ( Ext_eval (p,a)) where p be Polynomial of F;

      end;

      now

        let x be object;

        assume x in the set of all ( Ext_eval (p,a)) where p be Polynomial of F;

        then

        consider p be Polynomial of F such that

         A2: x = ( Ext_eval (p,a));

        

         A3: (g . p) = x by A2, ALGNUM_1:def 11;

        

         A4: ( dom g) = the carrier of ( Polynom-Ring F) by FUNCT_2:def 1;

        p is Element of the carrier of ( Polynom-Ring F) by POLYNOM3:def 10;

        hence x in ( rng g) by A3, A4, FUNCT_1: 3;

      end;

      hence thesis by A, TARSKI: 2;

    end;

    

     lemphi2: for F be Field, E be FieldExtension of F holds for a be Element of E holds ( rng ( hom_Ext_eval (a,F))) c= the carrier of ( RAdj (F, {a}))

    proof

      let F be Field, E be FieldExtension of F;

      let a be Element of E;

      set g = ( hom_Ext_eval (a,F));

      

       X: F is Subring of E by FIELD_4:def 1;

      then

       Z: the carrier of F c= the carrier of E by C0SP1:def 3;

      F is Subring of ( RAdj (F, {a})) by RAsub;

      then

       Y: the carrier of F c= the carrier of ( RAdj (F, {a})) by C0SP1:def 3;

      

       I1: for n be Nat holds (( power E) . (a,n)) in the carrier of ( RAdj (F, {a}))

      proof

        let n be Nat;

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

        

         H: {a} is Subset of ( RAdj (F, {a})) by RAt;

        a in {a} by TARSKI:def 1;

        then

        reconsider a1 = a as Element of ( RAdj (F, {a})) by H;

        (a1 |^ n1) = (a |^ n1) by pr5

        .= (( power E) . (a,n)) by BINOM:def 2;

        hence thesis;

      end;

      defpred P[ Nat] means for p be Element of the carrier of ( Polynom-Ring F) st ( deg p) = $1 holds ( Ext_eval (p,a)) in the carrier of ( RAdj (F, {a}));

      

       IA: for p be Element of the carrier of ( Polynom-Ring F) holds ( Ext_eval (( Leading-Monomial p),a)) in the carrier of ( RAdj (F, {a}))

      proof

        let p be Element of the carrier of ( Polynom-Ring F);

        reconsider x2 = (( power E) . (a,(( len p) -' 1))) as Element of ( RAdj (F, {a})) by I1;

        ( In ((p . (( len p) -' 1)),E)) = (p . (( len p) -' 1)) by Z, SUBSET_1:def 8;

        then

        reconsider x1 = ( In ((p . (( len p) -' 1)),E)) as Element of ( RAdj (F, {a})) by Y;

        the carrier of ( RAdj (F, {a})) = ( carrierRA {a}) by dRA;

        then

         L: [x1, x2] in [:( carrierRA {a}), ( carrierRA {a}):] by ZFMISC_1:def 2;

        ( Ext_eval (( Leading-Monomial p),a)) = (( In ((p . (( len p) -' 1)),E)) * (( power E) . (a,(( len p) -' 1)))) by X, ALGNUM_1: 17

        .= ((the multF of E || ( carrierRA {a})) . (x1,x2)) by FUNCT_1: 49, L

        .= (x1 * x2) by dRA;

        hence thesis;

      end;

       IS:

      now

        let k be Nat;

        assume

         IV: for n be Nat st n < k holds P[n];

        now

          let p be Element of the carrier of ( Polynom-Ring F);

          assume

           K0: ( deg p) = k;

          per cases ;

            suppose p = ( 0_. F);

            

            then ( Ext_eval (p,a)) = ( 0. E) by ALGNUM_1: 13

            .= ( 0. ( RAdj (F, {a}))) by dRA;

            hence ( Ext_eval (p,a)) in the carrier of ( RAdj (F, {a}));

          end;

            suppose p <> ( 0_. F);

            then

            consider q be Polynomial of F such that

             K1: ( len q) < ( len p) & p = (q + ( Leading-Monomial p)) & for n be Element of NAT st n < (( len p) - 1) holds (q . n) = (p . n) by POLYNOM4: 16, POLYNOM4: 5;

            reconsider q as Element of the carrier of ( Polynom-Ring F) by POLYNOM3:def 10;

            per cases ;

              suppose q = ( 0_. F);

              hence ( Ext_eval (p,a)) in the carrier of ( RAdj (F, {a})) by K1, IA;

            end;

              suppose q <> ( 0_. F);

              then

              reconsider degq = ( deg q) as Nat by FIELD_1: 1;

              ( deg p) = (( len p) - 1) by HURWITZ:def 2;

              then

               H: ( len q) < (k + 1) by K0, K1;

              ( deg q) = (( len q) - 1) by HURWITZ:def 2;

              then ( len q) = (( deg q) + 1);

              then degq < k by XREAL_1: 6, H;

              then

              reconsider x1 = ( Ext_eval (q,a)) as Element of ( RAdj (F, {a})) by IV;

              reconsider x2 = ( Ext_eval (( Leading-Monomial p),a)) as Element of ( RAdj (F, {a})) by IA;

              the carrier of ( RAdj (F, {a})) = ( carrierRA {a}) by dRA;

              then

               L: [x1, x2] in [:( carrierRA {a}), ( carrierRA {a}):] by ZFMISC_1:def 2;

              ( Ext_eval (p,a)) = (( Ext_eval (q,a)) + ( Ext_eval (( Leading-Monomial p),a))) by K1, ALGNUM_1: 15, X

              .= ((the addF of E || ( carrierRA {a})) . (x1,x2)) by FUNCT_1: 49, L

              .= (x1 + x2) by dRA;

              hence ( Ext_eval (p,a)) in the carrier of ( RAdj (F, {a}));

            end;

          end;

        end;

        hence P[k];

      end;

      

       I: for k be Nat holds P[k] from NAT_1:sch 4( IS);

      now

        let x be object;

        assume x in ( rng g);

        then

        consider p be object such that

         A1: p in ( dom g) & x = (g . p) by FUNCT_1:def 3;

        reconsider p as Element of the carrier of ( Polynom-Ring F) by A1;

        per cases ;

          suppose p = ( 0_. F);

          

          then x = ( Ext_eval (( 0_. F),a)) by A1, ALGNUM_1:def 11

          .= ( 0. E) by ALGNUM_1: 13

          .= ( 0. ( RAdj (F, {a}))) by dRA;

          hence x in the carrier of ( RAdj (F, {a}));

        end;

          suppose p <> ( 0_. F);

          then

          reconsider degp = ( deg p) as Nat by FIELD_1: 1;

           P[degp] by I;

          then ( Ext_eval (p,a)) in the carrier of ( RAdj (F, {a}));

          hence x in the carrier of ( RAdj (F, {a})) by A1, ALGNUM_1:def 11;

        end;

      end;

      hence thesis;

    end;

    

     lemphi3: for F be Field, E be ( Polynom-Ring F) -homomorphic FieldExtension of F holds for a be Element of E holds F is Subring of ( Image ( hom_Ext_eval (a,F)))

    proof

      let F be Field, E be ( Polynom-Ring F) -homomorphic FieldExtension of F;

      let a be Element of E;

      set R = ( Image ( hom_Ext_eval (a,F))), f = ( hom_Ext_eval (a,F));

      

       X: F is Subring of E by FIELD_4:def 1;

      then

       Y: the carrier of F c= the carrier of E by C0SP1:def 3;

       Z:

      now

        let x be object;

        assume x in the carrier of F;

        then

        reconsider b = x as Element of F;

        reconsider c = b as Element of E by Y;

        reconsider p = (b | F) as Element of the carrier of ( Polynom-Ring F) by POLYNOM3:def 10;

        reconsider q = (c | E) as Element of the carrier of ( Polynom-Ring E) by POLYNOM3:def 10;

        ( Ext_eval (p,a)) = ( eval (q,a)) by constpol, FIELD_4: 26

        .= b by RING_5: 8;

        then b in the set of all ( Ext_eval (p,a)) where p be Polynomial of F;

        hence x in ( rng ( hom_Ext_eval (a,F))) by lemphi1;

      end;

      then

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

      now

        let x be object;

        assume x in the carrier of F;

        then x in ( rng ( hom_Ext_eval (a,F))) by Z;

        hence x in the carrier of R by RING_2:def 6;

      end;

      then

       A: the carrier of F c= the carrier of R;

      set adF = the addF of F, adR = the addF of R;

      

       H1c: ( dom the addF of E) = [:the carrier of E, the carrier of E:] by FUNCT_2:def 1;

      adR = (the addF of E || ( rng f)) by RING_2:def 6

      .= (the addF of E | [:( rng f), ( rng f):]);

      then

       H1b: ( dom adR) = ( [:the carrier of E, the carrier of E:] /\ [:( rng f), ( rng f):]) by H1c, RELAT_1: 61;

      

       H1: ( dom (adR || the carrier of F)) = (( dom adR) /\ [:the carrier of F, the carrier of F:]) by RELAT_1: 61

      .= ( [:the carrier of E, the carrier of E:] /\ ( [:( rng f), ( rng f):] /\ [:the carrier of F, the carrier of F:])) by H1b, XBOOLE_1: 16

      .= ( [:the carrier of E, the carrier of E:] /\ [:the carrier of F, the carrier of F:]) by ZZ, ZFMISC_1: 96, XBOOLE_1: 28

      .= [:the carrier of F, the carrier of F:] by Y, ZFMISC_1: 96, XBOOLE_1: 28

      .= ( dom adF) by FUNCT_2:def 1;

      now

        let o be object;

        assume

         AS: o in ( dom adF);

        then

        consider a,b be object such that

         B1: a in the carrier of F & b in the carrier of F & o = [a, b] by ZFMISC_1:def 2;

        reconsider a, b as Element of F by B1;

        a in ( rng f) & b in ( rng f) by Z;

        then

         B3: o in [:( rng f), ( rng f):] by B1, ZFMISC_1:def 2;

        

         B5: the addF of F = (the addF of E || the carrier of F) by C0SP1:def 3, X;

        

        thus (adF . o) = (the addF of E . o) by AS, B5, FUNCT_1: 49

        .= ((the addF of E || ( rng f)) . o) by B3, FUNCT_1: 49

        .= (adR . o) by RING_2:def 6

        .= ((adR | [:the carrier of F, the carrier of F:]) . o) by AS, H1, FUNCT_1: 47;

      end;

      then

       B: the addF of F = (the addF of R || the carrier of F) by H1;

      set muF = the multF of F, muR = the multF of R;

      

       H1c: ( dom the multF of E) = [:the carrier of E, the carrier of E:] by FUNCT_2:def 1;

      muR = (the multF of E || ( rng f)) by RING_2:def 6

      .= (the multF of E | [:( rng f), ( rng f):]);

      then

       H1b: ( dom muR) = ( [:the carrier of E, the carrier of E:] /\ [:( rng f), ( rng f):]) by H1c, RELAT_1: 61;

      

       H1: ( dom (muR || the carrier of F)) = (( dom muR) /\ [:the carrier of F, the carrier of F:]) by RELAT_1: 61

      .= ( [:the carrier of E, the carrier of E:] /\ ( [:( rng f), ( rng f):] /\ [:the carrier of F, the carrier of F:])) by H1b, XBOOLE_1: 16

      .= ( [:the carrier of E, the carrier of E:] /\ [:the carrier of F, the carrier of F:]) by ZZ, ZFMISC_1: 96, XBOOLE_1: 28

      .= [:the carrier of F, the carrier of F:] by Y, ZFMISC_1: 96, XBOOLE_1: 28

      .= ( dom muF) by FUNCT_2:def 1;

      now

        let o be object;

        assume

         AS: o in ( dom muF);

        then

        consider a,b be object such that

         B1: a in the carrier of F & b in the carrier of F & o = [a, b] by ZFMISC_1:def 2;

        reconsider a, b as Element of F by B1;

        a in ( rng f) & b in ( rng f) by Z;

        then

         B3: o in [:( rng f), ( rng f):] by B1, ZFMISC_1:def 2;

        

         B5: the multF of F = (the multF of E || the carrier of F) by C0SP1:def 3, X;

        

        thus (muF . o) = (the multF of E . o) by AS, B5, FUNCT_1: 49

        .= ((the multF of E || ( rng f)) . o) by B3, FUNCT_1: 49

        .= (muR . o) by RING_2:def 6

        .= ((muR | [:the carrier of F, the carrier of F:]) . o) by AS, H1, FUNCT_1: 47;

      end;

      then

       C: the multF of F = (the multF of R || the carrier of F) by H1;

      

       D: ( 0. F) = ( 0. E) by X, C0SP1:def 3

      .= ( 0. R) by RING_2:def 6;

      ( 1. F) = ( 1. E) by X, C0SP1:def 3

      .= ( 1. R) by RING_2:def 6;

      hence thesis by A, B, C, D, C0SP1:def 3;

    end;

    theorem :: FIELD_6:44

    

     lemphi4: for F be Field, E be ( Polynom-Ring F) -homomorphic FieldExtension of F holds for a be Element of E holds ( RAdj (F, {a})) = ( Image ( hom_Ext_eval (a,F)))

    proof

      let F be Field, E be ( Polynom-Ring F) -homomorphic FieldExtension of F;

      let a be Element of E;

      

       A0: F is Subring of E by FIELD_4:def 1;

      set R = ( Image ( hom_Ext_eval (a,F))), S = ( RAdj (F, {a})), f = ( hom_Ext_eval (a,F));

      now

        let o be object;

        assume o in {a};

        then

         A1: o = a by TARSKI:def 1;

        reconsider p = <%( 0. F), ( 1. F)%> as Element of the carrier of ( Polynom-Ring F) by POLYNOM3:def 10;

        the carrier of ( Polynom-Ring F) c= the carrier of ( Polynom-Ring E) by FIELD_4: 10;

        then

        reconsider q = p as Element of the carrier of ( Polynom-Ring E);

        

         A2: ( dom f) = the carrier of ( Polynom-Ring F) by FUNCT_2:def 1;

        ( 0. E) = ( 0. F) & ( 1. E) = ( 1. F) by A0, C0SP1:def 3;

        then

         A3: q = <%( 0. E), ( 1. E)%> by A0, pr20;

        (f . p) = ( Ext_eval (p,a)) by ALGNUM_1:def 11

        .= ( eval (q,a)) by FIELD_4: 26

        .= (( 0. E) + (( 1. E) * a)) by A3, POLYNOM5: 44

        .= a;

        then a in ( rng f) by A2, FUNCT_1:def 3;

        hence o in the carrier of R by A1, RING_2:def 6;

      end;

      then

       A: {a} is Subset of the carrier of R by TARSKI:def 3;

      F is Subring of R by lemphi3;

      then S is Subring of R by A, RAsub2;

      then the carrier of ( RAdj (F, {a})) c= the carrier of ( Image f) by C0SP1:def 3;

      then

       V: the carrier of ( RAdj (F, {a})) c= ( rng ( hom_Ext_eval (a,F))) by RING_2:def 6;

      ( rng ( hom_Ext_eval (a,F))) c= the carrier of ( RAdj (F, {a})) by lemphi2;

      

      then the carrier of ( RAdj (F, {a})) = ( rng f) by V, TARSKI: 2

      .= the carrier of ( Image f) by RING_2:def 6;

      hence thesis by RE1;

    end;

    theorem :: FIELD_6:45

    

     lemphi5: for F be Field, E be ( Polynom-Ring F) -homomorphic FieldExtension of F holds for a be Element of E holds the carrier of ( RAdj (F, {a})) = the set of all ( Ext_eval (p,a)) where p be Polynomial of F

    proof

      let F be Field, E be ( Polynom-Ring F) -homomorphic FieldExtension of F;

      let a be Element of E;

      

      thus the carrier of ( RAdj (F, {a})) = the carrier of ( Image ( hom_Ext_eval (a,F))) by lemphi4

      .= ( rng ( hom_Ext_eval (a,F))) by RING_2:def 6

      .= the set of all ( Ext_eval (p,a)) where p be Polynomial of F by lemphi1;

    end;

    begin

    

     lemlin: for F be Field, E be F -finite FieldExtension of F holds for A be finite Subset of ( VecSp (E,F)) st ( card A) > ( dim ( VecSp (E,F))) holds A is linearly-dependent

    proof

      let F be Field, E be F -finite FieldExtension of F;

      let A be finite Subset of ( VecSp (E,F));

      assume

       H: ( card A) > ( dim ( VecSp (E,F)));

      

       Y: ( VecSp (E,F)) is finite-dimensional by FIELD_4:def 8;

      now

        assume A is linearly-independent;

        then

        consider I be Basis of ( VecSp (E,F)) such that

         X: A c= I by VECTSP_7: 19;

        

         Z: ( card I) = ( dim ( VecSp (E,F))) by Y, VECTSP_9:def 1;

        then

        reconsider I as finite set;

        reconsider A as finite set;

        thus contradiction by H, Z, X, CARD_1: 11, FIELD_5: 3;

      end;

      hence thesis;

    end;

    

     Lm12a: for F be Ring, E be RingExtension of F holds for a,b be Element of E holds for s be Element of F holds for v be Element of ( VecSp (E,F)) st a = s & b = v holds (a * b) = (s * v)

    proof

      let F be Ring, E be RingExtension of F;

      let a,b be Element of E;

      let s be Element of F, v be Element of ( VecSp (E,F)) such that

       A1: a = s & b = v;

      the carrier of ( VecSp (E,F)) = the carrier of E by FIELD_4:def 6;

      then

       A2: [s, v] in [:the carrier of F, the carrier of E:] by ZFMISC_1:def 2;

      

      thus (s * v) = ((the multF of E | [:the carrier of F, the carrier of E:]) . (s,v)) by FIELD_4:def 6

      .= (a * b) by A1, A2, FUNCT_1: 49;

    end;

    

     Lm12b: for F be Ring, E be RingExtension of F holds for a,b be Element of E holds for x,y be Element of F st a = x & b = y holds (a * b) = (x * y)

    proof

      let F be Ring, E be RingExtension of F;

      let a,b be Element of E;

      let x,y be Element of F such that

       A1: a = x & b = y;

      

       A2: F is Subring of E by FIELD_4:def 1;

      

       A3: [x, y] in [:the carrier of F, the carrier of F:] by ZFMISC_1:def 2;

      

      thus (x * y) = ((the multF of E || the carrier of F) . (x,y)) by A2, C0SP1:def 3

      .= (a * b) by A1, A3, FUNCT_1: 49;

    end;

    theorem :: FIELD_6:46

    

     lcsub: for F be Field holds for V be VectSp of F, W be Subspace of V holds for l1 be Linear_Combination of W holds ex l2 be Linear_Combination of V st ( Carrier l2) = ( Carrier l1) & for v be Element of V st v in ( Carrier l2) holds (l2 . v) = (l1 . v)

    proof

      let F be Field;

      let V be VectSp of F, W be Subspace of V;

      let l1 be Linear_Combination of W;

      

       H: the carrier of W c= the carrier of V by VECTSP_4:def 2;

      consider f be Function such that

       L1: l1 = f & ( dom f) = the carrier of W & ( rng f) c= the carrier of F by FUNCT_2:def 2;

      reconsider f as Function of W, F by L1;

      defpred P[ Element of V, Element of F] means ($1 in ( Carrier l1) & $2 = (f . $1)) or ( not $1 in ( Carrier l1) & $2 = ( 0. F));

      

       A: for x be Element of the carrier of V holds ex y be Element of the carrier of F st P[x, y]

      proof

        let v be Element of the carrier of V;

        per cases ;

          suppose

           A1: v in ( Carrier l1);

          then

          reconsider v1 = v as Element of W;

          reconsider y = (f . v1) as Element of F;

          take y;

          thus thesis by A1;

        end;

          suppose

           A1: not v in ( Carrier l1);

          take ( 0. F);

          thus thesis by A1;

        end;

      end;

      consider g be Function of V, F such that

       B: for x be Element of V holds P[x, (g . x)] from FUNCT_2:sch 3( A);

      ( dom g) = the carrier of V & ( rng g) c= the carrier of F by FUNCT_2:def 1;

      then

       C: g is Element of ( Funcs (the carrier of V,the carrier of F)) by FUNCT_2:def 2;

      for o be object st o in ( Carrier l1) holds o in the carrier of V by H;

      then

      reconsider C = ( Carrier l1) as finite Subset of V by TARSKI:def 3;

      for v be Element of V st not v in C holds (g . v) = ( 0. F) by B;

      then

      reconsider l2 = g as Linear_Combination of V by C, VECTSP_6:def 1;

      take l2;

       G:

      now

        let o be object;

        assume o in ( Carrier l2);

        then

        consider v be Element of V such that

         G1: o = v & (l2 . v) <> ( 0. F) by VECTSP_6: 1;

        thus o in ( Carrier l1) by B, G1;

      end;

      now

        let o be object;

        assume

         G0: o in ( Carrier l1);

        then

        consider v be Element of W such that

         G1: o = v & (l1 . v) <> ( 0. F) by VECTSP_6: 1;

        reconsider v1 = v as Element of V by H;

        v1 in ( Carrier l1) & (g . v1) = (f . v1) by B, G1, G0;

        hence o in ( Carrier l2) by L1, G1, VECTSP_6: 2;

      end;

      hence ( Carrier l2) = ( Carrier l1) by G, TARSKI: 2;

      hence thesis by B, L1;

    end;

    theorem :: FIELD_6:47

    

     lembasx2: for F be Field, E be FieldExtension of F holds for a be Element of E holds for n be Element of NAT holds for l be Linear_Combination of ( VecSp (E,F)) holds ex p be Polynomial of F st ( deg p) <= n & for i be Element of NAT st i <= n holds (p . i) = (l . (a |^ i))

    proof

      let F be Field, E be FieldExtension of F;

      let a be Element of E;

      let n be Element of NAT ;

      let l be Linear_Combination of ( VecSp (E,F));

      set V = ( VecSp (E,F));

      defpred P[ object, object] means (ex i be Nat st i <= n & $1 = i & $2 = (l . (a |^ i))) or (ex i be Nat st i > n & $1 = i & $2 = ( 0. F));

      

       A: for x be Element of NAT holds ex y be Element of the carrier of F st P[x, y]

      proof

        let x be Element of NAT ;

        reconsider v = (a |^ x) as Element of V by FIELD_4:def 6;

        per cases ;

          suppose

           A1: ex i be Nat st i <= n & x = i;

          reconsider y = (l . v) as Element of F;

          take y;

          thus thesis by A1;

        end;

          suppose

           A1: ex i be Nat st i > n & x = i;

          take ( 0. F);

          thus thesis by A1;

        end;

      end;

      consider p be Function of NAT , the carrier of F such that

       B: for x be Element of NAT holds P[x, (p . x)] from FUNCT_2:sch 3( A);

      

       C1: for i be Nat holds i <= n implies (p . i) = (l . (a |^ i))

      proof

        let i be Nat;

        assume

         C3: i <= n;

        i is Element of NAT by ORDINAL1:def 12;

        then P[i, (p . i)] by B;

        hence (l . (a |^ i)) = (p . i) by C3;

      end;

      

       C2: for i be Nat holds i >= (n + 1) implies (p . i) = ( 0. F)

      proof

        let i be Nat;

        assume

         C3: i >= (n + 1);

        i is Element of NAT by ORDINAL1:def 12;

        then P[i, (p . i)] by B;

        hence ( 0. F) = (p . i) by C3, NAT_1: 13;

      end;

      then

      reconsider p as Polynomial of F by ALGSEQ_1:def 1;

      take p;

      (n + 1) is_at_least_length_of p by C2, ALGSEQ_1:def 2;

      then ( len p) <= (n + 1) by ALGSEQ_1:def 3;

      then (( len p) - 1) <= ((n + 1) - 1) by XREAL_1: 9;

      hence ( deg p) <= n by HURWITZ:def 2;

      thus thesis by C1;

    end;

    theorem :: FIELD_6:48

    

     lembasx1a: for F be Field, E be FieldExtension of F holds for a be Element of E holds for n be Element of NAT holds for l be Linear_Combination of ( VecSp (E,F)), p be non zero Polynomial of F st (l . (a |^ ( deg p))) = ( LC p) & ( Carrier l) = {(a |^ ( deg p))} holds ( Sum l) = ( Ext_eval (( LM p),a))

    proof

      let F be Field, E be FieldExtension of F;

      let a be Element of E;

      let n be Element of NAT ;

      let l be Linear_Combination of ( VecSp (E,F));

      let p be non zero Polynomial of F;

      F is Subring of E by FIELD_4:def 1;

      then

       H2: the carrier of F c= the carrier of E by C0SP1:def 3;

      

       H3: {a} is Subset of ( FAdj (F, {a})) by FAt;

      a in {a} by TARSKI:def 1;

      then

      reconsider a1 = a as Element of ( FAdj (F, {a})) by H3;

      assume

       A: (l . (a |^ ( deg p))) = ( LC p) & ( Carrier l) = {(a |^ ( deg p))};

      reconsider LCp = ( LC p) as Element of E by H2;

      reconsider adegp = (a |^ ( deg p)) as Element of E;

      reconsider v = (a |^ ( deg p)) as Element of ( VecSp (E,F)) by FIELD_4:def 6;

      

      thus ( Sum l) = ((l . v) * v) by A, VECTSP_6: 20

      .= (LCp * adegp) by A, Lm12a

      .= ( Ext_eval (( LM p),a)) by exevalLM;

    end;

    theorem :: FIELD_6:49

    

     lembasx1: for F be Field, E be FieldExtension of F holds for a be Element of E holds for n be Element of NAT holds for M be Subset of ( VecSp (E,F)) st M = { (a |^ i) where i be Element of NAT : i <= n } & for i,j be Element of NAT st i < j & j <= n holds (a |^ i) <> (a |^ j) holds for l be Linear_Combination of M holds for p be Polynomial of F st ( deg p) <= n & for i be Element of NAT st i <= n holds (p . i) = (l . (a |^ i)) holds ( Ext_eval (p,a)) = ( Sum l)

    proof

      let F be Field, E be FieldExtension of F;

      let a be Element of E;

      let n be Element of NAT ;

      let M be Subset of ( VecSp (E,F));

      assume

       AS1: M = { (a |^ i) where i be Element of NAT : i <= n } & for i,j be Element of NAT st i < j & j <= n holds (a |^ i) <> (a |^ j);

      let l be Linear_Combination of M;

      let p be Polynomial of F;

      assume

       AS2: ( deg p) <= n & for i be Element of NAT st i <= n holds (p . i) = (l . (a |^ i));

      set V = ( VecSp (E,F));

      defpred P[ Nat] means for l be Linear_Combination of M st ( card ( Carrier l)) = $1 holds for p be Polynomial of F st ( deg p) <= n & for i be Element of NAT st i <= n holds (p . i) = (l . (a |^ i)) holds ( Sum l) = ( Ext_eval (p,a));

      

       IA: P[ 0 ]

      proof

        let l be Linear_Combination of M;

        assume ( card ( Carrier l)) = 0 ;

        then ( Carrier l) = {} ;

        then

         A2: l = ( ZeroLC V) by VECTSP_6:def 3;

        let p be Polynomial of F;

        assume

         A4: ( deg p) <= n & for i be Element of NAT st i <= n holds (p . i) = (l . (a |^ i));

        now

          let i be Element of NAT ;

          per cases ;

            suppose i > n;

            then

             A5: i > ( deg p) by A4, XXREAL_0: 2;

            ( deg p) = (( len p) - 1) by HURWITZ:def 2;

            then (i + 1) > ((( len p) - 1) + 1) by A5, XREAL_1: 6;

            hence (p . i) = (( 0_. F) . i) by NAT_1: 13, ALGSEQ_1: 8;

          end;

            suppose

             A5: i <= n;

            then (a |^ i) in M by AS1;

            then

            reconsider v = (a |^ i) as Element of V;

            

            thus (p . i) = (l . v) by A4, A5

            .= (( 0_. F) . i) by A2, VECTSP_6: 3;

          end;

        end;

        then p = ( 0_. F);

        

        hence ( Ext_eval (p,a)) = ( 0. E) by ALGNUM_1: 13

        .= ( 0. V) by FIELD_4:def 6

        .= ( Sum l) by A2, VECTSP_6: 15;

      end;

       IS:

      now

        let k be Nat;

        assume

         B0: P[k];

        now

          let l be Linear_Combination of M;

          assume

           B1: ( card ( Carrier l)) = (k + 1);

          let pp be Polynomial of F;

          assume

           B2: ( deg pp) <= n & for i be Element of NAT st i <= n holds (pp . i) = (l . (a |^ i));

          now

            assume

             C0: pp = ( 0_. F);

            now

              let o be object;

              assume

               C1: o in ( Carrier l);

              ( Carrier l) c= M by VECTSP_6:def 4;

              then o in M by C1;

              then

              consider i be Element of NAT such that

               C2: o = (a |^ i) & i <= n by AS1;

              (l . (a |^ i)) = (pp . i) by B2, C2

              .= ( 0. F) by C0;

              hence contradiction by C1, C2, VECTSP_6: 2;

            end;

            then ( Carrier l) = {} by XBOOLE_0:def 1;

            hence contradiction by B1;

          end;

          then

          reconsider p = pp as non zero Polynomial of F by UPROOTS:def 5;

          defpred Q[ object, object] means ($1 = (a |^ ( deg p)) & $2 = ( LC p)) or ($1 <> (a |^ ( deg p)) & $2 = ( 0. F));

          

           A: for x be object st x in the carrier of V holds ex y be object st y in the carrier of F & Q[x, y]

          proof

            let x be object;

            assume x in the carrier of V;

            per cases ;

              suppose x = (a |^ ( deg p));

              hence ex y be object st y in the carrier of F & Q[x, y];

            end;

              suppose x <> (a |^ ( deg p));

              hence ex y be object st y in the carrier of F & Q[x, y];

            end;

          end;

          consider lp be Function of the carrier of V, the carrier of F such that

           L: for x be object st x in the carrier of V holds Q[x, (lp . x)] from FUNCT_2:sch 1( A);

          reconsider lp as Element of ( Funcs (the carrier of V,the carrier of F)) by FUNCT_2: 8;

          

           U: M is finite

          proof

            deffunc F( Nat) = (a |^ $1);

            defpred P[ Nat] means $1 <= n;

            

             D: { F(i) where i be Nat : i <= n & P[i] } is finite from FINSEQ_1:sch 6;

             E:

            now

              let o be object;

              assume o in { F(i) where i be Nat : i <= n & P[i] };

              then

              consider i be Nat such that

               E1: o = (a |^ i) & i <= n & i <= n;

              i is Element of NAT by ORDINAL1:def 12;

              hence o in M by E1, AS1;

            end;

            now

              let o be object;

              assume o in M;

              then

              consider i be Element of NAT such that

               E1: o = (a |^ i) & i <= n by AS1;

              thus o in { F(i) where i be Nat : i <= n & P[i] } by E1;

            end;

            hence thesis by D, E, TARSKI: 2;

          end;

          for v be Element of V st not v in M holds (lp . v) = ( 0. F)

          proof

            let v be Element of V;

            assume not v in M;

            then v <> (a |^ ( deg p)) by B2, AS1;

            hence (lp . v) = ( 0. F) by L;

          end;

          then

          reconsider lp as Linear_Combination of V by U, VECTSP_6:def 1;

          now

            let o be object;

            assume o in ( Carrier lp);

            then

            consider v be Element of V such that

             A1: o = v & (lp . v) <> ( 0. F) by VECTSP_6: 1;

            v = (a |^ ( deg p)) & (lp . v) = ( LC p) by L, A1;

            hence o in M by A1, B2, AS1;

          end;

          then ( Carrier lp) c= M;

          then

          reconsider lp as Linear_Combination of M by VECTSP_6:def 4;

          

           X1: {a} is Subset of ( FAdj (F, {a})) by FAt;

          a in {a} by TARSKI:def 1;

          then

          reconsider a1 = a as Element of the carrier of ( FAdj (F, {a})) by X1;

          

           X: (a |^ ( deg p)) is Element of V by FIELD_4:def 6;

          

           C0: ( Carrier lp) = {(a |^ ( deg p))}

          proof

             C2:

            now

              let o be object;

              assume o in {(a |^ ( deg p))};

              then

               C3: o = (a |^ ( deg p)) by TARSKI:def 1;

              then (lp . o) <> ( 0. F) by X, L;

              hence o in ( Carrier lp) by X, C3, VECTSP_6: 2;

            end;

            now

              let o be object;

              assume

               C3: o in ( Carrier lp);

              ( Carrier lp) = { v where v be Element of V : (lp . v) <> ( 0. F) } by VECTSP_6:def 2;

              then

              consider v be Element of V such that

               C4: o = v & (lp . v) <> ( 0. F) by C3;

              o = (a |^ ( deg p)) by C4, L;

              hence o in {(a |^ ( deg p))} by TARSKI:def 1;

            end;

            hence thesis by C2, TARSKI: 2;

          end;

          (lp . (a |^ ( deg p))) = ( LC p) by X, L;

          then

           C: ( Ext_eval (( LM p),a)) = ( Sum lp) by C0, lembasx1a;

          set q = (p - ( LM p));

          reconsider lk = (l - lp) as Linear_Combination of M by VECTSP_6: 42;

          

           C2: l = (lk + lp)

          proof

            

            thus (lk + lp) = ((l + ( - lp)) + lp) by VECTSP_6:def 11

            .= (l + (( - lp) + lp)) by VECTSP_6: 26

            .= (l + (lp + ( - lp))) by VECTSP_6: 25

            .= (l + (lp - lp)) by VECTSP_6:def 11

            .= (l + ( ZeroLC V)) by VECTSP_6: 43

            .= l by VECTSP_6: 27;

          end;

          

           C3: ( Carrier lk) = (( Carrier l) \ ( Carrier lp))

          proof

             C4:

            now

              let o be object;

              assume o in ( Carrier lk);

              then

              consider v be Element of V such that

               C5: o = v & (lk . v) <> ( 0. F) by VECTSP_6: 1;

               C6:

              now

                assume

                 C7: v = (a |^ ( deg p));

                

                then

                 C9: (l . v) = (p . ( deg p)) by B2

                .= ( LC p) by thLC;

                (lk . v) = ((l . v) - (lp . v)) by VECTSP_6: 40

                .= (( LC p) - ( LC p)) by L, C7, C9;

                hence contradiction by C5, RLVECT_1: 15;

              end;

              then

               C7: not v in ( Carrier lp) by C0, TARSKI:def 1;

              (lk . v) = ((l . v) - (lp . v)) by VECTSP_6: 40

              .= ((l . v) - ( 0. F)) by C6, L;

              then v in ( Carrier l) by C5, VECTSP_6: 2;

              hence o in (( Carrier l) \ ( Carrier lp)) by C7, C5, XBOOLE_0:def 5;

            end;

            now

              let o be object;

              assume o in (( Carrier l) \ ( Carrier lp));

              then

               C5: o in ( Carrier l) & not o in ( Carrier lp) by XBOOLE_0:def 5;

              then

              consider v be Element of V such that

               C6: o = v & (l . v) <> ( 0. F) by VECTSP_6: 1;

              

               C7: o <> (a |^ ( deg p)) by C0, C5, TARSKI:def 1;

              (lk . v) = ((l . v) - (lp . v)) by VECTSP_6: 40

              .= ((l . v) - ( 0. F)) by C6, C7, L;

              hence o in ( Carrier lk) by C6, VECTSP_6: 1;

            end;

            hence thesis by C4, TARSKI: 2;

          end;

          now

            let o be object;

            assume

             C5: o in ( Carrier lp);

            then

             C4: o = (a |^ ( deg p)) by C0, TARSKI:def 1;

            reconsider v = o as Element of V by C5;

            (lp . v) = ( LC p) by L, C4

            .= (pp . ( deg p)) by thLC

            .= (l . v) by C4, B2;

            then (l . v) <> ( 0. F) by C5, VECTSP_6: 2;

            hence o in ( Carrier l) by VECTSP_6: 2;

          end;

          then ( Carrier lp) c= ( Carrier l);

          

          then

           A: ( card (( Carrier l) \ ( Carrier lp))) = (( card ( Carrier l)) - ( card ( Carrier lp))) by CARD_2: 44

          .= ((k + 1) - 1) by B1, C0, CARD_2: 42;

          

           B: ( deg q) < n by thdLM, B2, XXREAL_0: 2;

          for i be Element of NAT st i <= n holds (q . i) = (lk . (a |^ i))

          proof

            let i be Element of NAT ;

            assume

             B1: i <= n;

            reconsider v = (a |^ i) as Element of V by FIELD_4:def 6;

            per cases ;

              suppose

               B3: i = ( deg p);

              

              hence (q . i) = ((p . ( deg p)) - (( LM p) . ( deg p))) by POLYNOM3: 27

              .= ((p . ( deg p)) - (( LM p) . ( deg ( LM p)))) by thdegLM

              .= ((l . v) - (( LM p) . ( deg ( LM p)))) by B3, B2

              .= ((l . v) - ( LC ( LM p))) by thLC

              .= ((l . v) - ( LC p)) by thdegLC

              .= ((l . v) - (lp . v)) by B3, L

              .= (lk . (a |^ i)) by VECTSP_6: 40;

            end;

              suppose

               D2: i <> ( deg p);

              

               D3: (a |^ i) <> (a |^ ( deg p))

              proof

                per cases by D2, XXREAL_0: 1;

                  suppose i < ( deg p);

                  hence thesis by B2, AS1;

                end;

                  suppose i > ( deg p);

                  hence thesis by B1, AS1;

                end;

              end;

              p <> ( 0_. F);

              then ( len p) <> 0 by POLYNOM4: 5;

              then (( len p) + 1) > ( 0 + 1) by XREAL_1: 6;

              then ( len p) >= 1 by NAT_1: 13;

              then

               D5: (( len p) -' 1) = (( len p) - 1) by XREAL_0:def 2;

              

               D4: i <> (( len p) -' 1) by D5, D2, HURWITZ:def 2;

              

              thus (q . i) = ((p . i) - (( LM p) . i)) by POLYNOM3: 27

              .= ((p . i) - ( 0. F)) by D4, POLYNOM4:def 1

              .= ((l . v) - ( 0. F)) by B2, B1

              .= ((l . v) - (lp . v)) by D3, L

              .= (lk . (a |^ i)) by VECTSP_6: 40;

            end;

          end;

          then

           D: ( Ext_eval (q,a)) = ( Sum lk) by A, C3, B, B0;

          

          thus ( Sum l) = (( Sum lk) + ( Sum lp)) by C2, VECTSP_6: 44

          .= (the addF of E . (( Sum lk),( Sum lp))) by FIELD_4:def 6

          .= ((( Ext_eval (p,a)) - ( Ext_eval (( LM p),a))) + ( Ext_eval (( LM p),a))) by C, D, exevalminus2

          .= (( Ext_eval (p,a)) + (( - ( Ext_eval (( LM p),a))) + ( Ext_eval (( LM p),a)))) by RLVECT_1:def 3

          .= (( Ext_eval (p,a)) + ( 0. E)) by RLVECT_1: 5

          .= ( Ext_eval (pp,a));

        end;

        hence P[(k + 1)];

      end;

      

       I: for k be Nat holds P[k] from NAT_1:sch 2( IA, IS);

      consider n be Nat such that

       H: ( card ( Carrier l)) = n;

      thus thesis by AS2, I, H;

    end;

    begin

    notation

      let F be Field, E be FieldExtension of F;

      let a be F -algebraic Element of E;

      synonym MinPoly (a,F) for minimal_polynom (a,F);

    end

    

     lemminirred: for F be Field, E be FieldExtension of F, a be F -algebraic Element of E holds ( MinPoly (a,F)) is irreducible

    proof

      let F be Field, E be FieldExtension of F, a be F -algebraic Element of E;

      set m = ( MinPoly (a,F));

      

       X: F is Subring of E by FIELD_4:def 1;

      a is_integral_over F by alg1;

      then

       Z: m <> ( 0_. F) & ( {m} -Ideal ) = ( Ann_Poly (a,F)) & m = ( NormPolynomial m) by X, ALGNUM_1:def 9;

      then m in { p where p be Polynomial of F : ( Ext_eval (p,a)) = ( 0. E) } by IDEAL_1: 66;

      then

      consider m1 be Polynomial of F such that

       Z1: m1 = m & ( Ext_eval (m1,a)) = ( 0. E);

      reconsider m2 = m as Element of ( Polynom-Ring F);

      reconsider m1 as non zero Element of the carrier of ( Polynom-Ring F) by Z1, Z, UPROOTS:def 5;

      

       A2: m <> ( 0. ( Polynom-Ring F)) by Z, POLYNOM3:def 10;

       A3:

      now

        assume m2 is Unit of ( Polynom-Ring F);

        then

         A4: ( {m} -Ideal ) = ( [#] ( Polynom-Ring F)) by RING_2: 20;

        ( ker ( hom_Ext_eval (a,F))) is proper;

        hence contradiction by A4, Z, alg0;

      end;

      now

        let x be Element of ( Polynom-Ring F);

        assume

         B: x divides m;

        consider y be Element of ( Polynom-Ring F) such that

         A4: (x * y) = m2 by B;

        reconsider x1 = x, y1 = y as Polynomial of F by POLYNOM3:def 10;

        m1 = (x1 *' y1) by Z1, A4, POLYNOM3:def 10;

        then

         A5: ( Ext_eval (m1,a)) = (( Ext_eval (x1,a)) * ( Ext_eval (y1,a))) by ALGNUM_1: 20, X;

        per cases by A5, Z1, VECTSP_2:def 1;

          suppose ( Ext_eval (x1,a)) = ( 0. E);

          then x1 in ( {m} -Ideal ) by Z;

          then x1 in the set of all (m * r) where r be Element of ( Polynom-Ring F) by IDEAL_1: 64;

          then

          consider r be Element of ( Polynom-Ring F) such that

           A6: x = (m2 * r);

          m2 divides x by A6;

          hence (x is Unit of ( Polynom-Ring F) or x is_associated_to m) by B;

        end;

          suppose ( Ext_eval (y1,a)) = ( 0. E);

          then y1 in ( {m} -Ideal ) by Z;

          then y1 in the set of all (m * r) where r be Element of ( Polynom-Ring F) by IDEAL_1: 64;

          then

          consider r be Element of ( Polynom-Ring F) such that

           A6: y1 = (m * r);

          reconsider r1 = r as Polynomial of F by POLYNOM3:def 10;

          

           A8: (x * r) = (x1 *' r1) by POLYNOM3:def 10;

          (( 1. ( Polynom-Ring F)) * m) = (x * (r * m)) by A6, A4, GROUP_1:def 12

          .= ((x * r) * m) by GROUP_1:def 3;

          then (( 1_. F) *' m1) = ((x1 *' r1) *' m1) by Z1, A8, POLYNOM3:def 10;

          

          then ( 1_. F) = (x1 *' r1) by RATFUNC1: 7

          .= (x * r) by POLYNOM3:def 10;

          then ( 1. ( Polynom-Ring F)) = (x * r) by POLYNOM3:def 10;

          then x divides ( 1. ( Polynom-Ring F));

          hence (x is Unit of ( Polynom-Ring F) or x is_associated_to m) by GCD_1:def 2;

        end;

      end;

      hence thesis by A2, A3, RING_2:def 9;

    end;

    registration

      let F be Field, E be FieldExtension of F;

      let a be F -algebraic Element of E;

      cluster ( MinPoly (a,F)) -> monic irreducible;

      coherence

      proof

        

         X: F is Subring of E by FIELD_4:def 1;

        a is_integral_over F by alg1;

        then

         Z: ( MinPoly (a,F)) <> ( 0_. F) & ( MinPoly (a,F)) = ( NormPolynomial ( MinPoly (a,F))) by X, ALGNUM_1:def 9;

        then ( MinPoly (a,F)) is non zero by UPROOTS:def 5;

        hence ( MinPoly (a,F)) is monic by Z;

        thus thesis by lemminirred;

      end;

    end

    theorem :: FIELD_6:50

    

     mpol1: for F be Field, E be FieldExtension of F holds for a be F -algebraic Element of E, p be Element of the carrier of ( Polynom-Ring F) holds p = ( MinPoly (a,F)) iff (p is monic & p is irreducible & ( ker ( hom_Ext_eval (a,F))) = ( {p} -Ideal ))

    proof

      let F be Field, E be FieldExtension of F;

      let a be F -algebraic Element of E, p be Element of the carrier of ( Polynom-Ring F);

      set m = ( MinPoly (a,F));

      

       X: F is Subring of E by FIELD_4:def 1;

      

       Y: a is_integral_over F by alg1;

      then

       Z: m <> ( 0_. F) & ( {m} -Ideal ) = ( Ann_Poly (a,F)) & m = ( NormPolynomial m) by X, ALGNUM_1:def 9;

      now

        assume

         A0: p is monic & p is irreducible & ( ker ( hom_Ext_eval (a,F))) = ( {p} -Ideal );

        then

         A1: p <> ( 0_. F);

        

         A2: ( {p} -Ideal ) = ( Ann_Poly (a,F)) by A0, alg0;

        p = ( NormPolynomial p) by A0, RING_4: 24;

        hence p = m by X, Y, A1, A2, ALGNUM_1:def 9;

      end;

      hence thesis by Z, alg0;

    end;

    theorem :: FIELD_6:51

    

     mpol2: for F be Field, E be FieldExtension of F holds for a be F -algebraic Element of E, p be Element of the carrier of ( Polynom-Ring F) holds p = ( MinPoly (a,F)) iff (p is monic & ( Ext_eval (p,a)) = ( 0. E) & for q be non zero Polynomial of F st ( Ext_eval (q,a)) = ( 0. E) holds ( deg p) <= ( deg q))

    proof

      let F be Field, E be FieldExtension of F;

      let a be F -algebraic Element of E, p be Element of the carrier of ( Polynom-Ring F);

      set m = ( MinPoly (a,F)), g = ( hom_Ext_eval (a,F));

      

       X: F is Subring of E by FIELD_4:def 1;

      a is_integral_over F by alg1;

      then

       Z: m <> ( 0_. F) & ( {m} -Ideal ) = ( Ann_Poly (a,F)) & m = ( NormPolynomial m) by X, ALGNUM_1:def 9;

      then m in { p where p be Polynomial of F : ( Ext_eval (p,a)) = ( 0. E) } by IDEAL_1: 66;

      then

      consider m1 be Polynomial of F such that

       Z1: m1 = m & ( Ext_eval (m1,a)) = ( 0. E);

       A:

      now

        assume

         A1: p = ( MinPoly (a,F));

        hence p is monic;

        thus ( Ext_eval (p,a)) = ( 0. E) by Z1, A1;

        thus for q be non zero Polynomial of F st ( Ext_eval (q,a)) = ( 0. E) holds ( deg p) <= ( deg q)

        proof

          let q be non zero Polynomial of F;

          assume ( Ext_eval (q,a)) = ( 0. E);

          then q in ( {m} -Ideal ) by Z;

          then q in the set of all (m * r) where r be Element of ( Polynom-Ring F) by IDEAL_1: 64;

          then

          consider r be Element of the carrier of ( Polynom-Ring F) such that

           A2: q = (m * r);

          reconsider r1 = r as Polynomial of F;

          

           A3: (m1 *' r1) = (m * r) by Z1, POLYNOM3:def 10;

          

           A5: r1 <> ( 0_. F) by A2, A3;

          then

           A6: ( deg q) = (( deg p) + ( deg r1)) by A1, A3, A2, Z1, HURWITZ: 23;

          ( deg r1) is Nat by A5, FIELD_1: 1;

          hence ( deg p) <= ( deg q) by A6, INT_1: 6;

        end;

      end;

      now

        assume

         A: p is monic & ( Ext_eval (p,a)) = ( 0. E) & for q be non zero Polynomial of F st ( Ext_eval (q,a)) = ( 0. E) holds ( deg p) <= ( deg q);

        then

         A1: p <> ( 0_. F);

        reconsider p1 = p as Element of ( Polynom-Ring F);

         A2:

        now

          assume p1 is Unit of ( Polynom-Ring F);

          then p1 divides ( 1. ( Polynom-Ring F)) by GCD_1:def 2;

          then

          consider u1 be Element of ( Polynom-Ring F) such that

           A3: (p1 * u1) = ( 1. ( Polynom-Ring F));

          reconsider u = u1 as Element of the carrier of ( Polynom-Ring F);

          (p *' u) = ( 1. ( Polynom-Ring F)) by A3, POLYNOM3:def 10

          .= ( 1_. F) by POLYNOM3:def 10;

          

          then ( Ext_eval (( 1_. F),a)) = (( Ext_eval (p,a)) * ( Ext_eval (u,a))) by X, ALGNUM_1: 20

          .= ( 0. E) by A;

          then ( Ext_eval (( 1_. F),a)) <> ( 1. E);

          hence contradiction by X, ALGNUM_1: 14;

        end;

         B:

        now

          assume p is reducible;

          then

          consider q be Element of the carrier of ( Polynom-Ring F) such that

           A4: q divides p & 1 <= ( deg q) & ( deg q) < ( deg p) by A1, A2, RING_4: 41;

          reconsider q1 = q as Polynomial of F;

          consider u1 be Polynomial of F such that

           A3: (q1 *' u1) = p1 by A4, RING_4: 1;

          

           A6: q1 <> ( 0_. F) by A3, A;

          

           A7: u1 <> ( 0_. F) by A3, A;

          then

           Y: ( deg q1) is Nat & ( deg u1) is Element of NAT by A6, FIELD_1: 1;

          

           A11: ( deg p) = (( deg q1) + ( deg u1)) by A3, A7, A6, HURWITZ: 23;

          then

           A10: ( deg u1) <= ( deg p) by Y, INT_1: 6;

          

           A19: ( 0. E) = (( Ext_eval (q1,a)) * ( Ext_eval (u1,a))) by X, A3, A, ALGNUM_1: 20;

          per cases by A19, VECTSP_2:def 1;

            suppose

             A9: ( Ext_eval (q1,a)) = ( 0. E);

            q1 is non zero by A3, A;

            hence contradiction by A4, A9, A;

          end;

            suppose

             A9: ( Ext_eval (u1,a)) = ( 0. E);

            u1 is non zero by A3, A;

            then ( deg p) <= ( deg u1) by A9, A;

            then ( deg u1) = ( deg p) by A10, XXREAL_0: 1;

            hence contradiction by A4, A11;

          end;

        end;

        ( ker g) is principal by IDEAL_1:def 28;

        then

        consider u be Element of ( Polynom-Ring F) such that

         C1: ( ker g) = ( {u} -Ideal );

        (( hom_Ext_eval (a,F)) . p) = ( 0. E) by A, ALGNUM_1:def 11;

        then p in { v where v be Element of ( Polynom-Ring F) : (g . v) = ( 0. E) };

        then

         C2: p in ( {u} -Ideal ) by C1, VECTSP10:def 9;

        p in the set of all (u * r) where r be Element of ( Polynom-Ring F) by C2, IDEAL_1: 64;

        then

        consider v be Element of ( Polynom-Ring F) such that

         C3: p = (u * v);

        reconsider u1 = u, v1 = v, p1 = p as Polynomial of F by POLYNOM3:def 10;

        

         C3a: p = (u1 *' v1) by C3, POLYNOM3:def 10;

        then

         C3b: u1 <> ( 0_. F) & v1 <> ( 0_. F) by A;

        

         C3c: u1 is non zero by C3a, A;

        

         C4: ( deg p) = (( deg u1) + ( deg v1)) by C3a, C3b, HURWITZ: 23;

        u in ( ker g) by C1, IDEAL_1: 66;

        then u in { v where v be Element of ( Polynom-Ring F) : (g . v) = ( 0. E) } by VECTSP10:def 9;

        then

        consider w be Element of ( Polynom-Ring F) such that

         C5: u = w & (g . w) = ( 0. E);

        ( Ext_eval (u1,a)) = ( 0. E) by C5, ALGNUM_1:def 11;

        then

         C10: (( deg p) + ( deg v1)) <= ( deg p) by A, C3c, C4, XREAL_1: 6;

        reconsider degv = ( deg v1) as Element of NAT by C3b, FIELD_1: 1;

        ((( deg p) + ( deg v1)) - ( deg p)) <= (( deg p) - ( deg p)) by C10, XREAL_1: 9;

        then

        consider b be Element of F such that

         C6: v1 = (b | F) by RING_4: 20, RING_4:def 4;

        reconsider v2 = ((b " ) | F) as Element of ( Polynom-Ring F) by POLYNOM3:def 10;

        

         C7: b <> ( 0. F) by A, C3a, C6;

        ((u1 *' v1) *' ((b " ) | F)) = (u1 *' (v1 *' ((b " ) | F))) by POLYNOM3: 33

        .= (u1 *' (((b " ) * b) | F)) by C6, RING_4: 18

        .= (u1 *' (( 1. F) | F)) by C7, VECTSP_1:def 10

        .= (u1 *' ( 1_. F)) by RING_4: 14;

        

        then u1 = (p1 *' ((b " ) | F)) by C3, POLYNOM3:def 10

        .= (p * v2) by POLYNOM3:def 10;

        then u in the set of all (p * r) where r be Element of ( Polynom-Ring F);

        then u in ( {p} -Ideal ) by IDEAL_1: 64;

        then

         C: ( ker g) c= ( {p} -Ideal ) by C1, IDEAL_1: 67;

        ( {p} -Ideal ) c= ( ker g) by C1, C2, IDEAL_1: 67;

        hence p = ( MinPoly (a,F)) by A, B, mpol1, C, TARSKI: 2;

      end;

      hence thesis by A;

    end;

    theorem :: FIELD_6:52

    

     mpol3: for F be Field, E be FieldExtension of F holds for a be F -algebraic Element of E, p be Element of the carrier of ( Polynom-Ring F) holds p = ( MinPoly (a,F)) iff (p is monic & p is irreducible & ( Ext_eval (p,a)) = ( 0. E))

    proof

      let F be Field, E be FieldExtension of F;

      let a be F -algebraic Element of E, p be Element of the carrier of ( Polynom-Ring F);

      set m = ( MinPoly (a,F)), g = ( hom_Ext_eval (a,F));

      

       X: F is Subring of E by FIELD_4:def 1;

      a is_integral_over F by alg1;

      then m <> ( 0_. F) & ( {m} -Ideal ) = ( Ann_Poly (a,F)) & m = ( NormPolynomial m) by X, ALGNUM_1:def 9;

      then m in { p where p be Polynomial of F : ( Ext_eval (p,a)) = ( 0. E) } by IDEAL_1: 66;

      then

      consider m1 be Polynomial of F such that

       Z1: m1 = m & ( Ext_eval (m1,a)) = ( 0. E);

      now

        assume

         A: p is monic & p is irreducible & ( Ext_eval (p,a)) = ( 0. E);

        reconsider p1 = p as Element of ( Polynom-Ring F);

        ( ker g) is principal by IDEAL_1:def 28;

        then

        consider u be Element of ( Polynom-Ring F) such that

         C1: ( ker g) = ( {u} -Ideal );

        (( hom_Ext_eval (a,F)) . p) = ( 0. E) by A, ALGNUM_1:def 11;

        then p in { v where v be Element of ( Polynom-Ring F) : (g . v) = ( 0. E) };

        then

         C2: p in ( {u} -Ideal ) by C1, VECTSP10:def 9;

        p in the set of all (u * r) where r be Element of ( Polynom-Ring F) by C2, IDEAL_1: 64;

        then

        consider v be Element of ( Polynom-Ring F) such that

         C3: p = (u * v);

        reconsider u1 = u as Polynomial of F by POLYNOM3:def 10;

         A2:

        now

          assume u is Unit of ( Polynom-Ring F);

          then ( {u} -Ideal ) = ( [#] ( Polynom-Ring F)) by RING_2: 20;

          hence contradiction by C1;

        end;

        u divides p by C3;

        then u is_associated_to p by A2, A, RING_2:def 9;

        then ( {p} -Ideal ) = ( ker g) by C1, RING_2: 21;

        hence p = ( MinPoly (a,F)) by A, mpol1;

      end;

      hence thesis by Z1;

    end;

    theorem :: FIELD_6:53

    

     mpol4: for F be Field, E be FieldExtension of F holds for a be F -algebraic Element of E, p be Element of the carrier of ( Polynom-Ring F) holds ( Ext_eval (p,a)) = ( 0. E) iff ( MinPoly (a,F)) divides p

    proof

      let F be Field, E be FieldExtension of F;

      let a be F -algebraic Element of E, p be Element of the carrier of ( Polynom-Ring F);

      set ma = ( MinPoly (a,F)), g = ( hom_Ext_eval (a,F));

      

       X: F is Subring of E by FIELD_4:def 1;

      reconsider p1 = p, ma1 = ma as Element of ( Polynom-Ring F);

       A:

      now

        assume ( Ext_eval (p,a)) = ( 0. E);

        then (g . p) = ( 0. E) by ALGNUM_1:def 11;

        then p in { v where v be Element of ( Polynom-Ring F) : (g . v) = ( 0. E) };

        then p in ( ker g) by VECTSP10:def 9;

        then p in ( {ma} -Ideal ) by mpol1;

        hence ma divides p by RING_4:def 3, RING_2: 18;

      end;

      now

        assume ma divides p;

        then

        consider u be Polynomial of F such that

         H: (ma *' u) = p by RING_4: 1;

        ( 0. E) = ( Ext_eval (ma,a)) by mpol2;

        

        hence ( 0. E) = (( Ext_eval (ma,a)) * ( Ext_eval (u,a)))

        .= ( Ext_eval (p,a)) by X, H, ALGNUM_1: 20;

      end;

      hence thesis by A;

    end;

    theorem :: FIELD_6:54

    for F be Field, E be FieldExtension of F holds for a be F -algebraic Element of E holds ( MinPoly (a,F)) = ( rpoly (1,a)) iff a in the carrier of F

    proof

      let F be Field, E be FieldExtension of F;

      let a be F -algebraic Element of E;

      set ma = ( MinPoly (a,F)), g = ( hom_Ext_eval (a,F));

      

       X: F is Subring of E by FIELD_4:def 1;

       A:

      now

        assume a in the carrier of F;

        then

        reconsider a1 = a as Element of F;

        reconsider p = ( rpoly (1,a1)) as Element of the carrier of ( Polynom-Ring F) by POLYNOM3:def 10;

        

         A3: ( rpoly (1,a)) = ( rpoly (1,a1)) by FIELD_4: 21;

        ( deg p) = 1 by HURWITZ: 27;

        then

         A2: p is irreducible by RING_4: 42;

        ( Ext_eval (p,a)) = ( eval (p,a1)) by FIELD427

        .= (a1 - a1) by HURWITZ: 29

        .= ( 0. F) by RLVECT_1: 15

        .= ( 0. E) by X, C0SP1:def 3;

        hence ma = ( rpoly (1,a)) by A3, A2, mpol3;

      end;

      now

        assume ma = ( rpoly (1,a));

        then

        reconsider p = ( rpoly (1,a)) as Element of the carrier of ( Polynom-Ring F);

        ( - (p . 0 )) = ( - (( rpoly (1,a)) . 0 )) by X, Th19

        .= ( - ( - (( power E) . (a,(1 + 0 ))))) by HURWITZ: 25

        .= ( - ( - ((( power E) . (a, 0 )) * a))) by GROUP_1:def 7

        .= ( - ( - (( 1_ E) * a))) by GROUP_1:def 7

        .= a;

        hence a in the carrier of F;

      end;

      hence thesis by A;

    end;

    theorem :: FIELD_6:55

    

     mpol5: for F be Field, E be FieldExtension of F holds for a be F -algebraic Element of E holds for i,j be Element of NAT st i < j & j < ( deg ( MinPoly (a,F))) holds (a |^ i) <> (a |^ j)

    proof

      let F be Field, E be FieldExtension of F;

      let a be F -algebraic Element of E;

      let i,j be Element of NAT ;

      assume

       AS: i < j & j < ( deg ( MinPoly (a,F)));

      set ma = ( MinPoly (a,F));

      reconsider n = ( deg ma) as Element of NAT ;

      j >= ( 0 + 1) by AS, INT_1: 7;

      then

       X: ma is non linear by AS, FIELD_5:def 1;

      (j - i) <= j by XREAL_1: 43;

      then (j - i) < n by AS, XXREAL_0: 2;

      then

       Y3: (n - n) < (n - (j - i)) by XREAL_1: 15;

      then ( 0 + 1) <= ((i + n) - j) by INT_1: 7;

      then

       Y7: (( 0 + 1) - 1) <= (((i + n) - j) - 1) by XREAL_1: 9;

      (i - j) < 0 by AS, XREAL_1: 49;

      then

       Y4: (n + (i - j)) < (n + 0 ) by XREAL_1: 8;

      reconsider k = ((i + n) - j) as Element of NAT by Y3, INT_1: 3;

      

       Y8: ((n + (i - j)) - 1) < (n - 1) by Y4, XREAL_1: 9;

       Y9:

      now

        assume ((i + n) - j) >= n;

        then (((i + n) - j) - n) >= (n - n) by XREAL_1: 9;

        then ((i - j) + j) >= ( 0 + j) by XREAL_1: 6;

        hence contradiction by AS;

      end;

      reconsider h = (n - j) as Element of NAT by AS, INT_1: 5;

      set p = (( 0_. F) +* ((k,n) --> (( 1. F),( - ( 1. F)))));

      now

        let x be object;

        assume x in {k, n};

        per cases by TARSKI:def 2;

          suppose x = k;

          hence x in NAT ;

        end;

          suppose x = n;

          hence x in NAT ;

        end;

      end;

      then

       A: {k, n} c= NAT ;

      

       B: ( dom ((k,n) --> (( 1. F),( - ( 1. F))))) = {k, n} & ( dom ( 0_. F)) = NAT by FUNCT_2:def 1;

      

      then ( dom p) = ( NAT \/ {k, n}) by FUNCT_4:def 1

      .= NAT by A, XBOOLE_1: 12;

      then ( dom p) = NAT & ( rng p) c= the carrier of F;

      then

      reconsider p as sequence of F by FUNCT_2: 2;

      reconsider p as Element of the carrier of ( Polynom-Ring F) by POLYNOM3:def 10;

      k in ( dom ((k,n) --> (( 1. F),( - ( 1. F))))) by TARSKI:def 2, B;

      

      then (p . k) = (((k,n) --> (( 1. F),( - ( 1. F)))) . k) by FUNCT_4: 13

      .= ( 1. F) by Y4, FUNCT_4: 63;

      then p <> ( 0_. F);

      then

      reconsider p as non zero Element of the carrier of ( Polynom-Ring F) by UPROOTS:def 5;

      reconsider p1 = p, ma1 = ma as non zero Polynomial of F;

      reconsider q1 = (p1 + ma1) as Polynomial of F;

      now

        assume

         K: (p1 + ma1) = ( 0_. F);

        

         K1: ( - p1) = (( - p1) + ( 0_. F))

        .= ((p1 - p1) + ma1) by K, POLYNOM3: 26

        .= (( 0_. F) + ma1) by POLYNOM3: 29;

        set q = (( 0_. F) +* (((((n + i) - j) - 1),(n - 1)) --> (( - ( 1. F)),( 1. F))));

        now

          let x be object;

          assume x in {(((n + i) - j) - 1), (n - 1)};

          per cases by TARSKI:def 2;

            suppose x = (((n + i) - j) - 1);

            hence x in NAT by Y7, INT_1: 3;

          end;

            suppose x = (n - 1);

            hence x in NAT by AS, INT_1: 3;

          end;

        end;

        then

         Z2: {(((n + i) - j) - 1), (n - 1)} c= NAT ;

        

         Z3: ( dom (((((n + i) - j) - 1),(n - 1)) --> (( - ( 1. F)),( 1. F)))) = {(((n + i) - j) - 1), (n - 1)} & ( dom ( 0_. F)) = NAT by FUNCT_2:def 1;

        

        then ( dom q) = ( NAT \/ {(((n + i) - j) - 1), (n - 1)}) by FUNCT_4:def 1

        .= NAT by Z2, XBOOLE_1: 12;

        then ( dom q) = NAT & ( rng q) c= the carrier of F;

        then

        reconsider q as sequence of F by FUNCT_2: 2;

        reconsider q as Polynomial of F;

        

         K: ( <%( 0. F), ( 1. F)%> *' q) = ( - p1)

        proof

          now

            let u be Element of NAT ;

            per cases ;

              suppose

               K2: u = 0 ;

              then

               K3: not u in ( dom ((k,n) --> (( 1. F),( - ( 1. F))))) by AS, Y3;

              

               K4: ( 0. F) = (( 0_. F) . u)

              .= (p1 . u) by K3, FUNCT_4: 11;

              

              thus (( <%( 0. F), ( 1. F)%> *' q) . u) = ( - (p1 . u)) by K4, K2, thE2

              .= (( - p1) . u) by BHSP_1: 44;

            end;

              suppose u <> 0 ;

              then

              consider u1 be Nat such that

               K2: u = (u1 + 1) by NAT_1: 6;

              

               K5: (( <%( 0. F), ( 1. F)%> *' q) . u) = (q . u1) by K2, thE1;

              per cases ;

                suppose

                 K6: u = k;

                k in ( dom ((k,n) --> (( 1. F),( - ( 1. F))))) by TARSKI:def 2, B;

                

                then

                 K7: (p . k) = (((k,n) --> (( 1. F),( - ( 1. F)))) . k) by FUNCT_4: 13

                .= ( 1. F) by Y4, FUNCT_4: 63;

                

                 K8: u1 in ( dom (((((n + i) - j) - 1),(n - 1)) --> (( - ( 1. F)),( 1. F)))) by K2, K6, Z3, TARSKI:def 2;

                ((((((n + i) - j) - 1),(n - 1)) --> (( - ( 1. F)),( 1. F))) . u1) = ( - ( 1. F)) by K2, K6, Y8, FUNCT_4: 63;

                

                hence (( <%( 0. F), ( 1. F)%> *' q) . u) = ( - ( 1. F)) by K8, K5, FUNCT_4: 13

                .= (( - p1) . u) by K6, K7, BHSP_1: 44;

              end;

                suppose

                 K6: u = n;

                n in ( dom ((k,n) --> (( 1. F),( - ( 1. F))))) by TARSKI:def 2, B;

                

                then

                 K7: (p . n) = (((k,n) --> (( 1. F),( - ( 1. F)))) . n) by FUNCT_4: 13

                .= ( - ( 1. F)) by FUNCT_4: 63;

                

                 K8: u1 in ( dom (((((n + i) - j) - 1),(n - 1)) --> (( - ( 1. F)),( 1. F)))) by K2, K6, Z3, TARSKI:def 2;

                ((((((n + i) - j) - 1),(n - 1)) --> (( - ( 1. F)),( 1. F))) . u1) = ( 1. F) by K2, K6, FUNCT_4: 63;

                

                hence (( <%( 0. F), ( 1. F)%> *' q) . u) = ( - (p1 . u)) by K6, K7, K8, K5, FUNCT_4: 13

                .= (( - p1) . u) by BHSP_1: 44;

              end;

                suppose

                 K6: u <> k & u <> n;

                then not u in ( dom ((k,n) --> (( 1. F),( - ( 1. F))))) by TARSKI:def 2;

                

                then

                 K7: (p . u) = (( 0_. F) . u) by FUNCT_4: 11

                .= ( 0. F);

                u1 <> (((n + i) - j) - 1) & u1 <> (n - 1) by K2, K6;

                then not u1 in ( dom (((((n + i) - j) - 1),(n - 1)) --> (( - ( 1. F)),( 1. F)))) by TARSKI:def 2;

                

                then (q . u1) = (( 0_. F) . u1) by FUNCT_4: 11

                .= ( 0. F) by ORDINAL1:def 12, FUNCOP_1: 7;

                

                hence (( <%( 0. F), ( 1. F)%> *' q) . u) = ( - (p1 . u)) by K7, K2, thE1

                .= (( - p1) . u) by BHSP_1: 44;

              end;

            end;

          end;

          hence thesis;

        end;

        ( eval ( <%( 0. F), ( 1. F)%>,( 0. F))) = (( 0. F) + ( 0. F)) by POLYNOM5: 47;

        then <%( 0. F), ( 1. F)%> is with_roots by POLYNOM5:def 7, POLYNOM5:def 8;

        hence contradiction by K, K1, X;

      end;

      then

      reconsider q1 as non zero Polynomial of F by UPROOTS:def 5;

      reconsider q = q1 as Element of the carrier of ( Polynom-Ring F) by POLYNOM3:def 10;

      

       X: F is Subring of E by FIELD_4:def 1;

      now

        assume

         A0: (a |^ i) = (a |^ j);

        

         A1: (a |^ k) = (a |^ (i + h))

        .= ((a |^ i) * (a |^ h)) by BINOM: 10

        .= (a |^ (j + h)) by A0, BINOM: 10

        .= (a |^ n);

        

         A: ( deg q) < ( deg ma)

        proof

           D:

          now

            assume

             B0: ( deg q1) = ( deg ma1);

            

             B2: (( deg ma1) + 1) = ((( len ma1) - 1) + 1) & (( deg q1) + 1) = ((( len q1) - 1) + 1) by HURWITZ:def 2;

            

             B3: (( len ma1) -' 1) = n by B2, XREAL_0:def 2;

            n in ( dom ((k,n) --> (( 1. F),( - ( 1. F))))) by TARSKI:def 2, B;

            

            then (p . n) = (((k,n) --> (( 1. F),( - ( 1. F)))) . n) by FUNCT_4: 13

            .= ( - ( 1. F)) by FUNCT_4: 63;

            

            then (q1 . n) = (( - ( 1. F)) + (ma1 . n)) by NORMSP_1:def 2

            .= (( - ( 1. F)) + ( LC ma1)) by B3, RATFUNC1:def 6

            .= (( - ( 1. F)) + ( 1. F)) by RATFUNC1:def 7;

            hence contradiction by B2, B0, ALGSEQ_1: 10, RLVECT_1: 5;

          end;

          now

            assume

             G: ( deg p1) > n;

            

             B3: (( deg p1) + 1) = ((( len p1) - 1) + 1) by HURWITZ:def 2;

             not ( deg p1) in ( dom ((k,n) --> (( 1. F),( - ( 1. F))))) by G, Y9, TARSKI:def 2;

            

            then (p1 . ( deg p1)) = (( 0_. F) . ( deg p1)) by FUNCT_4: 11

            .= ( 0. F);

            hence contradiction by B3, ALGSEQ_1: 10;

          end;

          then ( max (( deg p1),( deg ma1))) = ( deg ma1) by XXREAL_0:def 10;

          then ( deg q) <= ( deg ma1) by HURWITZ: 22;

          hence thesis by D, XXREAL_0: 1;

        end;

        reconsider pE = (( anpoly (( 1. E),k)) + ( anpoly (( - ( 1. E)),n))) as Element of the carrier of ( Polynom-Ring E) by POLYNOM3:def 10;

        p = (( anpoly (( 1. E),k)) + ( anpoly (( - ( 1. E)),n)))

        proof

          set g = (( anpoly (( 1. E),k)) + ( anpoly (( - ( 1. E)),n)));

          now

            let u be Element of NAT ;

            per cases ;

              suppose

               H: u = k;

              k in ( dom ((k,n) --> (( 1. F),( - ( 1. F))))) by TARSKI:def 2, B;

              

              then

               H1: (p . k) = (((k,n) --> (( 1. F),( - ( 1. F)))) . k) by FUNCT_4: 13

              .= ( 1. F) by Y4, FUNCT_4: 63;

              

              thus (g . u) = ((( anpoly (( 1. E),k)) . u) + (( anpoly (( - ( 1. E)),n)) . u)) by NORMSP_1:def 2

              .= ((( anpoly (( 1. E),k)) . u) + ( 0. E)) by Y4, H, POLYDIFF: 25

              .= (( 1. E) + ( 0. E)) by H, POLYDIFF: 24

              .= (p . u) by H1, H, X, C0SP1:def 3;

            end;

              suppose

               H: u = n;

              n in ( dom ((k,n) --> (( 1. F),( - ( 1. F))))) by TARSKI:def 2, B;

              

              then

               H1: (p . n) = (((k,n) --> (( 1. F),( - ( 1. F)))) . n) by FUNCT_4: 13

              .= ( - ( 1. F)) by FUNCT_4: 63;

              

               H2: ( 1. E) = ( 1. F) by X, C0SP1:def 3;

              

              thus (g . u) = ((( anpoly (( 1. E),k)) . u) + (( anpoly (( - ( 1. E)),n)) . u)) by NORMSP_1:def 2

              .= (( 0. E) + (( anpoly (( - ( 1. E)),n)) . u)) by Y4, H, POLYDIFF: 25

              .= (( 0. E) + ( - ( 1. E))) by H, POLYDIFF: 24

              .= (p . u) by H2, H1, H, X, Th19;

            end;

              suppose

               H: u <> k & u <> n;

              then not u in ( dom ((k,n) --> (( 1. F),( - ( 1. F))))) by TARSKI:def 2;

              

              then

               H1: (p . u) = (( 0_. F) . u) by FUNCT_4: 11

              .= ( 0. F);

              

              thus (g . u) = ((( anpoly (( 1. E),k)) . u) + (( anpoly (( - ( 1. E)),n)) . u)) by NORMSP_1:def 2

              .= (( 0. E) + (( anpoly (( - ( 1. E)),n)) . u)) by H, POLYDIFF: 25

              .= (( 0. E) + ( 0. E)) by H, POLYDIFF: 25

              .= (p . u) by H1, X, C0SP1:def 3;

            end;

          end;

          hence thesis;

        end;

        

        then

         B: ( Ext_eval (p,a)) = ( eval (pE,a)) by FIELD_4: 26

        .= (( eval (( anpoly (( 1. E),k)),a)) + ( eval (( anpoly (( - ( 1. E)),n)),a))) by POLYNOM4: 19

        .= ((( 1. E) * (a |^ k)) + ( eval (( anpoly (( - ( 1. E)),n)),a))) by Y3, FIELD_1: 6

        .= ((( 1. E) * (a |^ k)) + (( - ( 1. E)) * (a |^ k))) by A1, AS, FIELD_1: 6

        .= ((( 1. E) + ( - ( 1. E))) * (a |^ k)) by VECTSP_1:def 3

        .= (( 0. E) * (a |^ k)) by RLVECT_1: 5;

        ( Ext_eval (q,a)) = (( Ext_eval (p,a)) + ( Ext_eval (ma,a))) by X, ALGNUM_1: 15

        .= (( 0. E) + ( 0. E)) by B, mpol3;

        hence contradiction by mpol4, A, RING_5: 13;

      end;

      hence thesis;

    end;

    theorem :: FIELD_6:56

    

     ch1: for F be Field, E be ( Polynom-Ring F) -homomorphic FieldExtension of F, a be Element of E holds a is F -algebraic iff ( FAdj (F, {a})) = ( RAdj (F, {a}))

    proof

      let F be Field, E be ( Polynom-Ring F) -homomorphic FieldExtension of F, a be Element of E;

      set f = ( hom_Ext_eval (a,F));

       A:

      now

        assume a is F -algebraic;

        then

        reconsider b = a as F -algebraic Element of E;

        (( Polynom-Ring F) / ( {( MinPoly (b,F))} -Ideal )) is Field;

        then

         A1: (( Polynom-Ring F) / ( ker f)) is Field by mpol1;

        ((( Polynom-Ring F) / ( ker f)),( Image f)) are_isomorphic by RING_2: 15;

        then

        reconsider K = ( Image f) as (( Polynom-Ring F) / ( ker f)) -isomorphic Ring by RING_3:def 4;

        K is Field by A1;

        then ( RAdj (F, {a})) is Field by lemphi4;

        hence ( FAdj (F, {a})) = ( RAdj (F, {a})) by RF2;

      end;

      now

        assume ( FAdj (F, {a})) = ( RAdj (F, {a}));

        then

         B1: ( Image f) is Field by lemphi4;

        (( Image f),(( Polynom-Ring F) / ( ker f))) are_isomorphic by RING_2: 15;

        then

        reconsider K = (( Polynom-Ring F) / ( ker f)) as ( Image f) -isomorphic Ring by RING_3:def 4;

        

         B2: K is Field by B1;

        ( {( 0. ( Polynom-Ring F))} -Ideal ) = {( 0. ( Polynom-Ring F))} by IDEAL_1: 47;

        hence a is F -algebraic by B2, RING_1: 21;

      end;

      hence thesis by A;

    end;

    theorem :: FIELD_6:57

    for F be Field, E be ( Polynom-Ring F) -homomorphic FieldExtension of F holds for a be non zero Element of E holds a is F -algebraic iff (a " ) in ( RAdj (F, {a}))

    proof

      let F be Field, E be ( Polynom-Ring F) -homomorphic FieldExtension of F;

      let a be non zero Element of E;

      

       X: F is Subring of E by FIELD_4:def 1;

       A:

      now

        assume a is F -algebraic;

        then

         A1: ( FAdj (F, {a})) = ( RAdj (F, {a})) by ch1;

        

         A2: {a} is Subset of ( FAdj (F, {a})) by FAt;

        a in {a} by TARSKI:def 1;

        then

        reconsider b = a as Element of the carrier of ( FAdj (F, {a})) by A2;

        (b " ) in the carrier of ( FAdj (F, {a}));

        hence (a " ) in ( RAdj (F, {a})) by A1, Th19f;

      end;

      now

        assume (a " ) in ( RAdj (F, {a}));

        then (a " ) in the set of all ( Ext_eval (p,a)) where p be Polynomial of F by lemphi5;

        then

        consider p be Polynomial of F such that

         A1: (a " ) = ( Ext_eval (p,a));

        set r = (( - ( 1. F)) | F);

        set q = ((( rpoly (1,( 0. F))) *' p) + r);

        ( - ( 0. F)) = ( 0. F);

        then ( - ( 1. F)) <> ( 0. F);

        then

         B0: ( deg r) = 0 by RING_4: 21;

        

         B5: ( deg ( rpoly (1,( 0. F)))) = 1 by HURWITZ: 27;

        q is non zero

        proof

          per cases ;

            suppose p = ( 0_. F);

            hence thesis by B0, HURWITZ: 20;

          end;

            suppose

             B3: p <> ( 0_. F);

            then

            reconsider degp = ( deg p) as Element of NAT by FIELD_1: 1;

            

             B4: ( deg (( rpoly (1,( 0. F))) *' p)) = (( deg ( rpoly (1,( 0. F)))) + degp) by B3, HURWITZ: 23;

            ( deg q) = ( max ((( deg ( rpoly (1,( 0. F)))) + ( deg p)), 0 )) by B0, B4, B5, HURWITZ: 21

            .= (( deg ( rpoly (1,( 0. F)))) + degp) by XXREAL_0:def 10;

            then q <> ( 0_. F) by HURWITZ: 20;

            hence thesis by UPROOTS:def 5;

          end;

        end;

        then

        reconsider q as non zero Polynomial of F;

        ( 1. E) = ( 1. F) by X, C0SP1:def 3;

        

        then

         A2: ( - ( 1. E)) = (( - ( 1. F)) * ( 1. F)) by X, Th19

        .= (( - ( 1. F)) * ( LC ( 1_. F))) by RATFUNC1:def 7

        .= ( LC (( - ( 1. F)) * ( 1_. F))) by RATFUNC1: 18

        .= ( LC (( - ( 1. F)) | F)) by RING_4: 16;

        

         A3: ( 0. E) = ( 0. F) by X, C0SP1:def 3;

        reconsider rpE = ( rpoly (1,( 0. E))) as Element of the carrier of ( Polynom-Ring E) by POLYNOM3:def 10;

        reconsider rpF = ( rpoly (1,( 0. F))) as Element of the carrier of ( Polynom-Ring F) by POLYNOM3:def 10;

        

         A5: a <> ( 0. E);

        ( Ext_eval (q,a)) = (( Ext_eval ((( rpoly (1,( 0. F))) *' p),a)) + ( Ext_eval (r,a))) by X, ALGNUM_1: 15

        .= ((( Ext_eval (( rpoly (1,( 0. F))),a)) * (a " )) + ( Ext_eval (r,a))) by X, A1, ALGNUM_1: 20

        .= ((( Ext_eval (rpF,a)) * (a " )) + ( - ( 1. E))) by A2, exevalconst

        .= ((( eval (rpE,a)) * (a " )) + ( - ( 1. E))) by A3, FIELD_4: 21, FIELD_4: 26

        .= (((a - ( 0. E)) * (a " )) + ( - ( 1. E))) by HURWITZ: 29

        .= (((a " ) * a) + ( - ( 1. E))) by GROUP_1:def 12

        .= (( 1. E) + ( - ( 1. E))) by A5, VECTSP_1:def 10

        .= ( 0. E) by RLVECT_1: 5;

        hence a is F -algebraic by alg00;

      end;

      hence thesis by A;

    end;

    theorem :: FIELD_6:58

    for F be Field, E be FieldExtension of F holds for a be Element of E holds a is F -transcendental iff (( RAdj (F, {a})),( Polynom-Ring F)) are_isomorphic

    proof

      let F be Field, E be FieldExtension of F;

      let a be Element of E;

      reconsider E1 = E as ( Polynom-Ring F) -homomorphic Field;

      reconsider g = ( hom_Ext_eval (a,F)) as Homomorphism of ( Polynom-Ring F), E1;

      

       H: ((( Polynom-Ring F) / ( ker g)),( Image g)) are_isomorphic by RING_2: 15;

       A:

      now

        assume a is F -transcendental;

        then ((( Polynom-Ring F) / ( ker g)),( Polynom-Ring F)) are_isomorphic by RING_2: 17;

        then (( Polynom-Ring F),( Image g)) are_isomorphic by H, RING_3: 44;

        hence (( Polynom-Ring F),( RAdj (F, {a}))) are_isomorphic by lemphi4;

      end;

      now

        assume (( RAdj (F, {a})),( Polynom-Ring F)) are_isomorphic ;

        then ( Polynom-Ring F) is ( RAdj (F, {a})) -isomorphic by RING_3:def 4;

        then ( RAdj (F, {a})) <> ( FAdj (F, {a}));

        hence a is F -transcendental by ch1;

      end;

      hence thesis by A;

    end;

    theorem :: FIELD_6:59

    for F be Field, E be ( Polynom-Ring F) -homomorphic FieldExtension of F holds for a be F -algebraic Element of E holds ((( Polynom-Ring F) / ( {( MinPoly (a,F))} -Ideal )),( FAdj (F, {a}))) are_isomorphic

    proof

      let F be Field, E be ( Polynom-Ring F) -homomorphic FieldExtension of F;

      let a be F -algebraic Element of E;

      set f = ( hom_Ext_eval (a,F));

      ((( Polynom-Ring F) / ( ker f)),( Image f)) are_isomorphic by RING_2: 15;

      then ((( Polynom-Ring F) / ( {( MinPoly (a,F))} -Ideal )),( Image f)) are_isomorphic by mpol1;

      then ((( Polynom-Ring F) / ( {( MinPoly (a,F))} -Ideal )),( RAdj (F, {a}))) are_isomorphic by lemphi4;

      hence thesis by ch1;

    end;

    begin

    definition

      let F be Field, E be FieldExtension of F;

      let a be F -algebraic Element of E;

      :: FIELD_6:def8

      func Base a -> non empty Subset of ( VecSp (( FAdj (F, {a})),F)) equals { (a |^ n) where n be Element of NAT : n < ( deg ( MinPoly (a,F))) };

      coherence

      proof

        set M = { (a |^ n) where n be Element of NAT : n < ( deg ( MinPoly (a,F))) };

        

         X: ( FAdj (F, {a})) is Subring of E by FIELD_5: 12;

        ( deg ( MinPoly (a,F))) > 0 by RING_4:def 4;

        then

         A: (a |^ 0 ) in M;

        now

          let o be object;

          assume o in M;

          then

          consider n be Element of NAT such that

           H: o = (a |^ n) & n < ( deg ( MinPoly (a,F)));

          

           I: the carrier of ( VecSp (( FAdj (F, {a})),F)) = the carrier of ( FAdj (F, {a})) by FIELD_4:def 6;

          reconsider U = {a} as Subset of E;

          

           K: {a} is Subset of the carrier of ( FAdj (F, {a})) by FAt;

          a in {a} by TARSKI:def 1;

          then

          reconsider a1 = a as Element of ( FAdj (F, {a})) by K;

          (a1 |^ n) in the carrier of ( FAdj (F, {a}));

          hence o in the carrier of ( VecSp (( FAdj (F, {a})),F)) by I, H, X, pr5;

        end;

        hence thesis by A, TARSKI:def 3;

      end;

    end

    registration

      let F be Field, E be FieldExtension of F;

      let a be F -algebraic Element of E;

      cluster ( Base a) -> finite;

      coherence

      proof

        reconsider n = ( deg ( MinPoly (a,F))) as Element of NAT ;

        deffunc F( Nat) = (a |^ $1);

        defpred P[ Nat] means $1 < n;

        

         D: { F(i) where i be Nat : i <= n & P[i] } is finite from FINSEQ_1:sch 6;

         E:

        now

          let o be object;

          assume o in { F(i) where i be Nat : i <= n & P[i] };

          then

          consider i be Nat such that

           E1: o = (a |^ i) & i <= n & i < n;

          i is Element of NAT by ORDINAL1:def 12;

          hence o in ( Base a) by E1;

        end;

        now

          let o be object;

          assume o in ( Base a);

          then

          consider i be Element of NAT such that

           E1: o = (a |^ i) & i < n;

          thus o in { F(i) where i be Nat : i <= n & P[i] } by E1;

        end;

        hence thesis by D, E, TARSKI: 2;

      end;

    end

    

     lembas1b: for F be Field, E be FieldExtension of F holds for a be F -algebraic Element of E holds for p be Polynomial of F st ( deg p) < ( deg ( MinPoly (a,F))) holds ( Ext_eval (( Leading-Monomial p),a)) in ( Lin ( Base a))

    proof

      let F be Field, E be FieldExtension of F;

      let a be F -algebraic Element of E;

      let p be Polynomial of F;

      assume

       AS: ( deg p) < ( deg ( MinPoly (a,F)));

      set LMp = ( Leading-Monomial p), V = ( VecSp (( FAdj (F, {a})),F)), ma = ( MinPoly (a,F)), K = ( FAdj (F, {a}));

      

       H0a: F is Subring of K by FIELD_4:def 1;

      per cases ;

        suppose

         J: p = ( 0_. F);

        then

         I: LMp = p by POLYNOM4: 13;

        

         H: ( Ext_eval (p,a)) = ( 0. E) by J, ALGNUM_1: 13

        .= ( 0. ( FAdj (F, {a}))) by dFA

        .= ( 0. V) by FIELD_4:def 6

        .= ( Sum ( ZeroLC V)) by VECTSP_6: 15;

        ( ZeroLC V) is Linear_Combination of ( Base a) by VECTSP_6: 5;

        hence thesis by I, H, VECTSP_7: 7;

      end;

        suppose

         J: p <> ( 0_. F);

        then

        reconsider n = ( deg p) as Element of NAT by FIELD_1: 1;

        

         J1: p is non zero by J, UPROOTS:def 5;

        defpred P[ object, object] means ($1 = (a |^ n) & $2 = ( LC p)) or ($1 <> (a |^ n) & $2 = ( 0. F));

        

         A: for x be object st x in the carrier of V holds ex y be object st y in the carrier of F & P[x, y]

        proof

          let x be object;

          assume x in the carrier of V;

          per cases ;

            suppose x = (a |^ n);

            hence ex y be object st y in the carrier of F & P[x, y];

          end;

            suppose x <> (a |^ n);

            hence ex y be object st y in the carrier of F & P[x, y];

          end;

        end;

        consider l be Function of the carrier of V, the carrier of F such that

         L: for x be object st x in the carrier of V holds P[x, (l . x)] from FUNCT_2:sch 1( A);

        reconsider l as Element of ( Funcs (the carrier of V,the carrier of F)) by FUNCT_2: 8;

        for v be Element of V st not v in ( Base a) holds (l . v) = ( 0. F)

        proof

          let v be Element of V;

          assume not v in ( Base a);

          then v <> (a |^ n) by AS;

          hence (l . v) = ( 0. F) by L;

        end;

        then

        reconsider l as Linear_Combination of V by VECTSP_6:def 1;

        now

          let o be object;

          assume o in ( Carrier l);

          then

          consider v be Element of V such that

           A1: o = v & (l . v) <> ( 0. F) by VECTSP_6: 1;

          v = (a |^ n) & (l . v) = ( LC p) by L, A1;

          hence o in ( Base a) by A1, AS;

        end;

        then ( Carrier l) c= ( Base a);

        then

        reconsider l as Linear_Combination of ( Base a) by VECTSP_6:def 4;

        

         J5: {a} is Subset of K by FAt;

        a in {a} by TARSKI:def 1;

        then

        reconsider ak = a as Element of K by J5;

        

         J4: K is Subring of E by FIELD_5: 12;

        (ak |^ n) is Element of K;

        then

         A8: (a |^ n) is Element of K by J4, pr5;

        then

        reconsider v = (a |^ n) as Element of V by FIELD_4:def 6;

        the carrier of F c= the carrier of K & the carrier of K c= the carrier of E by H0a, C0SP1:def 3, EC_PF_1:def 1;

        then

        reconsider p0 = ( LC p) as Element of E;

        reconsider a0 = (a |^ n) as Element of E;

        

         A3: [(l . v), v] in [:the carrier of F, the carrier of K:] by A8, ZFMISC_1:def 2;

        the carrier of F c= the carrier of K by H0a, C0SP1:def 3;

        then ( LC p) in the carrier of K;

        then

         A4: [p0, a0] in [:the carrier of K, the carrier of K:] by A8, ZFMISC_1:def 2;

        

         A9: ( Carrier l) = {v}

        proof

           Y:

          now

            let o be object;

            assume o in ( Carrier l);

            then

            consider w be Element of V such that

             A9b: o = w & (l . w) <> ( 0. F) by VECTSP_6: 1;

            o = v by A9b, L;

            hence o in {v} by TARSKI:def 1;

          end;

          now

            let o be object;

            assume o in {v};

            then

             A9c: o = v by TARSKI:def 1;

            p is non zero by J, UPROOTS:def 5;

            then (l . v) <> ( 0. F) by L;

            hence o in ( Carrier l) by A9c, VECTSP_6: 1;

          end;

          hence thesis by TARSKI: 2, Y;

        end;

        

         A5: the multF of K = (the multF of E || the carrier of K) by EC_PF_1:def 1;

        ( Sum l) = ((l . v) * v) by A9, VECTSP_6: 20

        .= ((the multF of K | [:the carrier of F, the carrier of K:]) . ((l . v),v)) by FIELD_4:def 6

        .= (the multF of K . ((l . v),v)) by A3, FUNCT_1: 49

        .= (the multF of K . (p0,a0)) by L

        .= (p0 * (a |^ n)) by A4, A5, FUNCT_1: 49

        .= ( Ext_eval (LMp,a)) by J1, exevalLM;

        hence ( Ext_eval (LMp,a)) in ( Lin ( Base a)) by VECTSP_7: 7;

      end;

    end;

    

     lembas1a: for F be Field, E be ( Polynom-Ring F) -homomorphic FieldExtension of F holds for a be F -algebraic Element of E holds for p be Polynomial of F st ( deg p) < ( deg ( MinPoly (a,F))) holds ( Ext_eval (p,a)) in ( Lin ( Base a))

    proof

      let F be Field, E be ( Polynom-Ring F) -homomorphic FieldExtension of F;

      let a be F -algebraic Element of E;

      let p be Polynomial of F;

      assume

       ASdeg: ( deg p) < ( deg ( MinPoly (a,F)));

      

       H0: F is Subring of E by FIELD_4:def 1;

      set V = ( VecSp (( FAdj (F, {a})),F)), ma = ( MinPoly (a,F)), K = ( FAdj (F, {a}));

      ( deg ma) >= ( 0 + 1) by INT_1: 7, RING_4:def 4;

      then

      reconsider degma = (( deg ( MinPoly (a,F))) - 1) as Element of NAT by INT_1: 3;

      

       H0a: F is Subring of K by FIELD_4:def 1;

      per cases ;

        suppose p = ( 0_. F);

        

        then

         H: ( Ext_eval (p,a)) = ( 0. E) by ALGNUM_1: 13

        .= ( 0. ( FAdj (F, {a}))) by dFA

        .= ( 0. V) by FIELD_4:def 6

        .= ( Sum ( ZeroLC V)) by VECTSP_6: 15;

        ( ZeroLC V) is Linear_Combination of ( Base a) by VECTSP_6: 5;

        hence thesis by H, VECTSP_7: 7;

      end;

        suppose

         X: p <> ( 0_. F);

        defpred Q[ Nat] means for p be Polynomial of F st ( deg p) = $1 holds ( Ext_eval (p,a)) in ( Lin ( Base a));

        

         IA: Q[ 0 ]

        proof

          now

            let p be Polynomial of F;

            assume

             AS1: ( deg p) = 0 ;

            then

             AS: p is constant by RATFUNC1:def 2;

            defpred P[ object, object] means ($1 = (a |^ 0 ) & $2 = (p . 0 )) or ($1 <> (a |^ 0 ) & $2 = ( 0. F));

            

             A: for x be object st x in the carrier of V holds ex y be object st y in the carrier of F & P[x, y]

            proof

              let x be object;

              assume x in the carrier of V;

              per cases ;

                suppose x = (a |^ 0 );

                hence ex y be object st y in the carrier of F & P[x, y];

              end;

                suppose x <> (a |^ 0 );

                hence ex y be object st y in the carrier of F & P[x, y];

              end;

            end;

            consider l be Function of the carrier of V, the carrier of F such that

             L: for x be object st x in the carrier of V holds P[x, (l . x)] from FUNCT_2:sch 1( A);

            reconsider l as Element of ( Funcs (the carrier of V,the carrier of F)) by FUNCT_2: 8;

            

             A2: not (( deg ( MinPoly (a,F))) <= 0 ) by RING_4:def 4;

            for v be Element of V st not v in ( Base a) holds (l . v) = ( 0. F)

            proof

              let v be Element of V;

              assume not v in ( Base a);

              then v <> (a |^ 0 ) by A2;

              hence (l . v) = ( 0. F) by L;

            end;

            then

            reconsider l as Linear_Combination of V by VECTSP_6:def 1;

            now

              let o be object;

              assume o in ( Carrier l);

              then

              consider v be Element of V such that

               A1: o = v & (l . v) <> ( 0. F) by VECTSP_6: 1;

              v = (a |^ 0 ) & (l . v) = (p . 0 ) by L, A1;

              hence o in ( Base a) by A1, A2;

            end;

            then ( Carrier l) c= ( Base a);

            then

            reconsider l as Linear_Combination of ( Base a) by VECTSP_6:def 4;

            

             A6: (a |^ 0 ) = ( 1_ E) by BINOM: 8

            .= ( 1. F) by H0, C0SP1:def 3;

            then

             A8: (a |^ 0 ) = ( 1. K) by H0a, C0SP1:def 3;

            then

            reconsider v = (a |^ 0 ) as Element of V by FIELD_4:def 6;

            the carrier of F c= the carrier of K by H0a, C0SP1:def 3;

            then

            reconsider p0 = (p . 0 ) as Element of K;

            reconsider a0 = (a |^ 0 ) as Element of K by A8;

            

             A3: [(l . v), v] in [:the carrier of F, the carrier of K:] by A8, ZFMISC_1:def 2;

             0 = (( len p) - 1) by AS1, HURWITZ:def 2;

            

            then

             A5: ( LC p) = (p . (1 -' 1)) by RATFUNC1:def 6

            .= (p . (1 - 1)) by XREAL_0:def 2;

            

             A7: [(p . 0 ), ( 1. F)] in [:the carrier of F, the carrier of F:] by ZFMISC_1:def 2;

            

             A9: ( Carrier l) = {v}

            proof

               Y:

              now

                let o be object;

                assume o in ( Carrier l);

                then

                consider w be Element of V such that

                 A9b: o = w & (l . w) <> ( 0. F) by VECTSP_6: 1;

                o = v by A9b, L;

                hence o in {v} by TARSKI:def 1;

              end;

              now

                let o be object;

                assume o in {v};

                then

                 A9c: o = v by TARSKI:def 1;

                p <> ( 0_. F) by AS1, HURWITZ: 20;

                then p is non zero by UPROOTS:def 5;

                then (l . v) <> ( 0. F) by L, A5;

                hence o in ( Carrier l) by A9c, VECTSP_6: 1;

              end;

              hence thesis by TARSKI: 2, Y;

            end;

            ( Sum l) = ((l . v) * v) by A9, VECTSP_6: 20

            .= ((the multF of K | [:the carrier of F, the carrier of K:]) . ((l . v),v)) by FIELD_4:def 6

            .= (the multF of K . ((l . v),v)) by A3, FUNCT_1: 49

            .= (the multF of K . ((p . 0 ),( 1. F))) by L, A6

            .= ((the multF of K || the carrier of F) . ((p . 0 ),( 1. F))) by A7, FUNCT_1: 49

            .= ((p . 0 ) * ( 1. F)) by H0a, C0SP1:def 3

            .= ( Ext_eval (p,a)) by A5, AS, exevalconst;

            hence ( Ext_eval (p,a)) in ( Lin ( Base a)) by VECTSP_7: 7;

          end;

          hence Q[ 0 ];

        end;

        

         IS: for k be Element of NAT st 0 <= k & k < degma holds (for j be Element of NAT st 0 <= j & j <= k holds Q[j]) implies Q[(k + 1)]

        proof

          let k be Element of NAT ;

          assume

           IV0: 0 <= k & k < degma;

          assume

           IV1: for j be Element of NAT st 0 <= j & j <= k holds Q[j];

          now

            let p be Polynomial of F;

            assume

             IS0: ( deg p) = (k + 1);

            

             IS: ( deg p) = (( len p) - 1) by HURWITZ:def 2;

            then ( len p) <> 0 by IS0;

            then

            consider r be Polynomial of F such that

             IS1: ( len r) < ( len p) & p = (r + ( Leading-Monomial p)) & for n be Element of NAT st n < (( len p) - 1) holds (r . n) = (p . n) by POLYNOM4: 16;

            (( len r) - 1) < (( len p) - 1) by IS1, XREAL_1: 9;

            then

             IS3: ( deg r) < ( deg p) by IS, HURWITZ:def 2;

            

             IS4: (k + 1) < (degma + 1) by IV0, XREAL_1: 8;

            per cases ;

              suppose r = ( 0_. F);

              hence ( Ext_eval (p,a)) in ( Lin ( Base a)) by IS1, IS4, IS0, lembas1b;

            end;

              suppose r <> ( 0_. F);

              then

              reconsider degr = ( deg r) as Element of NAT by FIELD_1: 1;

              degr <= k by IS3, IS0, NAT_1: 13;

              then

              consider lr be Linear_Combination of ( Base a) such that

               IS5: ( Ext_eval (r,a)) = ( Sum lr) by IV1, VECTSP_7: 7;

              set LMp = ( Leading-Monomial p);

              ( Ext_eval (LMp,a)) in ( Lin ( Base a)) by IS4, IS0, lembas1b;

              then

              consider l be Linear_Combination of ( Base a) such that

               IS6: ( Ext_eval (LMp,a)) = ( Sum l) by VECTSP_7: 7;

              reconsider ls = (l + lr) as Linear_Combination of ( Base a) by VECTSP_6: 24;

              ( Ext_eval (LMp,a)) in the set of all ( Ext_eval (p,a)) where p be Polynomial of F;

              then ( Ext_eval (LMp,a)) in ( RAdj (F, {a})) by lemphi5;

              then

               IS8: ( Ext_eval (LMp,a)) in ( FAdj (F, {a})) by ch1;

              ( Ext_eval (r,a)) in the set of all ( Ext_eval (p,a)) where p be Polynomial of F;

              then ( Ext_eval (r,a)) in ( RAdj (F, {a})) by lemphi5;

              then ( Ext_eval (r,a)) in ( FAdj (F, {a})) by ch1;

              then

               IS7: [( Sum l), ( Sum lr)] in [:the carrier of K, the carrier of K:] by IS5, IS6, IS8, ZFMISC_1:def 2;

              ( Sum ls) = (( Sum l) + ( Sum lr)) by VECTSP_6: 44

              .= (the addF of K . (( Sum l),( Sum lr))) by FIELD_4:def 6

              .= ((the addF of E || the carrier of K) . (( Sum l),( Sum lr))) by EC_PF_1:def 1

              .= (( Ext_eval (LMp,a)) + ( Ext_eval (r,a))) by IS5, IS6, IS7, FUNCT_1: 49

              .= ( Ext_eval (p,a)) by IS1, H0, ALGNUM_1: 15;

              hence ( Ext_eval (p,a)) in ( Lin ( Base a)) by VECTSP_7: 7;

            end;

          end;

          hence Q[(k + 1)];

        end;

        

         I: for j be Element of NAT st 0 <= j & j <= degma holds Q[j] from INT_1:sch 8( IA, IS);

        reconsider degp = ( deg p) as Element of NAT by FIELD_1: 1, X;

        (degp + 1) <= ( deg ma) by ASdeg, INT_1: 7;

        then ((degp + 1) - 1) <= (( deg ma) - 1) by XREAL_1: 9;

        hence thesis by I;

      end;

    end;

    theorem :: FIELD_6:60

    

     lembas1: for F be Field, E be FieldExtension of F holds for a be F -algebraic Element of E holds for p be Polynomial of F holds ( Ext_eval (p,a)) in ( Lin ( Base a))

    proof

      let F be Field, E be FieldExtension of F;

      let a be F -algebraic Element of E;

      let p be Polynomial of F;

      set ma = ( MinPoly (a,F)), r = (p mod ma);

      

       B: F is Subring of E by FIELD_4:def 1;

      

       C: p = (((p div ma) *' ma) + r) by RING_4: 4;

      

       D: ( deg r) < ( deg ma) by FIELD_5: 16;

      ( Ext_eval (p,a)) = (( Ext_eval (((p div ma) *' ma),a)) + ( Ext_eval (r,a))) by C, B, ALGNUM_1: 15

      .= ((( Ext_eval ((p div ma),a)) * ( Ext_eval (ma,a))) + ( Ext_eval (r,a))) by B, ALGNUM_1: 20

      .= ((( Ext_eval ((p div ma),a)) * ( 0. E)) + ( Ext_eval (r,a))) by mpol2

      .= ( Ext_eval (r,a));

      hence thesis by D, lembas1a;

    end;

    theorem :: FIELD_6:61

    

     lembas2a: for F be Field, E be FieldExtension of F holds for a be F -algebraic Element of E holds for l be Linear_Combination of ( Base a) holds ex p be Polynomial of F st ( deg p) < ( deg ( MinPoly (a,F))) & for i be Element of NAT st i < ( deg ( MinPoly (a,F))) holds (p . i) = (l . (a |^ i))

    proof

      let F be Field, E be FieldExtension of F;

      let a be F -algebraic Element of E;

      let l be Linear_Combination of ( Base a);

       not (( deg ( MinPoly (a,F))) <= 0 ) by RING_4:def 4;

      then

      reconsider n = (( deg ( MinPoly (a,F))) - 1) as Element of NAT by INT_1: 3;

      E is ( FAdj (F, {a})) -extending by FIELD_4: 7;

      then

       B: ( VecSp (( FAdj (F, {a})),F)) is Subspace of ( VecSp (E,F)) by FIELD_5: 14;

      consider l2 be Linear_Combination of ( VecSp (E,F)) such that

       K: ( Carrier l2) = ( Carrier l) & for v be Element of ( VecSp (E,F)) st v in ( Carrier l2) holds (l2 . v) = (l . v) by B, lcsub;

      consider p be Polynomial of F such that

       A: ( deg p) <= n & for i be Element of NAT st i <= n holds (p . i) = (l2 . (a |^ i)) by lembasx2;

      take p;

      (( deg p) + 0 ) < ((( deg ( MinPoly (a,F))) - 1) + 1) by A, XREAL_1: 8;

      hence ( deg p) < ( deg ( MinPoly (a,F)));

      now

        let i be Element of NAT ;

        assume i < ( deg ( MinPoly (a,F)));

        then i < (n + 1);

        then

         B: i <= n by NAT_1: 13;

        the carrier of ( VecSp (( FAdj (F, {a})),F)) = the carrier of ( FAdj (F, {a})) by FIELD_4:def 6;

        then

         V1: (a |^ i) is Element of ( VecSp (( FAdj (F, {a})),F)) by lcsub1;

        

         V2: (a |^ i) is Element of ( VecSp (E,F)) by FIELD_4:def 6;

        thus (p . i) = (l . (a |^ i))

        proof

          per cases ;

            suppose (a |^ i) in ( Carrier l2);

            then (l2 . (a |^ i)) = (l . (a |^ i)) by K;

            hence thesis by A, B;

          end;

            suppose

             C: not (a |^ i) in ( Carrier l2);

            

            then (l2 . (a |^ i)) = ( 0. F) by V2, VECTSP_6: 2

            .= (l . (a |^ i)) by V1, C, K, VECTSP_6: 2;

            hence thesis by A, B;

          end;

        end;

      end;

      hence thesis;

    end;

    theorem :: FIELD_6:62

    

     lembas2bb: for F be Field, E be FieldExtension of F holds for a be F -algebraic Element of E holds for l be Linear_Combination of ( Base a), p be non zero Polynomial of F st (l . (a |^ ( deg p))) = ( LC p) & ( Carrier l) = {(a |^ ( deg p))} holds ( Sum l) = ( Ext_eval (( LM p),a))

    proof

      let F be Field, E be FieldExtension of F;

      let a be F -algebraic Element of E;

      let l be Linear_Combination of ( Base a), p be non zero Polynomial of F;

      F is Subring of E by FIELD_4:def 1;

      then

       H2: the carrier of F c= the carrier of E by C0SP1:def 3;

      

       H3: {a} is Subset of ( FAdj (F, {a})) by FAt;

      a in {a} by TARSKI:def 1;

      then

      reconsider a1 = a as Element of ( FAdj (F, {a})) by H3;

      

       H7: ( FAdj (F, {a})) is Subring of E by FIELD_5: 12;

      assume

       A: (l . (a |^ ( deg p))) = ( LC p) & ( Carrier l) = {(a |^ ( deg p))};

      reconsider LCpE = ( LC p) as Element of E by H2;

      F is Subfield of ( FAdj (F, {a})) by FAsub;

      then the carrier of F c= the carrier of ( FAdj (F, {a})) by EC_PF_1:def 1;

      then

      reconsider LCp = ( LC p) as Element of ( FAdj (F, {a}));

      reconsider degp = ( deg p) as Nat;

      

       H8: (a |^ degp) = (a1 |^ degp) by H7, pr5;

      then

      reconsider adegp = (a |^ ( deg p)) as Element of ( FAdj (F, {a}));

      reconsider v = (a |^ ( deg p)) as Element of ( VecSp (( FAdj (F, {a})),F)) by H8, FIELD_4:def 6;

      

       B: E is FieldExtension of ( FAdj (F, {a})) by FIELD_4: 7;

      ( Sum l) = ((l . v) * v) by A, VECTSP_6: 20

      .= (LCp * adegp) by A, Lm12a

      .= (LCpE * (a |^ ( deg p))) by B, Lm12b

      .= ( Ext_eval (( LM p),a)) by exevalLM;

      hence thesis;

    end;

    theorem :: FIELD_6:63

    

     lembas2b: for F be Field, E be FieldExtension of F holds for a be F -algebraic Element of E holds for l be Linear_Combination of ( Base a) holds for p be Polynomial of F st ( deg p) < ( deg ( MinPoly (a,F))) & for i be Element of NAT st i < ( deg ( MinPoly (a,F))) holds (p . i) = (l . (a |^ i)) holds ( Sum l) = ( Ext_eval (p,a))

    proof

      let F be Field, E be FieldExtension of F;

      let a be F -algebraic Element of E;

      let l be Linear_Combination of ( Base a);

      let p be Polynomial of F;

      set V = ( VecSp (( FAdj (F, {a})),F));

      assume

       AS: ( deg p) < ( deg ( MinPoly (a,F))) & for i be Element of NAT st i < ( deg ( MinPoly (a,F))) holds (p . i) = (l . (a |^ i));

      defpred P[ Nat] means for l be Linear_Combination of ( Base a) st ( card ( Carrier l)) = $1 holds for p be Polynomial of F st ( deg p) < ( deg ( MinPoly (a,F))) & for i be Element of NAT st i < ( deg ( MinPoly (a,F))) holds (p . i) = (l . (a |^ i)) holds ( Sum l) = ( Ext_eval (p,a));

      

       IA: P[ 0 ]

      proof

        let l be Linear_Combination of ( Base a);

        assume ( card ( Carrier l)) = 0 ;

        then ( Carrier l) = {} ;

        then

         A2: l = ( ZeroLC V) by VECTSP_6:def 3;

        let p be Polynomial of F;

        assume

         A4: ( deg p) < ( deg ( MinPoly (a,F))) & for i be Element of NAT st i < ( deg ( MinPoly (a,F))) holds (p . i) = (l . (a |^ i));

        now

          let i be Element of NAT ;

          per cases ;

            suppose i >= ( deg ( MinPoly (a,F)));

            then

             A5: i > ( deg p) by A4, XXREAL_0: 2;

            ( deg p) = (( len p) - 1) by HURWITZ:def 2;

            then (i + 1) > ((( len p) - 1) + 1) by A5, XREAL_1: 6;

            hence (p . i) = (( 0_. F) . i) by NAT_1: 13, ALGSEQ_1: 8;

          end;

            suppose

             A5: i < ( deg ( MinPoly (a,F)));

            then (a |^ i) in ( Base a);

            then

            reconsider v = (a |^ i) as Element of V;

            

            thus (p . i) = (l . v) by A4, A5

            .= (( 0_. F) . i) by A2, VECTSP_6: 3;

          end;

        end;

        then p = ( 0_. F);

        

        hence ( Ext_eval (p,a)) = ( 0. E) by ALGNUM_1: 13

        .= ( 0. ( FAdj (F, {a}))) by dFA

        .= ( 0. V) by FIELD_4:def 6

        .= ( Sum l) by A2, VECTSP_6: 15;

      end;

       IS:

      now

        let k be Nat;

        assume

         B0: P[k];

        now

          let l be Linear_Combination of ( Base a);

          assume

           B1: ( card ( Carrier l)) = (k + 1);

          let pp be Polynomial of F;

          assume

           B2: ( deg pp) < ( deg ( MinPoly (a,F))) & for i be Element of NAT st i < ( deg ( MinPoly (a,F))) holds (pp . i) = (l . (a |^ i));

          now

            assume

             C0: pp = ( 0_. F);

            now

              let o be object;

              assume

               C1: o in ( Carrier l);

              ( Carrier l) c= ( Base a) by VECTSP_6:def 4;

              then o in ( Base a) by C1;

              then

              consider n be Element of NAT such that

               C2: o = (a |^ n) & n < ( deg ( MinPoly (a,F)));

              (l . (a |^ n)) = (pp . n) by B2, C2

              .= ( 0. F) by C0;

              hence contradiction by C1, C2, VECTSP_6: 2;

            end;

            then ( Carrier l) = {} by XBOOLE_0:def 1;

            hence contradiction by B1;

          end;

          then

          reconsider p = pp as non zero Polynomial of F by UPROOTS:def 5;

          defpred Q[ object, object] means ($1 = (a |^ ( deg p)) & $2 = ( LC p)) or ($1 <> (a |^ ( deg p)) & $2 = ( 0. F));

          

           A: for x be object st x in the carrier of V holds ex y be object st y in the carrier of F & Q[x, y]

          proof

            let x be object;

            assume x in the carrier of V;

            per cases ;

              suppose x = (a |^ ( deg p));

              hence ex y be object st y in the carrier of F & Q[x, y];

            end;

              suppose x <> (a |^ ( deg p));

              hence ex y be object st y in the carrier of F & Q[x, y];

            end;

          end;

          consider lp be Function of the carrier of V, the carrier of F such that

           L: for x be object st x in the carrier of V holds Q[x, (lp . x)] from FUNCT_2:sch 1( A);

          reconsider lp as Element of ( Funcs (the carrier of V,the carrier of F)) by FUNCT_2: 8;

          for v be Element of V st not v in ( Base a) holds (lp . v) = ( 0. F)

          proof

            let v be Element of V;

            assume not v in ( Base a);

            then v <> (a |^ ( deg p)) by B2;

            hence (lp . v) = ( 0. F) by L;

          end;

          then

          reconsider lp as Linear_Combination of V by VECTSP_6:def 1;

          now

            let o be object;

            assume o in ( Carrier lp);

            then

            consider v be Element of V such that

             A1: o = v & (lp . v) <> ( 0. F) by VECTSP_6: 1;

            v = (a |^ ( deg p)) & (lp . v) = ( LC p) by L, A1;

            hence o in ( Base a) by A1, B2;

          end;

          then ( Carrier lp) c= ( Base a);

          then

          reconsider lp as Linear_Combination of ( Base a) by VECTSP_6:def 4;

          

           X1: {a} is Subset of ( FAdj (F, {a})) by FAt;

          a in {a} by TARSKI:def 1;

          then

          reconsider a1 = a as Element of the carrier of ( FAdj (F, {a})) by X1;

          ( FAdj (F, {a})) is Subring of E by FIELD_5: 12;

          then (a |^ ( deg p)) = (a1 |^ ( deg p)) by pr5;

          then

           X: (a |^ ( deg p)) is Element of V by FIELD_4:def 6;

          

           C0: ( Carrier lp) = {(a |^ ( deg p))}

          proof

             C2:

            now

              let o be object;

              assume o in {(a |^ ( deg p))};

              then

               C3: o = (a |^ ( deg p)) by TARSKI:def 1;

              then (lp . o) <> ( 0. F) by X, L;

              hence o in ( Carrier lp) by X, C3, VECTSP_6: 2;

            end;

            now

              let o be object;

              assume

               C3: o in ( Carrier lp);

              ( Carrier lp) = { v where v be Element of V : (lp . v) <> ( 0. F) } by VECTSP_6:def 2;

              then

              consider v be Element of V such that

               C4: o = v & (lp . v) <> ( 0. F) by C3;

              o = (a |^ ( deg p)) by C4, L;

              hence o in {(a |^ ( deg p))} by TARSKI:def 1;

            end;

            hence thesis by C2, TARSKI: 2;

          end;

          (lp . (a |^ ( deg p))) = ( LC p) by X, L;

          then

           C: ( Ext_eval (( LM p),a)) = ( Sum lp) by C0, lembas2bb;

          set q = (p - ( LM p));

          reconsider lk = (l - lp) as Linear_Combination of ( Base a) by VECTSP_6: 42;

          

           C2: l = (lk + lp)

          proof

            

            thus (lk + lp) = ((l + ( - lp)) + lp) by VECTSP_6:def 11

            .= (l + (( - lp) + lp)) by VECTSP_6: 26

            .= (l + (lp + ( - lp))) by VECTSP_6: 25

            .= (l + (lp - lp)) by VECTSP_6:def 11

            .= (l + ( ZeroLC V)) by VECTSP_6: 43

            .= l by VECTSP_6: 27;

          end;

          

           C3: ( Carrier lk) = (( Carrier l) \ ( Carrier lp))

          proof

             C4:

            now

              let o be object;

              assume o in ( Carrier lk);

              then

              consider v be Element of V such that

               C5: o = v & (lk . v) <> ( 0. F) by VECTSP_6: 1;

               C6:

              now

                assume

                 C7: v = (a |^ ( deg p));

                

                then

                 C9: (l . v) = (p . ( deg p)) by B2

                .= ( LC p) by thLC;

                (lk . v) = ((l . v) - (lp . v)) by VECTSP_6: 40

                .= (( LC p) - ( LC p)) by L, C7, C9;

                hence contradiction by C5, RLVECT_1: 15;

              end;

              then

               C7: not v in ( Carrier lp) by C0, TARSKI:def 1;

              (lk . v) = ((l . v) - (lp . v)) by VECTSP_6: 40

              .= ((l . v) - ( 0. F)) by C6, L;

              then v in ( Carrier l) by C5, VECTSP_6: 2;

              hence o in (( Carrier l) \ ( Carrier lp)) by C7, C5, XBOOLE_0:def 5;

            end;

            now

              let o be object;

              assume o in (( Carrier l) \ ( Carrier lp));

              then

               C5: o in ( Carrier l) & not o in ( Carrier lp) by XBOOLE_0:def 5;

              then

              consider v be Element of V such that

               C6: o = v & (l . v) <> ( 0. F) by VECTSP_6: 1;

              

               C7: o <> (a |^ ( deg p)) by C0, C5, TARSKI:def 1;

              (lk . v) = ((l . v) - (lp . v)) by VECTSP_6: 40

              .= ((l . v) - ( 0. F)) by C6, C7, L;

              hence o in ( Carrier lk) by C6, VECTSP_6: 1;

            end;

            hence thesis by C4, TARSKI: 2;

          end;

          now

            let o be object;

            assume

             C5: o in ( Carrier lp);

            then

             C4: o = (a |^ ( deg p)) by C0, TARSKI:def 1;

            reconsider v = o as Element of V by C5;

            (lp . v) = ( LC p) by L, C4

            .= (pp . ( deg p)) by thLC

            .= (l . v) by C4, B2;

            then (l . v) <> ( 0. F) by C5, VECTSP_6: 2;

            hence o in ( Carrier l) by VECTSP_6: 2;

          end;

          then ( Carrier lp) c= ( Carrier l);

          

          then

           A: ( card (( Carrier l) \ ( Carrier lp))) = (( card ( Carrier l)) - ( card ( Carrier lp))) by CARD_2: 44

          .= ((k + 1) - 1) by B1, C0, CARD_2: 42;

          

           B: ( deg q) < ( deg ( MinPoly (a,F))) by thdLM, B2, XXREAL_0: 2;

          for i be Element of NAT st i < ( deg ( MinPoly (a,F))) holds (q . i) = (lk . (a |^ i))

          proof

            let i be Element of NAT ;

            assume

             B1: i < ( deg ( MinPoly (a,F)));

            ( FAdj (F, {a})) is Subring of E by FIELD_5: 12;

            then (a |^ i) = (a1 |^ i) by pr5;

            then

            reconsider v = (a |^ i) as Element of V by FIELD_4:def 6;

            per cases ;

              suppose

               B3: i = ( deg p);

              

              hence (q . i) = ((p . ( deg p)) - (( LM p) . ( deg p))) by POLYNOM3: 27

              .= ((p . ( deg p)) - (( LM p) . ( deg ( LM p)))) by thdegLM

              .= ((l . v) - (( LM p) . ( deg ( LM p)))) by B3, B2

              .= ((l . v) - ( LC ( LM p))) by thLC

              .= ((l . v) - ( LC p)) by thdegLC

              .= ((l . v) - (lp . v)) by B3, L

              .= (lk . (a |^ i)) by VECTSP_6: 40;

            end;

              suppose

               D2: i <> ( deg p);

              

               D3: (a |^ i) <> (a |^ ( deg p))

              proof

                per cases by D2, XXREAL_0: 1;

                  suppose i < ( deg p);

                  hence thesis by B2, mpol5;

                end;

                  suppose i > ( deg p);

                  hence thesis by B1, mpol5;

                end;

              end;

              p <> ( 0_. F);

              then ( len p) <> 0 by POLYNOM4: 5;

              then (( len p) + 1) > ( 0 + 1) by XREAL_1: 6;

              then ( len p) >= 1 by NAT_1: 13;

              then

               D5: (( len p) -' 1) = (( len p) - 1) by XREAL_0:def 2;

              

               D4: i <> (( len p) -' 1) by D5, D2, HURWITZ:def 2;

              

              thus (q . i) = ((p . i) - (( LM p) . i)) by POLYNOM3: 27

              .= ((p . i) - ( 0. F)) by D4, POLYNOM4:def 1

              .= ((l . v) - ( 0. F)) by B2, B1

              .= ((l . v) - (lp . v)) by D3, L

              .= (lk . (a |^ i)) by VECTSP_6: 40;

            end;

          end;

          then

           D: ( Ext_eval (q,a)) = ( Sum lk) by A, C3, B, B0;

          ( Sum lk) in the carrier of V & ( Sum lp) in the carrier of V;

          then ( Sum lk) in the carrier of ( FAdj (F, {a})) & ( Sum lp) in the carrier of ( FAdj (F, {a})) by FIELD_4:def 6;

          then ( Sum lk) in ( carrierFA {a}) & ( Sum lp) in ( carrierFA {a}) by dFA;

          then

           E: [( Sum lk), ( Sum lp)] in [:( carrierFA {a}), ( carrierFA {a}):] by ZFMISC_1:def 2;

          

          thus ( Sum l) = (( Sum lk) + ( Sum lp)) by C2, VECTSP_6: 44

          .= (the addF of ( FAdj (F, {a})) . (( Sum lk),( Sum lp))) by FIELD_4:def 6

          .= ((the addF of E || ( carrierFA {a})) . (( Sum lk),( Sum lp))) by dFA

          .= (the addF of E . (( Sum lk),( Sum lp))) by E, FUNCT_1: 49

          .= ((( Ext_eval (p,a)) - ( Ext_eval (( LM p),a))) + ( Ext_eval (( LM p),a))) by C, D, exevalminus2

          .= (( Ext_eval (p,a)) + (( - ( Ext_eval (( LM p),a))) + ( Ext_eval (( LM p),a)))) by RLVECT_1:def 3

          .= (( Ext_eval (p,a)) + ( 0. E)) by RLVECT_1: 5

          .= ( Ext_eval (pp,a));

        end;

        hence P[(k + 1)];

      end;

      

       I: for k be Nat holds P[k] from NAT_1:sch 2( IA, IS);

      consider n be Nat such that

       H: ( card ( Carrier l)) = n;

      thus thesis by AS, I, H;

    end;

    theorem :: FIELD_6:64

    

     lembas2: for F be Field, E be FieldExtension of F holds for a be F -algebraic Element of E holds for l be Linear_Combination of ( Base a) holds ( Sum l) = ( 0. F) implies l = ( ZeroLC ( VecSp (( FAdj (F, {a})),F)))

    proof

      let F be Field, E be FieldExtension of F;

      let a be F -algebraic Element of E;

      let l be Linear_Combination of ( Base a);

      assume

       AS: ( Sum l) = ( 0. F);

      set V = ( VecSp (( FAdj (F, {a})),F)), ma = ( MinPoly (a,F));

      

       H: F is Subring of E by FIELD_4:def 1;

      consider p be Polynomial of F such that

       A2: ( deg p) < ( deg ( MinPoly (a,F))) & for i be Element of NAT st i < ( deg ma) holds (p . i) = (l . (a |^ i)) by lembas2a;

      now

        assume

         A3: ( Carrier l) <> {} ;

        set x = the Element of ( Carrier l);

        consider v be Element of V such that

         A5: x = v & (l . v) <> ( 0. F) by A3, VECTSP_6: 1;

        ( Carrier l) c= ( Base a) by VECTSP_6:def 4;

        then v in ( Base a) by A3, A5;

        then

        consider i be Element of NAT such that

         A6: v = (a |^ i) & i < ( deg ( MinPoly (a,F)));

        (p . i) <> ( 0. F) by A2, A6, A5;

        then p <> ( 0_. F);

        then

        reconsider p as non zero Polynomial of F by UPROOTS:def 5;

        reconsider pp = p as non zero Element of the carrier of ( Polynom-Ring F) by POLYNOM3:def 10;

        ( Ext_eval (pp,a)) = ( 0. F) by A2, AS, lembas2b

        .= ( 0. E) by H, C0SP1:def 3;

        hence contradiction by mpol4, A2, RING_5: 13;

      end;

      hence thesis by VECTSP_6:def 3;

    end;

    theorem :: FIELD_6:65

    

     lembas: for F be Field, E be ( Polynom-Ring F) -homomorphic FieldExtension of F holds for a be F -algebraic Element of E holds ( Base a) is Basis of ( VecSp (( FAdj (F, {a})),F))

    proof

      let F be Field, E be ( Polynom-Ring F) -homomorphic FieldExtension of F;

      let a be F -algebraic Element of E;

      set V = ( VecSp (( FAdj (F, {a})),F)), ma = ( MinPoly (a,F));

      

       H0: F is Subring of E by FIELD_4:def 1;

       A:

      now

        let l be Linear_Combination of ( Base a);

        assume

         A1: ( Sum l) = ( 0. V);

        ( 0. V) = ( 0. ( FAdj (F, {a}))) by FIELD_4:def 6

        .= ( 0. E) by dFA

        .= ( 0. F) by H0, C0SP1:def 3;

        then l = ( ZeroLC V) by A1, lembas2;

        hence ( Carrier l) = {} by VECTSP_6:def 3;

      end;

       E:

      now

        let o be object;

        assume o in the carrier of the ModuleStr of V;

        then o in the carrier of ( FAdj (F, {a})) by FIELD_4:def 6;

        then o in the carrier of ( RAdj (F, {a})) by ch1;

        then o in the set of all ( Ext_eval (p,a)) where p be Polynomial of F by lemphi5;

        then

        consider p be Polynomial of F such that

         A1: o = ( Ext_eval (p,a));

        o in ( Lin ( Base a)) by A1, lembas1;

        hence o in the carrier of ( Lin ( Base a));

      end;

      now

        let o be object;

        assume

         G: o in the carrier of ( Lin ( Base a));

        the carrier of ( Lin ( Base a)) c= the carrier of V by VECTSP_4:def 2;

        hence o in the carrier of V by G;

      end;

      then ( Lin ( Base a)) = the ModuleStr of V by VECTSP_4: 31, E, TARSKI: 2;

      hence thesis by A, VECTSP_7:def 3, VECTSP_7:def 1;

    end;

    theorem :: FIELD_6:66

    

     lembascard: for F be Field, E be FieldExtension of F holds for a be F -algebraic Element of E holds ( card ( Base a)) = ( deg ( MinPoly (a,F)))

    proof

      let F be Field, E be FieldExtension of F;

      let a be F -algebraic Element of E;

      set ma = ( MinPoly (a,F)), m = ( deg ( MinPoly (a,F)));

      defpred P[ object, object] means ex x be Element of ( Seg m), y be Element of NAT st $1 = x & y = (x - 1) & $2 = (a |^ y);

      

       B1: for x,y1,y2 be object st x in ( Seg m) & P[x, y1] & P[x, y2] holds y1 = y2;

       B2:

      now

        let x be object;

        assume

         B3: x in ( Seg m);

        then

        reconsider n = x as Element of ( Seg m);

        1 <= n by B3, FINSEQ_1: 1;

        then

        reconsider z = (n - 1) as Element of NAT by INT_1: 3;

        thus ex y be object st P[x, y]

        proof

          take (a |^ z);

          thus thesis;

        end;

      end;

      consider f be Function such that

       C: ( dom f) = ( Seg m) & for x be object st x in ( Seg m) holds P[x, (f . x)] from FUNCT_1:sch 2( B1, B2);

       A1:

      now

        let o be object;

        assume o in ( Base a);

        then

        consider n be Element of NAT such that

         A2: o = (a |^ n) & n < m;

        

         A3: ( 0 + 1) <= (n + 1) & (n + 1) <= m by A2, INT_1: 7;

        then

        reconsider x = (n + 1) as Element of ( Seg m) by FINSEQ_1: 1;

        

         A4: x in ( Seg m) by FINSEQ_1: 1, A3;

         P[x, (f . x)] by C, FINSEQ_1: 1, A3;

        hence o in ( rng f) by A4, C, A2, FUNCT_1:def 3;

      end;

      now

        let o be object;

        assume o in ( rng f);

        then

        consider u be object such that

         A2: u in ( dom f) & o = (f . u) by FUNCT_1:def 3;

         P[u, (f . u)] by C, A2;

        then

        consider x be Element of ( Seg m), y be Element of NAT such that

         A3: u = x & y = (x - 1) & (f . x) = (a |^ y);

         not (( deg ma) <= 0 ) by RING_4:def 4;

        then m in ( Seg m) by FINSEQ_1: 3;

        then 1 <= x & x <= m by FINSEQ_1: 1;

        then y < ((m - 1) + 1) by A3, XREAL_1: 9, NAT_1: 13;

        hence o in ( Base a) by A2, A3;

      end;

      then

       A: ( rng f) = ( Base a) by A1, TARSKI: 2;

      now

        assume not f is one-to-one;

        then

        consider x1,x2 be object such that

         A1: x1 in ( dom f) & x2 in ( dom f) & (f . x1) = (f . x2) & x1 <> x2;

        consider n1 be Element of ( Seg m), y1 be Element of NAT such that

         A2: x1 = n1 & y1 = (n1 - 1) & (f . x1) = (a |^ y1) by A1, C;

        consider n2 be Element of ( Seg m), y2 be Element of NAT such that

         A3: x2 = n2 & y2 = (n2 - 1) & (f . x2) = (a |^ y2) by A1, C;

        n1 <= m & n2 <= m by C, A1, FINSEQ_1: 1;

        then ((y1 + 1) - 1) <= (m - 1) & ((y2 + 1) - 1) <= (m - 1) by A3, A2, XREAL_1: 9;

        then

         A4: y1 < ((m - 1) + 1) & y2 < ((m - 1) + 1) by NAT_1: 13;

        

         A5: y1 <> y2 by A1, A2, A3;

        per cases by A5, XXREAL_0: 1;

          suppose y1 < y2;

          hence contradiction by A1, A2, A3, A4, mpol5;

        end;

          suppose y1 > y2;

          hence contradiction by A1, A2, A3, A4, mpol5;

        end;

      end;

      

      then ( card ( Base a)) = ( card ( Seg m)) by A, C, CARD_1: 70

      .= m by FINSEQ_1: 57;

      hence thesis;

    end;

    theorem :: FIELD_6:67

    for F be Field, E be FieldExtension of F holds for a be F -algebraic Element of E holds ( deg (( FAdj (F, {a})),F)) = ( deg ( MinPoly (a,F)))

    proof

      let F be Field, E be FieldExtension of F;

      let a be F -algebraic Element of E;

      set B = ( Base a), m = ( deg ( MinPoly (a,F)));

      

       B: ( card B) = m by lembascard;

      

       C: B is Basis of ( VecSp (( FAdj (F, {a})),F)) by lembas;

      then

       A: ( VecSp (( FAdj (F, {a})),F)) is finite-dimensional by MATRLIN:def 1;

      then ( dim ( VecSp (( FAdj (F, {a})),F))) = ( deg ( MinPoly (a,F))) by C, B, VECTSP_9:def 1;

      hence thesis by A, FIELD_4:def 7;

    end;

    registration

      let F be Field, E be FieldExtension of F;

      let a be F -algebraic Element of E;

      cluster ( FAdj (F, {a})) -> F -finite;

      coherence

      proof

        ( Base a) is Basis of ( VecSp (( FAdj (F, {a})),F)) by lembas;

        then ( VecSp (( FAdj (F, {a})),F)) is finite-dimensional by MATRLIN:def 1;

        hence ( FAdj (F, {a})) is F -finite by FIELD_4:def 8;

      end;

    end

    theorem :: FIELD_6:68

    for F be Field, E be FieldExtension of F holds for a be Element of E holds a is F -algebraic iff ( FAdj (F, {a})) is F -finite

    proof

      let F be Field, E be FieldExtension of F;

      let a be Element of E;

      now

        assume

         AS: ( FAdj (F, {a})) is F -finite;

        then

        reconsider n = ( deg (( FAdj (F, {a})),F)) as Element of NAT by ORDINAL1:def 12;

        

         H: n = ( dim ( VecSp (( FAdj (F, {a})),F))) by FIELD_4:def 7;

        per cases ;

          suppose ex i,j be Element of NAT st i < j & j <= n & (a |^ i) = (a |^ j);

          then

          consider i,j be Element of NAT such that

           U: i < j & j <= n & (a |^ i) = (a |^ j);

          set p1 = ( <%( 0. F), ( 1. F)%> `^ j), p2 = ( <%( 0. F), ( 1. F)%> `^ i);

          set p = (p1 - p2);

          now

            assume p = ( 0_. F);

            

            then ( 0. F) = (p . j)

            .= ((p1 . j) - (p2 . j)) by POLYNOM3: 27

            .= (( 1. F) - (p2 . j)) by help1

            .= (( 1. F) - ( 0. F)) by U, help2;

            hence contradiction;

          end;

          then

          reconsider p as non zero Polynomial of F by UPROOTS:def 5;

          per cases ;

            suppose

             T: i = 0 ;

            then

             W: (a |^ i) = ( 1_ E) by BINOM: 8;

            ( Ext_eval (p,a)) = (( Ext_eval (p1,a)) - ( Ext_eval (p2,a))) by exevalminus2

            .= (( Ext_eval (p1,a)) - ( Ext_eval (( 1_. F),a))) by T, POLYNOM5: 15

            .= (( Ext_eval (p1,a)) - ( 1. E)) by FIELD_4: 23

            .= ((a |^ j) - ( 1. E)) by U, help3

            .= ( 0. E) by W, U, RLVECT_1: 15;

            hence a is F -algebraic by alg00;

          end;

            suppose

             T: i is non zero;

            ( Ext_eval (p,a)) = (( Ext_eval (p1,a)) - ( Ext_eval (p2,a))) by exevalminus2

            .= ((a |^ j) - ( Ext_eval (p2,a))) by U, help3

            .= ((a |^ j) - (a |^ i)) by T, help3

            .= ( 0. E) by U, RLVECT_1: 15;

            hence a is F -algebraic by alg00;

          end;

        end;

          suppose

           U: not ex i,j be Element of NAT st i < j & j <= n & (a |^ i) = (a |^ j);

          set M = { (a |^ i) where i be Element of NAT : i <= n }, V = ( VecSp (( FAdj (F, {a})),F));

          

           X: {a} is Subset of ( FAdj (F, {a})) by FAt;

          a in {a} by TARSKI:def 1;

          then

          reconsider a1 = a as Element of ( FAdj (F, {a})) by X;

          

           I: M c= the carrier of ( VecSp (( FAdj (F, {a})),F))

          proof

            now

              let o be object;

              assume o in M;

              then

              consider i be Element of NAT such that

               H: o = (a |^ i) & i <= n;

              

               I: the carrier of ( VecSp (( FAdj (F, {a})),F)) = the carrier of ( FAdj (F, {a})) by FIELD_4:def 6;

              ( FAdj (F, {a})) is Subring of E by FIELD_5: 12;

              then (a |^ i) = (a1 |^ i) by pr5;

              hence o in the carrier of ( VecSp (( FAdj (F, {a})),F)) by H, I;

            end;

            hence thesis;

          end;

          M is finite

          proof

            deffunc F( Nat) = (a |^ $1);

            defpred P[ Nat] means $1 <= n;

            

             D: { F(i) where i be Nat : i <= n & P[i] } is finite from FINSEQ_1:sch 6;

             E:

            now

              let o be object;

              assume o in { F(i) where i be Nat : i <= n & P[i] };

              then

              consider i be Nat such that

               E1: o = (a |^ i) & i <= n & i <= n;

              i is Element of NAT by ORDINAL1:def 12;

              hence o in M by E1;

            end;

            now

              let o be object;

              assume o in M;

              then

              consider i be Element of NAT such that

               E1: o = (a |^ i) & i <= n;

              thus o in { F(i) where i be Nat : i <= n & P[i] } by E1;

            end;

            hence thesis by D, E, TARSKI: 2;

          end;

          then

          reconsider M as finite Subset of ( VecSp (( FAdj (F, {a})),F)) by I;

          ( card M) = (n + 1)

          proof

            set m = (n + 1);

            defpred P[ object, object] means ex x be Element of ( Seg m), y be Element of NAT st $1 = x & y = (x - 1) & $2 = (a |^ y);

            

             B1: for x,y1,y2 be object st x in ( Seg m) & P[x, y1] & P[x, y2] holds y1 = y2;

             B2:

            now

              let x be object;

              assume

               B3: x in ( Seg m);

              then

              reconsider i = x as Element of ( Seg m);

              1 <= i by B3, FINSEQ_1: 1;

              then

              reconsider z = (i - 1) as Element of NAT by INT_1: 3;

              thus ex y be object st P[x, y]

              proof

                take (a |^ z);

                thus thesis;

              end;

            end;

            consider f be Function such that

             C: ( dom f) = ( Seg m) & for x be object st x in ( Seg m) holds P[x, (f . x)] from FUNCT_1:sch 2( B1, B2);

             A1:

            now

              let o be object;

              assume o in M;

              then

              consider i be Element of NAT such that

               A2: o = (a |^ i) & i <= n;

              

               A3: ( 0 + 1) <= (i + 1) & (i + 1) <= (n + 1) by A2, XREAL_1: 6;

              then

              reconsider x = (i + 1) as Element of ( Seg m) by FINSEQ_1: 1;

              

               A4: x in ( Seg m) by FINSEQ_1: 1, A3;

               P[x, (f . x)] by C, FINSEQ_1: 1, A3;

              hence o in ( rng f) by A4, C, A2, FUNCT_1:def 3;

            end;

            now

              let o be object;

              assume o in ( rng f);

              then

              consider u be object such that

               A2: u in ( dom f) & o = (f . u) by FUNCT_1:def 3;

               P[u, (f . u)] by C, A2;

              then

              consider x be Element of ( Seg m), y be Element of NAT such that

               A3: u = x & y = (x - 1) & (f . x) = (a |^ y);

              m in ( Seg m) by FINSEQ_1: 3;

              then 1 <= x & x <= m by FINSEQ_1: 1;

              then y < ((m - 1) + 1) by A3, XREAL_1: 9, NAT_1: 13;

              then y <= n by NAT_1: 13;

              hence o in M by A2, A3;

            end;

            then

             A: ( rng f) = M by A1, TARSKI: 2;

            now

              assume not f is one-to-one;

              then

              consider x1,x2 be object such that

               A1: x1 in ( dom f) & x2 in ( dom f) & (f . x1) = (f . x2) & x1 <> x2;

              consider n1 be Element of ( Seg m), y1 be Element of NAT such that

               A2: x1 = n1 & y1 = (n1 - 1) & (f . x1) = (a |^ y1) by A1, C;

              consider n2 be Element of ( Seg m), y2 be Element of NAT such that

               A3: x2 = n2 & y2 = (n2 - 1) & (f . x2) = (a |^ y2) by A1, C;

              n1 <= m & n2 <= m by C, A1, FINSEQ_1: 1;

              then

               A4: y1 < ((m - 1) + 1) & y2 < ((m - 1) + 1) by A3, A2, XREAL_1: 9, NAT_1: 13;

              

               A5: y1 <> y2 by A1, A2, A3;

              

               A6: y1 <= n & y2 <= n by A4, NAT_1: 13;

              per cases by A5, XXREAL_0: 1;

                suppose y1 < y2;

                hence contradiction by U, A1, A2, A3, A6;

              end;

                suppose y1 > y2;

                hence contradiction by U, A1, A2, A3, A6;

              end;

            end;

            

            then ( card M) = ( card ( Seg m)) by A, C, CARD_1: 70

            .= m by FINSEQ_1: 57;

            hence thesis;

          end;

          then ( card M) > n by NAT_1: 13;

          then M is linearly-dependent by H, AS, lemlin;

          then

          consider l be Linear_Combination of M such that

           D1: ( Sum l) = ( 0. V) & ( Carrier l) <> {} by VECTSP_7:def 1;

          set z = the Element of ( Carrier l);

          consider v be Element of V such that

           D2: z = v & (l . v) <> ( 0. F) by D1, VECTSP_6: 1;

          

           H1: M = { (a1 |^ i) where i be Element of NAT : i <= n }

          proof

            

             V: ( FAdj (F, {a})) is Subring of E by FIELD_5: 12;

             A:

            now

              let o be object;

              assume o in M;

              then

              consider i be Element of NAT such that

               B: o = (a |^ i) & i <= n;

              (a |^ i) = (a1 |^ i) by V, pr5;

              hence o in { (a1 |^ i) where i be Element of NAT : i <= n } by B;

            end;

            now

              let o be object;

              assume o in { (a1 |^ i) where i be Element of NAT : i <= n };

              then

              consider i be Element of NAT such that

               B: o = (a1 |^ i) & i <= n;

              (a |^ i) = (a1 |^ i) by V, pr5;

              hence o in M by B;

            end;

            hence thesis by A, TARSKI: 2;

          end;

          

           H2: for i,j be Element of NAT st i < j & j <= n holds (a1 |^ i) <> (a1 |^ j)

          proof

            let i,j be Element of NAT ;

            assume

             W: i < j & j <= n;

            

             V: ( FAdj (F, {a})) is Subring of E by FIELD_5: 12;

            assume (a1 |^ i) = (a1 |^ j);

            

            then (a |^ i) = (a1 |^ j) by V, pr5

            .= (a |^ j) by V, pr5;

            hence thesis by W, U;

          end;

          

           I: E is ( FAdj (F, {a})) -extending by FIELD_4: 7;

          ( Carrier l) c= M by VECTSP_6:def 4;

          then z in M by D1;

          then

          consider i be Element of NAT such that

           D3: z = (a |^ i) & i <= n;

          ( FAdj (F, {a})) is Subring of E by FIELD_5: 12;

          then

           D3a: (a |^ i) = (a1 |^ i) by pr5;

          consider pM be Polynomial of F such that

           D4a: ( deg pM) <= n & for i be Element of NAT st i <= n holds (pM . i) = (l . (a1 |^ i)) by lembasx2;

          (pM . i) <> ( 0. F) by D3a, D3, D2, D4a;

          then pM <> ( 0_. F);

          then

          reconsider pM as non zero Polynomial of F by UPROOTS:def 5;

          reconsider pMC = pM as Element of the carrier of ( Polynom-Ring F) by POLYNOM3:def 10;

          ( Ext_eval (pMC,a)) = ( Ext_eval (pMC,a1)) by I, lemma7

          .= ( 0. V) by H1, H2, D1, D4a, lembasx1

          .= ( 0. ( FAdj (F, {a}))) by FIELD_4:def 6

          .= ( 0. E) by dFA;

          hence a is F -algebraic by alg00;

        end;

      end;

      hence thesis;

    end;