field_4.miz



    begin

    reserve K,F,E for Field,

R,S for Ring;

    

     Th1: R is Subring of R by LIOUVIL2: 18;

    theorem :: FIELD_4:1

    K is Subfield of K

    proof

      

       A1: the addF of K = (the addF of K || the carrier of K);

      

       A2: the multF of K = (the multF of K || the carrier of K);

      the carrier of K c= the carrier of K & ( 1. K) = ( 1. K) & ( 0. K) = ( 0. K);

      hence thesis by A1, A2, EC_PF_1:def 1;

    end;

    registration

      let R be non degenerated Ring;

      cluster -> non degenerated for Subring of R;

      coherence

      proof

        let S be Subring of R;

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

        hence thesis;

      end;

    end

    registration

      let R be comRing;

      cluster -> commutative for Subring of R;

      coherence

      proof

        let S be Subring of R;

        now

          let a,b be Element of S;

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

          then

          reconsider x = a, y = b as Element of R;

          

           A1: [x, y] in [:the carrier of S, the carrier of S:] by ZFMISC_1:def 2;

          

           A2: [y, x] in [:the carrier of S, the carrier of S:] by ZFMISC_1:def 2;

          

          thus (a * b) = ((the multF of R || the carrier of S) . (x,y)) by C0SP1:def 3

          .= (x * y) by A1, FUNCT_1: 49

          .= (y * x) by GROUP_1:def 12

          .= ((the multF of R || the carrier of S) . (b,a)) by A2, FUNCT_1: 49

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

        end;

        hence thesis;

      end;

    end

    registration

      let R be domRing;

      cluster -> domRing-like for Subring of R;

      coherence

      proof

        let S be Subring of R;

        now

          let a,b be Element of S;

          assume

           A1: (a * b) = ( 0. S);

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

          then

          reconsider x = a, y = b as Element of R;

          

           A2: [x, y] in [:the carrier of S, the carrier of S:] by ZFMISC_1:def 2;

          

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

          (a * b) = ((the multF of R || the carrier of S) . (x,y)) by C0SP1:def 3

          .= (x * y) by A2, FUNCT_1: 49;

          hence a = ( 0. S) or b = ( 0. S) by A1, A3, VECTSP_2:def 1;

        end;

        hence thesis by VECTSP_2:def 1;

      end;

    end

    theorem :: FIELD_4:2

    

     Th2: for S be Subring of R, F be FinSequence of R, G be FinSequence of S st F = G holds ( Sum F) = ( Sum G)

    proof

      let S be Subring of R, F be FinSequence of R, G be FinSequence of S;

      assume

       A1: F = G;

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

      then ( In (( Sum G),R)) = ( Sum G) by SUBSET_1:def 8;

      hence thesis by A1, ALGNUM_1: 10;

    end;

    begin

    definition

      let R,S be Ring;

      :: FIELD_4:def1

      attr S is R -extending means

      : Def1: R is Subring of S;

    end

    registration

      let R be Ring;

      cluster R -extending for Ring;

      existence

      proof

        take R;

        thus thesis by Th1;

      end;

    end

    registration

      let R be comRing;

      cluster R -extending for comRing;

      existence

      proof

        take R;

        thus thesis by Th1;

      end;

    end

    registration

      let R be domRing;

      cluster R -extending for domRing;

      existence

      proof

        take R;

        thus thesis by Th1;

      end;

    end

    registration

      let F be Field;

      cluster F -extending for Field;

      existence

      proof

        take F;

        thus thesis by Th1;

      end;

    end

    definition

      let R be Ring;

      mode RingExtension of R is R -extending Ring;

    end

    definition

      let R be comRing;

      mode comRingExtension of R is R -extending comRing;

    end

    definition

      let R be domRing;

      mode domRingExtension of R is R -extending domRing;

    end

    definition

      let F be Field;

      mode FieldExtension of F is F -extending Field;

    end

    theorem :: FIELD_4:3

    R is RingExtension of R

    proof

      R is Subring of R by Th1;

      hence thesis by Def1;

    end;

    theorem :: FIELD_4:4

    for R be comRing holds R is comRingExtension of R

    proof

      let R be comRing;

      R is Subring of R by Th1;

      hence thesis by Def1;

    end;

    theorem :: FIELD_4:5

    for R be domRing holds R is domRingExtension of R

    proof

      let R be domRing;

      R is Subring of R by Th1;

      hence thesis by Def1;

    end;

    theorem :: FIELD_4:6

    

     Th3: F is FieldExtension of F

    proof

      F is Subring of F by Th1;

      hence thesis by Def1;

    end;

    theorem :: FIELD_4:7

    

     Th4: E is FieldExtension of F iff F is Subfield of E

    proof

       A1:

      now

        assume E is FieldExtension of F;

        then F is Subring of E by Def1;

        hence F is Subfield of E by RING_3: 45;

      end;

      now

        assume F is Subfield of E;

        then F is Subring of E by RING_3: 43;

        hence E is FieldExtension of F by Def1;

      end;

      hence thesis by A1;

    end;

    registration

      cluster F_Complex -> F_Real -extending;

      coherence by RING_3: 43, RING_3: 48;

    end

    registration

      cluster F_Real -> F_Rat -extending;

      coherence by RING_3: 43, GAUSSINT: 14;

    end

    registration

      cluster F_Rat -> INT.Ring -extending;

      coherence by RING_3: 47;

    end

    registration

      let R be Ring, S be RingExtension of R;

      cluster -> R -extending for RingExtension of S;

      coherence

      proof

        let T be RingExtension of S;

        S is Subring of T & R is Subring of S by Def1;

        hence thesis by ALGNUM_1: 1;

      end;

    end

    registration

      let R be comRing, S be comRingExtension of R;

      cluster -> R -extending for comRingExtension of S;

      coherence ;

    end

    registration

      let R be domRing, S be domRingExtension of R;

      cluster -> R -extending for domRingExtension of S;

      coherence ;

    end

    registration

      let F be Field, E be FieldExtension of F;

      cluster -> F -extending for FieldExtension of E;

      coherence ;

    end

    registration

      let R be non degenerated Ring;

      cluster -> non degenerated for RingExtension of R;

      coherence

      proof

        let S be RingExtension of R;

        

         A1: R is Subring of S by Def1;

        now

          assume S is degenerated;

          

          then ( 1. R) = ( 0. S) by A1, C0SP1:def 3

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

          hence contradiction;

        end;

        hence thesis;

      end;

    end

    begin

    theorem :: FIELD_4:8

    

     Th5: for S be RingExtension of R, p be Polynomial of R holds p is Polynomial of S

    proof

      let S be RingExtension of R, p be Polynomial of R;

      

       A1: R is Subring of S by Def1;

      then

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

      

       A3: ( 0. S) = ( 0. R) by A1, C0SP1:def 3;

      ( rng p) c= the carrier of R by RELAT_1:def 19;

      then ( rng p) c= the carrier of S by A2;

      then

      reconsider p1 = p as sequence of the carrier of S by FUNCT_2: 6;

      

       A4: ( Support p) is finite by POLYNOM1:def 5;

      now

        let o be object;

        assume

         A5: o in ( Support p1);

        then

        reconsider n = o as Element of NAT ;

        

         A6: ( 0. R) <> (p . n) by A3, A5, POLYNOM1:def 3;

        ( dom p) = NAT by FUNCT_2:def 1;

        hence o in ( Support p) by A6, POLYNOM1:def 3;

      end;

      then ( Support p1) c= ( Support p);

      hence thesis by A4, POLYNOM1:def 5;

    end;

    theorem :: FIELD_4:9

    for R be Subring of S, p be Polynomial of R holds p is Polynomial of S

    proof

      let R be Subring of S, p be Polynomial of R;

      

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

      

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

      ( rng p) c= the carrier of R by RELAT_1:def 19;

      then ( rng p) c= the carrier of S by A2;

      then

      reconsider p1 = p as sequence of the carrier of S by FUNCT_2: 6;

      

       A4: ( Support p) is finite by POLYNOM1:def 5;

      now

        let o be object;

        assume

         A5: o in ( Support p1);

        then

        reconsider n = o as Element of NAT ;

        

         A6: ( 0. R) <> (p . n) by A3, A5, POLYNOM1:def 3;

        ( dom p) = NAT by FUNCT_2:def 1;

        hence o in ( Support p) by A6, POLYNOM1:def 3;

      end;

      then ( Support p1) c= ( Support p);

      hence thesis by A4, POLYNOM1:def 5;

    end;

    theorem :: FIELD_4:10

    

     Th6: for S be RingExtension of R holds the carrier of ( Polynom-Ring R) c= the carrier of ( Polynom-Ring S)

    proof

      let S be RingExtension of R;

      now

        let o be object;

        assume o in the carrier of ( Polynom-Ring R);

        then o is Polynomial of R by POLYNOM3:def 10;

        then o is Polynomial of S by Th5;

        hence o in the carrier of ( Polynom-Ring S) by POLYNOM3:def 10;

      end;

      hence thesis;

    end;

    theorem :: FIELD_4:11

    

     Th7: S is RingExtension of R implies ( 0. ( Polynom-Ring S)) = ( 0. ( Polynom-Ring R))

    proof

      assume S is R -extending Ring;

      then

       A1: R is Subring of S by Def1;

      

      thus ( 0. ( Polynom-Ring R)) = ( 0_. R) by POLYNOM3:def 10

      .= ( NAT --> ( 0. R)) by POLYNOM3:def 7

      .= ( NAT --> ( 0. S)) by A1, C0SP1:def 3

      .= ( 0_. S) by POLYNOM3:def 7

      .= ( 0. ( Polynom-Ring S)) by POLYNOM3:def 10;

    end;

    theorem :: FIELD_4:12

    

     Th8: S is RingExtension of R implies ( 0_. S) = ( 0_. R)

    proof

      assume

       A1: S is R -extending Ring;

      

      thus ( 0_. S) = ( 0. ( Polynom-Ring S)) by POLYNOM3:def 10

      .= ( 0. ( Polynom-Ring R)) by A1, Th7

      .= ( 0_. R) by POLYNOM3:def 10;

    end;

    theorem :: FIELD_4:13

    

     Th9: S is RingExtension of R implies ( 1. ( Polynom-Ring S)) = ( 1. ( Polynom-Ring R))

    proof

      assume

       A1: S is R -extending Ring;

      then

       A2: R is Subring of S by Def1;

      

      thus ( 1. ( Polynom-Ring R)) = ( 1_. R) by POLYNOM3:def 10

      .= (( 0_. R) +* ( 0 ,( 1. R))) by POLYNOM3:def 8

      .= (( 0_. R) +* ( 0 ,( 1. S))) by A2, C0SP1:def 3

      .= (( 0_. S) +* ( 0 ,( 1. S))) by A1, Th8

      .= ( 1_. S) by POLYNOM3:def 8

      .= ( 1. ( Polynom-Ring S)) by POLYNOM3:def 10;

    end;

    theorem :: FIELD_4:14

    for S be RingExtension of R holds ( 1_. S) = ( 1_. R)

    proof

      let S be R -extending Ring;

      

      thus ( 1_. S) = ( 1. ( Polynom-Ring S)) by POLYNOM3:def 10

      .= ( 1. ( Polynom-Ring R)) by Th9

      .= ( 1_. R) by POLYNOM3:def 10;

    end;

    theorem :: FIELD_4:15

    

     Th10: for S be RingExtension of R, p,q be Polynomial of R holds for p1,q1 be Polynomial of S st p = p1 & q = q1 holds (p + q) = (p1 + q1)

    proof

      let S be RingExtension of R, p,q be Polynomial of R;

      let p1,q2 be Polynomial of S;

      assume

       A1: p = p1 & q = q2;

      

       A2: R is Subring of S by Def1;

      now

        let n be Element of NAT ;

        (p . n) = (p1 . n) & (q . n) = (q2 . n) by A1;

        then

         A3: [(p1 . n), (q2 . n)] in [:the carrier of R, the carrier of R:] by ZFMISC_1:def 2;

        

        thus ((p + q) . n) = ((p . n) + (q . n)) by NORMSP_1:def 2

        .= ((the addF of S || the carrier of R) . ((p1 . n),(q2 . n))) by A1, A2, C0SP1:def 3

        .= ((p1 . n) + (q2 . n)) by A3, FUNCT_1: 49

        .= ((p1 + q2) . n) by NORMSP_1:def 2;

      end;

      hence thesis;

    end;

    theorem :: FIELD_4:16

    

     Th11: for S be RingExtension of R holds the addF of ( Polynom-Ring R) = (the addF of ( Polynom-Ring S) || the carrier of ( Polynom-Ring R))

    proof

      let S be RingExtension of R;

      set aR = the addF of ( Polynom-Ring R), aS = (the addF of ( Polynom-Ring S) || the carrier of ( Polynom-Ring R));

      set cR = the carrier of ( Polynom-Ring R), cS = the carrier of ( Polynom-Ring S);

      

       A1: cR c= cS by Th6;

      

       A2: ( dom aS) = (( dom the addF of ( Polynom-Ring S)) /\ [:cR, cR:]) by RELAT_1: 61

      .= ( [:cS, cS:] /\ [:cR, cR:]) by FUNCT_2:def 1

      .= [:cR, cR:] by A1, ZFMISC_1: 96, XBOOLE_1: 28

      .= ( dom aR) by FUNCT_2:def 1;

      now

        let o be object;

        assume

         A3: o in ( dom aR);

        then

        consider p,q be object such that

         A4: p in the carrier of ( Polynom-Ring R) & q in the carrier of ( Polynom-Ring R) & o = [p, q] by ZFMISC_1:def 2;

        reconsider p, q as Element of cR by A4;

        reconsider p1 = p, q1 = q as Element of cS by A1;

        reconsider p2 = p, q2 = q as Polynomial of R;

        reconsider p3 = p1, q3 = q1 as Polynomial of S;

        

        thus (aR . o) = (p + q) by A4

        .= (p2 + q2) by POLYNOM3:def 10

        .= (p3 + q3) by Th10

        .= (p1 + q1) by POLYNOM3:def 10

        .= (aS . o) by A2, A3, A4, FUNCT_1: 47;

      end;

      hence thesis by A2;

    end;

    theorem :: FIELD_4:17

    

     Th12: for S be RingExtension of R holds for p,q be Polynomial of R holds for p1,q1 be Polynomial of S st p = p1 & q = q1 holds (p *' q) = (p1 *' q1)

    proof

      let S be RingExtension of R;

      let p,q be Polynomial of R;

      let p1,q2 be Polynomial of S;

      assume

       A1: p = p1 & q = q2;

      

       A2: R is Subring of S by Def1;

      now

        let n be Element of NAT ;

        consider r be FinSequence of the carrier of R such that

         A3: ( len r) = (n + 1) & ((p *' q) . n) = ( Sum r) & for k be Element of NAT st k in ( dom r) holds (r . k) = ((p . (k -' 1)) * (q . ((n + 1) -' k))) by POLYNOM3:def 9;

        consider r1 be FinSequence of the carrier of S such that

         A4: ( len r1) = (n + 1) & ((p1 *' q2) . n) = ( Sum r1) & for k be Element of NAT st k in ( dom r1) holds (r1 . k) = ((p1 . (k -' 1)) * (q2 . ((n + 1) -' k))) by POLYNOM3:def 9;

        

         A5: ( dom r1) = ( Seg ( len r)) by A3, A4, FINSEQ_1:def 3

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

        now

          let m be Nat;

          assume

           A6: m in ( dom r);

          (p . (m -' 1)) = (p1 . (m -' 1)) & (q . ((n + 1) -' m)) = (q2 . ((n + 1) -' m)) by A1;

          then

           A7: [(p1 . (m -' 1)), (q2 . ((n + 1) -' m))] in [:the carrier of R, the carrier of R:] by ZFMISC_1:def 2;

          

          thus (r . m) = ((p . (m -' 1)) * (q . ((n + 1) -' m))) by A6, A3

          .= ((the multF of S || the carrier of R) . ((p1 . (m -' 1)),(q2 . ((n + 1) -' m)))) by A1, A2, C0SP1:def 3

          .= ((p1 . (m -' 1)) * (q2 . ((n + 1) -' m))) by A7, FUNCT_1: 49

          .= (r1 . m) by A6, A5, A4;

        end;

        then r = r1 by A5;

        hence ((p *' q) . n) = ((p1 *' q2) . n) by A4, A3, A2, Th2;

      end;

      hence thesis;

    end;

    theorem :: FIELD_4:18

    

     Th13: S is RingExtension of R implies the multF of ( Polynom-Ring R) = (the multF of ( Polynom-Ring S) || the carrier of ( Polynom-Ring R))

    proof

      assume

       AS: S is RingExtension of R;

      set mR = the multF of ( Polynom-Ring R), mS = (the multF of ( Polynom-Ring S) || the carrier of ( Polynom-Ring R));

      set cR = the carrier of ( Polynom-Ring R), cS = the carrier of ( Polynom-Ring S);

      

       A1: cR c= cS by AS, Th6;

      

       A2: ( dom mS) = (( dom the multF of ( Polynom-Ring S)) /\ [:cR, cR:]) by RELAT_1: 61

      .= ( [:cS, cS:] /\ [:cR, cR:]) by FUNCT_2:def 1

      .= [:cR, cR:] by A1, ZFMISC_1: 96, XBOOLE_1: 28

      .= ( dom mR) by FUNCT_2:def 1;

      now

        let o be object;

        assume

         A3: o in ( dom mR);

        then

        consider p,q be object such that

         A4: p in cR & q in cR & o = [p, q] by ZFMISC_1:def 2;

        reconsider p, q as Element of cR by A4;

        reconsider p1 = p, q1 = q as Element of cS by A1;

        reconsider p2 = p, q2 = q as Polynomial of R;

        reconsider p3 = p1, q3 = q1 as Polynomial of S;

        

        thus (mR . o) = (p * q) by A4

        .= (p2 *' q2) by POLYNOM3:def 10

        .= (p3 *' q3) by AS, Th12

        .= (p1 * q1) by POLYNOM3:def 10

        .= (mS . o) by A4, A2, A3, FUNCT_1: 47;

      end;

      hence thesis by A2;

    end;

    registration

      let R be Ring;

      let S be RingExtension of R;

      cluster ( Polynom-Ring S) -> ( Polynom-Ring R) -extending;

      coherence

      proof

        set PS = ( Polynom-Ring S), PR = ( Polynom-Ring R);

        

         A1: the addF of PR = (the addF of PS || the carrier of PR) by Th11;

        

         A2: the multF of PR = (the multF of PS || the carrier of PR) by Th13;

        ( 1. PS) = ( 1. PR) & ( 0. PS) = ( 0. PR) by Th7, Th9;

        hence thesis by Th6, A1, A2, C0SP1:def 3;

      end;

    end

    theorem :: FIELD_4:19

    for R be Ring, S be RingExtension of R holds ( Polynom-Ring S) is RingExtension of ( Polynom-Ring R);

    theorem :: FIELD_4:20

    for S be RingExtension of R, p be Element of the carrier of ( Polynom-Ring R), q be Element of the carrier of ( Polynom-Ring S) st p = q holds ( deg p) = ( deg q)

    proof

      let S be RingExtension of R;

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

      assume

       A1: p = q;

      

       A2: R is Subring of S by Def1;

      per cases ;

        suppose q is zero;

        then ( len q) = 0 by UPROOTS: 17;

        then

         A3: ( deg q) = ( 0 - 1) by HURWITZ:def 2;

        

        then q = ( 0_. S) by HURWITZ: 20

        .= ( 0. ( Polynom-Ring S)) by POLYNOM3:def 10

        .= ( 0. ( Polynom-Ring R)) by Th7

        .= ( 0_. R) by POLYNOM3:def 10;

        hence ( deg p) = ( deg q) by A1, A3, HURWITZ: 20;

      end;

        suppose

         A4: q is non zero;

        then ( len q) > 0 by UPROOTS: 17;

        then

         A5: (( len q) -' 1) = (( len q) - 1) by XREAL_0:def 2;

        then

        reconsider lenq = (( len q) - 1) as Element of NAT ;

         A6:

        now

          let i be Nat;

          assume i >= ( len q);

          then (q . i) = ( 0. S) by ALGSEQ_1: 8;

          hence (p . i) = ( 0. R) by A1, A2, C0SP1:def 3;

        end;

        now

          let m be Nat;

          assume

           A7: m is_at_least_length_of p;

          now

            assume ( len q) > m;

            then (lenq + 1) > m;

            then lenq >= m by NAT_1: 13;

            then (p . (( len q) -' 1)) = ( 0. R) by A5, A7, ALGSEQ_1:def 2;

            then

             A8: (q . (( len q) -' 1)) = ( 0. S) by A1, A2, C0SP1:def 3;

            ( 0 + 1) < (( len q) + 1) by A4, XREAL_1: 8, UPROOTS: 17;

            then ( len q) >= 1 by NAT_1: 13;

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

            hence contradiction by A8, ALGSEQ_1: 10;

          end;

          hence ( len q) <= m;

        end;

        then ( len p) = ( len q) by A6, ALGSEQ_1:def 3, ALGSEQ_1:def 2;

        

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

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

      end;

    end;

    

     Lm2: for S be RingExtension of R, a be Element of R, b be Element of S st a = b holds ( - a) = ( - b)

    proof

      let S be RingExtension of R;

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

      assume

       A1: a = b;

      

       A2: R is Subring of S by Def1;

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

      then

      reconsider x = ( - a) as Element of S;

      

       A3: [a, ( - a)] in [:the carrier of R, the carrier of R:] by ZFMISC_1:def 2;

      

       A4: (the addF of S || the carrier of R) = the addF of R by A2, C0SP1:def 3;

      (b + x) = (a + ( - a)) by A1, A4, A3, FUNCT_1: 49

      .= ( 0. R) by RLVECT_1: 5

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

      hence thesis by RLVECT_1:def 10;

    end;

    theorem :: FIELD_4:21

    for R be non degenerated Ring, S be RingExtension of R, a be Element of R, b be Element of S st a = b holds ( rpoly (1,a)) = ( rpoly (1,b))

    proof

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

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

      assume

       A1: a = b;

      

       A2: R is Subring of S by Def1;

      

       A3: the carrier of ( Polynom-Ring R) c= the carrier of ( Polynom-Ring S) by Th6;

      set q = ( rpoly (1,b));

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

      reconsider p as Element of the carrier of ( Polynom-Ring S) by A3;

      reconsider p as Polynomial of S;

      ( len q) > 0 by UPROOTS: 17;

      then

       A4: (( len q) -' 1) = (( len q) - 1) by XREAL_0:def 2;

      then

      reconsider lenq = (( len q) - 1) as Element of NAT ;

      

       A5: 1 = ( deg q) by HURWITZ: 27

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

      then

       A6: ( len q) = (1 + 1);

       A7:

      now

        let i be Nat;

        assume

         A8: i >= ( len q);

        reconsider j = i as Element of NAT by ORDINAL1:def 12;

        j <> 0 & j <> 1 by A8, A6;

        then (( rpoly (1,a)) . j) = ( 0. R) by HURWITZ: 26;

        hence (p . i) = ( 0. S) by A2, C0SP1:def 3;

      end;

      now

        let m be Nat;

        assume

         A9: m is_at_least_length_of p;

        reconsider j = lenq as Element of NAT ;

        now

          assume ( len q) > m;

          then (lenq + 1) > m;

          then lenq >= m by NAT_1: 13;

          then

           A10: (p . (( len q) -' 1)) = ( 0. S) by A4, A9, ALGSEQ_1:def 2;

          (( rpoly (1,a)) . 1) = ( 1_ R) by HURWITZ: 25

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

          hence contradiction by A10, A5, XREAL_0:def 2;

        end;

        hence ( len q) <= m;

      end;

      then

       A11: ( len p) = ( len q) by A7, ALGSEQ_1:def 3, ALGSEQ_1:def 2;

      now

        let k be Nat;

        assume

         A12: k < ( len q);

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

        .= 1 by HURWITZ: 27;

        then k < (1 + 1) by A12;

        then

         A13: k <= 1 by NAT_1: 13;

        per cases ;

          suppose

           A14: k = 0 ;

          

          then

           A15: (( rpoly (1,a)) . k) = ( - (( power R) . (a,( 0 + 1)))) by HURWITZ: 25

          .= ( - ((( power R) . (a, 0 )) * a)) by GROUP_1:def 7

          .= ( - (( 1_ R) * a)) by GROUP_1:def 7

          .= ( - b) by A1, Lm2;

          (q . k) = ( - (( power S) . (b,( 0 + 1)))) by A14, HURWITZ: 25

          .= ( - ((( power S) . (b, 0 )) * b)) by GROUP_1:def 7

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

          .= ( - b);

          hence (p . k) = (q . k) by A15;

        end;

          suppose k <> 0 ;

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

          then

           A16: k >= 1 by NAT_1: 13;

          then

           A17: k = 1 by A13, XXREAL_0: 1;

          (( rpoly (1,a)) . 1) = ( 1_ R) by HURWITZ: 25

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

          

          hence (p . k) = ( 1_ S) by A16, A13, XXREAL_0: 1

          .= (q . k) by A17, HURWITZ: 25;

        end;

      end;

      hence thesis by A11, ALGSEQ_1: 12;

    end;

    begin

    theorem :: FIELD_4:22

    for a be Element of S holds S is RingExtension of R implies ( Ext_eval (( 0_. R),a)) = ( 0. S) by ALGNUM_1: 13;

    theorem :: FIELD_4:23

    for R be non degenerated Ring, S be RingExtension of R, a be Element of S holds ( Ext_eval (( 1_. R),a)) = ( 1. S)

    proof

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

      let a be Element of S;

      R is Subring of S by Def1;

      hence thesis by ALGNUM_1: 14;

    end;

    theorem :: FIELD_4:24

    for S be RingExtension of R, 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 S be RingExtension of R, a be Element of S;

      let p,q be Polynomial of R;

      R is Subring of S by Def1;

      hence thesis by ALGNUM_1: 15;

    end;

    theorem :: FIELD_4:25

    for R be comRing, S be comRingExtension of R, 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 comRing, S be comRingExtension of R;

      let a be Element of S;

      let p,q be Polynomial of R;

      R is Subring of S by Def1;

      hence thesis by ALGNUM_1: 20;

    end;

    

     Th14: for S be RingExtension of R, 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 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 Def1;

      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_4:26

    

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

    proof

      let S be RingExtension of R;

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

      let a be Element of S;

      assume

       A1: p = q;

      

       A2: R is Subring of S by Def1;

      per cases ;

        suppose q is zero;

        then

         A3: q = ( 0_. S) by UPROOTS:def 5;

        p = ( 0. ( Polynom-Ring S)) by A1, A3, POLYNOM3:def 10

        .= ( 0. ( Polynom-Ring R)) by Th7

        .= ( 0_. R) by POLYNOM3:def 10;

        

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

        .= ( eval (q,a)) by A3, POLYNOM4: 17;

      end;

        suppose

         A4: q is non zero;

        then ( len q) > 0 by UPROOTS: 17;

        then

         A5: (( len q) -' 1) = (( len q) - 1) by XREAL_0:def 2;

        then

        reconsider lenq = (( len q) - 1) as Element of NAT ;

        consider Fp be FinSequence of S such that

         A6: ( 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)),S)) * (( power S) . (a,(n -' 1)))) by ALGNUM_1:def 1;

        consider Fq be FinSequence of the carrier of S such that

         A7: ( eval (q,a)) = ( Sum Fq) & ( len Fq) = ( len q) & for n be Element of NAT st n in ( dom Fq) holds (Fq . n) = ((q . (n -' 1)) * (( power S) . (a,(n -' 1)))) by POLYNOM4:def 2;

         A8:

        now

          let i be Nat;

          assume i >= ( len q);

          then (q . i) = ( 0. S) by ALGSEQ_1: 8;

          hence (p . i) = ( 0. R) by A1, A2, C0SP1:def 3;

        end;

        now

          let m be Nat;

          assume

           A9: m is_at_least_length_of p;

          now

            assume ( len q) > m;

            then (lenq + 1) > m;

            then lenq >= m by NAT_1: 13;

            then (p . (( len q) -' 1)) = ( 0. R) by A5, A9, ALGSEQ_1:def 2;

            then

             A10: (q . (( len q) -' 1)) = ( 0. S) by A1, A2, C0SP1:def 3;

            ( 0 + 1) < (( len q) + 1) by A4, XREAL_1: 8, UPROOTS: 17;

            then ( len q) >= 1 by NAT_1: 13;

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

            hence contradiction by A10, ALGSEQ_1: 10;

          end;

          hence ( len q) <= m;

        end;

        then ( len p) = ( len q) by A8, ALGSEQ_1:def 3, ALGSEQ_1:def 2;

        

        then

         A11: ( dom Fq) = ( Seg ( len p)) by A7, FINSEQ_1:def 3

        .= ( dom Fp) by A6, FINSEQ_1:def 3;

        for n be Nat st n in ( dom Fp) holds (Fq . n) = (Fp . n)

        proof

          let n be Nat;

          assume

           A12: n in ( dom Fp);

          

          hence (Fp . n) = (( In ((p . (n -' 1)),S)) * (( power S) . (a,(n -' 1)))) by A6

          .= ((q . (n -' 1)) * (( power S) . (a,(n -' 1)))) by A1

          .= (Fq . n) by A7, A11, A12;

        end;

        hence thesis by A6, A7, A11, FINSEQ_1: 13;

      end;

    end;

    theorem :: FIELD_4:27

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

    proof

      let S be RingExtension of R, p be Element of the carrier of ( Polynom-Ring R), q be Element of the carrier of ( Polynom-Ring S), a be Element of R, b be Element of S;

      assume that

       A1: p = q and

       A2: a = b;

      

      thus ( eval (p,a)) = ( Ext_eval (p,b)) by A2, Th14

      .= ( eval (q,b)) by A1, Th15;

    end;

    definition

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

      :: FIELD_4:def2

      pred a is_a_root_of p,S means ( Ext_eval (p,a)) = ( 0. S);

    end

    definition

      let R be Ring, S be RingExtension of R;

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

      :: FIELD_4:def3

      pred p is_with_roots_in S means ex a be Element of S st a is_a_root_of (p,S);

    end

    definition

      let R be Ring, S be RingExtension of R;

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

      :: FIELD_4:def4

      func Roots (S,p) -> Subset of S equals { a where a be Element of S : a is_a_root_of (p,S) };

      coherence

      proof

        now

          let o be object;

          assume o in { a where a be Element of S : a is_a_root_of (p,S) };

          then

          consider a be Element of S such that

           A1: o = a & a is_a_root_of (p,S);

          thus o in the carrier of S by A1;

        end;

        hence thesis by TARSKI:def 3;

      end;

    end

    theorem :: FIELD_4:28

    for S be RingExtension of R, p be Element of the carrier of ( Polynom-Ring R) holds ( Roots p) c= ( Roots (S,p))

    proof

      let S be RingExtension of R;

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

      

       A1: R is Subring of S by Def1;

      then

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

      now

        let o be object;

        assume

         A3: o in ( Roots p);

        then

        reconsider a = o as Element of R;

        

         A4: a is_a_root_of p by A3, POLYNOM5:def 10;

        reconsider b = a as Element of S by A2;

        ( Ext_eval (p,b)) = ( eval (p,a)) by Th14

        .= ( 0. R) by A4, POLYNOM5:def 7

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

        then b is_a_root_of (p,S);

        hence o in ( Roots (S,p));

      end;

      hence thesis;

    end;

    definition

      let R be Ring, S be non degenerated Ring;

      let p be Polynomial of R;

      :: FIELD_4:def5

      pred p splits_in S means ex a be non zero Element of S, q be Ppoly of S st p = (a * q);

    end

    theorem :: FIELD_4:29

    for F be Field, p be Polynomial of F st ( deg p) = 1 holds p splits_in F

    proof

      let F be Field;

      let p be Polynomial of F;

      assume ( deg p) = 1;

      then

      consider x,z be Element of F such that

       A1: x <> ( 0. F) & p = (x * ( rpoly (1,z))) by HURWITZ: 28;

      reconsider x as non zero Element of F by A1, STRUCT_0:def 12;

      reconsider q = ( rpoly (1,z)) as Ppoly of F by RING_5: 51;

      p = (x * q) by A1;

      hence thesis;

    end;

    begin

    definition

      let R be Ring, S be RingExtension of R;

      :: FIELD_4:def6

      func VecSp (S,R) -> strict ModuleStr over R means

      : Def5: the carrier of it = the carrier of S & the addF of it = the addF of S & the ZeroF of it = ( 0. S) & the lmult of it = (the multF of S | [:the carrier of R, the carrier of S:]);

      existence

      proof

        set C = the carrier of S;

        R is Subring of S by Def1;

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

        then [:the carrier of R, C:] c= [:C, C:] by ZFMISC_1: 96;

        then

        reconsider lm = (the multF of S | [:the carrier of R, C:]) as Function of [:the carrier of R, C:], C by FUNCT_2: 32;

        take ModuleStr (# C, the addF of S, ( 0. S), lm #);

        thus thesis;

      end;

      uniqueness ;

    end

    registration

      let R be Ring, S be RingExtension of R;

      cluster ( VecSp (S,R)) -> non empty;

      coherence

      proof

        ( 0. S) in the carrier of S;

        hence thesis by Def5;

      end;

    end

    registration

      let R be Ring, S be RingExtension of R;

      cluster ( VecSp (S,R)) -> Abelian add-associative right_zeroed right_complementable;

      coherence

      proof

        set E = S, F = R;

        set P = ( VecSp (E,F));

        

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

        hereby

          let x,y be Element of P;

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

          

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

          .= (b + a) by RLVECT_1:def 2

          .= (y + x) by Def5;

        end;

        hereby

          let x,y,z be Element of P;

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

          

           A2: (y + z) = (b + c) by Def5;

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

          

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

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

          .= (x + (y + z)) by A2, Def5;

        end;

        hereby

          let x be Element of P;

          reconsider a = x as Element of E by Def5;

          

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

          .= x;

        end;

        let x be Element of P;

        reconsider a = x as Element of E by Def5;

        consider b be Element of E such that

         A3: (a + b) = ( 0. E) by ALGSTR_0:def 11;

        reconsider y = b as Element of P by Def5;

        take y;

        

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

        .= ( 0. P) by A3, Def5;

      end;

    end

    

     Lm3: for E be RingExtension of R, a,b be Element of E, s be Element of R, v be Element of ( VecSp (E,R)) st a = s & b = v holds (a * b) = (s * v)

    proof

      let E be RingExtension of R;

      let a,b be Element of E;

      let s be Element of R, v be Element of ( VecSp (E,R)) such that

       A1: a = s & b = v;

      the carrier of ( VecSp (E,R)) = the carrier of E by Def5;

      then

       A2: [s, v] in [:the carrier of R, the carrier of E:] by ZFMISC_1:def 2;

      

      thus (s * v) = ((the multF of E | [:the carrier of R, the carrier of E:]) . (s,v)) by Def5

      .= (a * b) by A1, A2, FUNCT_1: 49;

    end;

    

     Lm4: for E be RingExtension of R, a,b be Element of E, x,y be Element of R st a = x & b = y holds (a + b) = (x + y)

    proof

      let E be RingExtension of R;

      let a,b be Element of E;

      let x,y be Element of R such that

       A1: a = x & b = y;

      

       A2: R is Subring of E by Def1;

      

       A3: [x, y] in [:the carrier of R, the carrier of R:] by ZFMISC_1:def 2;

      

      thus (x + y) = ((the addF of E || the carrier of R) . (x,y)) by A2, C0SP1:def 3

      .= (a + b) by A1, A3, FUNCT_1: 49;

    end;

    

     Lm5: for E be RingExtension of R, a,b be Element of E, x,y be Element of R st a = x & b = y holds (a * b) = (x * y)

    proof

      let E be RingExtension of R;

      let a,b be Element of E;

      let x,y be Element of R such that

       A1: a = x & b = y;

      

       A2: R is Subring of E by Def1;

      

       A3: [x, y] in [:the carrier of R, the carrier of R:] by ZFMISC_1:def 2;

      

      thus (x * y) = ((the multF of E || the carrier of R) . (x,y)) by A2, C0SP1:def 3

      .= (a * b) by A1, A3, FUNCT_1: 49;

    end;

    registration

      let R be Ring, S be RingExtension of R;

      cluster ( VecSp (S,R)) -> scalar-distributive scalar-associative scalar-unital vector-distributive;

      coherence

      proof

        set E = S, F = R;

        set P = ( VecSp (E,F));

        

         A1: F is Subring of E by Def1;

        then

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

        hereby

          let x,y be Element of F;

          let v be Element of P;

          reconsider a = x, b = y, c = v as Element of E by A2, Def5;

          

           A3: ((a + b) * c) = ((a * c) + (b * c)) by VECTSP_1:def 3;

          (x * v) = (a * c) & (y * v) = (b * c) by Lm3;

          then ((x * v) + (y * v)) = ((a * c) + (b * c)) by Def5;

          hence ((x + y) * v) = ((x * v) + (y * v)) by A3, Lm3, Lm4;

        end;

        hereby

          let x,y be Element of F;

          let v be Element of P;

          reconsider a = x, b = y, c = v as Element of E by A2, Def5;

          

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

          

           A5: ((a * b) * c) = ((x * y) * v) by Lm3, Lm5;

          (b * c) = (y * v) by Lm3;

          hence ((x * y) * v) = (x * (y * v)) by A4, A5, Lm3;

        end;

        hereby

          let v be Element of P;

          reconsider c = v as Element of E by Def5;

          

           A6: ( 1. F) = ( 1. E) by C0SP1:def 3, A1;

          (( 1. E) * c) = c;

          hence (( 1. F) * v) = v by Lm3, A6;

        end;

        hereby

          let x be Element of F;

          let v,w be Element of P;

          reconsider a = x, b = v, c = w as Element of E by A2, Def5;

          

           A7: (a * (b + c)) = ((a * b) + (a * c)) by VECTSP_1:def 2;

          (b + c) = (v + w) by Def5;

          then

           A8: (a * (b + c)) = (x * (v + w)) by Lm3;

          (a * b) = (x * v) & (a * c) = (x * w) by Lm3;

          hence (x * (v + w)) = ((x * v) + (x * w)) by A7, A8, Def5;

        end;

      end;

    end

    theorem :: FIELD_4:30

    for S be RingExtension of R holds ( VecSp (S,R)) is VectSp of R;

    definition

      let F be Field, E be FieldExtension of F;

      :: FIELD_4:def7

      func deg (E,F) -> Integer equals

      : Def6: ( dim ( VecSp (E,F))) if ( VecSp (E,F)) is finite-dimensional

      otherwise ( - 1);

      coherence ;

      consistency ;

    end

    registration

      let F be Field, E be FieldExtension of F;

      cluster ( deg (E,F)) -> dim-like;

      coherence

      proof

        now

          assume

           A1: not ( deg (E,F)) = ( - 1);

          ( dim ( VecSp (E,F))) is Nat;

          hence ( deg (E,F)) is natural by Def6, A1;

        end;

        hence thesis;

      end;

    end

    definition

      let F be Field, E be FieldExtension of F;

      :: FIELD_4:def8

      attr E is F -finite means

      : Def7: ( VecSp (E,F)) is finite-dimensional;

    end

    registration

      let F be Field;

      cluster F -finite for FieldExtension of F;

      existence

      proof

        reconsider E = F as FieldExtension of F by Th3;

        take E;

        set V = ( VecSp (E,F));

        

         A1: the carrier of V = the carrier of E by Def5;

        reconsider e = ( 1. E) as Vector of V by Def5;

        for x be object st x in {( 1. E)} holds x in the carrier of V by A1;

        then

        reconsider A = {e} as Subset of V by TARSKI:def 3;

        ( 0. V) = ( 0. E) by Def5;

        then

         A2: A is linearly-independent by VECTSP_7: 3;

        

         A3: the carrier of ( Lin A) = the set of all ( Sum l) where l be Linear_Combination of A by VECTSP_7:def 2;

         A4:

        now

          let o be object;

          assume o in the carrier of V;

          then

          reconsider v = o as Element of the carrier of V;

          reconsider a = v as Element of E by Def5;

          defpred P[ object, object] means ($1 = e & $2 = a) or ($1 <> e & $2 = ( 0. E));

          

           A6: for x be object st x in the carrier of V holds ex y be object st y in the carrier of E & P[x, y]

          proof

            let o be object;

            assume o in the carrier of V;

            per cases ;

              suppose

               A7: o = e;

              take a;

              thus thesis by A7;

            end;

              suppose

               A8: o <> e;

              take ( 0. E);

              thus thesis by A8;

            end;

          end;

          consider f be Function of the carrier of V, the carrier of E such that

           A9: for x be object st x in the carrier of V holds P[x, (f . x)] from FUNCT_2:sch 1( A6);

          ( dom f) = the carrier of V & ( rng f) c= the carrier of E by RELAT_1:def 19, FUNCT_2:def 1;

          then

          reconsider f as Element of ( Funcs (the carrier of V,the carrier of E)) by FUNCT_2:def 2;

          ex T be finite Subset of V st for v be Element of V st not v in T holds (f . v) = ( 0. E)

          proof

            e in the carrier of V;

            then for x be object holds x in {e} implies x in the carrier of V by TARSKI:def 1;

            then

            reconsider T = {e} as finite Subset of V by TARSKI:def 3;

            take T;

            now

              let u be Element of V;

              assume not u in T;

              then u <> e by TARSKI:def 1;

              hence (f . u) = ( 0. E) by A9;

            end;

            hence thesis;

          end;

          then

          reconsider l = f as Linear_Combination of V by VECTSP_6:def 1;

          now

            let o be object;

            assume o in ( Carrier l);

            then o in { v where v be Element of V : (l . v) <> ( 0. E) } by VECTSP_6:def 2;

            then

            consider u be Element of V such that

             A10: o = u & (l . u) <> ( 0. E);

            u = e by A10, A9;

            hence o in A by A10, TARSKI:def 1;

          end;

          then ( Carrier l) c= A;

          then

          reconsider l as Linear_Combination of A by VECTSP_6:def 4;

          ( Sum l) = ((l . e) * e) by VECTSP_6: 17

          .= ((the multF of E | [:the carrier of F, the carrier of E:]) . ((l . e),e)) by Def5

          .= (a * ( 1. E)) by A9

          .= v;

          hence o in the set of all ( Sum l) where l be Linear_Combination of A;

        end;

        now

          let o be object;

          assume o in the set of all ( Sum l) where l be Linear_Combination of A;

          then

          consider l be Linear_Combination of A such that

           A11: o = ( Sum l);

          thus o in the carrier of V by A11;

        end;

        then the carrier of V = the set of all ( Sum l) where l be Linear_Combination of A by A4, TARSKI: 2;

        then A is Basis of V by A3, A2, VECTSP_4: 31, VECTSP_7:def 3;

        hence thesis by MATRLIN:def 1;

      end;

    end

    registration

      let F be Field;

      let E be F -finite FieldExtension of F;

      cluster ( deg (E,F)) -> natural;

      coherence

      proof

        ( dim ( VecSp (E,F))) is Nat;

        hence ( deg (E,F)) is natural by Def7, Def6;

      end;

    end

    begin

    registration

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

      cluster the carrier of ( Polynom-Ring p) -> F -polynomial-membered;

      coherence

      proof

        

         A1: the carrier of ( Polynom-Ring p) = { q where q be Polynomial of F : ( deg q) < ( deg p) } by RING_4:def 8;

        now

          let o be object;

          assume o in the carrier of ( Polynom-Ring p);

          then

          consider q be Polynomial of F such that

           A2: q = o & ( deg q) < ( deg p) by A1;

          thus o is Polynomial of F by A2;

        end;

        hence thesis;

      end;

      cluster ( Polynom-Ring p) -> F -polynomial-membered;

      coherence ;

    end

    definition

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

      :: FIELD_4:def9

      func KroneckerIso p -> Function of the carrier of ( Polynom-Ring p), the carrier of ( KroneckerField (F,p)) means

      : Def8: for q be Element of the carrier of ( Polynom-Ring p) holds (it . q) = ( Class (( EqRel (( Polynom-Ring F),( {p} -Ideal ))),q));

      existence

      proof

        deffunc F( object) = ( Class (( EqRel (( Polynom-Ring F),( {p} -Ideal ))),$1));

        

         A1: the carrier of ( Polynom-Ring p) = { q where q be Polynomial of F : ( deg q) < ( deg p) } by RING_4:def 8;

         A2:

        now

          let x be object;

          assume

           A3: x in the carrier of ( Polynom-Ring p);

          for a be Element of ( Polynom-Ring p) holds a in the carrier of ( Polynom-Ring F)

          proof

            let a be Element of ( Polynom-Ring p);

            a in { q where q be Polynomial of F : ( deg q) < ( deg p) } by A1;

            then ex r be Polynomial of F st r = a & ( deg r) < ( deg p);

            hence thesis by POLYNOM3:def 10;

          end;

          then

          reconsider a = x as Element of ( Polynom-Ring F) by A3;

          ( Class (( EqRel (( Polynom-Ring F),( {p} -Ideal ))),a)) is Element of (( Polynom-Ring F) / ( {p} -Ideal )) by RING_1: 12;

          then ( Class (( EqRel (( Polynom-Ring F),( {p} -Ideal ))),a)) in the carrier of (( Polynom-Ring F) / ( {p} -Ideal ));

          hence F(x) in the carrier of ( KroneckerField (F,p)) by FIELD_1:def 3;

        end;

        consider g be Function of the carrier of ( Polynom-Ring p), the carrier of ( KroneckerField (F,p)) such that

         A4: for x be object st x in the carrier of ( Polynom-Ring p) holds (g . x) = F(x) from FUNCT_2:sch 2( A2);

        take g;

        thus thesis by A4;

      end;

      uniqueness

      proof

        set R = ( Polynom-Ring p);

        let F1,F2 be Function of the carrier of ( Polynom-Ring p), the carrier of ( KroneckerField (F,p)) such that

         A5: for q be Element of R holds (F1 . q) = ( Class (( EqRel (( Polynom-Ring F),( {p} -Ideal ))),q)) and

         A6: for q be Element of R holds (F2 . q) = ( Class (( EqRel (( Polynom-Ring F),( {p} -Ideal ))),q));

        now

          let q be Element of R;

          

          thus (F1 . q) = ( Class (( EqRel (( Polynom-Ring F),( {p} -Ideal ))),q)) by A5

          .= (F2 . q) by A6;

        end;

        hence thesis;

      end;

    end

    

     Lm6: for L be Ring, a be Element of ( Polynom-Ring L), p be Polynomial of L st a = p holds ( - a) = ( - p)

    proof

      let L be Ring, a be Element of ( Polynom-Ring L), p be Polynomial of L;

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

      assume a = p;

      

      then (a + x) = (p + ( - p)) by POLYNOM3:def 10

      .= (p - p) by POLYNOM3:def 6

      .= ( 0_. L) by POLYNOM3: 29

      .= ( 0. ( Polynom-Ring L)) by POLYNOM3:def 10;

      then a = ( - x) by RLVECT_1: 6;

      hence ( - a) = ( - p);

    end;

    

     Lm7: for L be Ring, a,b be Element of ( Polynom-Ring L), p,q be Polynomial of L st a = p & b = q holds (a - b) = (p - q)

    proof

      let L be Ring, a,b be Element of ( Polynom-Ring L), p,q be Polynomial of L;

      assume

       A1: a = p & b = q;

      then ( - b) = ( - q) by Lm6;

      

      hence (a - b) = (p + ( - q)) by A1, POLYNOM3:def 10

      .= (p - q) by POLYNOM3:def 6;

    end;

    

     Lm8: for F be Field, p be irreducible Element of the carrier of ( Polynom-Ring F), a be Element of ( Polynom-Ring p) holds a in the carrier of ( Polynom-Ring F)

    proof

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

      the carrier of ( Polynom-Ring p) = { q where q be Polynomial of F : ( deg q) < ( deg p) } by RING_4:def 8;

      then a in { q where q be Polynomial of F : ( deg q) < ( deg p) };

      then ex r be Polynomial of F st r = a & ( deg r) < ( deg p);

      hence a in the carrier of ( Polynom-Ring F) by POLYNOM3:def 10;

    end;

    

     Lm9: for F be Field, p be irreducible Element of the carrier of ( Polynom-Ring F), a be Element of the carrier of ( Polynom-Ring F), q be Element of ( Polynom-Ring p) st a = q holds ( - a) = ( - q)

    proof

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

      reconsider x = ( - q) as Element of ( Polynom-Ring F) by Lm8;

      

       A1: the addF of ( Polynom-Ring p) = (the addF of ( Polynom-Ring F) || the carrier of ( Polynom-Ring p)) by RING_4:def 8;

      

       A2: the ZeroF of ( Polynom-Ring p) = ( 0_. F) by RING_4:def 8;

      assume

       A3: a = q;

       [a, x] in [:the carrier of ( Polynom-Ring p), the carrier of ( Polynom-Ring p):] by A3, ZFMISC_1:def 2;

      

      then (a + x) = (q + ( - q)) by A3, A1, FUNCT_1: 49

      .= ( 0. ( Polynom-Ring p)) by RLVECT_1: 5

      .= ( 0. ( Polynom-Ring F)) by A2, POLYNOM3:def 10;

      then a = ( - x) by RLVECT_1: 6;

      hence ( - a) = ( - q);

    end;

    

     Lm10: for F be Field, p be irreducible Element of the carrier of ( Polynom-Ring F), a,b be Element of the carrier of ( Polynom-Ring F), q,r be Element of ( Polynom-Ring p) st a = q & b = r holds (a - b) = (q - r)

    proof

      let F be Field, p be irreducible Element of the carrier of ( Polynom-Ring F), a,b be Element of the carrier of ( Polynom-Ring F), q,r be Element of ( Polynom-Ring p);

      assume

       A1: a = q & b = r;

      then ( - b) = ( - r) by Lm9;

      then

       A2: [a, ( - b)] in [:the carrier of ( Polynom-Ring p), the carrier of ( Polynom-Ring p):] by A1, ZFMISC_1:def 2;

      

       A3: the addF of ( Polynom-Ring p) = (the addF of ( Polynom-Ring F) || the carrier of ( Polynom-Ring p)) by RING_4:def 8;

      (a - b) = (the addF of ( Polynom-Ring p) . (a,( - b))) by A2, A3, FUNCT_1: 49

      .= (q - r) by A1, Lm9;

      hence thesis;

    end;

    registration

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

      cluster ( KroneckerIso p) -> additive multiplicative unity-preserving one-to-one onto;

      coherence

      proof

        set R = ( Polynom-Ring p), f = ( KroneckerIso p);

        now

          let a,b be Element of R;

          reconsider r = a, q = b as Element of ( Polynom-Ring F) by Lm8;

          reconsider fa = (f . a), fb = (f . b) as Element of (( Polynom-Ring F) / ( {p} -Ideal )) by FIELD_1:def 3;

          

           A1: fa = ( Class (( EqRel (( Polynom-Ring F),( {p} -Ideal ))),a)) by Def8;

          

           A2: fb = ( Class (( EqRel (( Polynom-Ring F),( {p} -Ideal ))),b)) by Def8;

          

           A3: [a, b] in [:the carrier of R, the carrier of R:] by ZFMISC_1:def 2;

          

           A4: (a + b) = ((the addF of ( Polynom-Ring F) || the carrier of R) . (a,b)) by RING_4:def 8

          .= (r + q) by A3, FUNCT_1: 49;

          

          thus ((f . a) + (f . b)) = (fa + fb) by FIELD_1:def 3

          .= ( Class (( EqRel (( Polynom-Ring F),( {p} -Ideal ))),(a + b))) by A4, A1, A2, RING_1: 13

          .= (f . (a + b)) by Def8;

        end;

        hence f is additive;

        now

          let a,b be Element of R;

          reconsider r = a, q = b as Element of the carrier of ( Polynom-Ring F) by Lm8;

          reconsider fa = (f . a), fb = (f . b) as Element of (( Polynom-Ring F) / ( {p} -Ideal )) by FIELD_1:def 3;

          

           A5: fa = ( Class (( EqRel (( Polynom-Ring F),( {p} -Ideal ))),a)) by Def8;

          

           A6: fb = ( Class (( EqRel (( Polynom-Ring F),( {p} -Ideal ))),b)) by Def8;

          

           A7: [a, b] in [:the carrier of R, the carrier of R:] by ZFMISC_1:def 2;

          

           A8: (a * b) = ((( poly_mult_mod p) || the carrier of R) . (a,b)) by RING_4:def 8

          .= (( poly_mult_mod p) . (r,q)) by A7, FUNCT_1: 49

          .= ((r *' q) mod p) by RING_4:def 7;

          reconsider c = ((r *' q) mod p) as Element of the carrier of ( Polynom-Ring F) by POLYNOM3:def 10;

          reconsider d = ((r *' q) div p) as Element of the carrier of ( Polynom-Ring F) by POLYNOM3:def 10;

          

           A9: ((r *' q) - ((r *' q) mod p)) = (((((r *' q) div p) *' p) + ((r *' q) mod p)) - ((r *' q) mod p)) by RING_4: 4

          .= (((((r *' q) div p) *' p) + ((r *' q) mod p)) + ( - ((r *' q) mod p))) by POLYNOM3:def 6

          .= ((((r *' q) div p) *' p) + (((r *' q) mod p) + ( - ((r *' q) mod p)))) by POLYNOM3: 26

          .= ((((r *' q) div p) *' p) + (((r *' q) mod p) - ((r *' q) mod p))) by POLYNOM3:def 6

          .= ((((r *' q) div p) *' p) + ( 0_. F)) by POLYNOM3: 29

          .= (((r *' q) div p) *' p);

          (r * q) = (r *' q) by POLYNOM3:def 10;

          

          then

           A10: ((r * q) - c) = (((r *' q) div p) *' p) by A9, Lm7

          .= (p * d) by POLYNOM3:def 10;

          ( {p} -Ideal ) = the set of all (p * r) where r be Element of ( Polynom-Ring F) by IDEAL_1: 64;

          then

           A11: ((r * q) - c) in ( {p} -Ideal ) by A10;

          

          thus ((f . a) * (f . b)) = (fa * fb) by FIELD_1:def 3

          .= ( Class (( EqRel (( Polynom-Ring F),( {p} -Ideal ))),(r * q))) by A5, A6, RING_1: 14

          .= ( Class (( EqRel (( Polynom-Ring F),( {p} -Ideal ))),(a * b))) by A11, A8, RING_1: 6

          .= (f . (a * b)) by Def8;

        end;

        hence f is multiplicative;

        (f . ( 1_ R)) = ( Class (( EqRel (( Polynom-Ring F),( {p} -Ideal ))),( 1. R))) by Def8

        .= ( Class (( EqRel (( Polynom-Ring F),( {p} -Ideal ))),( 1_. F))) by RING_4:def 8

        .= ( Class (( EqRel (( Polynom-Ring F),( {p} -Ideal ))),( 1. ( Polynom-Ring F)))) by POLYNOM3:def 10

        .= ( 1. (( Polynom-Ring F) / ( {p} -Ideal ))) by RING_1:def 6

        .= ( 1_ ( KroneckerField (F,p))) by FIELD_1:def 3;

        hence f is unity-preserving;

        now

          let x1,x2 be object;

          assume

           A12: x1 in ( dom f) & x2 in ( dom f) & (f . x1) = (f . x2);

          then

          reconsider a = x1, b = x2 as Element of the carrier of ( Polynom-Ring p);

          reconsider q = a, r = b as Element of the carrier of ( Polynom-Ring F) by Lm8;

          ( Class (( EqRel (( Polynom-Ring F),( {p} -Ideal ))),q)) = (f . b) by A12, Def8

          .= ( Class (( EqRel (( Polynom-Ring F),( {p} -Ideal ))),r)) by Def8;

          then (q - r) in ( {p} -Ideal ) by RING_1: 6;

          then (q - r) in the set of all (p * s) where s be Element of ( Polynom-Ring F) by IDEAL_1: 64;

          then

          consider u be Element of the carrier of ( Polynom-Ring F) such that

           A13: (q - r) = (p * u);

          reconsider s = (p *' u) as Polynomial of F;

          

           A14: (q - r) = (a - b) by Lm10;

          now

            assume

             A15: u <> ( 0_. F);

            then

            reconsider degu = ( deg u) as Element of NAT by FIELD_1: 1;

            degu >= 0 ;

            then

             A16: (( deg p) + ( deg u)) >= (( deg p) + 0 ) by XREAL_1: 6;

            now

              assume (p *' u) in { q where q be Polynomial of F : ( deg q) < ( deg p) };

              then

              consider s be Polynomial of F such that

               A17: s = (p *' u) & ( deg s) < ( deg p);

              thus contradiction by A17, A16, A15, HURWITZ: 23;

            end;

            then not (p *' u) in the carrier of ( Polynom-Ring p) by RING_4:def 8;

            then not (q - r) in the carrier of ( Polynom-Ring p) by A13, POLYNOM3:def 10;

            hence contradiction by A14;

          end;

          

          then (q - r) = (p *' ( 0_. F)) by A13, POLYNOM3:def 10

          .= ( 0. ( Polynom-Ring F)) by POLYNOM3:def 10;

          hence x1 = x2 by RLVECT_1: 21;

        end;

        hence f is one-to-one;

         A18:

        now

          let x be object;

          assume

           A19: x in ( rng f);

          ( rng f) c= the carrier of ( KroneckerField (F,p)) by RELAT_1:def 19;

          hence x in the carrier of ( KroneckerField (F,p)) by A19;

        end;

        now

          let x be object;

          assume x in the carrier of ( KroneckerField (F,p));

          then x in the carrier of (( Polynom-Ring F) / ( {p} -Ideal )) by FIELD_1:def 3;

          then

          consider q be Element of the carrier of ( Polynom-Ring F) such that

           A20: x = ( Class (( EqRel (( Polynom-Ring F),( {p} -Ideal ))),q)) by RING_1: 11;

          reconsider d = (q div p) as Element of the carrier of ( Polynom-Ring F) by POLYNOM3:def 10;

          p <> ( 0_. F);

          then

          consider t be Polynomial of F such that

           A21: q = (((q div p) *' p) + t) & ( deg t) < ( deg p) by HURWITZ:def 5;

          reconsider r = t as Element of the carrier of ( Polynom-Ring F) by POLYNOM3:def 10;

          (q - ((q div p) *' p)) = ((((q div p) *' p) + t) + ( - ((q div p) *' p))) by A21, POLYNOM3:def 6

          .= (t + (((q div p) *' p) + ( - ((q div p) *' p)))) by POLYNOM3: 26

          .= (t + (((q div p) *' p) - ((q div p) *' p))) by POLYNOM3:def 6

          .= (t + ( 0_. F)) by POLYNOM3: 29

          .= t;

          then

           A22: r = (q mod p) by HURWITZ:def 6;

          r in { q where q be Polynomial of F : ( deg q) < ( deg p) } by A21;

          then

           A23: r in the carrier of ( Polynom-Ring p) by RING_4:def 8;

          then

           A24: r in ( dom f) by FUNCT_2:def 1;

          q = (((q div p) *' p) + (q mod p)) by RING_4: 4;

          

          then

           A25: (q - r) = ((((q div p) *' p) + (q mod p)) - (q mod p)) by A22, Lm7

          .= ((((q div p) *' p) + (q mod p)) + ( - (q mod p))) by POLYNOM3:def 6

          .= (((q div p) *' p) + ((q mod p) + ( - (q mod p)))) by POLYNOM3: 26

          .= (((q div p) *' p) + ((q mod p) - (q mod p))) by POLYNOM3:def 6

          .= (((q div p) *' p) + ( 0_. F)) by POLYNOM3: 29

          .= (p * d) by POLYNOM3:def 10;

          ( {p} -Ideal ) = the set of all (p * r) where r be Element of ( Polynom-Ring F) by IDEAL_1: 64;

          then

           A26: (q - r) in ( {p} -Ideal ) by A25;

          (f . r) = ( Class (( EqRel (( Polynom-Ring F),( {p} -Ideal ))),r)) by A23, Def8

          .= ( Class (( EqRel (( Polynom-Ring F),( {p} -Ideal ))),q)) by A26, RING_1: 6;

          hence x in ( rng f) by A20, A24, FUNCT_1: 3;

        end;

        hence f is onto by A18, TARSKI: 2;

      end;

    end

    registration

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

      cluster ( KroneckerField (F,p)) -> ( Polynom-Ring p) -homomorphic( Polynom-Ring p) -monomorphic( Polynom-Ring p) -isomorphic;

      coherence

      proof

        

         A1: ( KroneckerIso p) is linear one-to-one;

        hence ( KroneckerField (F,p)) is ( Polynom-Ring p) -homomorphic by RING_2:def 4;

        thus ( KroneckerField (F,p)) is ( Polynom-Ring p) -monomorphic by A1, RING_3:def 3;

        thus ( KroneckerField (F,p)) is ( Polynom-Ring p) -isomorphic by A1, RING_3:def 4;

      end;

      cluster ( Polynom-Ring p) -> ( KroneckerField (F,p)) -homomorphic( KroneckerField (F,p)) -monomorphic( KroneckerField (F,p)) -isomorphic;

      coherence

      proof

        reconsider g = (( KroneckerIso p) " ) as Isomorphism of ( KroneckerField (F,p)), ( Polynom-Ring p) by RING_3: 73;

        g is Homomorphism of ( KroneckerField (F,p)), ( Polynom-Ring p);

        hence ( Polynom-Ring p) is ( KroneckerField (F,p)) -homomorphic by RING_2:def 4;

        g is monomorphism;

        hence ( Polynom-Ring p) is ( KroneckerField (F,p)) -monomorphic by RING_3:def 3;

        g is Isomorphism of ( KroneckerField (F,p)), ( Polynom-Ring p);

        hence ( Polynom-Ring p) is ( KroneckerField (F,p)) -isomorphic by RING_3:def 4;

      end;

      cluster ( Polynom-Ring p) -> F -homomorphicF -monomorphic;

      coherence ;

    end

    

     Lm11: for F be polynomial_disjoint Field holds for p be irreducible Element of the carrier of ( Polynom-Ring F) holds ex E be FieldExtension of F st p is_with_roots_in E

    proof

      let F be polynomial_disjoint Field;

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

       A1:

      now

        assume not (F,( Polynom-Ring p)) are_disjoint ;

        then

         A2: (( [#] F) /\ ( [#] ( Polynom-Ring p))) <> {} by FIELD_2:def 1;

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

        

         A3: a in the carrier of F & a in the carrier of ( Polynom-Ring p) by A2, XBOOLE_0:def 4;

        the carrier of ( Polynom-Ring p) = { q where q be Polynomial of F : ( deg q) < ( deg p) } by RING_4:def 8;

        then

        consider q be Polynomial of F such that

         A4: a = q & ( deg q) < ( deg p) by A3;

        a in the carrier of ( Polynom-Ring F) by A4, POLYNOM3:def 10;

        then a in (( [#] F) /\ ( [#] ( Polynom-Ring F))) by A3, XBOOLE_0:def 4;

        hence contradiction by FIELD_3:def 3;

      end;

      reconsider KroneckerIsop = (( KroneckerIso p) " ) as Isomorphism of ( KroneckerField (F,p)), ( Polynom-Ring p) by RING_3: 73;

      set h = (KroneckerIsop * ( emb p));

      reconsider h as Function of F, ( Polynom-Ring p) by FUNCT_2: 13;

      h is linear one-to-one by RINGCAT1: 1;

      then

      reconsider h as Monomorphism of F, ( Polynom-Ring p);

      reconsider E = ( embField h) as Field by A1, FIELD_2: 12;

      ( emb_iso h) is onto by A1, FIELD_2: 15;

      then

      reconsider embisoh = (( emb_iso h) " ) as Function of ( Polynom-Ring p), E by FUNCT_2: 25;

      

       A5: ( emb_iso h) is linear one-to-one onto by A1, FIELD_2: 13, FIELD_2: 14, FIELD_2: 15;

      then

      reconsider P = ( Polynom-Ring p) as E -isomorphic Field by RING_3:def 4;

      reconsider embisoh as Isomorphism of P, E by A5, RING_3: 73;

      set iso = (embisoh * KroneckerIsop), u = ( KrRoot p);

      reconsider iso as Function of ( KroneckerField (F,p)), E by FUNCT_2: 13;

      

       A6: iso is RingHomomorphism by RINGCAT1: 1;

      then

      reconsider E as ( KroneckerField (F,p)) -homomorphic Field by RING_2:def 4;

      reconsider iso as Homomorphism of ( KroneckerField (F,p)), E by A6;

      u is_a_root_of ( emb (p,p)) by FIELD_1: 42;

      then

       A7: ( eval ((( PolyHom iso) . ( emb (p,p))),(iso . u))) = ( 0. E) by FIELD_1: 33, POLYNOM5:def 7;

      F is Subfield of E by FIELD_2: 17;

      then

      reconsider E as FieldExtension of F by Th4;

      take E;

      reconsider a = (iso . u) as Element of E;

      (( PolyHom iso) . ( emb (p,p))) = p

      proof

        set g = (( PolyHom iso) . ( emb (p,p)));

        

         A8: ( KroneckerField (F,p)) = (( Polynom-Ring F) / ( {p} -Ideal )) by FIELD_1:def 3;

        

         A9: for a be Element of F holds (h . a) = (a | F)

        proof

          let a be Element of F;

          ( dom ( emb p)) = the carrier of F by FUNCT_2:def 1;

          

          then

           A10: (h . a) = (KroneckerIsop . (( emb p) . a)) by FUNCT_1: 13

          .= (KroneckerIsop . ( Class (( EqRel (( Polynom-Ring F),( {p} -Ideal ))),(a | F)))) by FIELD_1: 39;

          

           A11: the carrier of ( Polynom-Ring p) = { q where q be Polynomial of F : ( deg q) < ( deg p) } by RING_4:def 8;

          ( deg (a | F)) <= 0 & ( deg p) > 0 by RATFUNC1:def 2, RING_4:def 4;

          then (a | F) in the carrier of ( Polynom-Ring p) by A11;

          then

          reconsider b1 = (a | F) as Element of ( Polynom-Ring p);

          

           A12: ( dom ( KroneckerIso p)) = the carrier of ( Polynom-Ring p) by FUNCT_2:def 1;

          (( KroneckerIso p) . b1) = ( Class (( EqRel (( Polynom-Ring F),( {p} -Ideal ))),b1)) by Def8;

          hence thesis by A12, A10, FUNCT_1: 32;

        end;

        

         A13: for a be Element of F holds (iso . (( emb p) . a)) = a

        proof

          let a be Element of F;

          ( rng ( KroneckerIso p)) = the carrier of ( KroneckerField (F,p)) by FUNCT_2:def 3;

          then

           A14: ( dom KroneckerIsop) = the carrier of ( KroneckerField (F,p)) by FUNCT_1: 33;

          reconsider b = (a | F) as Element of the carrier of ( Polynom-Ring F) by POLYNOM3:def 10;

          

           A15: the carrier of ( Polynom-Ring p) = { q where q be Polynomial of F : ( deg q) < ( deg p) } by RING_4:def 8;

          ( deg (a | F)) <= 0 & ( deg p) > 0 by RATFUNC1:def 2, RING_4:def 4;

          then (a | F) in the carrier of ( Polynom-Ring p) by A15;

          then

          reconsider b1 = (a | F) as Element of ( Polynom-Ring p);

          reconsider v = ( Class (( EqRel (( Polynom-Ring F),( {p} -Ideal ))),b)) as Element of ( KroneckerField (F,p)) by A8, RING_1: 12;

          

           A16: (( KroneckerIso p) . b1) = ( Class (( EqRel (( Polynom-Ring F),( {p} -Ideal ))),b1)) by Def8;

          

           A17: ( dom ( KroneckerIso p)) = the carrier of ( Polynom-Ring p) by FUNCT_2:def 1;

          the carrier of ( embField h) = ( carr h) by FIELD_2:def 7

          .= ((( [#] ( Polynom-Ring p)) \ ( rng h)) \/ ( [#] F)) by FIELD_2:def 2;

          then

          reconsider a1 = a as Element of ( embField h) by XBOOLE_0:def 3;

          a in F;

          

          then

           A18: (( emb_iso h) . a1) = (h . a) by FIELD_2:def 8

          .= (a | F) by A9;

          

           A19: ( dom ( emb_iso h)) = the carrier of ( embField h) by FUNCT_2:def 1;

          

          thus (iso . (( emb p) . a)) = (iso . v) by FIELD_1: 39

          .= (embisoh . (KroneckerIsop . v)) by A14, FUNCT_1: 13

          .= (embisoh . b) by A16, A17, FUNCT_1: 32

          .= a by A18, A19, FUNCT_1: 32;

        end;

        now

          let x be object;

          assume x in NAT ;

          then

          reconsider i = x as Element of NAT ;

          (g . i) = (iso . (( emb (p,p)) . i)) by FIELD_1:def 2

          .= (iso . ( Class (( EqRel (( Polynom-Ring F),( {p} -Ideal ))),((p . i) | F)))) by FIELD_1: 40

          .= (iso . (( emb p) . (p . i))) by FIELD_1: 39;

          hence (g . x) = (p . x) by A13;

        end;

        hence thesis;

      end;

      then a is_a_root_of (p,E) by A7, Th15;

      hence thesis;

    end;

    theorem :: FIELD_4:31

    for F be polynomial_disjoint Field holds for f be non constant Element of the carrier of ( Polynom-Ring F) holds ex E be FieldExtension of F st f is_with_roots_in E

    proof

      let F be polynomial_disjoint Field;

      let f be non constant Element of the carrier of ( Polynom-Ring F);

      consider p be Element of the carrier of ( Polynom-Ring F) such that

       A1: p is_a_irreducible_factor_of f by FIELD_1: 3;

      reconsider p as irreducible Element of the carrier of ( Polynom-Ring F) by A1, FIELD_1:def 1;

      consider q be Element of the carrier of ( Polynom-Ring F) such that

       A2: (p * q) = f by A1, FIELD_1:def 1, GCD_1:def 1;

      consider E be FieldExtension of F such that

       A3: p is_with_roots_in E by Lm11;

      take E;

      consider a be Element of E such that

       A4: a is_a_root_of (p,E) by A3;

      reconsider p1 = p, q1 = q as Polynomial of F;

      

       A5: F is Subring of E by Def1;

      ( Ext_eval (f,a)) = ( Ext_eval ((p1 *' q1),a)) by A2, POLYNOM3:def 10

      .= (( Ext_eval (p1,a)) * ( Ext_eval (q1,a))) by A5, ALGNUM_1: 20

      .= ( 0. E) by A4;

      then a is_a_root_of (f,E);

      hence thesis;

    end;