field_1.miz



    begin

    reserve n for Nat;

    notation

      let L be non empty ZeroStr;

      let p be Polynomial of L;

      synonym LM p for Leading-Monomial p;

    end

    theorem :: FIELD_1:1

    

     Th2: for L be non empty ZeroStr, p be Polynomial of L holds ( deg p) is Element of NAT iff p <> ( 0_. L)

    proof

      let L be non empty ZeroStr;

      let p be Polynomial of L;

      now

        assume p <> ( 0_. L);

        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;

        hence ( deg p) is Element of NAT by INT_1: 3;

      end;

      hence thesis by HURWITZ: 20;

    end;

    definition

      let R be non degenerated Ring;

      let p be non zero Polynomial of R;

      :: original: deg

      redefine

      func deg p -> Element of NAT ;

      coherence

      proof

        p <> ( 0_. R);

        hence thesis by Th2;

      end;

    end

    registration

      let R be add-associative right_zeroed right_complementable right-distributive non empty doubleLoopStr;

      let f be additive Function of R, R;

      reduce (f . ( 0. R)) to ( 0. R);

      reducibility by RING_2: 6;

    end

    theorem :: FIELD_1:2

    

     Th3: for R be Ring, I be Ideal of R holds for x be Element of (R / I), a be Element of R st x = ( Class (( EqRel (R,I)),a)) holds for n be Nat holds (x |^ n) = ( Class (( EqRel (R,I)),(a |^ n)))

    proof

      let R be Ring, I be Ideal of R;

      let x be Element of (R / I), a be Element of R;

      assume

       A1: x = ( Class (( EqRel (R,I)),a));

      let n be Nat;

      defpred P[ Nat] means (x |^ $1) = ( Class (( EqRel (R,I)),(a |^ $1)));

      (x |^ 0 ) = ( 1_ (R / I)) by BINOM: 8

      .= ( Class (( EqRel (R,I)),( 1_ R))) by RING_1:def 6

      .= ( Class (( EqRel (R,I)),(a |^ 0 ))) by BINOM: 8;

      then

       A2: P[ 0 ];

       A3:

      now

        let i be Nat;

        assume

         A4: P[i];

        ( Class (( EqRel (R,I)),(a |^ (i + 1)))) = ( Class (( EqRel (R,I)),((a |^ i) * (a |^ 1)))) by BINOM: 10

        .= ( Class (( EqRel (R,I)),((a |^ i) * a))) by BINOM: 8

        .= ((x |^ i) * x) by A1, A4, RING_1: 14

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

        .= (x |^ (i + 1)) by BINOM: 10;

        hence P[(i + 1)];

      end;

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

      hence thesis;

    end;

    definition

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

      :: FIELD_1:def1

      pred b is_a_irreducible_factor_of a means b divides a & b is irreducible;

    end

    registration

      cluster non almost_left_invertible factorial for domRing;

      existence ;

    end

    theorem :: FIELD_1:3

    

     Th4: for R be non almost_left_invertible factorial domRing, a be non zero NonUnit of R holds ex b be Element of R st b is_a_irreducible_factor_of a

    proof

      let R be non almost_left_invertible factorial domRing, a be non zero NonUnit of R;

      consider F be non empty FinSequence of R such that

       A1: F is_a_factorization_of a by RING_2:def 12;

      ( len F) <> 0 ;

      then

      consider G be FinSequence of R, d be Element of R such that

       A2: F = (G ^ <*d*>) by FINSEQ_2: 19;

      take d;

      (( Product G) * ( Product <*d*>)) = a by A1, A2, GROUP_4: 5;

      then

       A3: ( Product <*d*>) divides a by GCD_1:def 1;

      reconsider lf = ( len F) as Element of ( dom F) by FINSEQ_5: 6;

      ( len F) = (( len G) + ( len <*d*>)) by A2, FINSEQ_1: 22

      .= (( len G) + 1) by FINSEQ_1: 39;

      then (F . lf) = d by A2, FINSEQ_1: 42;

      hence thesis by A1, A3, GROUP_4: 9;

    end;

    begin

    notation

      let R be Ring;

      let a be Element of R;

      let n be Nat;

      synonym anpoly (a,n) for seq (n,a);

    end

    

     Lm1: for R be non degenerated Ring, a be non zero Element of R holds ( deg ( anpoly (a,n))) = n

    proof

      let R be non degenerated Ring, a be non zero Element of R;

      ( len ( anpoly (a,n))) = (n + 1) by POLYDIFF: 27;

      hence thesis;

    end;

    registration

      let R be non degenerated Ring, a be non zero Element of R, n be Nat;

      cluster ( anpoly (a,n)) -> non zero;

      coherence

      proof

        ( deg ( anpoly (a,n))) = n & n <> ( - 1) by Lm1;

        hence thesis by HURWITZ: 20, UPROOTS:def 5;

      end;

    end

    registration

      let R be Ring, a be zero Element of R, n be Nat;

      cluster ( anpoly (a,n)) -> zero;

      coherence

      proof

        set q = ( anpoly (a,n));

        

         A1: a = ( 0. R) by STRUCT_0:def 12;

        now

          let i be Element of NAT ;

          per cases ;

            suppose

             A2: i = n;

            (q . n) = ( 0. R) by A1, POLYDIFF: 24

            .= (( 0_. R) . n) by FUNCOP_1: 7, ORDINAL1:def 12;

            hence (q . i) = (( 0_. R) . i) by A2;

          end;

            suppose i <> n;

            

            then (q . i) = ( 0. R) by POLYDIFF: 25

            .= (( 0_. R) . i) by FUNCOP_1: 7;

            hence (q . i) = (( 0_. R) . i);

          end;

        end;

        then q = ( 0_. R);

        hence thesis;

      end;

    end

    theorem :: FIELD_1:4

    for R be non degenerated Ring, a be non zero Element of R holds ( deg ( anpoly (a,n))) = n by Lm1;

    theorem :: FIELD_1:5

    for R be non degenerated Ring, a be Element of R holds ( LC ( anpoly (a,n))) = a

    proof

      let R be non degenerated Ring, a be Element of R;

      set q = ( anpoly (a,n));

      per cases ;

        suppose

         A1: a = ( 0. R);

        then q = ( 0_. R) by UPROOTS:def 5;

        then (q . (( len q) -' 1)) = ( 0. R) by FUNCOP_1: 7;

        hence thesis by A1, RATFUNC1:def 6;

      end;

        suppose a <> ( 0. R);

        then a is non zero;

        

        then

         A2: n = ( deg q) by Lm1

        .= (( len q) - 1);

        then (n + 1) = ( len q);

        then (( len q) -' 1) = n by A2, XREAL_1: 233, NAT_1: 11;

        

        hence a = (q . (( len q) -' 1)) by POLYDIFF: 24

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

      end;

    end;

    theorem :: FIELD_1:6

    for R be non degenerated Ring, n be non zero Nat, a,x be Element of R holds ( eval (( anpoly (a,n)),x)) = (a * (x |^ n))

    proof

      let R be non degenerated Ring, n be non zero Nat, a,x be Element of R;

      set q = ( anpoly (a,n));

      per cases ;

        suppose

         A1: a = ( 0. R);

        then q = ( 0_. R) by UPROOTS:def 5;

        hence ( eval (q,x)) = (a * (x |^ n)) by A1, POLYNOM4: 17;

      end;

        suppose a <> ( 0. R);

        then

         A2: a is non zero;

        consider F be FinSequence of R such that

         A3: ( eval (q,x)) = ( Sum F) and

         A4: ( len F) = ( len q) and

         A5: for j be Element of NAT st j in ( dom F) holds (F . j) = ((q . (j -' 1)) * (( power R) . (x,(j -' 1)))) by POLYNOM4:def 2;

        n = ( deg q) by A2, Lm1

        .= (( len q) - 1);

        then

         A7: ( dom F) = ( Seg (n + 1)) by A4, FINSEQ_1:def 3;

        

         A8: 1 <= (n + 1) by NAT_1: 11;

        

         A9: ((n + 1) -' 1) = ((n + 1) - 1) by NAT_1: 11, XREAL_1: 233;

        

         A10: (F /. (n + 1)) = (F . (n + 1)) by A7, FINSEQ_1: 3, PARTFUN1:def 6

        .= ((q . n) * (( power R) . (x,((n + 1) -' 1)))) by A9, A5, A8, A7, FINSEQ_1: 1

        .= (a * (( power R) . (x,((n + 1) -' 1)))) by POLYDIFF: 24

        .= (a * (x |^ n)) by A9, BINOM:def 2;

        now

          let j be Element of NAT ;

          assume

           A11: j in ( dom F) & j <> (n + 1);

          then

           A12: 1 <= j <= (n + 1) by A7, FINSEQ_1: 1;

          then j < (n + 1) by A11, XXREAL_0: 1;

          then

           A13: 1 <= j <= n by A11, NAT_1: 13, A7, FINSEQ_1: 1;

          

           A14: (j -' 1) = (j - 1) by A12, XREAL_0:def 2;

          

           A15: (j - 1) < (j - 0 ) by XREAL_1: 15;

          

          thus (F /. j) = (F . j) by A11, PARTFUN1:def 6

          .= ((q . (j -' 1)) * (( power R) . (x,(j -' 1)))) by A5, A11

          .= (( 0. R) * (( power R) . (x,(j -' 1)))) by A15, A13, A14, POLYDIFF: 25

          .= ( 0. R);

        end;

        hence thesis by A3, A10, A7, FINSEQ_1: 3, POLYNOM2: 3;

      end;

    end;

    theorem :: FIELD_1:7

    for R be non degenerated Ring, a be Element of R holds ( anpoly (a, 0 )) = (a | R);

    theorem :: FIELD_1:8

    

     Th9: for R be non degenerated Ring, n be non zero Element of NAT holds ( anpoly (( 1. R),n)) = ( rpoly (n,( 0. R)))

    proof

      let R be non degenerated Ring, n be non zero Element of NAT ;

      set p = ( anpoly (( 1. R),n)), r = ( rpoly (n,( 0. R)));

      now

        let i be Element of NAT ;

        

         A1: 1 <= n by NAT_1: 53;

        per cases ;

          suppose

           A2: i = 0 ;

          

          then (r . i) = ( - (( power R) . (( 0. R),n))) by HURWITZ: 25

          .= ( - (( 0. R) |^ n)) by BINOM:def 2

          .= ( - ( 0. R)) by A1, EC_PF_2: 5

          .= (p . i) by A2, POLYDIFF: 25;

          hence (p . i) = (r . i);

        end;

          suppose

           A3: i = n;

          

          then (r . i) = ( 1_ R) by HURWITZ: 25

          .= (p . i) by A3, POLYDIFF: 24;

          hence (p . i) = (r . i);

        end;

          suppose

           A4: i <> 0 & i <> n;

          

          then (r . i) = ( 0. R) by HURWITZ: 26

          .= (p . i) by A4, POLYDIFF: 25;

          hence (p . i) = (r . i);

        end;

      end;

      hence thesis;

    end;

    theorem :: FIELD_1:9

    

     Th10: for R be non degenerated comRing, a,b be non zero Element of R holds (b * ( anpoly (a,n))) = ( anpoly ((a * b),n))

    proof

      let R be non degenerated comRing, a,b be non zero Element of R;

      now

        let i be Element of NAT ;

        set p = ( anpoly (a,n)), q = ( anpoly ((a * b),n));

        per cases ;

          suppose

           A1: i = n;

          ((b * p) . i) = (b * (p . i)) by POLYNOM5:def 4

          .= (b * a) by A1, POLYDIFF: 24

          .= (q . i) by A1, POLYDIFF: 24;

          hence ((b * p) . i) = (q . i);

        end;

          suppose

           A2: i <> n;

          ((b * p) . i) = (b * (p . i)) by POLYNOM5:def 4

          .= (b * ( 0. R)) by A2, POLYDIFF: 25

          .= (q . i) by A2, POLYDIFF: 25;

          hence ((b * p) . i) = (q . i);

        end;

      end;

      hence thesis;

    end;

    theorem :: FIELD_1:10

    

     Th11: for R be non degenerated comRing, a,b be non zero Element of R, n,m be Nat holds (( anpoly (a,n)) *' ( anpoly (b,m))) = ( anpoly ((a * b),(n + m)))

    proof

      let R be non degenerated comRing, a,b be non zero Element of R, n,m be Nat;

      set p = ( anpoly (a,n)), q = ( anpoly (b,m)), r = ( anpoly ((a * b),(n + m)));

      per cases ;

        suppose

         A1: n = 0 ;

        

        hence (p *' q) = ((a | R) *' q)

        .= ((a * ( 1_. R)) *' q) by RING_4: 16

        .= (a * (( 1_. R) *' q)) by RING_4: 10

        .= r by A1, Th10;

      end;

        suppose

         A2: m = 0 ;

        

        hence (p *' q) = (p *' (b | R))

        .= (p *' (b * ( 1_. R))) by RING_4: 16

        .= (b * (p *' ( 1_. R))) by RING_4: 10

        .= r by A2, Th10;

      end;

        suppose

         A3: n <> 0 & m <> 0 ;

        then

         A4: n >= ( 0 + 1) & m >= ( 0 + 1) by NAT_1: 13;

        now

          let i be Element of NAT ;

          consider F be FinSequence of the carrier of R such that

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

          

           A6: for k be Element of NAT st k in ( dom F) & k <> ( len p) holds (F /. k) = ( 0. R)

          proof

            let k be Element of NAT ;

            assume

             A7: k in ( dom F) & k <> ( len p);

            

             A8: ( deg p) = n by Lm1;

            now

              assume

               A9: (k -' 1) = n;

              then (k - 1) = (k -' 1) by A3, XREAL_0:def 2;

              hence contradiction by A7, A9, A8;

            end;

            then

             A10: (p . (k -' 1)) = ( 0. R) by POLYDIFF: 25;

            

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

            .= (( 0. R) * (q . ((i + 1) -' k))) by A10, A7, A5

            .= ( 0. R);

          end;

          

           A11: ( dom F) = ( Seg (i + 1)) by FINSEQ_1:def 3, A5;

          per cases ;

            suppose

             A12: i = (n + m);

            

             A13: ( deg p) = n by Lm1;

            then

             A14: ( len p) <= ((n + 1) + m) by NAT_1: 11;

            

             A15: ( dom F) = ( Seg ((n + m) + 1)) by A12, A5, FINSEQ_1:def 3;

            ((( len p) - 1) + 1) >= (1 + 1) by A13, A4, XREAL_1: 6;

            then

             A16: 1 <= ( len p) by XXREAL_0: 2;

            

             A17: (( len p) -' 1) = n by A13, XREAL_0:def 2;

            m = ((i + 1) - ( len p)) by A13, A12;

            then

             A18: ((i + 1) -' ( len p)) = m by XREAL_0:def 2;

            ( Sum F) = (F /. ( len p)) by A16, A6, A14, A15, FINSEQ_1: 1, POLYNOM2: 3

            .= (F . ( len p)) by A16, A14, A15, FINSEQ_1: 1, PARTFUN1:def 6

            .= ((p . n) * (q . m)) by A16, A14, A15, FINSEQ_1: 1, A17, A18, A5

            .= (a * (q . m)) by POLYDIFF: 24

            .= (a * b) by POLYDIFF: 24;

            hence (r . i) = ((p *' q) . i) by A5, A12, POLYDIFF: 24;

          end;

            suppose

             A19: i <> (n + m);

            ( Sum F) = ( 0. R)

            proof

              per cases ;

                suppose i < (( len p) - 1);

                then

                 A20: (i + 1) < ((( len p) - 1) + 1) by XREAL_1: 6;

                now

                  let k be Element of NAT ;

                  assume

                   A21: k in ( dom F);

                  then 1 <= k <= (i + 1) by A11, FINSEQ_1: 1;

                  

                  hence ( 0. R) = (F /. k) by A20, A21, A6

                  .= (F . k) by A21, PARTFUN1:def 6;

                end;

                hence thesis by POLYNOM3: 1;

              end;

                suppose

                 A22: i >= (( len p) - 1);

                now

                  let k be Element of NAT ;

                  assume

                   A23: k in ( dom F);

                  per cases ;

                    suppose k <> ( len p);

                    

                    hence ( 0. R) = (F /. k) by A23, A6

                    .= (F . k) by A23, PARTFUN1:def 6;

                  end;

                    suppose

                     A24: k = ( len p);

                    

                     A25: ( deg p) = n by Lm1;

                    (i + 1) >= ((( len p) - 1) + 1) by A22, XREAL_1: 6;

                    then ((i + 1) - ( len p)) >= (( len p) - ( len p)) by XREAL_1: 6;

                    then ((i + 1) -' ( len p)) = (i - n) by A25, XREAL_0:def 2;

                    then

                     A26: ((i + 1) -' ( len p)) <> m by A19;

                    

                    thus (F . k) = ((p . (( len p) -' 1)) * (q . ((i + 1) -' ( len p)))) by A5, A23, A24

                    .= ((p . (( len p) -' 1)) * ( 0. R)) by A26, POLYDIFF: 25

                    .= ( 0. R);

                  end;

                end;

                hence thesis by POLYNOM3: 1;

              end;

            end;

            hence (r . i) = ((p *' q) . i) by A5, A19, POLYDIFF: 25;

          end;

        end;

        hence thesis;

      end;

    end;

    theorem :: FIELD_1:11

    

     Th12: for R be non degenerated Ring, p be non zero Polynomial of R holds ( LM p) = ( anpoly ((p . ( deg p)),( deg p)))

    proof

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

      set q = ( anpoly ((p . ( deg p)),( deg p))), r = ( LM p), n = ( deg p);

      reconsider degp = ( deg p) as Element of NAT ;

      

       A1: n = (( len p) -' 1) by XREAL_0:def 2;

      now

        let i be Element of NAT ;

        per cases ;

          suppose

           A3: i <> n;

          

          then (r . i) = ( 0. R) by A1, POLYNOM4:def 1

          .= (q . i) by A3, POLYDIFF: 25;

          hence (r . i) = (q . i);

        end;

          suppose

           A4: i = n;

          

          then (r . i) = (p . n) by A1, POLYNOM4:def 1

          .= (q . i) by A4, POLYDIFF: 24;

          hence (r . i) = (q . i);

        end;

      end;

      hence thesis;

    end;

    theorem :: FIELD_1:12

    

     Th13: for R be non degenerated comRing holds ( <%( 0. R), ( 1. R)%> `^ n) = ( anpoly (( 1. R),n))

    proof

      let R be non degenerated comRing;

      defpred P[ Nat] means ( <%( 0. R), ( 1. R)%> `^ $1) = ( anpoly (( 1. R),$1));

      

       A1: P[ 0 ]

      proof

        

        thus ( <%( 0. R), ( 1. R)%> `^ 0 ) = ( 1_. R) by POLYNOM5: 15

        .= ( anpoly (( 1. R), 0 ));

      end;

       A2:

      now

        let n be Nat;

        assume P[n];

        

        then ( <%( 0. R), ( 1. R)%> `^ (n + 1)) = (( anpoly (( 1. R),n)) *' <%( - ( 0. R)), ( 1. R)%>) by POLYNOM5: 19

        .= (( anpoly (( 1. R),n)) *' ( rpoly (1,( 0. R)))) by RING_5: 10

        .= (( anpoly (( 1. R),n)) *' ( anpoly (( 1. R),1))) by Th9

        .= ( anpoly ((( 1. R) * ( 1. R)),(n + 1))) by Th11

        .= ( anpoly (( 1. R),(n + 1)));

        hence P[(n + 1)];

      end;

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

      hence thesis;

    end;

    begin

    theorem :: FIELD_1:13

    

     Th14: for R be Ring, S be R -homomorphic Ring holds for h be Homomorphism of R, S holds for a be Element of R, n be Nat holds (h . (a |^ n)) = ((h . a) |^ n)

    proof

      let R be Ring, S be R -homomorphic Ring;

      let h be Homomorphism of R, S;

      let a be Element of R, n be Nat;

      defpred P[ Nat] means (h . (a |^ $1)) = ((h . a) |^ $1);

      

       A1: P[ 0 ]

      proof

        

        thus (h . (a |^ 0 )) = (h . ( 1_ R)) by BINOM: 8

        .= ( 1_ S) by GROUP_1:def 13

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

      end;

       A2:

      now

        let k be Nat;

        assume

         A3: P[k];

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

        .= ((h . (a |^ k)) * (h . (a |^ 1))) by GROUP_6:def 6

        .= (((h . a) |^ k) * (h . a)) by A3, BINOM: 8

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

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

        hence P[(k + 1)];

      end;

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

      hence thesis;

    end;

    theorem :: FIELD_1:14

    for R be Ring, S be R -homomorphic Ring holds for h be Homomorphism of R, S holds (h . ( Sum ( <*> the carrier of R))) = ( 0. S)

    proof

      let R be Ring, S be R -homomorphic Ring;

      let h be Homomorphism of R, S;

      

      thus (h . ( Sum ( <*> the carrier of R))) = (h . ( 0. R)) by RLVECT_1: 43

      .= ( 0. S) by RING_2: 6;

    end;

    theorem :: FIELD_1:15

    for R be Ring, S be R -homomorphic Ring holds for h be Homomorphism of R, S holds for F be FinSequence of R, a be Element of R holds (h . ( Sum ( <*a*> ^ F))) = ((h . a) + (h . ( Sum F)))

    proof

      let R be Ring, S be R -homomorphic Ring;

      let h be Homomorphism of R, S;

      let F be FinSequence of R, a be Element of R;

      

      thus (h . ( Sum ( <*a*> ^ F))) = (h . (( Sum <*a*>) + ( Sum F))) by RLVECT_1: 41

      .= ((h . ( Sum <*a*>)) + (h . ( Sum F))) by VECTSP_1:def 20

      .= ((h . a) + (h . ( Sum F))) by RLVECT_1: 44;

    end;

    theorem :: FIELD_1:16

    

     Th17: for R be Ring, S be R -homomorphic Ring holds for h be Homomorphism of R, S holds for F be FinSequence of R, a be Element of R holds (h . ( Sum (F ^ <*a*>))) = ((h . ( Sum F)) + (h . a))

    proof

      let R be Ring, S be R -homomorphic Ring;

      let h be Homomorphism of R, S;

      let F be FinSequence of R, a be Element of R;

      

      thus (h . ( Sum (F ^ <*a*>))) = (h . (( Sum F) + ( Sum <*a*>))) by RLVECT_1: 41

      .= ((h . ( Sum F)) + (h . ( Sum <*a*>))) by VECTSP_1:def 20

      .= ((h . ( Sum F)) + (h . a)) by RLVECT_1: 44;

    end;

    theorem :: FIELD_1:17

    for R be Ring, S be R -homomorphic Ring holds for h be Homomorphism of R, S holds for F,G be FinSequence of R holds (h . ( Sum (F ^ G))) = ((h . ( Sum F)) + (h . ( Sum G)))

    proof

      let R be Ring, S be R -homomorphic Ring;

      let h be Homomorphism of R, S;

      let F,G be FinSequence of R;

      

      thus (h . ( Sum (F ^ G))) = (h . (( Sum F) + ( Sum G))) by RLVECT_1: 41

      .= ((h . ( Sum F)) + (h . ( Sum G))) by VECTSP_1:def 20;

    end;

    theorem :: FIELD_1:18

    for R be Ring, S be R -homomorphic Ring holds for h be Homomorphism of R, S holds (h . ( Product ( <*> the carrier of R))) = ( 1. S)

    proof

      let R be Ring, S be R -homomorphic Ring;

      let h be Homomorphism of R, S;

      

      thus (h . ( Product ( <*> the carrier of R))) = (h . ( 1_ R)) by GROUP_4: 8

      .= ( 1_ S) by GROUP_1:def 13

      .= ( 1. S);

    end;

    theorem :: FIELD_1:19

    for R be Ring, S be R -homomorphic Ring holds for h be Homomorphism of R, S holds for F be FinSequence of R, a be Element of R holds (h . ( Product ( <*a*> ^ F))) = ((h . a) * (h . ( Product F)))

    proof

      let R be Ring, S be R -homomorphic Ring;

      let h be Homomorphism of R, S;

      let F be FinSequence of R, a be Element of R;

      

      thus (h . ( Product ( <*a*> ^ F))) = (h . (( Product <*a*>) * ( Product F))) by GROUP_4: 5

      .= ((h . ( Product <*a*>)) * (h . ( Product F))) by GROUP_6:def 6

      .= ((h . a) * (h . ( Product F))) by GROUP_4: 9;

    end;

    theorem :: FIELD_1:20

    for R be Ring, S be R -homomorphic Ring holds for h be Homomorphism of R, S holds for F be FinSequence of R, a be Element of R holds (h . ( Product (F ^ <*a*>))) = ((h . ( Product F)) * (h . a))

    proof

      let R be Ring, S be R -homomorphic Ring;

      let h be Homomorphism of R, S;

      let F be FinSequence of R, a be Element of R;

      

      thus (h . ( Product (F ^ <*a*>))) = (h . (( Product F) * ( Product <*a*>))) by GROUP_4: 5

      .= ((h . ( Product F)) * (h . ( Product <*a*>))) by GROUP_6:def 6

      .= ((h . ( Product F)) * (h . a)) by GROUP_4: 9;

    end;

    theorem :: FIELD_1:21

    for R be Ring, S be R -homomorphic Ring holds for h be Homomorphism of R, S holds for F,G be FinSequence of R holds (h . ( Product (F ^ G))) = ((h . ( Product F)) * (h . ( Product G)))

    proof

      let R be Ring, S be R -homomorphic Ring;

      let h be Homomorphism of R, S;

      let F,G be FinSequence of R;

      

      thus (h . ( Product (F ^ G))) = (h . (( Product F) * ( Product G))) by GROUP_4: 5

      .= ((h . ( Product F)) * (h . ( Product G))) by GROUP_6:def 6;

    end;

    begin

    definition

      let R,S be Ring;

      let f be Function of ( Polynom-Ring R), ( Polynom-Ring S);

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

      :: original: .

      redefine

      func f . p -> Element of the carrier of ( Polynom-Ring S) ;

      coherence

      proof

        (f . p) is Element of ( Polynom-Ring S);

        hence thesis;

      end;

    end

    definition

      let R be Ring, S be R -homomorphic Ring;

      let h be additive Function of R, S;

      :: FIELD_1:def2

      func PolyHom h -> Function of ( Polynom-Ring R), ( Polynom-Ring S) means

      : Def2: for f be Element of the carrier of ( Polynom-Ring R) holds for i be Nat holds ((it . f) . i) = (h . (f . i));

      existence

      proof

        

         A1: for f be Polynomial of R holds ex g be Polynomial of S st for i be Nat holds (g . i) = (h . (f . i))

        proof

          let f be Polynomial of R;

          deffunc F( Nat) = (h . (f . $1));

          consider q be AlgSequence of S such that

           A2: ( len q) <= ( len f) & for k be Nat st k < ( len f) holds (q . k) = F(k) from ALGSEQ_1:sch 1;

          take q;

          now

            let i be Nat;

            per cases ;

              suppose i < ( len f);

              hence (q . i) = (h . (f . i)) by A2;

            end;

              suppose

               A3: i >= ( len f);

              then (f . i) = ( 0. R) by ALGSEQ_1: 8;

              

              hence (h . (f . i)) = ( 0. S) by RING_2: 6

              .= (q . i) by A3, A2, ALGSEQ_1: 8, XXREAL_0: 2;

            end;

          end;

          hence thesis;

        end;

        defpred P[ object, object] means ex f be Polynomial of R, g be Polynomial of S st $1 = f & $2 = g & for i be Nat holds (g . i) = (h . (f . i));

        

         A4: for x be object st x in the carrier of ( Polynom-Ring R) holds ex y be object st y in the carrier of ( Polynom-Ring S) & P[x, y]

        proof

          let x be object;

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

          then

          reconsider y = x as Polynomial of R by POLYNOM3:def 10;

          consider z be Polynomial of S such that

           A5: for i be Nat holds (z . i) = (h . (y . i)) by A1;

          take z;

          thus thesis by A5, POLYNOM3:def 10;

        end;

        consider F be Function of the carrier of ( Polynom-Ring R), the carrier of ( Polynom-Ring S) such that

         A6: for x be object st x in the carrier of ( Polynom-Ring R) holds P[x, (F . x)] from FUNCT_2:sch 1( A4);

        take F;

        now

          let f be Polynomial of R, g be Polynomial of S;

          assume

           A7: g = (F . f);

          let i be Nat;

          f in the carrier of ( Polynom-Ring R) by POLYNOM3:def 10;

          then P[f, (F . f)] by A6;

          hence (g . i) = (h . (f . i)) by A7;

        end;

        hence thesis;

      end;

      uniqueness

      proof

        let F,G be Function of ( Polynom-Ring R), ( Polynom-Ring S);

        assume that

         A8: for f be Element of the carrier of ( Polynom-Ring R) holds for i be Nat holds ((F . f) . i) = (h . (f . i)) and

         A9: for f be Element of the carrier of ( Polynom-Ring R) holds for i be Nat holds ((G . f) . i) = (h . (f . i));

        now

          let o be object;

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

          then

          reconsider p = o as Element of the carrier of ( Polynom-Ring R);

          now

            let u be object;

            assume u in NAT ;

            then

            reconsider m = u as Nat;

            ((F . p) . m) = (h . (p . m)) by A8

            .= ((G . p) . m) by A9;

            hence ((F . p) . u) = ((G . p) . u);

          end;

          then (F . p) = (G . p);

          hence (F . o) = (G . o);

        end;

        hence F = G;

      end;

    end

    registration

      let R be Ring, S be R -homomorphic Ring;

      let h be Homomorphism of R, S;

      cluster ( PolyHom h) -> additive multiplicative unity-preserving;

      coherence

      proof

        set g = ( PolyHom h);

        set RP = ( Polynom-Ring R), SP = ( Polynom-Ring S);

        reconsider 1RP = ( 1_ RP) as Element of the carrier of ( Polynom-Ring R);

        reconsider 1SP = ( 1_ SP) as Element of the carrier of ( Polynom-Ring S);

        now

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

          reconsider gab = ((g . a) + (g . b)) as Element of the carrier of ( Polynom-Ring S);

          reconsider a1 = a, b1 = b as sequence of R;

          set ab1 = (a1 + b1);

          set ga = (g . a), gb = (g . b);

          reconsider ga1 = ga, gb1 = gb as sequence of S;

          set gab1 = (ga1 + gb1);

          now

            let m be Element of NAT ;

            (a1 + b1) = (a + b) by POLYNOM3:def 10;

            

            then ((g . (a + b)) . m) = (h . (ab1 . m)) by Def2

            .= (h . ((a1 . m) + (b1 . m))) by NORMSP_1:def 2

            .= ((h . (a . m)) + (h . (b . m))) by VECTSP_1:def 20

            .= (((g . a) . m) + (h . (b . m))) by Def2

            .= ((ga1 . m) + (gb1 . m)) by Def2

            .= (gab1 . m) by NORMSP_1:def 2;

            hence ((g . (a + b)) . m) = (gab . m) by POLYNOM3:def 10;

          end;

          hence (g . (a + b)) = ((g . a) + (g . b)) by FUNCT_2: 63;

        end;

        hence g is additive;

        now

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

          reconsider ab = (a * b) as Element of the carrier of ( Polynom-Ring R);

          reconsider gab = ((g . a) * (g . b)) as Element of the carrier of ( Polynom-Ring S);

          reconsider a1 = a, b1 = b as sequence of R;

          reconsider ab1 = (a1 *' b1) as sequence of R;

          reconsider ga = (g . a), gb = (g . b) as Element of the carrier of ( Polynom-Ring S);

          reconsider ga1 = ga, gb1 = gb as sequence of S;

          set gab1 = (ga1 *' gb1);

          now

            let m be Element of NAT ;

            consider r be FinSequence of the carrier of R such that

             A1: ( len r) = (m + 1) & (ab1 . m) = ( Sum r) & for k be Element of NAT st k in ( dom r) holds (r . k) = ((a1 . (k -' 1)) * (b1 . ((m + 1) -' k))) by POLYNOM3:def 9;

            consider s be FinSequence of the carrier of S such that

             A2: ( len s) = (m + 1) & (gab1 . m) = ( Sum s) & for k be Element of NAT st k in ( dom s) holds (s . k) = ((ga1 . (k -' 1)) * (gb1 . ((m + 1) -' k))) by POLYNOM3:def 9;

            

             A5: ( dom r) = ( Seg (m + 1)) by A1, FINSEQ_1:def 3

            .= ( dom s) by A2, FINSEQ_1:def 3;

            

             A3: for k be Element of NAT st k in ( dom r) holds (h . (r . k)) = (s . k)

            proof

              let k be Element of NAT ;

              assume

               A4: k in ( dom r);

              

              hence (h . (r . k)) = (h . ((a1 . (k -' 1)) * (b1 . ((m + 1) -' k)))) by A1

              .= ((h . (a1 . (k -' 1))) * (h . (b1 . ((m + 1) -' k)))) by GROUP_6:def 6

              .= ((ga1 . (k -' 1)) * (h . (b1 . ((m + 1) -' k)))) by Def2

              .= ((ga1 . (k -' 1)) * (gb1 . ((m + 1) -' k))) by Def2

              .= (s . k) by A5, A4, A2;

            end;

            reconsider m1 = (m + 1) as Element of NAT ;

            

             A6: 1 <= (m + 1) by NAT_1: 11;

            defpred P[ Nat] means (h . ( Sum (r | $1))) = ( Sum (s | $1));

            

             A7: P[1]

            proof

              

               A8: ( len (r | 1)) = 1 by A1, NAT_1: 11, FINSEQ_1: 59;

              

               A9: ( dom (r | 1)) = ( Seg 1) by A1, A6, FINSEQ_1: 17;

              then ((r | 1) . 1) in ( rng (r | 1)) by FINSEQ_1: 3, FUNCT_1: 3;

              then

              reconsider a = ((r | 1) . 1) as Element of the carrier of R;

              (r | 1) = <*a*> by A8, FINSEQ_1: 40;

              then

               A11: (h . ( Sum (r | 1))) = (h . a) by RLVECT_1: 44;

              

               A12: ( len (s | 1)) = 1 by A2, NAT_1: 11, FINSEQ_1: 59;

              

               A13: ( dom (s | 1)) = ( Seg 1) by A2, A6, FINSEQ_1: 17;

              then ((s | 1) . 1) in ( rng (s | 1)) by FINSEQ_1: 3, FUNCT_1: 3;

              then

              reconsider b = ((s | 1) . 1) as Element of the carrier of S;

              

               A15: (s | 1) = <*b*> by A12, FINSEQ_1: 40;

              

               A16: ( dom r) = ( Seg (m + 1)) by A1, FINSEQ_1:def 3;

              

               A17: 1 in ( dom (s | ( Seg 1))) by A13;

              1 in ( dom (r | ( Seg 1))) by A9;

              

              then (h . a) = (h . (r . 1)) by FUNCT_1: 47

              .= (s . 1) by A16, A3, A6, FINSEQ_1: 1

              .= b by A17, FUNCT_1: 47;

              hence thesis by A11, A15, RLVECT_1: 44;

            end;

             A19:

            now

              let j be Element of NAT ;

              assume

               A20: 1 <= j & j < m1;

              assume

               A21: P[j];

              

               A22: (j + 1) <= (m + 1) by A20, NAT_1: 13;

              then

               A23: ( len (r | (j + 1))) = (j + 1) by A1, FINSEQ_1: 59;

              

               A24: (r | ( Seg j)) = (r | j);

              then

              reconsider rj = (r | ( Seg j)) as FinSequence of R;

              ((r | (j + 1)) | j) = (r | j) by NAT_1: 11, FINSEQ_1: 82;

              then

              consider q be FinSequence such that

               A25: (r | (j + 1)) = (rj ^ q) by FINSEQ_1: 80;

              

               a26: 1 <= (j + 1) by NAT_1: 11;

              then

               A27: (r . (j + 1)) in ( rng r) by FUNCT_1: 3, A1, A22, FINSEQ_3: 25;

              

               A28: (j + 1) = ( len (r | (j + 1))) by A22, A1, FINSEQ_1: 59

              .= (( len rj) + ( len q)) by A25, FINSEQ_1: 22

              .= (j + ( len q)) by A20, A24, A1, FINSEQ_1: 59;

              then ( dom q) = ( Seg 1) by FINSEQ_1:def 3;

              then

               A29: 1 in ( dom q);

              

               A30: ( len (r | j)) = j by A20, A1, FINSEQ_1: 59;

              then

               A31: ((r | (j + 1)) . (j + 1)) = (q . 1) by A25, A29, FINSEQ_1:def 7;

              ( dom (r | (j + 1))) = ( Seg (j + 1)) by A23, FINSEQ_1:def 3;

              then

               A32: (r . (j + 1)) = ((r | (j + 1)) . (j + 1)) by FUNCT_1: 47, FINSEQ_1: 3;

              then

              reconsider a = (q . 1) as Element of R by A30, A27, A25, A29, FINSEQ_1:def 7;

              

               A33: (h . a) = (s . (j + 1)) by A31, A32, a26, A3, A1, A22, FINSEQ_3: 25;

              q = <*a*> by A28, FINSEQ_1: 40;

              

              then (h . ( Sum (r | (j + 1)))) = ((h . ( Sum rj)) + (h . a)) by A25, Th17

              .= (( Sum (s | j)) + ( Sum <*(h . a)*>)) by RLVECT_1: 44, A21

              .= ( Sum ((s | j) ^ <*(h . a)*>)) by RLVECT_1: 41

              .= ( Sum (s | (j + 1))) by A20, A2, A33, FINSEQ_5: 83;

              hence P[(j + 1)];

            end;

            

             A34: for i be Element of NAT st 1 <= i & i <= m1 holds P[i] from INT_1:sch 7( A7, A19);

            

             A35: ( Sum s) = ( Sum (s | (m + 1))) by A2, FINSEQ_1: 58

            .= (h . ( Sum (r | (m + 1)))) by A34, A6

            .= (h . ( Sum r)) by A1, FINSEQ_1: 58;

            (a1 *' b1) = (a * b) by POLYNOM3:def 10;

            then ((g . (a * b)) . m) = (gab1 . m) by A35, A2, A1, Def2;

            hence ((g . (a * b)) . m) = (gab . m) by POLYNOM3:def 10;

          end;

          hence (g . (a * b)) = ((g . a) * (g . b)) by FUNCT_2: 63;

        end;

        hence g is multiplicative;

        now

          let m be Element of NAT ;

          per cases ;

            suppose

             A36: m = 0 ;

            

            then (h . (1RP . m)) = (h . (( 1_. R) . 0 )) by POLYNOM3:def 10

            .= (h . ( 1_ R)) by POLYNOM3: 30

            .= ( 1_ S) by GROUP_1:def 13

            .= (( 1_. S) . 0 ) by POLYNOM3: 30

            .= (1SP . m) by A36, POLYNOM3:def 10;

            hence ((g . ( 1_ RP)) . m) = (1SP . m) by Def2;

          end;

            suppose

             A37: m <> 0 ;

            (h . (1RP . m)) = (h . (( 1_. R) . m)) by POLYNOM3:def 10

            .= (h . ( 0. R)) by A37, POLYNOM3: 30

            .= ( 0. S) by RING_2: 6

            .= (( 1_. S) . m) by A37, POLYNOM3: 30

            .= (1SP . m) by POLYNOM3:def 10;

            hence ((g . ( 1_ RP)) . m) = (1SP . m) by Def2;

          end;

        end;

        hence thesis by FUNCT_2: 63;

      end;

    end

    theorem :: FIELD_1:22

    

     Th23: for R be Ring, S be R -homomorphic Ring holds for h be Homomorphism of R, S holds (( PolyHom h) . ( 0_. R)) = ( 0_. S)

    proof

      let R be Ring, S be R -homomorphic Ring;

      let h be Homomorphism of R, S;

      

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

      reconsider f = (( PolyHom h) . ( 0. ( Polynom-Ring R))) as Element of the carrier of ( Polynom-Ring S);

      now

        let i be Element of NAT ;

        (f . i) = (h . (( 0_. R) . i)) by Def2, A1

        .= (h . ( 0. R)) by FUNCOP_1: 7

        .= ( 0. S) by RING_2: 6

        .= (( 0_. S) . i) by FUNCOP_1: 7;

        hence (f . i) = (( 0_. S) . i);

      end;

      hence thesis by A1, FUNCT_2: 63;

    end;

    theorem :: FIELD_1:23

    for R be Ring, S be R -homomorphic Ring holds for h be Homomorphism of R, S holds (( PolyHom h) . ( 1_. R)) = ( 1_. S)

    proof

      let R be Ring, S be R -homomorphic Ring;

      let h be Homomorphism of R, S;

      

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

      .= ( 1_ ( Polynom-Ring S)) by GROUP_1:def 13

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

    end;

    theorem :: FIELD_1:24

    for R be Ring, S be R -homomorphic Ring holds for h be Homomorphism of R, S holds for p,q be Element of the carrier of ( Polynom-Ring R) holds (( PolyHom h) . (p + q)) = ((( PolyHom h) . p) + (( PolyHom h) . q)) by VECTSP_1:def 20;

    theorem :: FIELD_1:25

    for R be Ring, S be R -homomorphic Ring holds for h be Homomorphism of R, S holds for p,q be Element of the carrier of ( Polynom-Ring R) holds (( PolyHom h) . (p * q)) = ((( PolyHom h) . p) * (( PolyHom h) . q)) by GROUP_6:def 6;

    theorem :: FIELD_1:26

    

     Th27: for R be Ring, S be R -homomorphic Ring holds for h be Homomorphism of R, S holds for p be Element of the carrier of ( Polynom-Ring R), b be Element of R holds (( PolyHom h) . (b * p)) = ((h . b) * (( PolyHom h) . p))

    proof

      let R be Ring, S be R -homomorphic Ring;

      let h be Homomorphism of R, S;

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

      reconsider q = (b * p) as Element of the carrier of ( Polynom-Ring R) by POLYNOM3:def 10;

      reconsider f = (( PolyHom h) . q) as Element of the carrier of ( Polynom-Ring S);

      now

        let i be Element of NAT ;

        (f . i) = (h . (q . i)) by Def2

        .= (h . (b * (p . i))) by POLYNOM5:def 4

        .= ((h . b) * (h . (p . i))) by GROUP_6:def 6

        .= ((h . b) * ((( PolyHom h) . p) . i)) by Def2

        .= (((h . b) * (( PolyHom h) . p)) . i) by POLYNOM5:def 4;

        hence (f . i) = (((h . b) * (( PolyHom h) . p)) . i);

      end;

      hence thesis by FUNCT_2: 63;

    end;

    

     Lm2: for R be Ring, S be R -homomorphic Ring holds for h be Homomorphism of R, S holds for p be Element of the carrier of ( Polynom-Ring R) holds ( len (( PolyHom h) . p)) <= ( len p)

    proof

      let R be Ring, S be R -homomorphic Ring;

      let h be Homomorphism of R, S;

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

      reconsider f = (( PolyHom h) . p) as Element of the carrier of ( Polynom-Ring S);

      now

        let i be Nat;

        assume i >= ( len p);

        then (p . i) = ( 0. R) by ALGSEQ_1: 8;

        

        hence (f . i) = (h . ( 0. R)) by Def2

        .= ( 0. S) by RING_2: 6;

      end;

      then ( len p) is_at_least_length_of f;

      hence thesis by ALGSEQ_1:def 3;

    end;

    

     Lm3: for R be Ring, S be R -homomorphic Ring holds for h be Homomorphism of R, S holds for p be Element of the carrier of ( Polynom-Ring R) st ( len p) <> 0 holds ( len (( PolyHom h) . p)) = ( len p) iff (h . (p . (( len p) -' 1))) <> ( 0. S)

    proof

      let R be Ring, S be R -homomorphic Ring;

      let h be Homomorphism of R, S;

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

      set lp1 = (( len p) -' 1);

      assume ( len p) <> 0 ;

      then

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

      then

       A3: (lp1 + 1) = ( len p);

      

       A4: ( len (( PolyHom h) . p)) <= ( len p) by Lm2;

       A5:

      now

        assume (h . (p . (( len p) -' 1))) <> ( 0. S);

        then

         A6: ((( PolyHom h) . p) . (( len p) -' 1)) <> ( 0. S) by Def2;

        now

          assume ( len (( PolyHom h) . p)) < ( len p);

          then ( len (( PolyHom h) . p)) <= lp1 by A3, NAT_1: 13;

          hence contradiction by A6, ALGSEQ_1: 8;

        end;

        hence ( len (( PolyHom h) . p)) = ( len p) by A4, XXREAL_0: 1;

      end;

      now

        assume ( len (( PolyHom h) . p)) = ( len p);

        then ( len (( PolyHom h) . p)) = (lp1 + 1) by A2;

        then ((( PolyHom h) . p) . lp1) <> ( 0. S) by ALGSEQ_1: 10;

        hence (h . (p . (( len p) -' 1))) <> ( 0. S) by Def2;

      end;

      hence thesis by A5;

    end;

    

     Lm4: for R be Ring, S be R -homomorphic Ring holds for h be Homomorphism of R, S holds for p,L be Element of the carrier of ( Polynom-Ring R) st L = ( LM p) holds for a be Element of R holds (h . ( eval (( LM p),a))) = ( eval ((( PolyHom h) . L),(h . a)))

    proof

      let R be Ring, S be R -homomorphic Ring;

      let h be Homomorphism of R, S;

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

      assume

       A1: L = ( LM p);

      let a be Element of R;

      per cases ;

        suppose

         A2: p = ( 0_. R);

        then

         A3: L = ( 0_. R) by A1, POLYNOM4: 13;

        

        thus (h . ( eval (( LM p),a))) = (h . ( eval (( 0_. R),a))) by A2, POLYNOM4: 13

        .= (h . ( 0. R)) by POLYNOM4: 17

        .= ( 0. S) by RING_2: 6

        .= ( eval (( 0_. S),(h . a))) by POLYNOM4: 17

        .= ( eval ((( PolyHom h) . L),(h . a))) by A3, Th23;

      end;

        suppose

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

        set f = ( PolyHom h);

        reconsider q = (( PolyHom h) . L) as Polynomial of S;

        consider F be FinSequence of the carrier of R such that

         A5: ( eval (( LM p),a)) = ( Sum F) & ( len F) = ( len ( LM p)) & for n be Element of NAT st n in ( dom F) holds (F . n) = ((( LM p) . (n -' 1)) * (( power R) . (a,(n -' 1)))) by POLYNOM4:def 2;

        

         A6: ( Sum F) = ((p . (( len p) -' 1)) * (( power R) . (a,(( len p) -' 1)))) by A5, POLYNOM4: 22

        .= ((( LM p) . (( len p) -' 1)) * (( power R) . (a,(( len p) -' 1)))) by POLYNOM4:def 1;

        consider G be FinSequence of the carrier of S such that

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

        

         A8: ( len q) <= ( len L) by Lm2;

        

         A9: ( len G) <= ( len F) by A1, A5, A7, Lm2;

        

         A10: ( len F) = ( len p) by A5, POLYNOM4: 15;

        then

         A11: ( len F) <> 0 by A4, POLYNOM4: 5;

        then

         A12: ( 0 + 1) <= ( len F) by NAT_1: 13;

        

         A13: (( len p) -' 1) = (( len p) - 1) by A11, A10, XREAL_0:def 2;

        

         A15: for n be Element of NAT st n in ( dom G) holds n in ( dom F)

        proof

          let n be Element of NAT ;

          assume n in ( dom G);

          then 1 <= n <= ( len q) by A7, FINSEQ_3: 25;

          then 1 <= n <= ( len L) by A8, XXREAL_0: 2;

          hence thesis by A1, A5, FINSEQ_3: 25;

        end;

        

         A16: for n be Element of NAT st n in ( dom G) holds (h . (F . n)) = (G . n)

        proof

          let n be Element of NAT ;

          assume

           A17: n in ( dom G);

          

          hence (h . (F . n)) = (h . ((( LM p) . (n -' 1)) * (( power R) . (a,(n -' 1))))) by A15, A5

          .= ((h . (L . (n -' 1))) * (h . (( power R) . (a,(n -' 1))))) by A1, GROUP_6:def 6

          .= ((q . (n -' 1)) * (h . (( power R) . (a,(n -' 1))))) by Def2

          .= ((q . (n -' 1)) * (h . (a |^ (n -' 1)))) by BINOM:def 2

          .= ((q . (n -' 1)) * ((h . a) |^ (n -' 1))) by Th14

          .= ((q . (n -' 1)) * (( power S) . ((h . a),(n -' 1)))) by BINOM:def 2

          .= (G . n) by A17, A7;

        end;

        

         A18: for n be Element of NAT st n in ( dom G) & n <> ( len p) holds (G /. n) = ( 0. S)

        proof

          let n be Element of NAT ;

          assume

           A19: n in ( dom G) & n <> ( len p);

          then 1 <= n by FINSEQ_3: 25;

          then (n - 1) = (n -' 1) by XREAL_0:def 2;

          then

           A20: (n -' 1) <> (( len p) -' 1) by A19, A13;

          

          thus (G /. n) = (G . n) by A19, PARTFUN1:def 6

          .= (h . (F . n)) by A16, A19

          .= (h . ((( LM p) . (n -' 1)) * (( power R) . (a,(n -' 1))))) by A5, A19, A15

          .= (h . (( 0. R) * (( power R) . (a,(n -' 1))))) by A20, POLYNOM4:def 1

          .= ( 0. S) by RING_2: 6;

        end;

        per cases by A9, XXREAL_0: 1;

          suppose

           A21: ( len G) = ( len F);

          then

           A22: ( len G) in ( dom G) by A12, FINSEQ_3: 25;

          ( Sum G) = (G /. ( len G)) by A18, A21, A10, POLYNOM2: 3, A12, FINSEQ_3: 25

          .= (G . ( len G)) by A22, PARTFUN1:def 6

          .= (h . (F . ( len F))) by A12, FINSEQ_3: 25, A16, A21

          .= (h . ( Sum F)) by A6, FINSEQ_3: 25, A12, A5, A10;

          hence thesis by A5, A7;

        end;

          suppose

           A23: ( len G) < ( len F);

          

          then ( 0. S) = (h . (L . (( len L) -' 1))) by A7, A5, A1, Lm3

          .= (h . (L . (( len p) -' 1))) by A1, POLYNOM4: 15

          .= (h . (p . (( len p) -' 1))) by A1, POLYNOM4:def 1;

          

          then

           A24: ( 0. S) = ((h . (p . (( len p) -' 1))) * (h . (( power R) . (a,(( len p) -' 1)))))

          .= (h . ((p . (( len p) -' 1)) * (( power R) . (a,(( len p) -' 1))))) by GROUP_6:def 6

          .= (h . ( eval (( LM p),a))) by POLYNOM4: 22;

          now

            let n be Element of NAT ;

            assume

             A25: n in ( dom G);

            then n in ( Seg ( len G)) by FINSEQ_1:def 3;

            then n <> ( len p) by A23, A10, FINSEQ_1: 1;

            

            hence ( 0. S) = (G /. n) by A25, A18

            .= (G . n) by A25, PARTFUN1:def 6;

          end;

          hence thesis by A24, A7, POLYNOM3: 1;

        end;

      end;

    end;

    theorem :: FIELD_1:27

    

     Th28: for R be Ring, S be R -homomorphic Ring holds for h be Homomorphism of R, S holds for p be Element of the carrier of ( Polynom-Ring R), a be Element of R holds (h . ( eval (p,a))) = ( eval ((( PolyHom h) . p),(h . a)))

    proof

      let R be Ring, S be R -homomorphic Ring;

      let h be Homomorphism of R, S;

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

      defpred P[ Nat] means for p be Element of the carrier of ( Polynom-Ring R), a be Element of R st ( len p) = $1 holds (h . ( eval (p,a))) = ( eval ((( PolyHom h) . p),(h . a)));

      

       A1: P[ 0 ]

      proof

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

        assume

         A2: ( len p) = 0 ;

        then

         A3: p = ( 0_. R) by POLYNOM4: 5;

        

        thus (h . ( eval (p,a))) = (h . ( eval (( 0_. R),a))) by A2, POLYNOM4: 5

        .= (h . ( 0. R)) by POLYNOM4: 17

        .= ( 0. S) by RING_2: 6

        .= ( eval (( 0_. S),(h . a))) by POLYNOM4: 17

        .= ( eval ((( PolyHom h) . p),(h . a))) by A3, Th23;

      end;

       A4:

      now

        let k be Nat;

        assume

         A5: for m be Nat st m < k holds P[m];

        now

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

          assume

           A6: ( len p) = k;

          per cases ;

            suppose k = 0 ;

            hence (h . ( eval (p,a))) = ( eval ((( PolyHom h) . p),(h . a))) by A6, A1;

          end;

            suppose k > 0 ;

            then

            consider q be Polynomial of R such that

             A7: ( len q) < ( len p) & p = (q + ( LM p)) & for n be Element of NAT st n < (( len p) - 1) holds (q . n) = (p . n) by A6, POLYNOM4: 16;

            reconsider g = q as Element of the carrier of ( Polynom-Ring R) by POLYNOM3:def 10;

            reconsider LMp = ( LM p) as Element of the carrier of ( Polynom-Ring R) by POLYNOM3:def 10;

            reconsider g1 = (( PolyHom h) . g), g2 = (( PolyHom h) . LMp) as Polynomial of S;

            

             A8: ((( PolyHom h) . g) + (( PolyHom h) . LMp)) = (g1 + g2) by POLYNOM3:def 10;

            

             A9: (h . ( eval (q,a))) = ( eval ((( PolyHom h) . g),(h . a))) by A6, A7, A5;

            

            thus (h . ( eval (p,a))) = (h . (( eval (q,a)) + ( eval (LMp,a)))) by A7, POLYNOM4: 19

            .= ((h . ( eval (q,a))) + (h . ( eval (LMp,a)))) by VECTSP_1:def 20

            .= (( eval ((( PolyHom h) . g),(h . a))) + ( eval ((( PolyHom h) . LMp),(h . a)))) by A9, Lm4

            .= ( eval ((g1 + g2),(h . a))) by POLYNOM4: 19

            .= ( eval ((( PolyHom h) . (g + LMp)),(h . a))) by A8, VECTSP_1:def 20

            .= ( eval ((( PolyHom h) . p),(h . a))) by A7, POLYNOM3:def 10;

          end;

        end;

        hence P[k];

      end;

      

       A10: for k be Nat holds P[k] from NAT_1:sch 4( A4);

      ex n be Nat st n = ( len p);

      hence thesis by A10;

    end;

    theorem :: FIELD_1:28

    for R be domRing, S be R -homomorphic domRing holds for h be Homomorphism of R, S holds for p be Element of the carrier of ( Polynom-Ring R), b,x be Element of R holds (h . ( eval ((b * p),x))) = ((h . b) * ( eval ((( PolyHom h) . p),(h . x))))

    proof

      let R be domRing, S be R -homomorphic domRing;

      let h be Homomorphism of R, S;

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

      reconsider q = (b * p) as Element of the carrier of ( Polynom-Ring R) by POLYNOM3:def 10;

      (h . ( eval ((b * p),x))) = ( eval ((( PolyHom h) . q),(h . x))) by Th28

      .= ( eval (((h . b) * (( PolyHom h) . p)),(h . x))) by Th27

      .= ((h . b) * ( eval ((( PolyHom h) . p),(h . x)))) by RING_5: 7;

      hence thesis;

    end;

    registration

      let R be Ring;

      cluster R -homomorphicR -monomorphic for Ring;

      existence

      proof

        take R;

        ( id R) is RingHomomorphism;

        hence R is R -homomorphic;

        ( id R) is RingMonomorphism;

        hence R is R -monomorphic by RING_3:def 3;

      end;

      cluster R -homomorphicR -isomorphic for Ring;

      existence

      proof

        take R;

        ( id R) is RingHomomorphism;

        hence R is R -homomorphic;

        ( id R) is RingIsomorphism;

        hence R is R -isomorphic by RING_3:def 4;

      end;

    end

    registration

      let R be Ring;

      cluster R -monomorphic -> R -homomorphic for Ring;

      coherence ;

    end

    registration

      let R be Ring, S be R -homomorphicR -monomorphic Ring;

      let h be Monomorphism of R, S;

      cluster ( PolyHom h) -> monomorphism;

      coherence

      proof

        set f = ( PolyHom h);

        now

          let x1,x2 be object;

          assume

           A1: x1 in the carrier of ( Polynom-Ring R) & x2 in the carrier of ( Polynom-Ring R) & (f . x1) = (f . x2);

          then

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

          now

            let i be Element of NAT ;

            (h . (p . i)) = ((f . q) . i) by A1, Def2

            .= (h . (q . i)) by Def2;

            hence (p . i) = (q . i) by FUNCT_2: 19;

          end;

          then p = q;

          hence x1 = x2;

        end;

        then f is one-to-one by FUNCT_2: 19;

        hence thesis;

      end;

    end

    registration

      let R be Ring, S be R -isomorphicR -homomorphic Ring;

      let h be Isomorphism of R, S;

      cluster ( PolyHom h) -> isomorphism;

      coherence

      proof

        set f = ( PolyHom h);

        

         A1: for o be object st o in ( rng f) holds o in the carrier of ( Polynom-Ring S);

        now

          let o be object;

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

          then

          reconsider p = o as Element of the carrier of ( Polynom-Ring S);

          deffunc F( object) = ((h " ) . (p . $1));

          

           A2: for o be object st o in NAT holds F(o) in the carrier of R

          proof

            let o be object;

            assume o in NAT ;

            then

            reconsider i = o as Element of NAT ;

             F(i) = ((h " ) . (p . i));

            hence thesis;

          end;

          consider q be Function of NAT , the carrier of R such that

           A3: for x be object st x in NAT holds (q . x) = F(x) from FUNCT_2:sch 2( A2);

          ex n be Nat st for i be Nat st i >= n holds (q . i) = ( 0. R)

          proof

            take n = ( len p);

            now

              let i be Nat;

              

               A4: (h " ) is Isomorphism of S, R by RING_3: 73;

              assume i >= n;

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

              

              hence (q . i) = ((h " ) . ( 0. S)) by A3, ORDINAL1:def 12

              .= ( 0. R) by A4, RING_2: 6;

            end;

            hence thesis;

          end;

          then

          reconsider q as Polynomial of R by ALGSEQ_1:def 1;

          reconsider q as Element of the carrier of ( Polynom-Ring R) by POLYNOM3:def 10;

          

           A5: ( dom f) = the carrier of ( Polynom-Ring R) by FUNCT_2:def 1;

          now

            let i be Element of NAT ;

            

             A6: ( dom (h " )) = the carrier of S by FUNCT_2:def 1;

            ((f . q) . i) = (h . (q . i)) by Def2

            .= (((h " ) " ) . ((h " ) . (p . i))) by A3

            .= (p . i) by A6, FUNCT_1: 34;

            hence ((f . q) . i) = (p . i);

          end;

          then (f . q) = p;

          hence o in ( rng f) by A5, FUNCT_1:def 3;

        end;

        then f is onto by A1, TARSKI: 2;

        hence thesis;

      end;

    end

    theorem :: FIELD_1:29

    for R be Ring, S be R -homomorphic Ring holds for h be Homomorphism of R, S holds for p be Element of the carrier of ( Polynom-Ring R) holds ( deg (( PolyHom h) . p)) <= ( deg p) by Lm2, XREAL_1: 6;

    theorem :: FIELD_1:30

    for R be non degenerated Ring, S be R -homomorphic Ring holds for h be Homomorphism of R, S holds for p be non zero Element of the carrier of ( Polynom-Ring R) holds ( deg (( PolyHom h) . p)) = ( deg p) iff (h . ( LC p)) <> ( 0. S)

    proof

      let R be non degenerated Ring, S be R -homomorphic Ring;

      let h be Homomorphism of R, S;

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

      p <> ( 0_. R);

      then

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

      hereby

        assume ( deg (( PolyHom h) . p)) = ( deg p);

        then (h . (p . (( len p) -' 1))) <> ( 0. S) by A1, Lm3;

        hence (h . ( LC p)) <> ( 0. S) by RATFUNC1:def 6;

      end;

      assume (h . ( LC p)) <> ( 0. S);

      then (h . (p . (( len p) -' 1))) <> ( 0. S) by RATFUNC1:def 6;

      hence ( deg (( PolyHom h) . p)) = ( deg p) by A1, Lm3;

    end;

    theorem :: FIELD_1:31

    

     Th32: for R be Ring, S be R -monomorphicR -homomorphic Ring holds for h be Monomorphism of R, S holds for p be Element of the carrier of ( Polynom-Ring R) holds ( deg (( PolyHom h) . p)) = ( deg p)

    proof

      let R be Ring, S be R -monomorphicR -homomorphic Ring;

      let h be Monomorphism of R, S;

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

      reconsider f = (( PolyHom h) . p) as Element of the carrier of ( Polynom-Ring S);

       A1:

      now

        let i be Nat;

        assume i >= ( len p);

        then (p . i) = ( 0. R) by ALGSEQ_1: 8;

        

        hence (f . i) = (h . ( 0. R)) by Def2

        .= ( 0. S) by RING_2: 6;

      end;

      now

        let m be Nat;

        assume

         A2: m is_at_least_length_of f;

        now

          assume ( len p) > m;

          then (( len p) - 1) > (m - 1) by XREAL_1: 6;

          then

           A3: (( len p) - 1) >= ((m - 1) + 1) by INT_1: 7;

          then

          reconsider lp = (( len p) - 1) as Element of NAT by INT_1: 3;

          

           A4: (lp + 1) = ( len p);

          (h . ( 0. R)) = ( 0. S) by RING_2: 6

          .= (f . lp) by A3, A2

          .= (h . (p . lp)) by Def2;

          then (p . lp) = ( 0. R) by FUNCT_2: 19;

          hence contradiction by A4, ALGSEQ_1: 10;

        end;

        hence ( len p) <= m;

      end;

      hence thesis by A1, ALGSEQ_1:def 2, ALGSEQ_1:def 3;

    end;

    theorem :: FIELD_1:32

    

     Th33: for R be Ring, S be R -monomorphicR -homomorphic Ring holds for h be Monomorphism of R, S holds for p be Element of the carrier of ( Polynom-Ring R) holds ( LM (( PolyHom h) . p)) = (( PolyHom h) . ( LM p))

    proof

      let R be Ring, S be R -monomorphicR -homomorphic Ring;

      let h be Monomorphism of R, S;

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

      reconsider f = (( PolyHom h) . p) as Element of the carrier of ( Polynom-Ring S);

      reconsider LMp = ( LM p) as Element of the carrier of ( Polynom-Ring R) by POLYNOM3:def 10;

      

       A1: ( deg f) = ( deg p) by Th32

      .= (( len p) - 1);

      now

        let i be Element of NAT ;

        per cases ;

          suppose

           A2: i = (( len p) -' 1);

          

          then (( LM f) . i) = (f . (( len p) -' 1)) by A1, POLYNOM4:def 1

          .= (h . (p . (( len p) -' 1))) by Def2

          .= (h . (( LM p) . i)) by A2, POLYNOM4:def 1

          .= ((( PolyHom h) . LMp) . i) by Def2;

          hence (( LM f) . i) = ((( PolyHom h) . LMp) . i);

        end;

          suppose

           A3: i <> (( len p) -' 1);

          

          then (( LM f) . i) = ( 0. S) by A1, POLYNOM4:def 1

          .= (h . ( 0. R)) by RING_2: 6

          .= (h . (( LM p) . i)) by A3, POLYNOM4:def 1

          .= ((( PolyHom h) . LMp) . i) by Def2;

          hence (( LM f) . i) = ((( PolyHom h) . LMp) . i);

        end;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: FIELD_1:33

    

     Th34: for R be Ring, S be R -homomorphic Ring holds for h be Homomorphism of R, S holds for p be Element of the carrier of ( Polynom-Ring R), a be Element of R holds a is_a_root_of p implies (h . a) is_a_root_of (( PolyHom h) . p)

    proof

      let R be Ring, S be R -homomorphic Ring;

      let h be Homomorphism of R, S;

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

      assume a is_a_root_of p;

      then ( eval (p,a)) = ( 0. R) by POLYNOM5:def 7;

      

      then ( eval ((( PolyHom h) . p),(h . a))) = (h . ( 0. R)) by Th28

      .= ( 0. S) by RING_2: 6;

      hence thesis by POLYNOM5:def 7;

    end;

    theorem :: FIELD_1:34

    

     Th35: for R be Ring, S be R -monomorphicR -homomorphic Ring holds for h be Monomorphism of R, S holds for p be Element of the carrier of ( Polynom-Ring R), a be Element of R holds a is_a_root_of p iff (h . a) is_a_root_of (( PolyHom h) . p)

    proof

      let R be Ring, S be R -monomorphicR -homomorphic Ring;

      let h be Monomorphism of R, S;

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

      now

        assume

         A1: (h . a) is_a_root_of (( PolyHom h) . p);

        (h . ( 0. R)) = ( 0. S) by RING_2: 6

        .= ( eval ((( PolyHom h) . p),(h . a))) by A1, POLYNOM5:def 7

        .= (h . ( eval (p,a))) by Th28;

        then ( eval (p,a)) = ( 0. R) by FUNCT_2: 19;

        hence a is_a_root_of p by POLYNOM5:def 7;

      end;

      hence thesis by Th34;

    end;

    theorem :: FIELD_1:35

    

     Th36: for R be Ring, S be R -isomorphicR -homomorphic Ring holds for h be Isomorphism of R, S holds for p be Element of the carrier of ( Polynom-Ring R), b be Element of S holds b is_a_root_of (( PolyHom h) . p) iff ex a be Element of R st a is_a_root_of p & (h . a) = b

    proof

      let R be Ring, S be R -isomorphicR -homomorphic Ring;

      let h be Isomorphism of R, S;

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

       A1:

      now

        assume

         A2: b is_a_root_of (( PolyHom h) . p);

        set a = ((h " ) . b);

        

         A3: ( dom (h " )) = the carrier of S by FUNCT_2:def 1;

        

         A4: (h . a) = (((h " ) " ) . ((h " ) . b))

        .= b by A3, FUNCT_1: 34;

        (h . ( eval (p,a))) = ( eval ((( PolyHom h) . p),(h . a))) by Th28

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

        .= (h . ( 0. R)) by RING_2: 6;

        then ( eval (p,a)) = ( 0. R) by FUNCT_2: 19;

        hence ex a be Element of R st (h . a) = b & a is_a_root_of p by A4, POLYNOM5:def 7;

      end;

      now

        assume ex a be Element of R st (h . a) = b & a is_a_root_of p;

        then

        consider a be Element of R such that

         A5: (h . a) = b & a is_a_root_of p;

        ( eval ((( PolyHom h) . p),b)) = (h . ( eval (p,a))) by A5, Th28

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

        .= ( 0. S) by RING_2: 6;

        hence b is_a_root_of (( PolyHom h) . p) by POLYNOM5:def 7;

      end;

      hence thesis by A1;

    end;

    theorem :: FIELD_1:36

    

     Th37: for R be Ring, S be R -homomorphic Ring holds for h be Homomorphism of R, S holds for p be Element of the carrier of ( Polynom-Ring R) holds ( Roots p) c= { a where a be Element of R : (h . a) in ( Roots (( PolyHom h) . p)) }

    proof

      let R be Ring, S be R -homomorphic Ring;

      let h be Homomorphism of R, S;

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

      let o be object;

      assume

       A1: o in ( Roots p);

      then

      reconsider a = o as Element of R;

      a is_a_root_of p by A1, POLYNOM5:def 10;

      then (h . a) is_a_root_of (( PolyHom h) . p) by Th34;

      then (h . a) in ( Roots (( PolyHom h) . p)) by POLYNOM5:def 10;

      hence o in { a where a be Element of R : (h . a) in ( Roots (( PolyHom h) . p)) };

    end;

    theorem :: FIELD_1:37

    for R be Ring, S be R -monomorphicR -homomorphic Ring holds for h be Monomorphism of R, S holds for p be Element of the carrier of ( Polynom-Ring R) holds ( Roots p) = { a where a be Element of R : (h . a) in ( Roots (( PolyHom h) . p)) }

    proof

      let R be Ring, S be R -monomorphicR -homomorphic Ring;

      let h be Monomorphism of R, S;

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

      

       A1: ( Roots p) c= { a where a be Element of R : (h . a) in ( Roots (( PolyHom h) . p)) } by Th37;

      now

        let o be object;

        assume o in { a where a be Element of R : (h . a) in ( Roots (( PolyHom h) . p)) };

        then

        consider a be Element of R such that

         A2: o = a & (h . a) in ( Roots (( PolyHom h) . p));

        (h . a) is_a_root_of (( PolyHom h) . p) by A2, POLYNOM5:def 10;

        then a is_a_root_of p by Th35;

        hence o in ( Roots p) by A2, POLYNOM5:def 10;

      end;

      hence thesis by TARSKI: 2, A1;

    end;

    theorem :: FIELD_1:38

    

     Th39: for R be Ring, S be R -isomorphicR -homomorphic Ring holds for h be Isomorphism of R, S holds for p be Element of the carrier of ( Polynom-Ring R) holds ( Roots (( PolyHom h) . p)) = { (h . a) where a be Element of R : a in ( Roots p) }

    proof

      let R be Ring, S be R -isomorphicR -homomorphic Ring;

      let h be Isomorphism of R, S;

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

       A1:

      now

        let o be object;

        assume

         A2: o in ( Roots (( PolyHom h) . p));

        then

        reconsider b = o as Element of S;

        b is_a_root_of (( PolyHom h) . p) by A2, POLYNOM5:def 10;

        then

        consider a be Element of R such that

         A3: a is_a_root_of p & (h . a) = b by Th36;

        a in ( Roots p) by A3, POLYNOM5:def 10;

        hence o in { (h . a) where a be Element of R : a in ( Roots p) } by A3;

      end;

      now

        let o be object;

        assume o in { (h . a) where a be Element of R : a in ( Roots p) };

        then

        consider a be Element of R such that

         A4: o = (h . a) & a in ( Roots p);

        a is_a_root_of p by A4, POLYNOM5:def 10;

        then (h . a) is_a_root_of (( PolyHom h) . p) by Th36;

        hence o in ( Roots (( PolyHom h) . p)) by A4, POLYNOM5:def 10;

      end;

      hence thesis by A1, TARSKI: 2;

    end;

    begin

    reserve F for Field,

p for irreducible Element of the carrier of ( Polynom-Ring F),

f for Element of the carrier of ( Polynom-Ring F),

a for Element of F;

    definition

      let F, p;

      :: FIELD_1:def3

      func KroneckerField (F,p) -> Field equals (( Polynom-Ring F) / ( {p} -Ideal ));

      coherence ;

    end

    definition

      let F, p;

      :: FIELD_1:def4

      func emb p -> Function of F, ( KroneckerField (F,p)) equals (( canHom ( {p} -Ideal )) * ( canHom F));

      coherence ;

    end

    registration

      let F, p;

      cluster ( emb p) -> additive multiplicative unity-preserving;

      coherence ;

    end

    registration

      let F, p;

      cluster ( emb p) -> monomorphism;

      coherence ;

    end

    registration

      let F, p;

      cluster ( KroneckerField (F,p)) -> F -homomorphicF -monomorphic;

      coherence

      proof

        ( emb p) is monomorphism;

        hence thesis by RING_3:def 3;

      end;

    end

    definition

      let F, p, f;

      :: FIELD_1:def5

      func emb (f,p) -> Element of the carrier of ( Polynom-Ring ( KroneckerField (F,p))) equals (( PolyHom ( emb p)) . f);

      coherence ;

    end

    definition

      let F, p;

      :: FIELD_1:def6

      func KrRoot p -> Element of ( KroneckerField (F,p)) equals ( Class (( EqRel (( Polynom-Ring F),( {p} -Ideal ))), <%( 0. F), ( 1. F)%>));

      coherence

      proof

        set E = ( KroneckerField (F,p));

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

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

        hence thesis;

      end;

    end

    theorem :: FIELD_1:39

    

     Th40: for F, p, a holds (( emb p) . a) = ( Class (( EqRel (( Polynom-Ring F),( {p} -Ideal ))),(a | F)))

    proof

      let F, p, a;

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

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

      

      hence (( emb p) . a) = (( canHom ( {p} -Ideal )) . (( canHom F) . a)) by FUNCT_1: 13

      .= (( canHom ( {p} -Ideal )) . pa) by RING_4:def 6

      .= ( Class (( EqRel (( Polynom-Ring F),( {p} -Ideal ))),(a | F))) by RING_2:def 5;

    end;

    theorem :: FIELD_1:40

    

     Th41: (( emb (f,p)) . n) = ( Class (( EqRel (( Polynom-Ring F),( {p} -Ideal ))),((f . n) | F)))

    proof

      

      thus (( emb (f,p)) . n) = (( emb p) . (f . n)) by Def2

      .= ( Class (( EqRel (( Polynom-Ring F),( {p} -Ideal ))),((f . n) | F))) by Th40;

    end;

    

     Lm5: ( eval (( LM ( emb (f,p))),( KrRoot p))) = ( Class (( EqRel (( Polynom-Ring F),( {p} -Ideal ))),( LM f)))

    proof

      set LMf = ( Leading-Monomial f), LMfe = ( Leading-Monomial ( emb (f,p)));

      set z = ( KrRoot p), E = ( KroneckerField (F,p));

      set efp = ( emb (f,p));

      set n = (( len efp) -' 1);

      per cases ;

        suppose

         A1: f = ( 0_. F);

        then ( emb (f,p)) = ( 0_. E) by Th23;

        then LMfe = ( 0_. E) by POLYNOM4: 13;

        

        then

         A2: ( eval (LMfe,( KrRoot p))) = ( 0. E) by POLYNOM4: 17

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

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

        hence thesis by A1, A2, POLYNOM4: 13;

      end;

        suppose f <> ( 0_. F);

        then

        reconsider f1 = f as non zero Polynomial of F by UPROOTS:def 5;

        reconsider fnF = ((f . n) | F) as Element of the carrier of ( Polynom-Ring F) by POLYNOM3:def 10;

        reconsider x = <%( 0. F), ( 1. F)%> as Element of the carrier of ( Polynom-Ring F) by POLYNOM3:def 10;

        

         A3: (efp . n) = ( Class (( EqRel (( Polynom-Ring F),( {p} -Ideal ))),((f . n) | F))) by Th41;

        

         A4: (( power E) . (z,n)) = (z |^ n) by BINOM:def 2

        .= ( Class (( EqRel (( Polynom-Ring F),( {p} -Ideal ))),(x |^ n))) by Th3;

        set a = (f . n);

        

         A5: ( deg f) = ( deg efp) by Th32

        .= (( len efp) - 1);

        then

         A6: n = ( deg f1) by XREAL_0:def 2;

        ( LC f1) is non zero;

        then

         A7: a is non zero by A5, RATFUNC1:def 6;

        (x |^ n) = (( power ( Polynom-Ring F)) . ( <%( 0. F), ( 1. F)%>,n)) by BINOM:def 2

        .= ( <%( 0. F), ( 1. F)%> `^ n) by POLYNOM5:def 3

        .= ( anpoly (( 1. F),n)) by Th13;

        

        then

         A8: (fnF * (x |^ n)) = (( anpoly (a, 0 )) *' ( anpoly (( 1. F),n))) by POLYNOM3:def 10

        .= ( anpoly ((a * ( 1. F)),( 0 + n))) by A7, Th11

        .= ( LM f) by A6, Th12;

        

        thus ( eval (LMfe,( KrRoot p))) = ((efp . n) * (( power E) . (z,n))) by POLYNOM4: 22

        .= ( Class (( EqRel (( Polynom-Ring F),( {p} -Ideal ))),LMf)) by A8, A3, A4, RING_1: 14;

      end;

    end;

    theorem :: FIELD_1:41

    

     Th42: ( eval (( emb (f,p)),( KrRoot p))) = ( Class (( EqRel (( Polynom-Ring F),( {p} -Ideal ))),f))

    proof

      set z = ( KrRoot p), E = ( KroneckerField (F,p)), h = ( canHom ( emb p));

      defpred P[ Nat] means for f st ( len f) = $1 holds ( eval (( emb (f,p)),z)) = ( Class (( EqRel (( Polynom-Ring F),( {p} -Ideal ))),f));

       A1:

      now

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

        assume ( len f) = 0 ;

        then f = ( 0_. F) by POLYNOM4: 5;

        then

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

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

        .= ( emb (f,p)) by A2, RING_2: 6;

        

        hence ( eval (( emb (f,p)),z)) = ( 0. E) by POLYNOM4: 17

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

      end;

       A3:

      now

        let k be Nat;

        assume

         A4: for m be Nat st m < k holds P[m];

        now

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

          assume

           A5: ( len f) = k;

          per cases ;

            suppose k = 0 ;

            hence ( eval (( emb (f,p)),z)) = ( Class (( EqRel (( Polynom-Ring F),( {p} -Ideal ))),f)) by A5, A1;

          end;

            suppose k > 0 ;

            then

            consider q be Polynomial of F such that

             A6: ( len q) < ( len f) & f = (q + ( Leading-Monomial f)) & for n be Element of NAT st n < (( len f) - 1) holds (q . n) = (f . n) by A5, POLYNOM4: 16;

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

            reconsider LMf = ( LM f) as Element of the carrier of ( Polynom-Ring F) by POLYNOM3:def 10;

            reconsider r1 = ( emb (LMf,p)), r2 = ( emb (g,p)) as Polynomial of E;

            

             A7: ( emb ((LMf + g),p)) = (( emb (LMf,p)) + ( emb (g,p))) by VECTSP_1:def 20

            .= (r1 + r2) by POLYNOM3:def 10;

            ( Leading-Monomial ( emb (f,p))) = ( emb (LMf,p)) by Th33;

            then

             A8: ( eval (( emb (LMf,p)),z)) = ( Class (( EqRel (( Polynom-Ring F),( {p} -Ideal ))),LMf)) by Lm5;

            

             A9: ( eval (( emb (g,p)),z)) = ( Class (( EqRel (( Polynom-Ring F),( {p} -Ideal ))),g)) by A6, A5, A4;

            

             A10: (( eval (( emb (LMf,p)),z)) + ( eval (( emb (g,p)),z))) = ( Class (( EqRel (( Polynom-Ring F),( {p} -Ideal ))),(LMf + g))) by A9, A8, RING_1: 13

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

            

            thus ( eval (( emb (f,p)),z)) = ( eval ((r1 + r2),z)) by A7, A6, POLYNOM3:def 10

            .= ( Class (( EqRel (( Polynom-Ring F),( {p} -Ideal ))),f)) by A10, POLYNOM4: 19;

          end;

        end;

        hence P[k];

      end;

      

       A11: for k be Nat holds P[k] from NAT_1:sch 4( A3);

      ex n be Nat st ( len f) = n;

      hence thesis by A11;

    end;

    theorem :: FIELD_1:42

    

     Th43: ( KrRoot p) is_a_root_of ( emb (p,p))

    proof

      

       A1: (p - ( 0. ( Polynom-Ring F))) in ( {p} -Ideal ) by IDEAL_1: 66;

      ( eval (( emb (p,p)),( KrRoot p))) = ( Class (( EqRel (( Polynom-Ring F),( {p} -Ideal ))),p)) by Th42

      .= ( Class (( EqRel (( Polynom-Ring F),( {p} -Ideal ))),( 0. ( Polynom-Ring F)))) by A1, RING_1: 6

      .= ( 0. ( KroneckerField (F,p))) by RING_1:def 6;

      hence thesis by POLYNOM5:def 7;

    end;

    theorem :: FIELD_1:43

    f is non constant implies ex p be irreducible Element of the carrier of ( Polynom-Ring F) st ( emb (f,p)) is with_roots

    proof

      assume f is non constant;

      then

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

       A2: p is_a_irreducible_factor_of f by Th4;

      reconsider p as irreducible Element of the carrier of ( Polynom-Ring F) by A2;

      take p;

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

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

      

       A4: ( emb (f,p)) = ((( PolyHom ( emb p)) . p) * (( PolyHom ( emb p)) . q)) by A3, GROUP_6:def 6

      .= (( emb (p,p)) *' ( emb (q,p))) by POLYNOM3:def 10;

      ( KrRoot p) is_a_root_of ( emb (p,p)) by Th43;

      then ( emb (p,p)) is with_roots by POLYNOM5:def 8;

      hence thesis by A4;

    end;

    theorem :: FIELD_1:44

    

     Th45: ( emb p) is isomorphism implies p is with_roots

    proof

      set h = ( emb p);

      assume

       A1: ( emb p) is isomorphism;

      then

      reconsider K = ( KroneckerField (F,p)) as F -isomorphicF -homomorphic Ring by RING_3:def 4;

      reconsider h as Isomorphism of F, K by A1;

      

       A2: ( Roots (( PolyHom h) . p)) = { (h . a) where a be Element of F : a in ( Roots p) } by Th39;

      ( KrRoot p) is_a_root_of ( emb (p,p)) by Th43;

      then ( KrRoot p) in ( Roots (( PolyHom h) . p)) by POLYNOM5:def 10;

      then ex a be Element of F st ( KrRoot p) = (h . a) & a in ( Roots p) by A2;

      hence thesis;

    end;

    theorem :: FIELD_1:45

    p is non with_roots implies ( emb p) is non isomorphism by Th45;