ring_4.miz



    begin

    definition

      let R be non empty doubleLoopStr, a be Element of R;

      :: original: {

      redefine

      func {a} -> Subset of R ;

      coherence

      proof

        now

          let x be object;

          assume x in {a};

          then x = a by TARSKI:def 1;

          hence x in the carrier of R;

        end;

        hence thesis by TARSKI:def 3;

      end;

    end

    registration

      cluster almost_left_invertible commutative -> almost_right_invertible for Ring;

      coherence

      proof

        let R be Ring;

        assume

         AS: R is almost_left_invertible commutative;

        now

          let x be Element of R;

          assume x <> ( 0. R);

          then x is left_invertible by AS;

          then

          consider y be Element of R such that

           A1: (y * x) = ( 1. R);

          (x * y) = ( 1. R) by A1, AS, GROUP_1:def 12;

          hence x is right_invertible;

        end;

        hence thesis;

      end;

      cluster almost_right_invertible commutative -> almost_left_invertible for Ring;

      coherence

      proof

        let R be Ring;

        assume

         AS: R is almost_right_invertible commutative;

        now

          let x be Element of R;

          assume x <> ( 0. R);

          then x is right_invertible by AS;

          then

          consider y be Element of R such that

           A1: (x * y) = ( 1. R);

          (y * x) = ( 1. R) by A1, AS, GROUP_1:def 12;

          hence x is left_invertible;

        end;

        hence thesis;

      end;

      cluster almost_left_cancelable commutative -> almost_right_cancelable for Ring;

      coherence

      proof

        let R be Ring;

        assume

         AS: R is almost_left_cancelable commutative;

        now

          let x be Element of R;

          assume x <> ( 0. R);

          then

           AS1: x is left_mult-cancelable by AS;

          now

            let y,z be Element of R;

            assume (y * x) = (z * x);

            

            then (x * y) = (z * x) by AS, GROUP_1:def 12

            .= (x * z) by AS, GROUP_1:def 12;

            hence y = z by AS1;

          end;

          hence x is right_mult-cancelable;

        end;

        hence thesis;

      end;

      cluster almost_right_cancelable commutative -> almost_left_cancelable for Ring;

      coherence

      proof

        let R be Ring;

        assume

         AS: R is almost_right_cancelable commutative;

        now

          let x be Element of R;

          assume x <> ( 0. R);

          then

           AS1: x is right_mult-cancelable by AS;

          now

            let y,z be Element of R;

            assume (x * y) = (x * z);

            

            then (y * x) = (x * z) by AS, GROUP_1:def 12

            .= (z * x) by AS, GROUP_1:def 12;

            hence y = z by AS1;

          end;

          hence x is left_mult-cancelable;

        end;

        hence thesis;

      end;

    end

    definition

      let L be non empty ZeroStr;

      let X be set;

      :: RING_4:def1

      attr X is L -polynomial-membered means

      : polymem: for p be object st p in X holds p is Polynomial of L;

    end

    definition

      let L be non empty ZeroStr;

      let X be 1-sorted;

      :: RING_4:def2

      attr X is L -polynomial-membered means

      : polymem1: the carrier of X is L -polynomial-membered;

    end

    registration

      let L be non empty ZeroStr;

      cluster non emptyL -polynomial-membered for set;

      existence

      proof

        take s = {( 0_. L)};

        thus s is non empty;

        thus s is L -polynomial-membered by TARSKI:def 1;

      end;

    end

    registration

      let L be non empty ZeroStr;

      cluster non emptyL -polynomial-membered for 1-sorted;

      existence

      proof

        take 1-sorted (# the non emptyL -polynomial-membered set #);

        thus thesis;

      end;

    end

    registration

      let L be non empty ZeroStr;

      let X be non emptyL -polynomial-membered 1-sorted;

      cluster the carrier of X -> L -polynomial-membered;

      coherence by polymem1;

    end

    registration

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

      cluster ( Polynom-Ring L) -> L -polynomial-membered;

      coherence

      proof

        thus the carrier of ( Polynom-Ring L) is L -polynomial-membered by POLYNOM3:def 10;

      end;

    end

    definition

      let L be non empty ZeroStr;

      let X be non emptyL -polynomial-membered set;

      :: original: Element

      redefine

      mode Element of X -> Polynomial of L ;

      coherence by polymem;

    end

     lm:

    now

      let L be add-associative right_zeroed right_complementable distributive non empty doubleLoopStr, 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

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

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

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

      hence ( - a) = ( - p);

    end;

    registration

      let R be Ring;

      cluster zero for Element of the carrier of ( Polynom-Ring R);

      existence

      proof

        take ( 0_. R);

        thus thesis by POLYNOM3:def 10;

      end;

      cluster zero for Element of ( Polynom-Ring R);

      existence

      proof

        take ( 0. ( Polynom-Ring R));

        thus thesis;

      end;

      cluster zero for Polynomial of R;

      existence

      proof

        take ( 0_. R);

        thus thesis;

      end;

    end

    registration

      let R be non degenerated Ring;

      cluster non zero for Element of the carrier of ( Polynom-Ring R);

      existence

      proof

        take ( 1_. R);

        thus thesis by POLYNOM3:def 10;

      end;

      cluster non zero for Element of ( Polynom-Ring R);

      existence

      proof

        take ( 1. ( Polynom-Ring R));

        thus thesis;

      end;

    end

    

     T8a: for L be add-associative right_zeroed right_complementable distributive non trivial doubleLoopStr, p be Element of the carrier of ( Polynom-Ring L) holds ( deg p) is Element of NAT iff p <> ( 0. ( Polynom-Ring L))

    proof

      let L be add-associative right_zeroed right_complementable distributive non trivial doubleLoopStr;

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

      set R = ( Polynom-Ring L);

      reconsider pp = p as Polynomial of L;

       A:

      now

        assume ( deg p) is Element of NAT ;

        then p <> ( 0_. L) by HURWITZ: 20;

        hence p <> ( 0. R) by POLYNOM3:def 10;

      end;

      now

        assume p <> ( 0. R);

        then p <> ( 0_. L) by POLYNOM3:def 10;

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

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

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

        then (( len p) - 1) >= (1 - 1) by XREAL_1: 9;

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

      end;

      hence thesis by A;

    end;

    

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

        then (( len p) - 1) >= (1 - 1) by XREAL_1: 9;

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

      end;

      hence thesis by HURWITZ: 20;

    end;

    definition

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

      let p,q be Polynomial of L;

      :: RING_4:def3

      pred p divides q means ex a,b be Element of ( Polynom-Ring L) st a = p & b = q & a divides b;

    end

    theorem :: RING_4:1

    

     T2: for L be add-associative right_zeroed right_complementable distributive non empty doubleLoopStr holds for p,q be Polynomial of L holds p divides q iff ex r be Polynomial of L st (p *' r) = q

    proof

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

      let p,q be Polynomial of L;

       X:

      now

        assume p divides q;

        then

        consider a,b be Element of ( Polynom-Ring L) such that

         B: a = p & b = q & a divides b;

        consider u be Element of ( Polynom-Ring L) such that

         C: (a * u) = b by B;

        reconsider z = u as Polynomial of L by POLYNOM3:def 10;

        q = (p *' z) by B, C, POLYNOM3:def 10;

        hence ex r be Polynomial of L st (p *' r) = q;

      end;

      now

        assume ex r be Polynomial of L st (p *' r) = q;

        then

        consider r be Polynomial of L such that

         H: q = (p *' r);

        reconsider a = p, b = q, u = r as Element of ( Polynom-Ring L) by POLYNOM3:def 10;

        b = (a * u) by H, POLYNOM3:def 10;

        then a divides b;

        hence p divides q;

      end;

      hence thesis by X;

    end;

    theorem :: RING_4:2

    

     div1: for F be Field, p,q be Polynomial of F st ( deg p) < ( deg q) holds (p mod q) = p

    proof

      let F be Field, p,q be Polynomial of F;

      assume

       A1: ( deg p) < ( deg q);

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

      

      then

       H: ( - ( 0_. F)) = ( - ( 0. ( Polynom-Ring F))) by lm

      .= ( 0. ( Polynom-Ring F));

       A0:

      now

        assume

         A0: q = ( 0_. F);

        then ( deg p) < ( - 1) by A1, HURWITZ: 20;

        hence contradiction by A0, A1, T8b;

      end;

      p = (( 0_. F) + p) by POLYNOM3: 28

      .= ((( 0_. F) *' q) + p) by POLYNOM3: 34;

      

      hence (p mod q) = (p - (( 0_. F) *' q)) by A0, A1, HURWITZ:def 5

      .= (p - ( 0_. F)) by POLYNOM3: 34

      .= (p + ( 0_. F)) by H, POLYNOM3:def 10

      .= p by POLYNOM3: 28;

    end;

    

     div0: for F be Field, p,q be Polynomial of F st q divides p holds ((p div q) *' q) = p

    proof

      let F be Field, p,q be Polynomial of F;

      assume q divides p;

      then

      consider r be Polynomial of F such that

       A2: (q *' r) = p by T2;

      per cases ;

        suppose

         A3: q = ( 0_. F);

        

        thus ((p div q) *' q) = ( 0_. F) by A3, POLYNOM3: 34

        .= p by A2, A3, POLYNOM3: 34;

      end;

        suppose

         A3: q <> ( 0_. F);

        

         A4: p = ((q *' r) + ( 0_. F)) by A2, POLYNOM3: 28;

        ( deg ( 0_. F)) = ( - 1) by HURWITZ: 20;

        then ( deg ( 0_. F)) < ( deg q) by T8b, A3;

        hence ((p div q) *' q) = p by A2, A4, HURWITZ:def 5;

      end;

    end;

    theorem :: RING_4:3

    

     div2: for F be Field, p,q be Polynomial of F holds (p mod q) = ( 0_. F) iff q divides p

    proof

      let F be Field, p,q be Polynomial of F;

       A:

      now

        assume (p mod q) = ( 0_. F);

        

        then ((p div q) *' q) = ((p - ((p div q) *' q)) + ((p div q) *' q)) by POLYNOM3: 28

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

        .= (p + (((p div q) *' q) - ((p div q) *' q)))

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

        .= p by POLYNOM3: 28;

        hence q divides p by T2;

      end;

      now

        assume

         A: q divides p;

        

        thus (p mod q) = (p - p) by A, div0

        .= ( 0_. F) by POLYNOM3: 29;

      end;

      hence thesis by A;

    end;

    theorem :: RING_4:4

    

     div5: for F be Field, p,q be Polynomial of F holds p = (((p div q) *' q) + (p mod q))

    proof

      let F be Field, p,q be Polynomial of F;

      

      thus p = (p + ( 0_. F)) by POLYNOM3: 28

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

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

      .= (((p div q) *' q) + (p mod q));

    end;

    theorem :: RING_4:5

    

     div4: for F be Field, p,r be Polynomial of F holds for q be non zero Polynomial of F holds ((p + r) div q) = ((p div q) + (r div q)) & ((p + r) mod q) = ((p mod q) + (r mod q))

    proof

      let F be Field, p,r be Polynomial of F;

      let q be non zero Polynomial of F;

      

       H: q <> ( 0_. F);

      

       A: (p + r) = ((((p div q) *' q) + (p mod q)) + r) by div5

      .= ((((p div q) *' q) + (p mod q)) + (((r div q) *' q) + (r mod q))) by div5

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

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

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

      .= ((((p div q) + (r div q)) *' q) + ((p mod q) + (r mod q))) by POLYNOM3: 32;

      

       B: ( deg ((p mod q) + (r mod q))) <= ( max (( deg (p mod q)),( deg (r mod q)))) by HURWITZ: 22;

      

       C: ( deg (p mod q)) < ( deg q) by RING_2: 29;

      ( deg (r mod q)) < ( deg q) by RING_2: 29;

      then ( max (( deg (p mod q)),( deg (r mod q)))) < ( max (( deg q),( deg q))) by C, XXREAL_0: 27;

      then

       D: ( deg ((p mod q) + (r mod q))) < ( deg q) by B, XXREAL_0: 2;

      hence ((p + r) div q) = ((p div q) + (r div q)) by A, H, HURWITZ:def 5;

      

      thus ((p + r) mod q) = (((((p div q) + (r div q)) *' q) + ((p mod q) + (r mod q))) - (((p div q) + (r div q)) *' q)) by D, A, H, HURWITZ:def 5

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

      .= (( 0_. F) + ((p mod q) + (r mod q))) by POLYNOM3: 29

      .= ((p mod q) + (r mod q)) by POLYNOM3: 28;

    end;

    theorem :: RING_4:6

    

     div3a: for F be Field, p,r be Polynomial of F holds for q be non zero Polynomial of F holds ((p *' r) mod q) = (((p mod q) *' (r mod q)) mod q)

    proof

      let F be Field, p,r be Polynomial of F;

      let q be non zero Polynomial of F;

      

       H1: ((((p div q) *' q) *' ((r div q) *' q)) + (((p div q) *' q) *' (r mod q))) = (((((p div q) *' q) *' (r div q)) *' q) + (((p div q) *' q) *' (r mod q))) by POLYNOM3: 33

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

      .= (q *' ((((p div q) *' q) *' (r div q)) + ((p div q) *' (r mod q)))) by POLYNOM3: 31;

      

       H2: ((p mod q) *' ((r div q) *' q)) = (q *' ((p mod q) *' (r div q))) by POLYNOM3: 33;

      (p *' r) = ((((p div q) *' q) + (p mod q)) *' r) by div5

      .= ((((p div q) *' q) + (p mod q)) *' (((r div q) *' q) + (r mod q))) by div5

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

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

      .= (((((p div q) *' q) *' ((r div q) *' q)) + (((p div q) *' q) *' (r mod q))) + (((p mod q) *' ((r div q) *' q)) + ((p mod q) *' (r mod q)))) by POLYNOM3: 31;

      

      hence ((p *' r) mod q) = ((((((p div q) *' q) *' ((r div q) *' q)) + (((p div q) *' q) *' (r mod q))) mod q) + ((((p mod q) *' ((r div q) *' q)) + ((p mod q) *' (r mod q))) mod q)) by div4

      .= (( 0_. F) + ((((p mod q) *' ((r div q) *' q)) + ((p mod q) *' (r mod q))) mod q)) by div2, H1, T2

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

      .= ((((p mod q) *' ((r div q) *' q)) mod q) + (((p mod q) *' (r mod q)) mod q)) by div4

      .= (( 0_. F) + (((p mod q) *' (r mod q)) mod q)) by div2, H2, T2

      .= (((p mod q) *' (r mod q)) mod q) by POLYNOM3: 28;

    end;

    theorem :: RING_4:7

    

     div3: for F be Field, r,q,u be Polynomial of F holds for p be non zero Polynomial of F holds ((((r *' q) mod p) *' u) mod p) = (((r *' q) *' u) mod p)

    proof

      let F be Field, r,q,u be Polynomial of F;

      let p be non zero Polynomial of F;

      

       A: ((((r *' q) mod p) *' u) mod p) = ((((r *' q) *' u) + (( - (((r *' q) div p) *' p)) *' u)) mod p) by POLYNOM3: 32

      .= ((((r *' q) *' u) mod p) + ((( - (((r *' q) div p) *' p)) *' u) mod p)) by div4;

      (( - (((r *' q) div p) *' p)) *' u) = ((p *' ( - ((r *' q) div p))) *' u) by HURWITZ: 12

      .= (p *' (( - ((r *' q) div p)) *' u)) by POLYNOM3: 33;

      

      hence ((((r *' q) mod p) *' u) mod p) = ((((r *' q) *' u) mod p) + ( 0_. F)) by A, div2, T2

      .= (((r *' q) *' u) mod p) by POLYNOM3: 28;

    end;

    theorem :: RING_4:8

    for L be add-associative right_zeroed right_complementable left-distributive non empty doubleLoopStr, p be sequence of L holds (( 0. L) * p) = ( 0_. L)

    proof

      let L be add-associative right_zeroed right_complementable left-distributive non empty doubleLoopStr, p be sequence of L;

      set t = (( 0. L) * p);

      now

        let x be object;

        assume x in NAT ;

        then

        reconsider i = x as Element of NAT ;

        

        thus (t . x) = (( 0. L) * (p . i)) by POLYNOM5:def 4

        .= (( 0_. L) . x) by FUNCOP_1: 7;

      end;

      hence thesis by FUNCT_2: 12;

    end;

    theorem :: RING_4:9

    

     poly2a: for L be left_unital non empty doubleLoopStr, p be sequence of L holds (( 1. L) * p) = p

    proof

      let L be left_unital non empty doubleLoopStr, p be sequence of L;

      set t = (( 1. L) * p);

      now

        let x be object;

        assume x in NAT ;

        then

        reconsider i = x as Element of NAT ;

        

        thus (t . x) = (( 1. L) * (p . i)) by POLYNOM5:def 4

        .= (p . x);

      end;

      hence thesis by FUNCT_2: 12;

    end;

    theorem :: RING_4:10

    

     poly2: for L be add-associative right_zeroed right_complementable right_unital distributive associative commutative non empty doubleLoopStr, p,q be sequence of L, a be Element of L holds (a * (p *' q)) = (p *' (a * q))

    proof

      let R be add-associative right_zeroed right_complementable right_unital distributive associative commutative non empty doubleLoopStr, p,q be sequence of R, a be Element of R;

      set t = (a * (p *' q));

      now

        let x be object;

        assume x in NAT ;

        then

        reconsider i = x as Element of NAT ;

        consider F be FinSequence of the carrier of R such that

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

        consider G be FinSequence of the carrier of R such that

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

        

         H3: ( dom F) = ( Seg (i + 1)) by H1, FINSEQ_1:def 3

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

        now

          let x be object;

          assume

           H4: x in ( dom F);

          then

          reconsider j = x as Element of NAT ;

          

           H5: (F . j) = ((p . (j -' 1)) * (q . ((i + 1) -' j))) by H4, H1;

          (G /. j) = (G . j) by H3, H4, PARTFUN1:def 6

          .= ((p . (j -' 1)) * ((a * q) . ((i + 1) -' j))) by H2, H4, H3

          .= ((p . (j -' 1)) * (a * (q . ((i + 1) -' j)))) by POLYNOM5:def 4

          .= (((p . (j -' 1)) * (q . ((i + 1) -' j))) * a) by GROUP_1:def 3

          .= (a * (F /. j)) by PARTFUN1:def 6, H5, H4;

          hence (G /. x) = (a * (F /. x));

        end;

        then G = (a * F) by H3, POLYNOM1:def 1;

        then ( Sum G) = (a * ( Sum F)) by POLYNOM1: 12;

        hence (t . x) = ((p *' (a * q)) . x) by H1, POLYNOM5:def 4, H2;

      end;

      hence thesis by FUNCT_2: 12;

    end;

    theorem :: RING_4:11

    

     poly3: for L be associative non empty multMagma, p be sequence of L, a,b be Element of L holds ((a * b) * p) = (a * (b * p))

    proof

      let L be associative non empty multMagma, p be sequence of L, a,b be Element of L;

      now

        let x be object;

        assume x in NAT ;

        then

        reconsider i = x as Element of NAT ;

        

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

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

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

        .= ((a * (b * p)) . x) by POLYNOM5:def 4;

      end;

      hence thesis by FUNCT_2: 12;

    end;

    theorem :: RING_4:12

    

     poly1: for L be add-associative right_zeroed right_complementable left-distributive left_unital non empty doubleLoopStr holds for p be sequence of L holds (( 1_. L) *' p) = p

    proof

      let R be add-associative right_zeroed right_complementable left-distributive left_unital non empty doubleLoopStr, p be sequence of R;

      set q = ( 1_. R);

      now

        let x be object;

        assume x in NAT ;

        then

        reconsider i = x as Element of NAT ;

        consider F be FinSequence of the carrier of R such that

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

         D:

        now

          let j be Element of NAT ;

          assume

           B: j in ( dom F) & j <> 1;

          then j in ( Seg ( len F)) by FINSEQ_1:def 3;

          then 1 <= j & j <= (i + 1) by H, FINSEQ_1: 1;

          then j > 1 by B, XXREAL_0: 1;

          then (q . (j -' 1)) = ( 0. R) by POLYNOM3: 30, NAT_D: 36;

          

          hence ( 0. R) = ((q . (j -' 1)) * (p . ((i + 1) -' j)))

          .= (F . j) by B, H

          .= (F /. j) by B, PARTFUN1:def 6;

        end;

        

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

        

         E: 1 <= 1 & 1 <= (i + 1) by NAT_1: 11;

        then

         F: ( Sum F) = (F /. 1) by D, POLYNOM2: 3, G, FINSEQ_1: 1;

        (F . 1) = ((q . (1 -' 1)) * (p . ((i + 1) -' 1))) by H, E, G, FINSEQ_1: 1

        .= ((q . 0 ) * (p . ((i + 1) -' 1))) by XREAL_1: 232

        .= ((q . 0 ) * (p . i)) by NAT_D: 34

        .= (( 1. R) * (p . i)) by POLYNOM3: 30

        .= (p . i);

        hence ((q *' p) . x) = (p . x) by E, H, F, PARTFUN1:def 6, G, FINSEQ_1: 1;

      end;

      hence thesis by FUNCT_2: 12;

    end;

    registration

      let L be add-associative right_zeroed right_complementable well-unital distributive non empty doubleLoopStr;

      cluster ( Polynom-Ring L) -> well-unital;

      coherence

      proof

        set R = ( Polynom-Ring L);

        now

          let x be Element of R;

          reconsider p = x as Polynomial of L by POLYNOM3:def 10;

          set e = ( 1. R);

          

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

          

          hence (x * e) = (p *' ( 1_. L)) by POLYNOM3:def 10

          .= x by POLYNOM3: 35;

          

          thus (e * x) = (( 1_. L) *' p) by A2, POLYNOM3:def 10

          .= x by poly1;

        end;

        hence thesis by VECTSP_1:def 6;

      end;

    end

    begin

    definition

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

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

      :: RING_4:def4

      attr x is constant means

      : defconst: ( deg x) <= 0 ;

    end

    registration

      let R be non degenerated Ring;

      cluster non zero constant for Element of ( Polynom-Ring R);

      existence

      proof

        reconsider a = ( 1_. R) as Element of ( Polynom-Ring R) by POLYNOM3:def 10;

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

        take a;

        thus a is non zero by POLYNOM3:def 10;

        thus a is constant by RATFUNC1:def 2;

      end;

      cluster non zero constant for Element of the carrier of ( Polynom-Ring R);

      existence

      proof

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

        take a;

        thus a is non zero;

        ( len ( 1_. R)) = 1 by POLYNOM4: 4;

        hence a is constant;

      end;

    end

    registration

      let R be domRing;

      cluster non constant for Element of ( Polynom-Ring R);

      existence

      proof

        set p = (( rpoly (1,( 0. R))) *' ( rpoly (1,( 0. R))));

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

        take a;

        ( deg (( rpoly (1,( 0. R))) *' ( rpoly (1,( 0. R))))) = (( deg ( rpoly (1,( 0. R)))) + ( deg ( rpoly (1,( 0. R))))) by HURWITZ: 23

        .= (1 + ( deg ( rpoly (1,( 0. R))))) by HURWITZ: 27

        .= (1 + 1) by HURWITZ: 27;

        hence a is non constant;

      end;

      cluster non constant for Element of the carrier of ( Polynom-Ring R);

      existence

      proof

        set p = (( rpoly (1,( 0. R))) *' ( rpoly (1,( 0. R))));

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

        take a;

        ( deg (( rpoly (1,( 0. R))) *' ( rpoly (1,( 0. R))))) = (( deg ( rpoly (1,( 0. R)))) + ( deg ( rpoly (1,( 0. R))))) by HURWITZ: 23

        .= (1 + ( deg ( rpoly (1,( 0. R))))) by HURWITZ: 27

        .= (1 + 1) by HURWITZ: 27;

        hence a is non constant;

      end;

    end

    definition

      let L be non empty ZeroStr;

      let a be Element of L;

      :: RING_4:def5

      func a | L -> sequence of L equals (( 0_. L) +* ( 0 ,a));

      coherence ;

    end

    registration

      let L be non empty ZeroStr;

      let a be Element of L;

      cluster (a | L) -> finite-Support;

      coherence

      proof

        take 1;

        let i be Nat;

        assume i >= 1;

        

        hence ((a | L) . i) = (( 0_. L) . i) by FUNCT_7: 32

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

      end;

    end

    

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

    proof

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

       0 in NAT ;

      then 0 in ( dom ( 0_. L)) by FUNCT_2:def 1;

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

      let n be Nat;

      assume n <> 0 ;

      

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

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

    end;

    

     T6: for L be non empty ZeroStr holds (( 0. L) | L) = ( 0_. L)

    proof

      let L be non empty ZeroStr;

      set p = (( 0. L) | L);

       A2:

      now

        let x be object;

        assume x in ( dom p);

        then

        reconsider i = x as Element of NAT ;

        per cases ;

          suppose i = 0 ;

          hence (p . x) = ( 0. L) by Th28;

        end;

          suppose i <> 0 ;

          hence (p . x) = ( 0. L) by Th28;

        end;

      end;

      ( dom p) = NAT by NORMSP_1: 12;

      hence thesis by A2, FUNCOP_1: 11;

    end;

    registration

      let L be non empty ZeroStr;

      let a be Element of L;

      cluster (a | L) -> constant;

      coherence

      proof

        per cases ;

          suppose a = ( 0. L);

          then (a | L) = ( 0_. L) by T6;

          then ( len (a | L)) = 0 by POLYNOM4: 3;

          then ( deg (a | L)) = ( - 1);

          hence thesis by RATFUNC1:def 2;

        end;

          suppose

           A0: a <> ( 0. L);

           A1:

          now

            let i be Nat;

            assume that

             A2: i is_at_least_length_of (a | L) and

             A3: ( 0 + 1) > i;

             0 >= i by A3, NAT_1: 13;

            then ((a | L) . 0 ) = ( 0. L) by A2, ALGSEQ_1:def 2;

            hence contradiction by A0, Th28;

          end;

          for i be Nat st i >= 1 holds ((a | L) . i) = ( 0. L) by Th28;

          then ( len (a | L)) = 1 by A1, ALGSEQ_1:def 3, ALGSEQ_1:def 2;

          then ( deg (a | L)) = 0 ;

          hence thesis by RATFUNC1:def 2;

        end;

      end;

    end

    registration

      let L be non trivial ZeroStr;

      let a be non zero Element of L;

      cluster (a | L) -> non zero;

      coherence

      proof

        ((a | L) . 0 ) = a by Th28;

        then (a | L) <> ( 0_. L) by FUNCOP_1: 7;

        hence thesis by UPROOTS:def 5;

      end;

    end

    registration

      let L be non trivial ZeroStr;

      cluster non zero constant for Polynomial of L;

      existence

      proof

        take ( the non zero Element of L | L);

        thus thesis;

      end;

    end

    theorem :: RING_4:13

    for L be non empty ZeroStr holds (( 0. L) | L) = ( 0_. L) by T6;

    theorem :: RING_4:14

    for L be non empty multLoopStr_0 holds (( 1. L) | L) = ( 1_. L);

    registration

      let L be non empty ZeroStr;

      cluster (( 0. L) | L) -> zero;

      coherence by T6;

    end

    registration

      let L be non degenerated multLoopStr_0;

      cluster (( 1. L) | L) -> non zero;

      coherence ;

    end

    theorem :: RING_4:15

    

     LX: for L be add-associative right_zeroed right_complementable distributive non empty doubleLoopStr, p be Element of the carrier of ( Polynom-Ring L) holds p is non zero constant iff ( deg p) = 0

    proof

      let L be add-associative right_zeroed right_complementable distributive non empty doubleLoopStr, p be Element of the carrier of ( Polynom-Ring L);

       A:

      now

        assume

         AS: p is non zero constant;

        now

          assume ( deg p) <> 0 ;

          then ((( len p) - 1) + 1) < ( 0 + 1) by AS, XREAL_1: 6;

          then ( len p) = 0 by NAT_1: 14;

          then ( deg p) = ( - 1);

          then p = ( 0_. L) by HURWITZ: 20;

          hence contradiction by AS;

        end;

        hence ( deg p) = 0 ;

      end;

      now

        assume

         AS: ( deg p) = 0 ;

        then p <> ( 0_. L) by HURWITZ: 20;

        hence p is non zero by UPROOTS:def 5;

        thus p is constant by AS;

      end;

      hence thesis by A;

    end;

    theorem :: RING_4:16

    

     LX1: for L be add-associative right_zeroed right_complementable right-distributive right_unital non empty doubleLoopStr, a be Element of L holds (a | L) = (a * ( 1_. L))

    proof

      let L be add-associative right_zeroed right_complementable right-distributive right_unital non empty doubleLoopStr, a be Element of L;

      now

        let x be object;

        assume x in NAT ;

        then

        reconsider i = x as Element of NAT ;

        per cases ;

          suppose

           A: i = 0 ;

          

          thus ((a * ( 1_. L)) . x) = (a * (( 1_. L) . i)) by POLYNOM5:def 4

          .= (a * ( 1. L)) by A, POLYNOM3: 30

          .= a

          .= ((a | L) . x) by Th28, A;

        end;

          suppose

           A: i > 0 ;

          

          thus ((a * ( 1_. L)) . x) = (a * (( 1_. L) . i)) by POLYNOM5:def 4

          .= (a * ( 0. L)) by A, POLYNOM3: 30

          .= ((a | L) . x) by Th28, A;

        end;

      end;

      hence thesis by FUNCT_2: 12;

    end;

    theorem :: RING_4:17

    

     T4a: for R be Ring holds for a,b be Element of R holds ((a | R) + (b | R)) = ((a + b) | R)

    proof

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

      set p = ((a | R) + (b | R)), q = ((a + b) | R);

      

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

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

      now

        let x be object;

        assume x in ( dom q);

        then

        reconsider i = x as Element of NAT ;

        

         B: (p . i) = (((a | R) . i) + ((b | R) . i)) by NORMSP_1:def 2;

        per cases ;

          suppose

           S: i = 0 ;

          

          hence (q . x) = (a + b) by Th28

          .= (((a | R) . i) + b) by S, Th28

          .= (p . x) by B, S, Th28;

        end;

          suppose

           S: i <> 0 ;

          

          hence (q . x) = ( 0. R) by Th28

          .= (((a | R) . i) + ( 0. R)) by S, Th28

          .= (p . x) by B, S, Th28;

        end;

      end;

      hence thesis by A, FUNCT_1: 2;

    end;

    theorem :: RING_4:18

    

     T4: for R be Ring holds for a,b be Element of R holds ((a | R) *' (b | R)) = ((a * b) | R)

    proof

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

      set p = (a | R), q = (b | R);

      now

        let x be object;

        assume x in NAT ;

        then

        reconsider i = x as Element of NAT ;

        consider F be FinSequence of the carrier of R such that

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

        per cases ;

          suppose

           A: i = 0 ;

          then 1 in ( Seg ( len F)) by H, FINSEQ_1: 1;

          then 1 in ( dom F) by FINSEQ_1:def 3;

          

          then (F . 1) = ((p . (( 0 + 1) -' 1)) * (q . ((i + 1) -' 1))) by H

          .= ((p . 0 ) * (q . ((i + 1) -' 1))) by NAT_D: 34

          .= ((p . 0 ) * (q . 0 )) by NAT_D: 34, A

          .= (a * (q . 0 )) by Th28

          .= (a * b) by Th28;

          then F = <*(a * b)*> by FINSEQ_1: 40, A, H;

          

          hence ((p *' q) . x) = (a * b) by H, RLVECT_1: 44

          .= (((a * b) | R) . x) by A, Th28;

        end;

          suppose

           A: i > 0 ;

          now

            let j be Element of NAT ;

            assume

             B: j in ( dom F);

            then j in ( Seg ( len F)) by FINSEQ_1:def 3;

            then

             C: 1 <= j & j <= (i + 1) by H, FINSEQ_1: 1;

            (p . (j -' 1)) = ( 0. R) or (q . ((i + 1) -' j)) = ( 0. R)

            proof

              assume (p . (j -' 1)) <> ( 0. R);

              then j <= 1 by NAT_D: 36, Th28;

              then j = 1 by C, XXREAL_0: 1;

              then ((i + 1) -' j) = i by NAT_D: 34;

              hence (q . ((i + 1) -' j)) = ( 0. R) by A, Th28;

            end;

            

            hence ( 0. R) = ((p . (j -' 1)) * (q . ((i + 1) -' j)))

            .= (F . j) by B, H;

          end;

          

          hence ((p *' q) . x) = ( 0. R) by H, POLYNOM3: 1

          .= (((a * b) | R) . x) by A, Th28;

        end;

      end;

      hence thesis by FUNCT_2: 12;

    end;

    theorem :: RING_4:19

    

     T9: for R be Ring holds for a,b be Element of R holds (a | R) = (b | R) iff a = b

    proof

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

      now

        assume (a | R) = (b | R);

        

        hence a = ((b | R) . 0 ) by Th28

        .= b by Th28;

      end;

      hence thesis;

    end;

    theorem :: RING_4:20

    

     T11: for R be Ring holds for p be Element of the carrier of ( Polynom-Ring R) holds p is constant iff ex a be Element of R st p = (a | R)

    proof

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

      reconsider g = p as Polynomial of L;

      now

        assume p is constant;

        then

         AS: ((( len p) - 1) + 1) <= ( 0 + 1) by XREAL_1: 6;

        per cases by AS, NAT_1: 25;

          suppose ( len p) = 0 ;

          

          then p = ( 0_. L) by POLYNOM4: 5

          .= (( 0. L) | L) by T6;

          hence ex a be Element of L st p = (a | L);

        end;

          suppose

           AS: ( len p) = 1;

          set q = ((p . 0 ) | L);

          now

            let x be object;

            assume x in NAT ;

            then

            reconsider i = x as Element of NAT ;

            per cases ;

              suppose i = 0 ;

              hence (q . x) = (p . x) by Th28;

            end;

              suppose

               B: i <> 0 ;

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

              then i >= ( len p) by AS, NAT_1: 13;

              

              hence (p . x) = ( 0. L) by ALGSEQ_1: 8

              .= (q . x) by B, Th28;

            end;

          end;

          hence ex a be Element of L st p = (a | L) by FUNCT_2: 12;

        end;

      end;

      hence thesis by RATFUNC1:def 2;

    end;

    theorem :: RING_4:21

    

     T11a: for R be Ring, a be Element of R holds ( deg (a | R)) = 0 iff a <> ( 0. R)

    proof

      let L be Ring, a be Element of L;

      now

        assume

         Y: a <> ( 0. L);

        now

          assume ( deg (a | L)) < 0 ;

          

          then (a | L) = ( 0_. L) by T8b

          .= (( 0. L) | L) by T6;

          hence contradiction by Y, T9;

        end;

        hence ( deg (a | L)) = 0 by RATFUNC1:def 2;

      end;

      hence thesis by T8b, T6;

    end;

    begin

    notation

      let L be non empty doubleLoopStr;

      let p be Polynomial of L;

      synonym p is monic for p is normalized;

    end

    registration

      let L be non degenerated doubleLoopStr;

      cluster ( 1_. L) -> monic;

      coherence

      proof

        (( len ( 1_. L)) -' 1) = (1 -' 1) by POLYNOM4: 4

        .= 0 by XREAL_1: 232;

        then ( LC ( 1_. L)) = ( 1. L) by POLYNOM3: 30;

        hence ( 1_. L) is monic by RATFUNC1:def 7;

      end;

      cluster ( 0_. L) -> non monic;

      coherence

      proof

        

         C: ( 1. L) <> ( 0. L);

        ( LC ( 0_. L)) = ( 0. L) by FUNCOP_1: 7;

        hence ( 0_. L) is non monic by C, RATFUNC1:def 7;

      end;

    end

    registration

      let L be non degenerated doubleLoopStr;

      cluster monic for Polynomial of L;

      existence

      proof

        ( 1_. L) is monic;

        hence thesis;

      end;

      cluster non monic for Polynomial of L;

      existence

      proof

        ( 0_. L) is non monic;

        hence thesis;

      end;

    end

    registration

      let L be add-associative right_zeroed right_complementable distributive non degenerated doubleLoopStr;

      cluster monic for Element of the carrier of ( Polynom-Ring L);

      existence

      proof

        ( 1_. L) is Element of the carrier of ( Polynom-Ring L) by POLYNOM3:def 10;

        hence thesis;

      end;

      cluster non monic for Element of the carrier of ( Polynom-Ring L);

      existence

      proof

        ( 0_. L) is Element of the carrier of ( Polynom-Ring L) by POLYNOM3:def 10;

        hence thesis;

      end;

    end

    registration

      let L be well-unital non degenerated doubleLoopStr;

      let x be Element of L;

      cluster ( rpoly (1,x)) -> monic;

      coherence

      proof

        set p = ( rpoly (1,x));

        1 = ( deg p) by HURWITZ: 27

        .= (( len p) - 1);

        then (1 + 1) = ( len p);

        then (( len p) -' 1) = 1 by NAT_D: 34;

        then ( LC p) = ( 1. L) by HURWITZ: 25;

        hence p is monic by RATFUNC1:def 7;

      end;

    end

    definition

      let L be Field;

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

      :: original: NormPolynomial

      redefine

      func NormPolynomial p -> Element of the carrier of ( Polynom-Ring L) ;

      coherence by POLYNOM3:def 10;

    end

    registration

      let F be Field;

      let p be non zero Polynomial of F;

      cluster ( NormPolynomial p) -> monic;

      coherence ;

    end

    registration

      let L be Field;

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

      cluster ( NormPolynomial p) -> monic;

      coherence ;

    end

    theorem :: RING_4:22

    

     npl0: for F be Field holds ( NormPolynomial ( 0_. F)) = ( 0_. F)

    proof

      let F be Field;

      set q = ( 0_. F);

      set p = ( NormPolynomial q);

      now

        let x be object;

        assume x in NAT ;

        then

        reconsider i = x as Element of NAT ;

        (p . i) = ((q . i) / (q . (( len q) -' 1))) by POLYNOM5:def 11

        .= (( 0. F) * ((q . (( len q) -' 1)) " )) by FUNCOP_1: 7

        .= (q . i) by FUNCOP_1: 7;

        hence (p . x) = (q . x);

      end;

      hence thesis by FUNCT_2: 12;

    end;

    theorem :: RING_4:23

    

     npl: for F be Field, p be non zero Element of the carrier of ( Polynom-Ring F) holds ( NormPolynomial p) = ((( LC p) " ) * p)

    proof

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

      now

        let x be object;

        assume x in NAT ;

        then

        reconsider i = x as Element of NAT ;

        

        thus (((( LC p) " ) * p) . x) = ((( LC p) " ) * (p . i)) by POLYNOM5:def 4

        .= ((p . i) / (p . (( len p) -' 1)))

        .= (( NormPolynomial p) . x) by POLYNOM5:def 11;

      end;

      hence thesis by FUNCT_2: 12;

    end;

    theorem :: RING_4:24

    for F be Field, p be non zero Element of the carrier of ( Polynom-Ring F) holds p is monic iff ( NormPolynomial p) = p

    proof

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

      hereby

        assume p is monic;

        then ( LC p) = ( 1. F) by RATFUNC1:def 7;

        

        hence ( NormPolynomial p) = ((( 1. F) " ) * p) by npl

        .= p by poly2a;

      end;

      thus thesis;

    end;

    theorem :: RING_4:25

    

     np1: for F be Field, p,q be Element of the carrier of ( Polynom-Ring F) holds q divides p iff ( NormPolynomial q) divides p

    proof

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

      per cases ;

        suppose q = ( 0_. F);

        hence thesis by npl0;

      end;

        suppose

         AS: q <> ( 0_. F);

        then

         AS1: q is non zero by UPROOTS:def 5;

         A:

        now

          assume q divides p;

          then

          consider r be Polynomial of F such that

           A1: p = (q *' r) by T2;

          set a = (( LC q) " );

          reconsider qq = ( NormPolynomial q) as Polynomial of F;

          q is non zero by AS, UPROOTS:def 5;

          then ( LC q) <> ( 0. F);

          then ((( LC q) " ) * ( LC q)) = ( 1. F) by VECTSP_1:def 10;

          then a <> ( 0. F);

          then ((a " ) * a) = ( 1. F) by VECTSP_1:def 10;

          

          then p = ((a * (a " )) * p) by poly2a

          .= (a * ((a " ) * (q *' r))) by A1, poly3

          .= (a * (q *' ((a " ) * r))) by poly2

          .= ((a * q) *' ((a " ) * r)) by poly2

          .= (qq *' ((a " ) * r)) by AS1, npl;

          hence ( NormPolynomial q) divides p by T2;

        end;

        now

          assume

           A0: ( NormPolynomial q) divides p;

          reconsider qq = ( NormPolynomial q) as Polynomial of F;

          consider r be Polynomial of F such that

           A1: p = (qq *' r) by A0, T2;

          p = (((( LC q) " ) * q) *' r) by AS1, A1, npl

          .= ((( LC q) " ) * (q *' r)) by poly2

          .= (q *' ((( LC q) " ) * r)) by poly2;

          hence q divides p by T2;

        end;

        hence thesis by A;

      end;

    end;

    theorem :: RING_4:26

    

     np2: for F be Field, p,q be Element of the carrier of ( Polynom-Ring F) holds q divides p iff q divides ( NormPolynomial p)

    proof

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

      per cases ;

        suppose p = ( 0_. F);

        hence thesis by npl0;

      end;

        suppose

         AS: p <> ( 0_. F);

        then

         AS1: p is non zero by UPROOTS:def 5;

         A:

        now

          assume q divides p;

          then

          consider r be Polynomial of F such that

           A1: p = (q *' r) by T2;

          set a = (( LC p) " );

          ( NormPolynomial p) = (a * (q *' r)) by AS1, A1, npl

          .= (q *' (a * r)) by poly2;

          hence q divides ( NormPolynomial p) by T2;

        end;

        now

          assume q divides ( NormPolynomial p);

          then

          consider r be Polynomial of F such that

           A1: ( NormPolynomial p) = (q *' r) by T2;

          set a = (( LC p) " );

          p is non zero by AS, UPROOTS:def 5;

          then ( LC p) <> ( 0. F);

          then ((( LC p) " ) * ( LC p)) = ( 1. F) by VECTSP_1:def 10;

          then a <> ( 0. F);

          then ((a " ) * a) = ( 1. F) by VECTSP_1:def 10;

          

          then p = (((a " ) * a) * p) by poly2a

          .= ((a " ) * (a * p)) by poly3

          .= ((a " ) * (q *' r)) by AS1, A1, npl

          .= (q *' ((a " ) * r)) by poly2;

          hence q divides p by T2;

        end;

        hence thesis by A;

      end;

    end;

    theorem :: RING_4:27

    

     np3: for F be Field, p be Element of the carrier of ( Polynom-Ring F) holds ( NormPolynomial p) is_associated_to p

    proof

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

      reconsider a = p, b = ( NormPolynomial p) as Element of ( Polynom-Ring F);

      

       A: (p *' ( 1_. F)) = p by POLYNOM3: 35;

      then

       B: p divides ( NormPolynomial p) by T2, np2;

      ( NormPolynomial p) divides p by A, np1, T2;

      hence thesis by B;

    end;

    theorem :: RING_4:28

    

     thirr2: for F be Field, p be Element of the carrier of ( Polynom-Ring F) holds ( NormPolynomial p) is irreducible iff p is irreducible

    proof

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

      now

        assume

         B: ( NormPolynomial p) is irreducible;

        ( NormPolynomial p) is_associated_to p by np3;

        hence p is irreducible by B, RING_2: 23;

      end;

      hence thesis by np3, RING_2: 23;

    end;

    theorem :: RING_4:29

    

     np00: for R be domRing, p,q be Element of the carrier of ( Polynom-Ring R) holds p is_associated_to q implies ( deg p) = ( deg q)

    proof

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

      assume

       A: p is_associated_to q;

      then

      consider c be Element of ( Polynom-Ring R) such that

       K2: q = (p * c) by GCD_1:def 1;

      reconsider r = c as Element of the carrier of ( Polynom-Ring R);

      consider d be Element of ( Polynom-Ring R) such that

       K3: p = (q * d) by A, GCD_1:def 1;

      reconsider s = d as Element of the carrier of ( Polynom-Ring R);

      

       K4: q = (p *' r) by K2, POLYNOM3:def 10;

      

       K5: p = (q *' s) by K3, POLYNOM3:def 10;

      per cases ;

        suppose p = ( 0_. R);

        hence thesis by K4, POLYNOM3: 34;

      end;

        suppose q = ( 0_. R);

        hence thesis by K5, POLYNOM3: 34;

      end;

        suppose

         A: p <> ( 0_. R) & q <> ( 0_. R);

        then

         A1: r <> ( 0_. R) & s <> ( 0_. R) by K4, K5, POLYNOM3: 34;

        then

         A2: ( deg r) is Element of NAT & ( deg s) is Element of NAT by T8b;

        

         A3: ( deg q) = (( deg p) + ( deg r)) & ( deg p) = (( deg q) + ( deg s)) by A, A1, K4, K5, HURWITZ: 23;

        then (( deg r) + ( deg s)) = 0 ;

        then ( deg r) = 0 & ( deg s) = 0 by A2;

        hence thesis by A3;

      end;

    end;

    theorem :: RING_4:30

    

     np0: for R be domRing, p,q be monic Element of the carrier of ( Polynom-Ring R) holds p is_associated_to q iff p = q

    proof

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

      

       K1: ( LC p) = ( 1. R) & ( LC q) = ( 1. R) by RATFUNC1:def 7;

      now

        assume

         AS: p is_associated_to q;

        then

        consider c be Element of ( Polynom-Ring R) such that

         K2: q = (p * c) by GCD_1:def 1;

        reconsider r = c as Element of the carrier of ( Polynom-Ring R);

        

         K3: q = (p *' r) by K2, POLYNOM3:def 10;

        r <> ( 0_. R) by K3, POLYNOM3: 34;

        

        then ( deg q) = (( deg p) + ( deg r)) by K3, HURWITZ: 23

        .= (( deg q) + ( deg r)) by AS, np00;

        then r is constant;

        then

        consider a be Element of R such that

         K5: r = (a | R) by T11;

        

         X: ( deg p) = ( deg q) by AS, np00;

        r = (a * ( 1_. R)) by K5, LX1;

        

        then q = (a * (p *' ( 1_. R))) by K3, poly2

        .= (a * p) by poly1;

        

        then (q . (( len q) -' 1)) = (a * ( 1. R)) by X, K1, POLYNOM5:def 4

        .= a;

        then r = ( 1_. R) by K5, K1;

        hence p = q by K3, poly1;

      end;

      hence thesis;

    end;

    begin

    definition

      let R be Ring;

      :: RING_4:def6

      func canHom R -> Function of R, ( Polynom-Ring R) means

      : defcanhom: for x be Element of R holds (it . x) = (x | R);

      existence

      proof

        set B = ( Polynom-Ring R);

        defpred P[ object, object] means ex a be Element of R st $1 = a & $2 = (a | R);

        

         X: for x be object st x in the carrier of R holds ex y be object st y in the carrier of B & P[x, y]

        proof

          let x be object;

          assume x in the carrier of R;

          then

          reconsider a = x as Element of R;

          reconsider y = (a | R) as Element of B by POLYNOM3:def 10;

          take y;

          thus thesis;

        end;

        consider g be Function of the carrier of R, the carrier of B such that

         Z: for x be object st x in the carrier of R holds P[x, (g . x)] from FUNCT_2:sch 1( X);

        now

          let x be Element of R;

          consider a be Element of R such that

           H: x = a & (g . x) = (a | R) by Z;

          thus (g . x) = (x | R) by H;

        end;

        then

        consider f be Function of R, B such that

         Y: for x be Element of R holds (f . x) = (x | R);

        take f;

        thus thesis by Y;

      end;

      uniqueness

      proof

        set B = ( Polynom-Ring R);

        let g1,g2 be Function of R, B such that

         A1: for a be Element of R holds (g1 . a) = (a | R) and

         A2: for a be Element of R holds (g2 . a) = (a | R);

        

         A: ( dom g1) = the carrier of R by FUNCT_2:def 1

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

        now

          let x be object;

          assume x in ( dom g1);

          then

          reconsider a = x as Element of R;

          

          thus (g1 . x) = (a | R) by A1

          .= (g2 . x) by A2;

        end;

        hence thesis by A, FUNCT_1: 2;

      end;

    end

    registration

      let R be Ring;

      cluster ( canHom R) -> additive multiplicative unity-preserving;

      coherence

      proof

        set f = ( canHom R);

        hereby

          let x,y be Element of R;

          (f . x) = (x | R) & (f . y) = (y | R) by defcanhom;

          

          hence ((f . x) + (f . y)) = ((x | R) + (y | R)) by POLYNOM3:def 10

          .= ((x + y) | R) by T4a

          .= (f . (x + y)) by defcanhom;

        end;

        hereby

          let x,y be Element of R;

          (f . x) = (x | R) & (f . y) = (y | R) by defcanhom;

          

          hence ((f . x) * (f . y)) = ((x | R) *' (y | R)) by POLYNOM3:def 10

          .= ((x * y) | R) by T4

          .= (f . (x * y)) by defcanhom;

        end;

        

        thus (f . ( 1_ R)) = (( 1. R) | R) by defcanhom

        .= ( 1_. R)

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

      end;

    end

    registration

      let R be Ring;

      cluster ( canHom R) -> monomorphism;

      coherence

      proof

        set f = ( canHom R);

        

         A: f is linear by RINGCAT1:def 1;

        now

          let x1,x2 be object;

          assume

           AS: x1 in the carrier of R & x2 in the carrier of R & (f . x1) = (f . x2);

          then

          reconsider a = x1, b = x2 as Element of R;

          (a | R) = (f . x2) by AS, defcanhom

          .= (b | R) by defcanhom;

          hence x1 = x2 by T9;

        end;

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

        hence thesis by A;

      end;

    end

    registration

      let R be Ring;

      cluster ( Polynom-Ring R) -> R -homomorphicR -monomorphic;

      coherence

      proof

        

         A: ( canHom R) is additive multiplicative unity-preserving monomorphism;

        hence ( Polynom-Ring R) is R -homomorphic by RING_2:def 4;

        thus thesis by A, RING_3:def 3;

      end;

    end

    theorem :: RING_4:31

    for R be Ring holds ( Char ( Polynom-Ring R)) = ( Char R) by RING_3: 88;

    registration

      let R be non degenerated Ring;

      cluster ( Polynom-Ring R) -> infinite;

      coherence

      proof

        set PR = ( Polynom-Ring R);

        defpred P[ Element of NAT , object] means $2 = ( rpoly ($1,( 0. R)));

        

         A0: for x be Element of NAT holds ex y be Element of the carrier of PR st P[x, y]

        proof

          let x be Element of NAT ;

          take ( rpoly (x,( 0. R)));

          thus thesis by POLYNOM3:def 10;

        end;

        consider f be Function of NAT , the carrier of PR such that

         A1: for x be Element of NAT holds P[x, (f . x)] from FUNCT_2:sch 3( A0);

        

         A2: ( dom f) = NAT by FUNCT_2:def 1;

        now

          let x1,x2 be object;

          assume

           A3: x1 in NAT & x2 in NAT & (f . x1) = (f . x2);

          then

          reconsider n = x1, m = x2 as Element of NAT ;

          ( rpoly (n,( 0. R))) = (f . m) by A1, A3

          .= ( rpoly (m,( 0. R))) by A1;

          

          then n = ( deg ( rpoly (m,( 0. R)))) by HURWITZ: 27

          .= m by HURWITZ: 27;

          hence x1 = x2;

        end;

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

        then ( rng f) is infinite by A2, CARD_1: 59;

        hence thesis;

      end;

    end

    registration

      cluster -> infinite for 0 -characteristic Ring;

      coherence

      proof

        let R be 0 -characteristic Ring;

        set f = ( canHom_Int R);

        ( dom f) = the carrier of INT.Ring by FUNCT_2:def 1;

        then ( rng f) is infinite by CARD_1: 59;

        hence thesis;

      end;

    end

    theorem :: RING_4:32

    for R be Ring st ( Char R) = 0 holds R is infinite

    proof

      let R be Ring;

      assume ( Char R) = 0 ;

      then R is 0 -characteristic by RING_3:def 6;

      hence thesis;

    end;

    registration

      let n be non trivial Nat;

      cluster ( Polynom-Ring ( Z/ n)) -> infinite;

      coherence ;

    end

    theorem :: RING_4:33

    for n be non trivial Nat holds ( Char ( Polynom-Ring ( Z/ n))) <> 0 ;

    registration

      let n be non trivial Nat;

      cluster n -characteristic infinite for Ring;

      existence

      proof

        take ( Polynom-Ring ( Z/ n));

        thus thesis;

      end;

    end

    begin

    

     lemr: for R be domRing holds ( Polynom-Ring R) is non almost_left_invertible

    proof

      let R be domRing;

      set PR = ( Polynom-Ring R);

      reconsider p = ( rpoly (2,( 0. R))) as Element of the carrier of PR by POLYNOM3:def 10;

      

       A3: p <> ( 0. PR) by POLYNOM3:def 10;

      now

        assume ex q be Element of PR st (q * p) = ( 1. PR);

        then

        consider q be Element of PR such that

         A1: (q * p) = ( 1. PR);

        

         A9: q <> ( 0. PR) by A1;

        reconsider q as Element of the carrier of PR;

        

         A4: q <> ( 0_. R) by A9, POLYNOM3:def 10;

        then

         A5: ( deg q) is Element of NAT by T8b;

        (q *' p) = ( 1. PR) by A1, POLYNOM3:def 10

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

        then

         A2: (( deg q) + ( deg p)) = ( deg ( 1_. R)) by A4, HURWITZ: 23;

        

         A8: ( len ( 1_. R)) = 1 by POLYNOM4: 4;

        ( deg p) = 2 by HURWITZ: 27;

        hence contradiction by A5, A8, A2;

      end;

      then not p is left_invertible;

      hence PR is non almost_left_invertible by A3;

    end;

    registration

      cluster non almost_left_invertible for domRing;

      existence

      proof

        take ( Polynom-Ring the Field);

        thus thesis by lemr;

      end;

    end

    

     lemf: for R be domRing holds R is Field iff for a be NonUnit of R holds a = ( 0. R)

    proof

      let R be domRing;

       A:

      now

        assume R is Field;

        then

         B: R is almost_left_invertible;

        let a be NonUnit of R;

        now

          assume a <> ( 0. R);

          then

          consider b be Element of R such that

           C: (b * a) = ( 1. R) by B, ALGSTR_0:def 27;

          a divides ( 1. R) by C;

          hence contradiction by GCD_1:def 2;

        end;

        hence a = ( 0. R);

      end;

      now

        assume

         B: for a be NonUnit of R holds a = ( 0. R);

        now

          let a be Element of R;

          assume a <> ( 0. R);

          then a is Unit of R by B;

          then a divides ( 1. R) by GCD_1:def 2;

          then

          consider b be Element of R such that

           C: (a * b) = ( 1. R);

          thus a is left_invertible by C;

        end;

        then R is almost_left_invertible;

        hence R is Field;

      end;

      hence thesis by A;

    end;

    registration

      let R be non almost_left_invertible domRing;

      cluster non zero for NonUnit of R;

      existence

      proof

        consider a be NonUnit of R such that

         H: a <> ( 0. R) by lemf;

        a is non zero by H;

        hence thesis;

      end;

    end

    registration

      cluster INT.Ring -> non almost_left_invertible;

      coherence

      proof

        set R = INT.Ring ;

        set a = (( 1. R) + ( 1. R));

        now

          assume ex y be Element of R st (y * a) = ( 1. R);

          then

          consider y be Element of R such that

           A1: (y * a) = ( 1. R);

          reconsider i = y as Integer;

          consider k be Nat such that

           A2: k = (1 * (2 " )) or ( - k) = (1 * (2 " )) by A1, INT_1:def 1;

          thus contradiction by A2, NAT_1: 14;

        end;

        then not a is left_invertible;

        hence R is non almost_left_invertible;

      end;

    end

    registration

      let R be domRing;

      cluster ( Polynom-Ring R) -> non almost_left_invertible;

      coherence by lemr;

    end

    theorem :: RING_4:34

    for R be domRing holds R is Field iff for a be NonUnit of R holds a = ( 0. R) by lemf;

    theorem :: RING_4:35

    

     Th90: for R be domRing, a be Element of R holds (a | R) is Unit of ( Polynom-Ring R) iff a is Unit of R

    proof

      let L be domRing, a be Element of L;

      set R = ( Polynom-Ring L);

      

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

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

       A:

      now

        assume

         AS: p is Unit of R;

        then (a | L) divides ( 1_. L) by H1, GCD_1:def 2;

        then

        consider q be Polynomial of L such that

         H3: ((a | L) *' q) = ( 1_. L) by T2;

        reconsider qq = q as Element of R by POLYNOM3:def 10;

        p <> ( 0. R) by AS;

        then

         H4: (a | L) <> ( 0_. L) by POLYNOM3:def 10;

        q <> ( 0_. L) by H3, POLYNOM3: 34;

        

        then

         H6: (( deg (a | L)) + ( deg q)) = ( deg ( 1_. L)) by H3, H4, HURWITZ: 23

        .= (1 - 1) by POLYNOM4: 4;

        ( deg (a | L)) is Element of NAT by H4, T8b;

        then qq is constant by H6;

        then

        consider b be Element of L such that

         H5: qq = (b | L) by T11;

        ((a * b) | L) = (( 1. L) | L) by H3, H5, T4;

        then a divides ( 1. L) by T9;

        hence a is Unit of L by GCD_1:def 2;

      end;

      now

        assume a is Unit of L;

        then a divides ( 1. L) by GCD_1:def 2;

        then

        consider b be Element of L such that

         H3: (a * b) = ( 1. L);

        ((a | L) *' (b | L)) = (( 1. L) | L) by T4, H3

        .= ( 1_. L);

        then (a | L) divides ( 1_. L) by T2;

        hence p is Unit of R by H1, GCD_1:def 2;

      end;

      hence thesis by A;

    end;

    theorem :: RING_4:36

    

     T88: for F be domRing, p be Element of the carrier of ( Polynom-Ring F) holds p is Unit of ( Polynom-Ring F) implies ( deg p) = 0

    proof

      let L be domRing;

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

      set R = ( Polynom-Ring L);

      

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

      assume

       AS: p is Unit of R;

      then

       H0: p <> ( 0. R);

      then

       H1: p <> ( 0_. L) by POLYNOM3:def 10;

      reconsider degp = ( deg p) as Element of NAT by H0, T8a;

      p divides ( 1_. L) by AS, H, GCD_1:def 2;

      then

      consider t be Polynomial of L such that

       H3: (p *' t) = ( 1_. L) by T2;

      reconsider t as Element of the carrier of R by POLYNOM3:def 10;

      

       H5: t <> ( 0_. L) by POLYNOM3: 34, H3;

      then t <> ( 0. R) by POLYNOM3:def 10;

      then

      reconsider degt = ( deg t) as Element of NAT by T8a;

      (degt + degp) = ( deg ( 1_. L)) by H1, H3, H5, HURWITZ: 23

      .= (1 - 1) by POLYNOM4: 4;

      hence ( deg p) = 0 ;

    end;

    theorem :: RING_4:37

    

     T8: for F be Field, p be Element of the carrier of ( Polynom-Ring F) holds p is Unit of ( Polynom-Ring F) iff ( deg p) = 0

    proof

      let L be Field;

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

      set R = ( Polynom-Ring L);

      

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

       A:

      now

        assume

         AS: p is Unit of R;

        then

         H0: p <> ( 0. R);

        then

         H1: p <> ( 0_. L) by POLYNOM3:def 10;

        reconsider degp = ( deg p) as Element of NAT by H0, T8a;

        p divides ( 1_. L) by AS, H, GCD_1:def 2;

        then

        consider t be Polynomial of L such that

         H3: (p *' t) = ( 1_. L) by T2;

        reconsider t as Element of the carrier of R by POLYNOM3:def 10;

        

         H5: t <> ( 0_. L) by POLYNOM3: 34, H3;

        then t <> ( 0. R) by POLYNOM3:def 10;

        then

        reconsider degt = ( deg t) as Element of NAT by T8a;

        (degt + degp) = ( deg ( 1_. L)) by H1, H3, H5, HURWITZ: 23

        .= (1 - 1) by POLYNOM4: 4;

        hence ( deg p) = 0 ;

      end;

      now

        assume

         AS: ( deg p) = 0 ;

        then

         AS1: p <> ( 0_. L) by HURWITZ: 20;

        p <> ( 0. R) by AS1, POLYNOM3:def 10;

        then

        reconsider degp = ( deg p) as Nat by T8a;

        p is constant by AS;

        then

        consider a be Element of L such that

         X: p = (a | L) by T11;

        

         H3: a <> ( 0. L) by X, AS, HURWITZ: 20, UPROOTS:def 5;

        set t = ((a " ) | L);

        (t *' p) = (((a " ) * a) | L) by X, T4

        .= ( 1_. L) by H3, VECTSP_1:def 10;

        then p divides ( 1_. L) by T2;

        hence p is Unit of R by H, GCD_1:def 2;

      end;

      hence thesis by A;

    end;

    theorem :: RING_4:38

    for R be domRing, p be Element of the carrier of ( Polynom-Ring R) holds p is Unit of ( Polynom-Ring R) implies p is non zero constant

    proof

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

      p is Unit of ( Polynom-Ring F) implies ( deg p) = 0 by T88;

      hence thesis by LX;

    end;

    theorem :: RING_4:39

    for F be Field, p be Element of the carrier of ( Polynom-Ring F) holds p is Unit of ( Polynom-Ring F) iff p is non zero constant

    proof

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

      p is Unit of ( Polynom-Ring F) iff ( deg p) = 0 by T8;

      hence thesis by LX;

    end;

    registration

      let R be domRing;

      cluster non constant -> non zero non unital for Element of ( Polynom-Ring R);

      coherence

      proof

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

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

        assume

         AS: a is non constant;

        then

         A: ( deg p) > 0 ;

        now

          assume a = ( 0. ( Polynom-Ring R));

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

          then ( len p) = 0 by POLYNOM4: 3;

          hence contradiction by A;

        end;

        hence a is non zero;

        thus a is non unital by AS, T88;

      end;

    end

    registration

      let F be domRing;

      cluster non constant -> non zero non unital for Element of the carrier of ( Polynom-Ring F);

      coherence

      proof

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

        assume

         AS: a is non constant;

        now

          assume a = ( 0_. F);

          then ( len a) = 0 by POLYNOM4: 3;

          hence contradiction by AS;

        end;

        hence a is non zero by UPROOTS:def 5;

        thus a is non unital by AS;

      end;

    end

    registration

      let F be Field;

      cluster non zero constant -> unital for Element of ( Polynom-Ring F);

      coherence

      proof

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

        assume

         AS: p is non zero constant;

        then

         A: p <> ( 0_. F) by POLYNOM3:def 10;

        reconsider pp = p as Element of the carrier of ( Polynom-Ring F);

        pp is non zero by A, UPROOTS:def 5;

        then ( deg pp) = 0 by AS;

        hence p is unital by T8;

      end;

      cluster unital -> non zero constant for Element of ( Polynom-Ring F);

      coherence ;

    end

    registration

      let F be Field;

      cluster non zero constant -> unital for Element of the carrier of ( Polynom-Ring F);

      coherence

      proof

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

        assume p is non zero constant;

        then ( deg p) = 0 ;

        hence p is unital by T8;

      end;

      cluster unital -> non zero constant for Element of the carrier of ( Polynom-Ring F);

      coherence

      proof

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

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

        assume

         AS: a is unital;

        then ( deg a) = 0 by T88;

        then a <> ( 0_. F) by HURWITZ: 20;

        hence a is non zero by UPROOTS:def 5;

        thus thesis by AS;

      end;

    end

    theorem :: RING_4:40

    

     T88a: for R be domRing holds for p be Element of the carrier of ( Polynom-Ring R) holds (ex q be Element of the carrier of ( Polynom-Ring R) st q divides p & 1 <= ( deg q) & ( deg q) < ( deg p)) implies p is reducible

    proof

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

      set K = ( Polynom-Ring R);

      reconsider pp = p as Polynomial of R;

      assume ex q be Element of the carrier of ( Polynom-Ring R) st q divides p & 1 <= ( deg q) & ( deg q) < ( deg p);

      then

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

       A0: q divides p & 1 <= ( deg q) & ( deg q) < ( deg p);

      

       A1: not q is Unit of K by T88, A0;

      now

        assume q is_associated_to p;

        then

        consider r be Element of K such that

         A2: r is unital & (q * r) = p by GCD_1: 18;

        reconsider rr = r as Element of the carrier of K;

        

         A5: p = (q *' rr) by A2, POLYNOM3:def 10;

        then

         A4: r <> ( 0_. R) by HURWITZ: 20, A0, POLYNOM3: 34;

        q <> ( 0_. R) by A5, A0, POLYNOM3: 34;

        

        then ( deg p) = (( deg q) + ( deg rr)) by A4, A5, HURWITZ: 23

        .= (( deg q) + 0 ) by A2, T88;

        hence contradiction by A0;

      end;

      hence p is reducible by A0, A1, RING_2:def 9;

    end;

    theorem :: RING_4:41

    

     T88b: for F be Field holds for p be Element of the carrier of ( Polynom-Ring F) holds p is reducible iff (p = ( 0_. F) or p is Unit of ( Polynom-Ring F) or ex q be Element of the carrier of ( Polynom-Ring F) st q divides p & 1 <= ( deg q) & ( deg q) < ( deg p))

    proof

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

      set K = ( Polynom-Ring R);

      reconsider pp = p as Polynomial of R;

       A:

      now

        assume p is reducible;

        then

         AS: p = ( 0. K) or p is Unit of K or ex a be Element of K st a divides p & not (a is Unit of K) & not (a is_associated_to p) by RING_2:def 9;

        thus p = ( 0_. R) or p is Unit of ( Polynom-Ring R) or ex q be Element of the carrier of ( Polynom-Ring R) st q divides p & 1 <= ( deg q) & ( deg q) < ( deg p)

        proof

          assume

           A0: not (p = ( 0_. R)) & not (p is Unit of K);

          then

          consider a be Element of K such that

           A1: a divides p & not (a is Unit of K) & not (a is_associated_to p) by AS, POLYNOM3:def 10;

          reconsider q = a as Polynomial of R by POLYNOM3:def 10;

          q divides pp by A1;

          then

          consider r be Polynomial of R such that

           A2: pp = (q *' r) by T2;

          reconsider rr = r as Element of K by POLYNOM3:def 10;

          

           A10: p = (a * rr) by A2, POLYNOM3:def 10;

          

           A5: q <> ( 0_. R) by A0, A2, POLYNOM3: 34;

          

           A6: r <> ( 0_. R) by A0, A2, POLYNOM3: 34;

          then

           A9: ( deg p) = (( deg q) + ( deg r)) by A2, A5, HURWITZ: 23;

          

           A11: ( deg q) is Element of NAT & ( deg r) is Element of NAT by A5, A6, T8b;

          then

           A7: ( deg q) <= ( deg p) by A9, NAT_1: 11;

           A3:

          now

            assume ( deg q) = ( deg p);

            then rr is Unit of K by A9, T8;

            hence contradiction by A1, A10, GCD_1: 18;

          end;

          thus ex b be Element of the carrier of K st b divides p & 1 <= ( deg b) & ( deg b) < ( deg p)

          proof

            reconsider qq = q as Element of the carrier of K;

            take qq;

            thus qq divides p by A1;

            thus 1 <= ( deg qq) by A1, A11, T8, NAT_1: 14;

            thus ( deg qq) < ( deg p) by A3, A7, XXREAL_0: 1;

          end;

        end;

      end;

      now

        assume

         AS: p = ( 0_. R) or p is Unit of ( Polynom-Ring R) or ex q be Element of the carrier of ( Polynom-Ring R) st q divides p & 1 <= ( deg q) & ( deg q) < ( deg p);

        per cases by AS;

          suppose p = ( 0_. R);

          then p = ( 0. K) by POLYNOM3:def 10;

          hence p is reducible;

        end;

          suppose p is Unit of ( Polynom-Ring R);

          hence p is reducible;

        end;

          suppose ex q be Element of the carrier of ( Polynom-Ring R) st q divides p & 1 <= ( deg q) & ( deg q) < ( deg p);

          hence p is reducible by T88a;

        end;

      end;

      hence thesis by A;

    end;

    theorem :: RING_4:42

    

     thirr0: for R be domRing, p be monic Element of the carrier of ( Polynom-Ring R) st ( deg p) = 1 holds p is irreducible

    proof

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

      set K = ( Polynom-Ring R);

      reconsider x = p as Element of K;

      assume

       AS: ( deg p) = 1;

      

      then (( len p) -' 1) = ((1 + 1) -' 1)

      .= 1 by NAT_D: 34;

      then ( LC p) = (p . 1);

      then

       E: (p . 1) = ( 1. R) by RATFUNC1:def 7;

      p <> ( 0_. R);

      then

       A: x <> ( 0. K) by POLYNOM3:def 10;

      

       B: not x is Unit of K by AS, T88;

      now

        let a be Element of K;

        assume a divides x;

        then

        consider b be Element of K such that

         H1: (a * b) = x;

        reconsider q = a, r = b as Element of the carrier of K;

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

        then

         H2: q <> ( 0_. R) & r <> ( 0_. R) by POLYNOM3: 34;

        

        then

         H4: (( deg q) + ( deg r)) = ( deg (q *' r)) by HURWITZ: 23

        .= 1 by AS, H1, POLYNOM3:def 10;

        per cases ;

          suppose ( deg q) = 0 ;

          then q is constant;

          then

          consider u be Element of R such that

           C1: q = (u | R) by T11;

          q = (u * ( 1_. R)) by LX1, C1;

          

          then (q *' r) = (u * (( 1_. R) *' r)) by poly2

          .= (u * r) by poly1;

          

          then (u * (r . 1)) = ((q *' r) . 1) by POLYNOM5:def 4

          .= ( 1. R) by H1, POLYNOM3:def 10, E;

          then u divides ( 1. R);

          then u is Unit of R by GCD_1:def 2;

          hence a is Unit of K or a is_associated_to x by Th90, C1;

        end;

          suppose ( deg q) <> 0 ;

          then ( deg q) > 0 by H2, T8b;

          then (( deg q) + ( deg r)) > ( 0 + ( deg r)) by XREAL_1: 6;

          then r is constant by H4, NAT_1: 14;

          then

          consider u be Element of R such that

           C1: r = (u | R) by T11;

          

           C3: r = (u * ( 1_. R)) by LX1, C1;

          (q *' r) = (u * (( 1_. R) *' q)) by C3, poly2

          .= (u * q) by poly1;

          

          then (u * (q . 1)) = ((q *' r) . 1) by POLYNOM5:def 4

          .= ( 1. R) by H1, POLYNOM3:def 10, E;

          then u divides ( 1. R);

          then u is Unit of R by GCD_1:def 2;

          then r is Unit of K by Th90, C1;

          hence a is Unit of K or a is_associated_to x by H1, GCD_1: 18;

        end;

      end;

      hence thesis by A, B, RING_2:def 9;

    end;

    theorem :: RING_4:43

    ex p be non monic Element of the carrier of ( Polynom-Ring INT.Ring ) st ( deg p) = 1 & p is reducible

    proof

      set R = INT.Ring ;

      set K = ( Polynom-Ring R);

      set a = (( 1. R) + ( 1. R));

      set p = ((a | R) *' ( rpoly (1,( 0. R))));

      a <> ( 0. R);

      then

      reconsider a as non zero Element of R by STRUCT_0:def 12;

      reconsider q = (a | R) as Element of the carrier of K by POLYNOM3:def 10;

      q is constant by RATFUNC1:def 2;

      then

      reconsider q as non zero constant Element of the carrier of K;

      reconsider r = ( rpoly (1,( 0. R))) as Element of the carrier of K by POLYNOM3:def 10;

      

       A1: p = ((a * ( 1_. R)) *' ( rpoly (1,( 0. R)))) by LX1

      .= (a * (( 1_. R) *' ( rpoly (1,( 0. R))))) by poly2

      .= (a * ( rpoly (1,( 0. R)))) by poly1;

      

       A2: ( deg p) = (( deg q) + ( deg ( rpoly (1,( 0. R))))) by HURWITZ: 23

      .= ( 0 + ( deg ( rpoly (1,( 0. R))))) by LX

      .= 1 by HURWITZ: 27;

      

      then (p . (( len p) -' 1)) = ((a * ( rpoly (1,( 0. R)))) . (2 - 1)) by A1, XREAL_1: 233

      .= (a * (( rpoly (1,( 0. R))) . 1)) by POLYNOM5:def 4

      .= (a * ( 1. R)) by HURWITZ: 25

      .= a;

      then ( LC p) = a;

      then

      reconsider pp = p as non monic Element of the carrier of K by RATFUNC1:def 7, POLYNOM3:def 10;

      take pp;

      thus ( deg pp) = 1 by A2;

      

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

      

       B1: q divides pp by B0, GCD_1:def 1;

       B4:

      now

        assume q is Unit of K;

        then a is Unit of R by Th90;

        then a divides ( 1. R) by GCD_1:def 2;

        then

        consider c be Element of the carrier of R such that

         C1: (a * c) = ( 1. R);

        thus contradiction by C1, INT_1: 9;

      end;

      now

        assume q is_associated_to pp;

        then

        consider c be Element of the carrier of K such that

         C1: c is unital & (q * c) = p by GCD_1: 18;

        

         C2: ((a | R) *' c) = p by C1, POLYNOM3:def 10;

        ( deg c) = 0 by C1, T88;

        then c <> ( 0_. R) by HURWITZ: 20;

        

        then 1 = (( deg q) + ( deg c)) by HURWITZ: 23, C2, A2

        .= ( 0 + ( deg c)) by LX;

        hence contradiction by C1, T88;

      end;

      hence pp is reducible by B1, B4, RING_2:def 9;

    end;

    theorem :: RING_4:44

    

     thirr: for F be Field, p be Element of the carrier of ( Polynom-Ring F) st ( deg p) = 1 holds p is irreducible

    proof

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

      set K = ( Polynom-Ring R);

      reconsider x = p as Element of K;

      assume

       AS: ( deg p) = 1;

      then p <> ( 0_. R) by HURWITZ: 20;

      then

       A: x <> ( 0. K) by POLYNOM3:def 10;

      

       B: not x is Unit of K by AS, T88;

      now

        let a be Element of K;

        assume a divides x;

        then

        consider b be Element of K such that

         H1: (a * b) = x;

        reconsider q = a, r = b as Element of the carrier of K;

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

        then

         H2: q <> ( 0_. R) & r <> ( 0_. R) by AS, HURWITZ: 20, POLYNOM3: 34;

        

        then

         H4: (( deg q) + ( deg r)) = ( deg (q *' r)) by HURWITZ: 23

        .= 1 by AS, H1, POLYNOM3:def 10;

        per cases ;

          suppose

           C0: ( deg q) = 0 ;

          then q is constant;

          then

          consider u be Element of R such that

           C1: q = (u | R) by T11;

          u is non zero by C1, C0, T11a;

          hence a is Unit of K or a is_associated_to x by Th90, C1;

        end;

          suppose ( deg q) <> 0 ;

          then ( deg q) > 0 by H2, T8b;

          then (( deg q) + ( deg r)) > ( 0 + ( deg r)) by XREAL_1: 6;

          then r is constant by H4, NAT_1: 14;

          then

          consider u be Element of R such that

           C1: r = (u | R) by T11;

          u is non zero by C1, T6, H2;

          then r is Unit of K by Th90, C1;

          hence a is Unit of K or a is_associated_to x by H1, GCD_1: 18;

        end;

      end;

      hence thesis by A, B, RING_2:def 9;

    end;

    theorem :: RING_4:45

    

     thirr1: for F be algebraic-closed Field, p be Element of the carrier of ( Polynom-Ring F) holds p is irreducible iff ( deg p) = 1

    proof

      let R be algebraic-closed Field, p be Element of the carrier of ( Polynom-Ring R);

      set K = ( Polynom-Ring R);

      now

        assume

         AS: p is irreducible;

        then p is non constant;

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

        then

        consider x be Element of R such that

         A: x is_a_root_of p by POLYNOM5:def 8, POLYNOM5:def 9;

        consider q be Polynomial of R such that

         B: p = (( rpoly (1,x)) *' q) by A, HURWITZ: 33;

        reconsider y = q, z = ( rpoly (1,x)) as Element of ( Polynom-Ring R) by POLYNOM3:def 10;

        p = (z * y) by B, POLYNOM3:def 10;

        then z divides p;

        then

         C: z is Unit of K or z is_associated_to p by AS, RING_2:def 9;

        z is non constant by HURWITZ: 27;

        then

        consider e be Element of K such that

         D: e is unital & (z * e) = p by C, GCD_1: 18;

        reconsider u = e as Element of the carrier of K;

        

         F: ( deg u) = 0 by D, T88;

        (( rpoly (1,x)) *' u) = p by D, POLYNOM3:def 10;

        

        hence ( deg p) = (( deg ( rpoly (1,x))) + ( deg u)) by D, HURWITZ: 23

        .= 1 by F, HURWITZ: 27;

      end;

      hence thesis by thirr;

    end;

    theorem :: RING_4:46

    for F be Field holds F is algebraic-closed iff for p be monic Element of the carrier of ( Polynom-Ring F) holds p is irreducible iff ( deg p) = 1

    proof

      let R be Field;

      now

        assume

         AS: for p be monic Element of the carrier of ( Polynom-Ring R) holds p is irreducible iff ( deg p) = 1;

        now

          let p be Polynomial of R;

          assume

           A: ( len p) > 1;

          then

           A1: p <> ( 0_. R) by POLYNOM4: 3;

          

           A4: (( len p) - 1) > (1 - 1) by A, XREAL_1: 9;

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

          then

           A3: ( deg p) >= 1 by NAT_1: 14, A4;

          defpred P[ Nat] means for p be Polynomial of R st ( deg p) = $1 holds p is with_roots;

          

           II: for k be Nat st k >= 1 & (for n be Nat st n >= 1 & n < k holds P[n]) holds P[k]

          proof

            let k be Nat;

            assume

             IAS: k >= 1 & for n be Nat st n >= 1 & n < k holds P[n];

            per cases by IAS, XXREAL_0: 1;

              suppose

               IA1: k = 1;

              thus P[k]

              proof

                now

                  let p be Polynomial of R;

                  assume ( deg p) = 1;

                  then

                  consider x,z be Element of R such that

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

                  ( eval (p,z)) = (x * ( eval (( rpoly (1,z)),z))) by I1, POLYNOM5: 30

                  .= (x * (z - z)) by HURWITZ: 29

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

                  hence p is with_roots by POLYNOM5:def 8, POLYNOM5:def 7;

                end;

                hence thesis by IA1;

              end;

            end;

              suppose

               IA1: k > 1;

              thus P[k]

              proof

                now

                  let p be Polynomial of R;

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

                  set q = ( NormPolynomial p);

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

                  assume

                   K: ( deg p) = k;

                  then ( len p) <> 0 ;

                  then

                   I3: ( deg q) > 1 by K, IA1, POLYNOM5: 57;

                  p <> ( 0_. R) by K, HURWITZ: 20;

                  then p is non zero by UPROOTS:def 5;

                  then

                   I4: qq is reducible by AS, I3;

                  

                   I5: pp <> ( 0_. R) by K, HURWITZ: 20;

                   not p is Unit of ( Polynom-Ring R) by T8, K, IA1;

                  then

                  consider r be Element of the carrier of ( Polynom-Ring R) such that

                   I6: r divides p & 1 <= ( deg r) & ( deg r) < ( deg p) by I4, I5, T88b, thirr2;

                  r <> ( 0_. R) by I6, HURWITZ: 20;

                  then ( deg r) is Element of NAT by T8b;

                  then

                  consider x be Element of R such that

                   I8: x is_a_root_of r by K, I6, IAS, POLYNOM5:def 8;

                  reconsider rr = r, ppp = p as Element of ( Polynom-Ring R) by POLYNOM3:def 10;

                  rr divides ppp by I6;

                  then

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

                   I10: ppp = (rr * u);

                  p = (r *' u) by I10, POLYNOM3:def 10;

                  

                  then ( eval (p,x)) = (( eval (r,x)) * ( eval (u,x))) by POLYNOM4: 24

                  .= (( 0. R) * ( eval (u,x))) by I8, POLYNOM5:def 7

                  .= ( 0. R);

                  hence p is with_roots by POLYNOM5:def 8, POLYNOM5:def 7;

                end;

                hence thesis;

              end;

            end;

          end;

          

           I: for k be Nat st 1 <= k holds P[k] from NAT_1:sch 9( II);

          ( deg p) is Element of NAT by A1, T8b;

          then

          consider n be Nat such that

           H: n >= 1 & ( deg p) = n by A3;

          thus p is with_roots by H, I;

        end;

        hence R is algebraic-closed by POLYNOM5:def 9;

      end;

      hence thesis by thirr1;

    end;

    registration

      let R be domRing;

      cluster irreducible for Element of ( Polynom-Ring R);

      existence

      proof

        set K = ( Polynom-Ring R);

        reconsider x = ( rpoly (1,( 0. R))) as Element of K by POLYNOM3:def 10;

        ( deg ( rpoly (1,( 0. R)))) = 1 by HURWITZ: 27;

        then x is irreducible by thirr0;

        hence thesis;

      end;

    end

    registration

      let R be domRing;

      cluster irreducible for Element of the carrier of ( Polynom-Ring R);

      existence

      proof

        set K = ( Polynom-Ring R);

        reconsider x = ( rpoly (1,( 0. R))) as Element of the carrier of K by POLYNOM3:def 10;

        ( deg ( rpoly (1,( 0. R)))) = 1 by HURWITZ: 27;

        then x is irreducible by thirr0;

        hence thesis;

      end;

    end

    registration

      let R be Ring;

      cluster reducible for Element of ( Polynom-Ring R);

      existence

      proof

        take p = ( 0. ( Polynom-Ring R));

        thus thesis;

      end;

    end

    registration

      let R be Ring;

      cluster reducible for Element of the carrier of ( Polynom-Ring R);

      existence

      proof

        take p = ( 0_. R);

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

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

        hence thesis;

      end;

    end

    registration

      let R be domRing;

      cluster ( IRR ( Polynom-Ring R)) -> non empty;

      coherence

      proof

        now

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

          p in { x where x be Element of ( Polynom-Ring R) : x is irreducible };

          hence p in ( IRR ( Polynom-Ring R)) by RING_2:def 10;

        end;

        hence thesis;

      end;

    end

    registration

      let F be Field;

      cluster constant -> reducible for Element of ( Polynom-Ring F);

      coherence ;

    end

    registration

      let F be Field;

      cluster constant -> reducible for Element of the carrier of ( Polynom-Ring F);

      coherence ;

    end

    registration

      let F be Field;

      cluster irreducible -> non constant for Element of ( Polynom-Ring F);

      coherence ;

    end

    registration

      let F be Field;

      cluster irreducible -> non constant for Element of the carrier of ( Polynom-Ring F);

      coherence ;

    end

    begin

    registration

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

      cluster (( Polynom-Ring F) / ( {p} -Ideal )) -> Abelian add-associative right_zeroed right_complementable commutative associative well-unital distributive;

      coherence ;

    end

    registration

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

      cluster (( Polynom-Ring F) / ( {p} -Ideal )) -> non degenerated almost_left_invertible;

      coherence by RING_2: 26, RING_1: 21;

    end

    definition

      let F be Field, p be Polynomial of F;

      :: RING_4:def7

      func poly_mult_mod p -> BinOp of ( Polynom-Ring F) means

      : defpmm: for r,q be Polynomial of F holds (it . (r,q)) = ((r *' q) mod p);

      existence

      proof

        set B = ( Polynom-Ring F);

        set D = the carrier of B;

        defpred P[ object, object, object] means ex r,q be Element of D st $1 = r & $2 = q & $3 = ((r *' q) mod p);

         I:

        now

          let x,y be object;

          assume x in D & y in D;

          then

          reconsider xx = x, yy = y as Element of D;

          reconsider r = xx, q = yy as Polynomial of F;

          thus ex z be object st z in D & P[x, y, z]

          proof

            take s = ((r *' q) mod p);

            thus s in D by POLYNOM3:def 10;

            take xx, yy;

            thus thesis;

          end;

        end;

        consider f be Function of [:D, D:], D such that

         H: for x,y be object st x in D & y in D holds P[x, y, (f . (x,y))] from BINOP_1:sch 1( I);

        take f;

        now

          let r,q be Polynomial of F;

          r in D & q in D by POLYNOM3:def 10;

          then P[r, q, (f . (r,q))] by H;

          then

          consider rr,qq be Element of D such that

           K: rr = r & qq = q & (f . (rr,qq)) = ((rr *' qq) mod p);

          thus (f . (r,q)) = ((r *' q) mod p) by K;

        end;

        hence thesis;

      end;

      uniqueness

      proof

        set B = ( Polynom-Ring F);

        let g1,g2 be BinOp of B such that

         A1: for r,q be Polynomial of F holds (g1 . (r,q)) = ((r *' q) mod p) and

         A2: for r,q be Polynomial of F holds (g2 . (r,q)) = ((r *' q) mod p);

        

         A: ( dom g1) = [:the carrier of B, the carrier of B:] by FUNCT_2:def 1

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

        now

          let x be object;

          assume x in ( dom g1);

          then

          consider r,q be object such that

           H: r in the carrier of B & q in the carrier of B & x = [r, q] by ZFMISC_1:def 2;

          reconsider r, q as Polynomial of F by H, POLYNOM3:def 10;

          

          thus (g1 . x) = (g1 . (r,q)) by H

          .= ((r *' q) mod p) by A1

          .= (g2 . (r,q)) by A2

          .= (g2 . x) by H;

        end;

        hence thesis by A, FUNCT_1: 2;

      end;

    end

    

     pr1: for F be Field, p be Element of the carrier of ( Polynom-Ring F) holds { q where q be Polynomial of F : ( deg q) < ( deg p) } is Preserv of the addF of ( Polynom-Ring F)

    proof

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

      set C = { q where q be Polynomial of F : ( deg q) < ( deg p) };

      now

        let x be set;

        assume x in C;

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

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

      end;

      then C c= the carrier of ( Polynom-Ring F);

      then

      reconsider C as Subset of the carrier of ( Polynom-Ring F);

      set A = the addF of ( Polynom-Ring F);

      now

        let x be set;

        assume x in [:C, C:];

        then

        consider a,b be object such that

         A2: a in C and

         A3: b in C and

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

        consider u be Polynomial of F such that

         A5: a = u & ( deg u) < ( deg p) by A2;

        consider v be Polynomial of F such that

         A6: b = v & ( deg v) < ( deg p) by A3;

        reconsider a, b as Element of ( Polynom-Ring F) by A5, A6, POLYNOM3:def 10;

        

         A7: ( deg (u + v)) <= ( max (( deg u),( deg v))) by HURWITZ: 22;

        ( max (( deg u),( deg v))) < ( deg p) by A5, A6, XXREAL_0: 29;

        then

         A8: ( deg (u + v)) < ( deg p) by A7, XXREAL_0: 2;

        (A . x) = (a + b) by A4

        .= (u + v) by A5, A6, POLYNOM3:def 10;

        hence (A . x) in C by A8;

      end;

      hence thesis by REALSET1:def 1;

    end;

    

     pr2: for F be Field, p be non constant Element of the carrier of ( Polynom-Ring F) holds { q where q be Polynomial of F : ( deg q) < ( deg p) } is Preserv of ( poly_mult_mod p)

    proof

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

      set C = { q where q be Polynomial of F : ( deg q) < ( deg p) };

      now

        let x be set;

        assume x in C;

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

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

      end;

      then C c= the carrier of ( Polynom-Ring F);

      then

      reconsider C as Subset of the carrier of ( Polynom-Ring F);

      set A = ( poly_mult_mod p);

      now

        let x be set;

        assume x in [:C, C:];

        then

        consider a,b be object such that

         A2: a in C and

         A3: b in C and

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

        consider u be Polynomial of F such that

         A5: a = u & ( deg u) < ( deg p) by A2;

        consider v be Polynomial of F such that

         A6: b = v & ( deg v) < ( deg p) by A3;

        reconsider a, b as Element of ( Polynom-Ring F) by A5, A6, POLYNOM3:def 10;

        

         A8: ( deg ((u *' v) mod p)) < ( deg p) by RING_2: 29;

        (A . x) = (( poly_mult_mod p) . (u,v)) by A5, A6, A4

        .= ((u *' v) mod p) by defpmm;

        hence (A . x) in C by A8;

      end;

      hence thesis by REALSET1:def 1;

    end;

    

     pr3: for F be Field, p be non constant Element of the carrier of ( Polynom-Ring F) holds ( 1_. F) in { q where q be Polynomial of F : ( deg q) < ( deg p) }

    proof

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

      

       A: ( deg p) > 0 by defconst;

      ( len ( 1_. F)) = 1 by POLYNOM4: 4;

      then ( deg ( 1_. F)) = 0 ;

      hence thesis by A;

    end;

    

     pr4: for F be Field, p be non constant Element of the carrier of ( Polynom-Ring F) holds ( 0_. F) in { q where q be Polynomial of F : ( deg q) < ( deg p) }

    proof

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

      ( deg ( 0_. F)) = ( - 1) by HURWITZ: 20;

      hence thesis;

    end;

    definition

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

      :: RING_4:def8

      func Polynom-Ring (p) -> strict doubleLoopStr means

      : defprfp: the carrier of it = { q where q be Polynomial of F : ( deg q) < ( deg p) } & the addF of it = (the addF of ( Polynom-Ring F) || the carrier of it ) & the multF of it = (( poly_mult_mod p) || the carrier of it ) & the OneF of it = ( 1_. F) & the ZeroF of it = ( 0_. F);

      existence

      proof

        set B = ( Polynom-Ring F);

        set C = { q where q be Polynomial of F : ( deg q) < ( deg p) };

        set A = the addF of B;

        set M = ( poly_mult_mod p);

        reconsider C1 = C as Preserv of A by pr1;

        reconsider ad = (A || C1) as BinOp of C;

        reconsider C2 = C as Preserv of M by pr2;

        reconsider mu = (M || C2) as BinOp of C;

        reconsider O = ( 1_. F) as Element of C by pr3;

        reconsider Z = ( 0_. F) as Element of C by pr4;

        take doubleLoopStr (# C, ad, mu, O, Z #);

        thus thesis;

      end;

      uniqueness ;

    end

    registration

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

      cluster ( Polynom-Ring p) -> non degenerated;

      coherence

      proof

        set P = ( Polynom-Ring p);

        ( 1. P) = ( 1_. F) by defprfp;

        hence ( 0. P) <> ( 1. P) by defprfp;

      end;

    end

    registration

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

      cluster ( Polynom-Ring p) -> Abelian add-associative right_zeroed right_complementable;

      coherence

      proof

        set P = ( Polynom-Ring p);

        set C = { q where q be Polynomial of F : ( deg q) < ( deg p) };

        

         H0: C = the carrier of P by defprfp;

        

         H1: ( 0. P) = ( 0_. F) by defprfp;

        now

          let x,y be Element of P;

          x in the carrier of P;

          then x in C by defprfp;

          then

          consider q be Polynomial of F such that

           A1: x = q & ( deg q) < ( deg p);

          y in the carrier of P;

          then y in C by defprfp;

          then

          consider r be Polynomial of F such that

           A2: y = r & ( deg r) < ( deg p);

          reconsider q, r as Element of ( Polynom-Ring F) by POLYNOM3:def 10;

          

           A3: [x, y] in [:C, C:] & [y, x] in [:C, C:] by H0, ZFMISC_1:def 2;

          

          thus (x + y) = ((the addF of ( Polynom-Ring F) || C) . (x,y)) by H0, defprfp

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

          .= (the addF of ( Polynom-Ring F) . (y,x)) by A1, A2, ALGSTR_0:def 1

          .= ((the addF of ( Polynom-Ring F) || C) . (y,x)) by A3, FUNCT_1: 49

          .= (y + x) by H0, defprfp;

        end;

        hence P is Abelian by RLVECT_1:def 2;

        now

          let x,y,z be Element of P;

          x in the carrier of P;

          then x in C by defprfp;

          then

          consider q be Polynomial of F such that

           A1: x = q & ( deg q) < ( deg p);

          y in the carrier of P;

          then y in C by defprfp;

          then

          consider r be Polynomial of F such that

           A2: y = r & ( deg r) < ( deg p);

          z in the carrier of P;

          then z in C by defprfp;

          then

          consider u be Polynomial of F such that

           A3: z = u & ( deg u) < ( deg p);

          

           A3a: [x, y] in [:C, C:] & [y, z] in [:C, C:] by H0, ZFMISC_1:def 2;

          

           A3b: [(x + y), z] in [:C, C:] & [x, (y + z)] in [:C, C:] by H0, ZFMISC_1:def 2;

          reconsider q, r, u as Element of ( Polynom-Ring F) by POLYNOM3:def 10;

          

           A4: (x + y) = ((the addF of ( Polynom-Ring F) || C) . (x,y)) by H0, defprfp

          .= (q + r) by A1, A2, A3a, FUNCT_1: 49;

          

           A5: (y + z) = ((the addF of ( Polynom-Ring F) || C) . (y,z)) by H0, defprfp

          .= (r + u) by A3, A2, A3a, FUNCT_1: 49;

          

           A6: ((x + y) + z) = ((the addF of ( Polynom-Ring F) || C) . ((x + y),z)) by H0, defprfp

          .= ((q + r) + u) by A3, A4, A3b, FUNCT_1: 49

          .= (q + (r + u)) by RLVECT_1:def 3;

          

          thus (x + (y + z)) = ((the addF of ( Polynom-Ring F) || C) . (x,(y + z))) by H0, defprfp

          .= ((x + y) + z) by A6, A5, A1, A3b, FUNCT_1: 49;

        end;

        hence P is add-associative by RLVECT_1:def 3;

        now

          let x be Element of P;

          x in the carrier of P;

          then x in C by defprfp;

          then

          consider q be Polynomial of F such that

           A1: x = q & ( deg q) < ( deg p);

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

          reconsider r = ( 0_. F) as Element of ( Polynom-Ring F) by POLYNOM3:def 10;

          

           A3: [x, ( 0. P)] in [:C, C:] by H0, ZFMISC_1:def 2;

          

          thus (x + ( 0. P)) = ((the addF of ( Polynom-Ring F) || C) . (x,( 0. P))) by H0, defprfp

          .= (the addF of ( Polynom-Ring F) . (x,( 0. P))) by A3, FUNCT_1: 49

          .= (q1 + r) by defprfp, A1

          .= (q + ( 0_. F)) by POLYNOM3:def 10

          .= x by A1, POLYNOM3: 28;

        end;

        hence P is right_zeroed by RLVECT_1:def 4;

        now

          let x be Element of P;

          x in the carrier of P;

          then x in C by defprfp;

          then

          consider q be Polynomial of F such that

           A1: x = q & ( deg q) < ( deg p);

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

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

          ( deg ( - q)) = ( deg q) by POLYNOM4: 8;

          then ( - q) in C by A1;

          then

          reconsider y = ( - q) as Element of P by defprfp;

          

           A3: [x, y] in [:C, C:] by H0, ZFMISC_1:def 2;

          (x + y) = ((the addF of ( Polynom-Ring F) || C) . (x,y)) by H0, defprfp

          .= (q1 + r) by A1, A3, FUNCT_1: 49

          .= (q - q) by POLYNOM3:def 10

          .= ( 0_. F) by POLYNOM3: 29;

          hence x is right_complementable by H1;

        end;

        hence P is right_complementable;

      end;

    end

    registration

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

      cluster ( Polynom-Ring p) -> associative well-unital distributive;

      coherence

      proof

        set P = ( Polynom-Ring p);

        set C = { q where q be Polynomial of F : ( deg q) < ( deg p) };

        

         H0: C = the carrier of P by defprfp;

        

         H2: ( 1. P) = ( 1_. F) by defprfp;

        reconsider p1 = p as Polynomial of F;

        now

          let x,y,z be Element of P;

          x in the carrier of P;

          then x in C by defprfp;

          then

          consider q be Polynomial of F such that

           A1: x = q & ( deg q) < ( deg p);

          y in the carrier of P;

          then y in C by defprfp;

          then

          consider r be Polynomial of F such that

           A2: y = r & ( deg r) < ( deg p);

          z in the carrier of P;

          then z in C by defprfp;

          then

          consider u be Polynomial of F such that

           A3: z = u & ( deg u) < ( deg p);

          

           A3a: [x, y] in [:C, C:] & [y, z] in [:C, C:] by H0, ZFMISC_1:def 2;

          

           A3b: [(x * y), z] in [:C, C:] & [x, (y * z)] in [:C, C:] by H0, ZFMISC_1:def 2;

          

           A4: (x * y) = ((( poly_mult_mod p) || C) . (x,y)) by H0, defprfp

          .= (( poly_mult_mod p) . (x,y)) by A3a, FUNCT_1: 49

          .= ((q *' r) mod p1) by A1, A2, defpmm;

          

           A5: (y * z) = ((( poly_mult_mod p) || C) . (y,z)) by H0, defprfp

          .= (( poly_mult_mod p) . (y,z)) by A3a, FUNCT_1: 49

          .= ((r *' u) mod p1) by A3, A2, defpmm;

          

           A6: ((x * y) * z) = ((( poly_mult_mod p) || C) . ((x * y),z)) by H0, defprfp

          .= (( poly_mult_mod p) . ((x * y),z)) by A3b, FUNCT_1: 49

          .= ((((q *' r) mod p1) *' u) mod p1) by A3, A4, defpmm

          .= (((q *' r) *' u) mod p1) by div3;

          

          thus (x * (y * z)) = ((( poly_mult_mod p) || C) . (x,(y * z))) by H0, defprfp

          .= (( poly_mult_mod p) . (x,(y * z))) by A3b, FUNCT_1: 49

          .= ((((r *' u) mod p1) *' q) mod p1) by A1, A5, defpmm

          .= (((r *' u) *' q) mod p1) by div3

          .= ((x * y) * z) by A6, POLYNOM3: 33;

        end;

        hence P is associative by GROUP_1:def 3;

        now

          let x be Element of P;

          x in the carrier of P;

          then x in C by defprfp;

          then

          consider q be Polynomial of F such that

           A1: x = q & ( deg q) < ( deg p);

          

           A3a: [x, ( 1. P)] in [:C, C:] & [( 1. P), x] in [:C, C:] by H0, ZFMISC_1:def 2;

          

          thus (x * ( 1. P)) = ((( poly_mult_mod p) || C) . (x,( 1. P))) by H0, defprfp

          .= (( poly_mult_mod p) . (x,( 1. P))) by A3a, FUNCT_1: 49

          .= ((q *' ( 1_. F)) mod p1) by H2, A1, defpmm

          .= (q mod p1) by POLYNOM3: 35

          .= x by A1, div1;

          

          thus (( 1. P) * x) = ((( poly_mult_mod p) || C) . (( 1. P),x)) by H0, defprfp

          .= (( poly_mult_mod p) . (( 1. P),x)) by A3a, FUNCT_1: 49

          .= ((( 1_. F) *' q) mod p1) by H2, A1, defpmm

          .= (q mod p1) by POLYNOM3: 35

          .= x by A1, div1;

        end;

        hence P is well-unital by VECTSP_1:def 6;

        now

          let x,y,z be Element of P;

          x in the carrier of P;

          then x in C by defprfp;

          then

          consider q be Polynomial of F such that

           A1: x = q & ( deg q) < ( deg p);

          y in the carrier of P;

          then y in C by defprfp;

          then

          consider r be Polynomial of F such that

           A2: y = r & ( deg r) < ( deg p);

          z in the carrier of P;

          then z in C by defprfp;

          then

          consider u be Polynomial of F such that

           A3: z = u & ( deg u) < ( deg p);

          reconsider q1 = q, r1 = r, u1 = u as Element of ( Polynom-Ring F) by POLYNOM3:def 10;

          

           A3a: [x, y] in [:C, C:] & [x, z] in [:C, C:] & [y, z] in [:C, C:] by H0, ZFMISC_1:def 2;

          

           A3b: [(x * y), (x * z)] in [:C, C:] & [x, (y * z)] in [:C, C:] & [x, (y + z)] in [:C, C:] by H0, ZFMISC_1:def 2;

          

           A4: (y + z) = ((the addF of ( Polynom-Ring F) || C) . (y,z)) by H0, defprfp

          .= (r1 + u1) by A2, A3, A3a, FUNCT_1: 49

          .= (r + u) by POLYNOM3:def 10;

          

           A5: (x * (y + z)) = ((( poly_mult_mod p) || C) . (x,(y + z))) by H0, defprfp

          .= (( poly_mult_mod p) . (x,(y + z))) by A3b, FUNCT_1: 49

          .= ((q *' (r + u)) mod p1) by A1, A4, defpmm;

          

           A6: (x * y) = ((( poly_mult_mod p) || C) . (x,y)) by H0, defprfp

          .= (( poly_mult_mod p) . (x,y)) by A3a, FUNCT_1: 49

          .= ((q *' r) mod p1) by A1, A2, defpmm;

          

           A7: (x * z) = ((( poly_mult_mod p) || C) . (x,z)) by H0, defprfp

          .= (( poly_mult_mod p) . (x,z)) by A3a, FUNCT_1: 49

          .= ((q *' u) mod p1) by A1, A3, defpmm;

          reconsider s = ((q *' r) mod p1) as Element of ( Polynom-Ring F) by POLYNOM3:def 10;

          reconsider t = ((q *' u) mod p1) as Element of ( Polynom-Ring F) by POLYNOM3:def 10;

          

          thus ((x * y) + (x * z)) = ((the addF of ( Polynom-Ring F) || C) . ((x * y),(x * z))) by H0, defprfp

          .= (s + t) by A6, A7, A3b, FUNCT_1: 49

          .= (((q *' r) mod p1) + ((q *' u) mod p1)) by POLYNOM3:def 10

          .= (((q *' r) + (q *' u)) mod p1) by div4

          .= (x * (y + z)) by A5, POLYNOM3: 31;

          

           A3a: [y, x] in [:C, C:] & [z, x] in [:C, C:] & [y, z] in [:C, C:] by H0, ZFMISC_1:def 2;

          

           A3b: [(y * x), (z * x)] in [:C, C:] & [x, (y * z)] in [:C, C:] & [(y + z), x] in [:C, C:] by H0, ZFMISC_1:def 2;

          

           A4: (y + z) = ((the addF of ( Polynom-Ring F) || C) . (y,z)) by H0, defprfp

          .= (r1 + u1) by A2, A3, A3a, FUNCT_1: 49

          .= (r + u) by POLYNOM3:def 10;

          

           A5: ((y + z) * x) = ((( poly_mult_mod p) || C) . ((y + z),x)) by H0, defprfp

          .= (( poly_mult_mod p) . ((y + z),x)) by A3b, FUNCT_1: 49

          .= (((r + u) *' q) mod p1) by A1, A4, defpmm;

          

           A6: (y * x) = ((( poly_mult_mod p) || C) . (y,x)) by H0, defprfp

          .= (( poly_mult_mod p) . (y,x)) by A3a, FUNCT_1: 49

          .= ((r *' q) mod p1) by A1, A2, defpmm;

          

           A7: (z * x) = ((( poly_mult_mod p) || C) . (z,x)) by H0, defprfp

          .= (( poly_mult_mod p) . (z,x)) by A3a, FUNCT_1: 49

          .= ((u *' q) mod p1) by A1, A3, defpmm;

          reconsider s = ((r *' q) mod p1) as Element of ( Polynom-Ring F) by POLYNOM3:def 10;

          reconsider t = ((u *' q) mod p1) as Element of ( Polynom-Ring F) by POLYNOM3:def 10;

          

          thus ((y * x) + (z * x)) = ((the addF of ( Polynom-Ring F) || C) . ((y * x),(z * x))) by H0, defprfp

          .= (s + t) by A6, A7, A3b, FUNCT_1: 49

          .= (((q *' r) mod p1) + ((q *' u) mod p1)) by POLYNOM3:def 10

          .= (((q *' r) + (q *' u)) mod p1) by div4

          .= ((y + z) * x) by A5, POLYNOM3: 31;

        end;

        hence P is distributive by VECTSP_1:def 7;

      end;

    end

    definition

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

      :: RING_4:def9

      func poly_mod p -> Function of ( Polynom-Ring F), ( Polynom-Ring p) means

      : dpm: for q be Polynomial of F holds (it . q) = (q mod p);

      existence

      proof

        set B = ( Polynom-Ring F);

        set D = the carrier of B;

        defpred P[ object, object] means ex q be Element of D st $1 = q & $2 = (q mod p);

        now

          let x be object;

          assume x in D;

          then

          reconsider xx = x as Element of D;

          reconsider r = xx as Polynomial of F;

          thus ex z be object st z in the carrier of ( Polynom-Ring p) & P[x, z]

          proof

            take s = (r mod p);

            ( deg s) < ( deg p) by RING_2: 29;

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

            hence s in the carrier of ( Polynom-Ring p) by defprfp;

            take xx;

            thus thesis;

          end;

        end;

        then

         I: for x be object st x in D holds ex y be object st y in the carrier of ( Polynom-Ring p) & P[x, y];

        consider f be Function of D, ( Polynom-Ring p) such that

         H: for x be object st x in D holds P[x, (f . x)] from FUNCT_2:sch 1( I);

        reconsider f as Function of B, ( Polynom-Ring p);

        take f;

        now

          let q be Polynomial of F;

          q in B by POLYNOM3:def 10;

          then P[q, (f . q)] by H;

          then

          consider qq be Element of D such that

           K: qq = q & (f . qq) = (qq mod p);

          thus (f . q) = (q mod p) by K;

        end;

        hence thesis;

      end;

      uniqueness

      proof

        set B = ( Polynom-Ring F);

        let g1,g2 be Function of B, ( Polynom-Ring p) such that

         A1: for q be Polynomial of F holds (g1 . q) = (q mod p) and

         A2: for q be Polynomial of F holds (g2 . q) = (q mod p);

        

         A: ( dom g1) = the carrier of B by FUNCT_2:def 1

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

        now

          let x be object;

          assume x in ( dom g1);

          then

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

          

          thus (g1 . x) = (q mod p) by A1

          .= (g2 . x) by A2;

        end;

        hence thesis by A, FUNCT_1: 2;

      end;

    end

    registration

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

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

      coherence

      proof

        set f = ( poly_mod p), K = ( Polynom-Ring p);

        set C = the carrier of K;

        hereby

          let x1,y1 be Element of ( Polynom-Ring F);

          reconsider x = x1, y = y1 as Element of the carrier of ( Polynom-Ring F);

          

           H: (f . x) = (x mod p) & (f . y) = (y mod p) by dpm;

          then

          reconsider fx = (f . x), fy = (f . y) as Element of ( Polynom-Ring F) by POLYNOM3:def 10;

          

           A3: [(f . x), (f . y)] in [:C, C:] by ZFMISC_1:def 2;

          

          thus ((f . x1) + (f . y1)) = ((the addF of ( Polynom-Ring F) || the carrier of K) . ((f . x1),(f . y1))) by defprfp

          .= (fx + fy) by A3, FUNCT_1: 49

          .= ((x mod p) + (y mod p)) by H, POLYNOM3:def 10

          .= ((x + y) mod p) by div4

          .= (f . (x + y)) by dpm

          .= (f . (x1 + y1)) by POLYNOM3:def 10;

        end;

        hereby

          let x1,y1 be Element of ( Polynom-Ring F);

          reconsider x = x1, y = y1 as Element of the carrier of ( Polynom-Ring F);

          

           H: (f . x) = (x mod p) & (f . y) = (y mod p) by dpm;

          then

          reconsider fx = (f . x), fy = (f . y) as Element of ( Polynom-Ring F) by POLYNOM3:def 10;

          

           A3: [(f . x), (f . y)] in [:C, C:] by ZFMISC_1:def 2;

          

          thus ((f . x1) * (f . y1)) = ((( poly_mult_mod p) || the carrier of K) . ((f . x1),(f . y1))) by defprfp

          .= (( poly_mult_mod p) . ((f . x),(f . y))) by A3, FUNCT_1: 49

          .= (((x mod p) *' (y mod p)) mod p) by H, defpmm

          .= ((x *' y) mod p) by div3a

          .= (f . (x *' y)) by dpm

          .= (f . (x1 * y1)) by POLYNOM3:def 10;

        end;

        ( deg p) > 0 by defconst;

        then

         H: ( deg ( 1_. F)) < ( deg p) by RATFUNC1:def 2;

        

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

        .= (( 1_. F) mod p) by dpm

        .= ( 1_. F) by H, div1

        .= ( 1_ K) by defprfp;

      end;

    end

    registration

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

      cluster ( Polynom-Ring p) -> ( Polynom-Ring F) -homomorphic;

      coherence

      proof

        ( poly_mod p) is linear

        proof

          thus ( poly_mod p) is additive multiplicative unity-preserving;

        end;

        hence thesis by RING_2:def 4;

      end;

    end

    registration

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

      cluster ( poly_mod p) -> onto;

      coherence

      proof

        set f = ( poly_mod p);

        now

          let x be object;

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

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

          then

          consider q be Polynomial of F such that

           B: q = x & ( deg q) < ( deg p);

          (q mod p) = q by B, div1;

          then

           C: (f . x) = q by B, dpm;

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

          then q in ( dom f) by POLYNOM3:def 10;

          hence x in ( rng f) by B, C, FUNCT_1:def 3;

        end;

        then for x be object holds x in ( rng f) iff x in the carrier of ( Polynom-Ring p);

        hence thesis by FUNCT_2:def 3, TARSKI: 2;

      end;

    end

    

     lemminuspoly: for R be Ring, a be Element of ( Polynom-Ring R), b be Polynomial of R st a = b holds ( - a) = ( - b)

    proof

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

      assume

       AS: a = b;

      set K = ( Polynom-Ring R);

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

      (a + c) = (b - b) by AS, POLYNOM3:def 10

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

      .= ( 0. K) by POLYNOM3:def 10

      .= (a + ( - a)) by RLVECT_1: 5;

      hence thesis by RLVECT_1: 8;

    end;

    theorem :: RING_4:47

    

     kerp: for F be Field, p be non constant Element of the carrier of ( Polynom-Ring F) holds ( ker ( poly_mod p)) = ( {p} -Ideal )

    proof

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

      set R = ( Polynom-Ring F), S = ( Polynom-Ring p);

      set f = ( poly_mod p);

      reconsider p1 = p as Element of R;

       A:

      now

        let x be object;

        assume

         A0: x in ( ker f);

        then x in { v where v be Element of R : (f . v) = ( 0. S) } by VECTSP10:def 9;

        then

        consider y be Element of R such that

         A1: y = x & (f . y) = ( 0. S);

        reconsider q = x as Element of the carrier of R by A0;

        reconsider q1 = x as Element of R by A0;

        

         A2: (q - ((q div p) *' p)) = (q mod p)

        .= ( 0. S) by A1, dpm

        .= ( 0_. F) by defprfp;

        reconsider qp = (q div p) as Element of R by POLYNOM3:def 10;

        (qp * p1) = ((q div p) *' p) by POLYNOM3:def 10;

        then

         A3: ( - (qp * p1)) = ( - ((q div p) *' p)) by lemminuspoly;

        (q1 - (qp * p1)) = (q + ( - ((q div p) *' p))) by A3, POLYNOM3:def 10

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

        then (qp * p1) = q1 by RLVECT_1: 21;

        then q in the set of all (p * r) where r be Element of R;

        hence x in ( {p} -Ideal ) by IDEAL_1: 64;

      end;

      now

        let x be object;

        assume x in ( {p} -Ideal );

        then x in the set of all (p * r) where r be Element of R by IDEAL_1: 64;

        then

        consider y be Element of R such that

         A1: x = (p * y);

        reconsider q = y as Element of the carrier of R;

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

        

        then (f . x) = ((p *' q) mod p) by A1, dpm

        .= ( 0_. F) by T2, div2

        .= ( 0. S) by defprfp;

        then x in { v where v be Element of R : (f . v) = ( 0. S) } by A1;

        hence x in ( ker ( poly_mod p)) by VECTSP10:def 9;

      end;

      hence thesis by A, TARSKI: 2;

    end;

    theorem :: RING_4:48

    

     ISO: for F be Field, p be non constant Element of the carrier of ( Polynom-Ring F) holds ((( Polynom-Ring F) / ( {p} -Ideal )),( Polynom-Ring p)) are_isomorphic

    proof

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

      set R = ( Polynom-Ring F), S = ( Polynom-Ring p);

      ((R / ( ker ( poly_mod p))),S) are_isomorphic by RING_2: 16;

      hence thesis by kerp;

    end;

    registration

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

      cluster ( Polynom-Ring p) -> commutative;

      coherence

      proof

        set R = (( Polynom-Ring F) / ( {p} -Ideal )), S = ( Polynom-Ring p);

        ex f be Function of R, S st f is RingIsomorphism by ISO, QUOFIELD:def 23;

        then ( Polynom-Ring p) is R -isomorphic by RING_3:def 4;

        hence S is commutative;

      end;

    end

    registration

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

      cluster ( Polynom-Ring p) -> almost_left_invertible;

      coherence

      proof

        set R = (( Polynom-Ring F) / ( {p} -Ideal )), S = ( Polynom-Ring p);

        ex f be Function of R, S st f is RingIsomorphism by ISO, QUOFIELD:def 23;

        then ( Polynom-Ring p) is R -isomorphic by RING_3:def 4;

        hence thesis;

      end;

    end

    begin

    definition

      let L be non empty multMagma;

      let x,y be Element of L;

      let z be Element of L;

      :: RING_4:def10

      attr z is x,y -gcd means

      : defGCD: z divides x & z divides y & for r be Element of L st r divides x & r divides y holds r divides z;

    end

    registration

      let L be gcdDomain;

      let x,y be Element of L;

      cluster x, y -gcd for Element of L;

      existence

      proof

        consider z be Element of L such that

         H: z divides x & z divides y & for zz be Element of L st zz divides x & zz divides y holds zz divides z by GCD_1:def 11;

        take z;

        thus thesis by H;

      end;

    end

    definition

      let L be gcdDomain;

      let x,y be Element of L;

      mode a_gcd of x,y is x, y -gcd Element of L;

    end

    theorem :: RING_4:49

    

     gcd1: for L be gcdDomain holds for x,y be Element of L holds for u,v be a_gcd of x, y holds u is_associated_to v

    proof

      let L be gcdDomain;

      let p,q be Element of L;

      let u,v be a_gcd of p, q;

      

       A: u divides p & u divides q by defGCD;

      v divides p & v divides q by defGCD;

      hence thesis by A, defGCD;

    end;

    registration

      let L be gcdDomain;

      let x,y be Element of L;

      cluster x, y -gcd -> y, x -gcd for Element of L;

      coherence ;

    end

    definition

      let F be Field;

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

      :: RING_4:def11

      func p gcd q -> Element of the carrier of ( Polynom-Ring F) means

      : dpg: it = ( 0_. F) if p = ( 0_. F) & q = ( 0_. F)

      otherwise it is a_gcd of p, q & it is monic;

      existence

      proof

        per cases ;

          suppose p = ( 0_. F) & q = ( 0_. F);

          hence thesis;

        end;

          suppose

           AS: p <> ( 0_. F) or q <> ( 0_. F);

          reconsider g = the a_gcd of p, q as Element of the carrier of ( Polynom-Ring F);

          reconsider p1 = p, q1 = q as Element of ( Polynom-Ring F);

          set r = ( NormPolynomial g);

          reconsider r1 = r as Element of ( Polynom-Ring F);

           A:

          now

            assume g is zero;

            then g = ( 0_. F) by UPROOTS:def 5;

            then

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

            g divides p1 by defGCD;

            then

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

             D2: (g * u) = p1;

            g divides q1 by defGCD;

            then

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

             D4: (g * v) = q1;

            thus contradiction by D1, D4, D2, AS, POLYNOM3:def 10;

          end;

          g divides p1 by defGCD;

          then g divides p;

          then

           F: r divides p by np1;

          g divides q1 by defGCD;

          then g divides q;

          then

           B: r divides q by np1;

          now

            let z be Element of ( Polynom-Ring F);

            reconsider z1 = z as Element of the carrier of ( Polynom-Ring F);

            assume z divides p & z divides q;

            then z divides g by defGCD;

            then z1 divides g;

            then z1 divides r by np2;

            hence z divides r1;

          end;

          then r1 is p, q -gcd by B, F;

          hence thesis by A;

        end;

      end;

      uniqueness

      proof

        per cases ;

          suppose p = ( 0_. F) & q = ( 0_. F);

          hence thesis;

        end;

          suppose p <> ( 0_. F) or q <> ( 0_. F);

          thus thesis by gcd1, np0;

        end;

      end;

      consistency ;

    end

    definition

      let F be Field;

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

      :: original: gcd

      redefine

      func p gcd q;

      commutativity

      proof

        now

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

          per cases ;

            suppose

             AS: p = ( 0_. F) & q = ( 0_. F);

            thus (p gcd q) = (q gcd p) by AS;

          end;

            suppose

             AS: p <> ( 0_. F) or q <> ( 0_. F);

            then (p gcd q) is a_gcd of p, q & (p gcd q) is monic by dpg;

            hence (p gcd q) = (q gcd p) by AS, dpg;

          end;

        end;

        hence thesis;

      end;

    end

    definition

      let F be Field;

      let p,q be Element of ( Polynom-Ring F);

      :: original: gcd

      redefine

      func p gcd q;

      commutativity

      proof

        for p,q be Element of ( Polynom-Ring F) holds (p gcd q) = (q gcd p);

        hence thesis;

      end;

    end

    registration

      let F be Field;

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

      cluster (p gcd q) -> p, q -gcd;

      coherence

      proof

        per cases ;

          suppose

           A: p = ( 0_. F) & q = ( 0_. F);

          reconsider g = (p gcd q) as Element of ( Polynom-Ring F);

          g divides p & g divides q by A, dpg;

          hence thesis by A, dpg;

        end;

          suppose

           A: p <> ( 0_. F) or q <> ( 0_. F);

          set g = (p gcd q);

          reconsider p1 = p, q1 = q as Element of ( Polynom-Ring F);

          set g1 = (p1 gcd q1);

          reconsider g1 as Element of ( Polynom-Ring F);

          thus thesis by A, dpg;

        end;

      end;

    end

    registration

      let F be Field;

      let p,q be Element of ( Polynom-Ring F);

      cluster (p gcd q) -> p, q -gcd;

      coherence ;

    end

    registration

      let F be Field;

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

      let q be non zero Element of the carrier of ( Polynom-Ring F);

      cluster (p gcd q) -> non zero monic;

      coherence

      proof

        reconsider p1 = p, q1 = q as Element of ( Polynom-Ring F);

        set g1 = (p1 gcd q1);

        set g = (p gcd q);

        reconsider g1 as Element of ( Polynom-Ring F);

         D:

        now

          assume g is zero;

          then g = ( 0_. F) by UPROOTS:def 5;

          then

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

          

           D3: q <> ( 0_. F);

          g1 divides q1 by defGCD;

          then

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

           D4: (g1 * v) = q;

          thus contradiction by D1, D4, D3, POLYNOM3:def 10;

        end;

        hence g is non zero;

        g <> ( 0_. F) by D;

        hence thesis by dpg;

      end;

    end

    registration

      let F be Field;

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

      let q be non zero Element of ( Polynom-Ring F);

      cluster (p gcd q) -> non zero monic;

      coherence

      proof

        set g = (p gcd q);

        reconsider g1 = g as Element of ( Polynom-Ring F);

        q <> ( 0. ( Polynom-Ring F));

        then

         D3: q <> ( 0_. F) by POLYNOM3:def 10;

        now

          assume g is zero;

          then g = ( 0_. F) by UPROOTS:def 5;

          then

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

          g1 divides q by defGCD;

          then

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

           D4: (g1 * v) = q;

          thus contradiction by D1, D4;

        end;

        hence g is non zero;

        thus thesis by D3, dpg;

      end;

    end

    registration

      let F be Field;

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

      cluster (p gcd q) -> zero;

      coherence

      proof

        reconsider g = (p gcd q) as Element of ( Polynom-Ring F);

        p = ( 0_. F) & q = ( 0_. F) by UPROOTS:def 5;

        hence (p gcd q) is zero by dpg;

      end;

    end

    registration

      let F be Field;

      let p,q be zero Element of ( Polynom-Ring F);

      cluster (p gcd q) -> zero;

      coherence

      proof

        reconsider g = (p gcd q) as Element of ( Polynom-Ring F);

        p = ( 0. ( Polynom-Ring F)) & q = ( 0. ( Polynom-Ring F)) by STRUCT_0:def 12;

        then p = ( 0_. F) & q = ( 0_. F) by POLYNOM3:def 10;

        hence (p gcd q) is zero;

      end;

    end

    theorem :: RING_4:50

    for F be Field, p,q be Element of the carrier of ( Polynom-Ring F) holds (p gcd q) divides p & (p gcd q) divides q & for r be Element of the carrier of ( Polynom-Ring F) st r divides p & r divides q holds r divides (p gcd q)

    proof

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

      set g = (p gcd q);

      reconsider g1 = (p gcd q) as Element of ( Polynom-Ring F);

      g1 divides p & g1 divides q by defGCD;

      hence g divides p & g divides q;

      now

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

        reconsider r1 = r as Element of ( Polynom-Ring F);

        assume r divides p & r divides q;

        then r1 divides g1 by defGCD;

        hence r divides g;

      end;

      hence thesis;

    end;

    theorem :: RING_4:51

    for F be Field, p,q be Element of ( Polynom-Ring F) holds (p gcd q) divides p & (p gcd q) divides q & for r be Element of ( Polynom-Ring F) st r divides p & r divides q holds r divides (p gcd q) by defGCD;

    definition

      let F be Field;

      let p,q be Polynomial of F;

      :: RING_4:def12

      func p gcd q -> Polynomial of F means

      : dd: ex a,b be Element of ( Polynom-Ring F) st a = p & b = q & it = (a gcd b);

      existence

      proof

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

        take (a gcd b);

        thus thesis;

      end;

      uniqueness ;

    end

    definition

      let F be Field;

      let p,q be Polynomial of F;

      :: original: gcd

      redefine

      func p gcd q;

      commutativity

      proof

        now

          let p,q be Polynomial of F;

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

          

          thus (p gcd q) = (a gcd b) by dd

          .= (q gcd p) by dd;

        end;

        hence thesis;

      end;

    end

    registration

      let F be Field;

      let p be Polynomial of F;

      let q be non zero Polynomial of F;

      cluster (p gcd q) -> non zero monic;

      coherence

      proof

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

        

         A0: (p gcd q) = (a gcd b) by dd;

        q <> ( 0_. F);

        then q <> ( 0. ( Polynom-Ring F)) by POLYNOM3:def 10;

        then

        reconsider b as non zero Element of ( Polynom-Ring F) by STRUCT_0:def 12;

        thus (p gcd q) is non zero by A0;

        thus thesis by A0;

      end;

    end

    registration

      let F be Field;

      let p,q be zero Polynomial of F;

      cluster (p gcd q) -> zero;

      coherence

      proof

        p = ( 0_. F) & q = ( 0_. F) by UPROOTS:def 5;

        then p = ( 0. ( Polynom-Ring F)) & q = ( 0. ( Polynom-Ring F)) by POLYNOM3:def 10;

        then

        reconsider a = p, b = q as zero Element of ( Polynom-Ring F);

        (p gcd q) = (a gcd b) by dd;

        hence (p gcd q) is zero;

      end;

    end

    theorem :: RING_4:52

    

     G1: for F be Field, p,q be Polynomial of F holds (p gcd q) divides p & (p gcd q) divides q & for r be Polynomial of F st r divides p & r divides q holds r divides (p gcd q)

    proof

      let F be Field, p,q be Polynomial of F;

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

      set g = (a gcd b);

      

       A0: (p gcd q) = g by dd;

      g divides a by defGCD;

      then

      consider c be Element of ( Polynom-Ring F) such that

       A1: (g * c) = a;

      reconsider r = c as Polynomial of F by POLYNOM3:def 10;

      ((p gcd q) *' r) = p by A0, A1, POLYNOM3:def 10;

      hence (p gcd q) divides p by T2;

      g divides b by defGCD;

      then

      consider c be Element of ( Polynom-Ring F) such that

       A1: (g * c) = b;

      reconsider r = c as Polynomial of F by POLYNOM3:def 10;

      ((p gcd q) *' r) = q by A0, A1, POLYNOM3:def 10;

      hence (p gcd q) divides q by T2;

      now

        let r be Polynomial of F;

        assume

         A1: r divides p & r divides q;

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

        consider s be Polynomial of F such that

         A2: (r *' s) = p by A1, T2;

        consider t be Polynomial of F such that

         A3: (r *' t) = q by A1, T2;

        reconsider x = s, y = t as Element of ( Polynom-Ring F) by POLYNOM3:def 10;

        (c * x) = a & (c * y) = b by A2, A3, POLYNOM3:def 10;

        then c divides a & c divides b;

        then c divides (a gcd b) by defGCD;

        hence r divides (p gcd q) by dd;

      end;

      hence thesis;

    end;

    theorem :: RING_4:53

    for F be Field holds for p be Polynomial of F holds for q be non zero Polynomial of F holds for s be monic Polynomial of F holds s = (p gcd q) iff (s divides p & s divides q & for r be Polynomial of F st r divides p & r divides q holds r divides s)

    proof

      let F be Field, p be Polynomial of F;

      let q be non zero Polynomial of F;

      let s be monic Polynomial of F;

      now

        assume

         AS: s divides p & s divides q & for r be Polynomial of F st r divides p & r divides q holds r divides s;

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

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

        

         B: b <> ( 0_. F);

        now

          let d be Element of ( Polynom-Ring F);

          assume

           C: d divides a & d divides b;

          reconsider h = d as Polynomial of F by POLYNOM3:def 10;

          h divides p & h divides q by C;

          then h divides s by AS;

          hence d divides g;

        end;

        then g is a, b -gcd by AS;

        then g = (a gcd b) by dpg, B;

        hence s = (p gcd q) by dd;

      end;

      hence thesis by G1;

    end;