P. 230 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 22901-23000   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	mdegpropd 22901*	Property deduction for polynomial degree. (Contributed by Stefan O'Rear, 28-Mar-2015.) (Proof shortened by AV, 27-Jul-2019.)
|- ( ph -> B = ( Base ` R ) )   &    |- ( ph -> B = ( Base ` S ) )   &    |- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x ( +g ` R ) y ) = ( x ( +g ` S ) y ) )   =>    |- ( ph -> ( I mDeg R ) = ( I mDeg S ) )
Theorem	deg1fvi 22902	Univariate polynomial degree respects protection. (Contributed by Stefan O'Rear, 28-Mar-2015.)
|- ( deg1 ` R ) = ( deg1 ` ( _I ` R ) )
Theorem	deg1propd 22903*	Property deduction for polynomial degree. (Contributed by Stefan O'Rear, 28-Mar-2015.)
|- ( ph -> B = ( Base ` R ) )   &    |- ( ph -> B = ( Base ` S ) )   &    |- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x ( +g ` R ) y ) = ( x ( +g ` S ) y ) )   =>    |- ( ph -> ( deg1 ` R ) = ( deg1 ` S ) )
Theorem	deg1z 22904	Degree of the zero univariate polynomial. (Contributed by Stefan O'Rear, 23-Mar-2015.)
|- D = ( deg1 ` R )   &    |- P = (Poly1 ` R )   &    |- .0. = ( 0g ` P )   =>    |- ( R e. Ring -> ( D ` .0. ) = -oo )
Theorem	deg1nn0cl 22905	Degree of a nonzero univariate polynomial. (Contributed by Stefan O'Rear, 23-Mar-2015.) (Revised by Mario Carneiro, 7-Oct-2015.)
|- D = ( deg1 ` R )   &    |- P = (Poly1 ` R )   &    |- .0. = ( 0g ` P )   &    |- B = ( Base ` P )   =>    |- ( ( R e. Ring /\ F e. B /\ F =/= .0. ) -> ( D ` F ) e. NN0 )
Theorem	deg1n0ima 22906	Degree image of a set of polynomials which does not include zero. (Contributed by Stefan O'Rear, 28-Mar-2015.)
|- D = ( deg1 ` R )   &    |- P = (Poly1 ` R )   &    |- .0. = ( 0g ` P )   &    |- B = ( Base ` P )   =>    |- ( R e. Ring -> ( D " ( B \ { .0. } ) ) C_ NN0 )
Theorem	deg1nn0clb 22907	A polynomial is nonzero iff it has definite degree. (Contributed by Stefan O'Rear, 23-Mar-2015.)
|- D = ( deg1 ` R )   &    |- P = (Poly1 ` R )   &    |- .0. = ( 0g ` P )   &    |- B = ( Base ` P )   =>    |- ( ( R e. Ring /\ F e. B ) -> ( F =/= .0. <-> ( D ` F ) e. NN0 ) )
Theorem	deg1lt0 22908	A polynomial is zero iff it has negative degree. (Contributed by Stefan O'Rear, 1-Apr-2015.)
|- D = ( deg1 ` R )   &    |- P = (Poly1 ` R )   &    |- .0. = ( 0g ` P )   &    |- B = ( Base ` P )   =>    |- ( ( R e. Ring /\ F e. B ) -> ( ( D ` F ) < 0 <-> F = .0. ) )
Theorem	deg1ldg 22909	A nonzero univariate polynomial always has a nonzero leading coefficient. (Contributed by Stefan O'Rear, 23-Mar-2015.)
|- D = ( deg1 ` R )   &    |- P = (Poly1 ` R )   &    |- .0. = ( 0g ` P )   &    |- B = ( Base ` P )   &    |- Y = ( 0g ` R )   &    |- A = (coe1 ` F )   =>    |- ( ( R e. Ring /\ F e. B /\ F =/= .0. ) -> ( A ` ( D ` F ) ) =/= Y )
Theorem	deg1ldgn 22910	An index at which a polynomial is zero, cannot be its degree. (Contributed by Stefan O'Rear, 23-Mar-2015.)
|- D = ( deg1 ` R )   &    |- P = (Poly1 ` R )   &    |- .0. = ( 0g ` P )   &    |- B = ( Base ` P )   &    |- Y = ( 0g ` R )   &    |- A = (coe1 ` F )   &    |- ( ph -> R e. Ring )   &    |- ( ph -> F e. B )   &    |- ( ph -> X e. NN0 )   &    |- ( ph -> ( A ` X ) = Y )   =>    |- ( ph -> ( D ` F ) =/= X )
Theorem	deg1ldgdomn 22911	A nonzero univariate polynomial over a domain always has a non-zero-divisor leading coefficient. (Contributed by Stefan O'Rear, 28-Mar-2015.)
|- D = ( deg1 ` R )   &    |- P = (Poly1 ` R )   &    |- .0. = ( 0g ` P )   &    |- B = ( Base ` P )   &    |- E = (RLReg ` R )   &    |- A = (coe1 ` F )   =>    |- ( ( R e. Domn /\ F e. B /\ F =/= .0. ) -> ( A ` ( D ` F ) ) e. E )
Theorem	deg1leb 22912*	Property of being of limited degree. (Contributed by Stefan O'Rear, 23-Mar-2015.)
|- D = ( deg1 ` R )   &    |- P = (Poly1 ` R )   &    |- B = ( Base ` P )   &    |- .0. = ( 0g ` R )   &    |- A = (coe1 ` F )   =>    |- ( ( F e. B /\ G e. RR* ) -> ( ( D ` F ) <_ G <-> A. x e. NN0 ( G < x -> ( A ` x ) = .0. ) ) )
Theorem	deg1val 22913	Value of the univariate degree as a supremum. (Contributed by Stefan O'Rear, 29-Mar-2015.) (Revised by AV, 25-Jul-2019.)
|- D = ( deg1 ` R )   &    |- P = (Poly1 ` R )   &    |- B = ( Base ` P )   &    |- .0. = ( 0g ` R )   &    |- A = (coe1 ` F )   =>    |- ( F e. B -> ( D ` F ) = sup ( ( A supp .0. ) , RR* , < ) )
Theorem	deg1lt 22914	If the degree of a univariate polynomial is less than some index, then that coefficient must be zero. (Contributed by Stefan O'Rear, 23-Mar-2015.)
|- D = ( deg1 ` R )   &    |- P = (Poly1 ` R )   &    |- B = ( Base ` P )   &    |- .0. = ( 0g ` R )   &    |- A = (coe1 ` F )   =>    |- ( ( F e. B /\ G e. NN0 /\ ( D ` F ) < G ) -> ( A ` G ) = .0. )
Theorem	deg1ge 22915	Conversely, a nonzero coefficient sets a lower bound on the degree. (Contributed by Stefan O'Rear, 23-Mar-2015.)
|- D = ( deg1 ` R )   &    |- P = (Poly1 ` R )   &    |- B = ( Base ` P )   &    |- .0. = ( 0g ` R )   &    |- A = (coe1 ` F )   =>    |- ( ( F e. B /\ G e. NN0 /\ ( A ` G ) =/= .0. ) -> G <_ ( D ` F ) )
Theorem	coe1mul3 22916	The coefficient vector of multiplication in the univariate polynomial ring, at indices high enough that at most one component can be active in the sum. (Contributed by Stefan O'Rear, 25-Mar-2015.)
|- Y = (Poly1 ` R )   &    |- .xb = ( .r ` Y )   &    |- .x. = ( .r ` R )   &    |- B = ( Base ` Y )   &    |- D = ( deg1 ` R )   &    |- ( ph -> R e. Ring )   &    |- ( ph -> F e. B )   &    |- ( ph -> I e. NN0 )   &    |- ( ph -> ( D ` F ) <_ I )   &    |- ( ph -> G e. B )   &    |- ( ph -> J e. NN0 )   &    |- ( ph -> ( D ` G ) <_ J )   =>    |- ( ph -> ( (coe1 ` ( F .xb G ) ) ` ( I + J ) ) = ( ( (coe1 ` F ) ` I ) .x. ( (coe1 ` G ) ` J ) ) )
Theorem	coe1mul4 22917	Value of the "leading" coefficient of a product of two nonzero polynomials. This will fail to actually be the leading coefficient only if it is zero (requiring the basic ring to contain zero divisors). (Contributed by Stefan O'Rear, 25-Mar-2015.)
|- Y = (Poly1 ` R )   &    |- .xb = ( .r ` Y )   &    |- .x. = ( .r ` R )   &    |- B = ( Base ` Y )   &    |- D = ( deg1 ` R )   &    |- .0. = ( 0g ` Y )   &    |- ( ph -> R e. Ring )   &    |- ( ph -> F e. B )   &    |- ( ph -> F =/= .0. )   &    |- ( ph -> G e. B )   &    |- ( ph -> G =/= .0. )   =>    |- ( ph -> ( (coe1 ` ( F .xb G ) ) ` ( ( D ` F ) + ( D ` G ) ) ) = ( ( (coe1 ` F ) ` ( D ` F ) ) .x. ( (coe1 ` G ) ` ( D ` G ) ) ) )
Theorem	deg1addle 22918	The degree of a sum is at most the maximum of the degrees of the factors. (Contributed by Stefan O'Rear, 26-Mar-2015.)
|- Y = (Poly1 ` R )   &    |- D = ( deg1 ` R )   &    |- ( ph -> R e. Ring )   &    |- B = ( Base ` Y )   &    |- .+ = ( +g ` Y )   &    |- ( ph -> F e. B )   &    |- ( ph -> G e. B )   =>    |- ( ph -> ( D ` ( F .+ G ) ) <_ if ( ( D ` F ) <_ ( D ` G ) , ( D ` G ) , ( D ` F ) ) )
Theorem	deg1addle2 22919	If both factors have degree bounded by L, then the sum of the polynomials also has degree bounded by L. (Contributed by Stefan O'Rear, 1-Apr-2015.)
|- Y = (Poly1 ` R )   &    |- D = ( deg1 ` R )   &    |- ( ph -> R e. Ring )   &    |- B = ( Base ` Y )   &    |- .+ = ( +g ` Y )   &    |- ( ph -> F e. B )   &    |- ( ph -> G e. B )   &    |- ( ph -> L e. RR* )   &    |- ( ph -> ( D ` F ) <_ L )   &    |- ( ph -> ( D ` G ) <_ L )   =>    |- ( ph -> ( D ` ( F .+ G ) ) <_ L )
Theorem	deg1add 22920	Exact degree of a sum of two polynomials of unequal degree. (Contributed by Stefan O'Rear, 28-Mar-2015.)
|- Y = (Poly1 ` R )   &    |- D = ( deg1 ` R )   &    |- ( ph -> R e. Ring )   &    |- B = ( Base ` Y )   &    |- .+ = ( +g ` Y )   &    |- ( ph -> F e. B )   &    |- ( ph -> G e. B )   &    |- ( ph -> ( D ` G ) < ( D ` F ) )   =>    |- ( ph -> ( D ` ( F .+ G ) ) = ( D ` F ) )
Theorem	deg1vscale 22921	The degree of a scalar times a polynomial is at most the degree of the original polynomial. (Contributed by Stefan O'Rear, 26-Mar-2015.)
|- Y = (Poly1 ` R )   &    |- D = ( deg1 ` R )   &    |- ( ph -> R e. Ring )   &    |- B = ( Base ` Y )   &    |- K = ( Base ` R )   &    |- .x. = ( .s ` Y )   &    |- ( ph -> F e. K )   &    |- ( ph -> G e. B )   =>    |- ( ph -> ( D ` ( F .x. G ) ) <_ ( D ` G ) )
Theorem	deg1vsca 22922	The degree of a scalar times a polynomial is exactly the degree of the original polynomial when the scalar is not a zero divisor. (Contributed by Stefan O'Rear, 28-Mar-2015.)
|- Y = (Poly1 ` R )   &    |- D = ( deg1 ` R )   &    |- ( ph -> R e. Ring )   &    |- B = ( Base ` Y )   &    |- E = (RLReg ` R )   &    |- .x. = ( .s ` Y )   &    |- ( ph -> F e. E )   &    |- ( ph -> G e. B )   =>    |- ( ph -> ( D ` ( F .x. G ) ) = ( D ` G ) )
Theorem	deg1invg 22923	The degree of the negated polynomial is the same as the original. (Contributed by Stefan O'Rear, 28-Mar-2015.)
|- Y = (Poly1 ` R )   &    |- D = ( deg1 ` R )   &    |- ( ph -> R e. Ring )   &    |- B = ( Base ` Y )   &    |- N = ( invg ` Y )   &    |- ( ph -> F e. B )   =>    |- ( ph -> ( D ` ( N ` F ) ) = ( D ` F ) )
Theorem	deg1suble 22924	The degree of a difference of polynomials is bounded by the maximum of degrees. (Contributed by Stefan O'Rear, 26-Mar-2015.)
|- Y = (Poly1 ` R )   &    |- D = ( deg1 ` R )   &    |- ( ph -> R e. Ring )   &    |- B = ( Base ` Y )   &    |- .- = ( -g ` Y )   &    |- ( ph -> F e. B )   &    |- ( ph -> G e. B )   =>    |- ( ph -> ( D ` ( F .- G ) ) <_ if ( ( D ` F ) <_ ( D ` G ) , ( D ` G ) , ( D ` F ) ) )
Theorem	deg1sub 22925	Exact degree of a difference of two polynomials of unequal degree. (Contributed by Stefan O'Rear, 28-Mar-2015.)
|- Y = (Poly1 ` R )   &    |- D = ( deg1 ` R )   &    |- ( ph -> R e. Ring )   &    |- B = ( Base ` Y )   &    |- .- = ( -g ` Y )   &    |- ( ph -> F e. B )   &    |- ( ph -> G e. B )   &    |- ( ph -> ( D ` G ) < ( D ` F ) )   =>    |- ( ph -> ( D ` ( F .- G ) ) = ( D ` F ) )
Theorem	deg1mulle2 22926	Produce a bound on the product of two univariate polynomials given bounds on the factors. (Contributed by Stefan O'Rear, 26-Mar-2015.)
|- Y = (Poly1 ` R )   &    |- D = ( deg1 ` R )   &    |- ( ph -> R e. Ring )   &    |- B = ( Base ` Y )   &    |- .x. = ( .r ` Y )   &    |- ( ph -> F e. B )   &    |- ( ph -> G e. B )   &    |- ( ph -> J e. NN0 )   &    |- ( ph -> K e. NN0 )   &    |- ( ph -> ( D ` F ) <_ J )   &    |- ( ph -> ( D ` G ) <_ K )   =>    |- ( ph -> ( D ` ( F .x. G ) ) <_ ( J + K ) )
Theorem	deg1sublt 22927	Subtraction of two polynomials limited to the same degree with the same leading coefficient gives a polynomial with a smaller degree. (Contributed by Stefan O'Rear, 26-Mar-2015.)
|- D = ( deg1 ` R )   &    |- P = (Poly1 ` R )   &    |- B = ( Base ` P )   &    |- .- = ( -g ` P )   &    |- ( ph -> L e. NN0 )   &    |- ( ph -> R e. Ring )   &    |- ( ph -> F e. B )   &    |- ( ph -> ( D ` F ) <_ L )   &    |- ( ph -> G e. B )   &    |- ( ph -> ( D ` G ) <_ L )   &    |- A = (coe1 ` F )   &    |- C = (coe1 ` G )   &    |- ( ph -> ( (coe1 ` F ) ` L ) = ( (coe1 ` G ) ` L ) )   =>    |- ( ph -> ( D ` ( F .- G ) ) < L )
Theorem	deg1le0 22928	A polynomial has nonpositive degree iff it is a constant. (Contributed by Stefan O'Rear, 29-Mar-2015.)
|- D = ( deg1 ` R )   &    |- P = (Poly1 ` R )   &    |- B = ( Base ` P )   &    |- A = (algSc ` P )   =>    |- ( ( R e. Ring /\ F e. B ) -> ( ( D ` F ) <_ 0 <-> F = ( A ` ( (coe1 ` F ) ` 0 ) ) ) )
Theorem	deg1sclle 22929	A scalar polynomial has nonpositive degree. (Contributed by Stefan O'Rear, 29-Mar-2015.)
|- D = ( deg1 ` R )   &    |- P = (Poly1 ` R )   &    |- K = ( Base ` R )   &    |- A = (algSc ` P )   =>    |- ( ( R e. Ring /\ F e. K ) -> ( D ` ( A ` F ) ) <_ 0 )
Theorem	deg1scl 22930	A nonzero scalar polynomial has zero degree. (Contributed by Stefan O'Rear, 29-Mar-2015.)
|- D = ( deg1 ` R )   &    |- P = (Poly1 ` R )   &    |- K = ( Base ` R )   &    |- A = (algSc ` P )   &    |- .0. = ( 0g ` R )   =>    |- ( ( R e. Ring /\ F e. K /\ F =/= .0. ) -> ( D ` ( A ` F ) ) = 0 )
Theorem	deg1mul2 22931	Degree of multiplication of two nonzero polynomials when the first leads with a non-zero-divisor coefficient. (Contributed by Stefan O'Rear, 26-Mar-2015.)
|- D = ( deg1 ` R )   &    |- P = (Poly1 ` R )   &    |- E = (RLReg ` R )   &    |- B = ( Base ` P )   &    |- .x. = ( .r ` P )   &    |- .0. = ( 0g ` P )   &    |- ( ph -> R e. Ring )   &    |- ( ph -> F e. B )   &    |- ( ph -> F =/= .0. )   &    |- ( ph -> ( (coe1 ` F ) ` ( D ` F ) ) e. E )   &    |- ( ph -> G e. B )   &    |- ( ph -> G =/= .0. )   =>    |- ( ph -> ( D ` ( F .x. G ) ) = ( ( D ` F ) + ( D ` G ) ) )
Theorem	deg1mul3 22932	Degree of multiplication of a polynomial on the left by a non-zero-dividing scalar. (Contributed by Stefan O'Rear, 29-Mar-2015.) (Proof shortened by AV, 25-Jul-2019.)
|- D = ( deg1 ` R )   &    |- P = (Poly1 ` R )   &    |- E = (RLReg ` R )   &    |- B = ( Base ` P )   &    |- .x. = ( .r ` P )   &    |- A = (algSc ` P )   =>    |- ( ( R e. Ring /\ F e. E /\ G e. B ) -> ( D ` ( ( A ` F ) .x. G ) ) = ( D ` G ) )
Theorem	deg1mul3le 22933	Degree of multiplication of a polynomial on the left by a scalar. (Contributed by Stefan O'Rear, 1-Apr-2015.)
|- D = ( deg1 ` R )   &    |- P = (Poly1 ` R )   &    |- K = ( Base ` R )   &    |- B = ( Base ` P )   &    |- .x. = ( .r ` P )   &    |- A = (algSc ` P )   =>    |- ( ( R e. Ring /\ F e. K /\ G e. B ) -> ( D ` ( ( A ` F ) .x. G ) ) <_ ( D ` G ) )
Theorem	deg1tmle 22934	Limiting degree of a polynomial term. (Contributed by Stefan O'Rear, 27-Mar-2015.)
|- D = ( deg1 ` R )   &    |- K = ( Base ` R )   &    |- P = (Poly1 ` R )   &    |- X = (var1 ` R )   &    |- .x. = ( .s ` P )   &    |- N = (mulGrp ` P )   &    |- .^ = (.g ` N )   =>    |- ( ( R e. Ring /\ C e. K /\ F e. NN0 ) -> ( D ` ( C .x. ( F .^ X ) ) ) <_ F )
Theorem	deg1tm 22935	Exact degree of a polynomial term. (Contributed by Stefan O'Rear, 27-Mar-2015.)
|- D = ( deg1 ` R )   &    |- K = ( Base ` R )   &    |- P = (Poly1 ` R )   &    |- X = (var1 ` R )   &    |- .x. = ( .s ` P )   &    |- N = (mulGrp ` P )   &    |- .^ = (.g ` N )   &    |- .0. = ( 0g ` R )   =>    |- ( ( R e. Ring /\ ( C e. K /\ C =/= .0. ) /\ F e. NN0 ) -> ( D ` ( C .x. ( F .^ X ) ) ) = F )
Theorem	deg1pwle 22936	Limiting degree of a variable power. (Contributed by Stefan O'Rear, 1-Apr-2015.)
|- D = ( deg1 ` R )   &    |- P = (Poly1 ` R )   &    |- X = (var1 ` R )   &    |- N = (mulGrp ` P )   &    |- .^ = (.g ` N )   =>    |- ( ( R e. Ring /\ F e. NN0 ) -> ( D ` ( F .^ X ) ) <_ F )
Theorem	deg1pw 22937	Exact degree of a variable power over a nontrivial ring. (Contributed by Stefan O'Rear, 1-Apr-2015.)
|- D = ( deg1 ` R )   &    |- P = (Poly1 ` R )   &    |- X = (var1 ` R )   &    |- N = (mulGrp ` P )   &    |- .^ = (.g ` N )   =>    |- ( ( R e. NzRing /\ F e. NN0 ) -> ( D ` ( F .^ X ) ) = F )
Theorem	ply1nz 22938	Univariate polynomials over a nonzero ring are a nonzero ring. (Contributed by Stefan O'Rear, 29-Mar-2015.)
|- P = (Poly1 ` R )   =>    |- ( R e. NzRing -> P e. NzRing )
Theorem	ply1nzb 22939	Univariate polynomials are nonzero iff the base is nonzero. Or in contraposition, the univariate polynomials over the zero ring are also zero. (Contributed by Mario Carneiro, 13-Jun-2015.)
|- P = (Poly1 ` R )   =>    |- ( R e. Ring -> ( R e. NzRing <-> P e. NzRing ) )
Theorem	ply1domn 22940	Corollary of deg1mul2 22931: the univariate polynomials over a domain are a domain. This is true for multivariate but with a much more complicated proof. (Contributed by Stefan O'Rear, 28-Mar-2015.)
|- P = (Poly1 ` R )   =>    |- ( R e. Domn -> P e. Domn )
Theorem	ply1idom 22941	The ring of univariate polynomials over an integral domain is itself an integral domain. (Contributed by Stefan O'Rear, 29-Mar-2015.)
|- P = (Poly1 ` R )   =>    |- ( R e. IDomn -> P e. IDomn )
14.1.2  The division algorithm for univariate polynomials
Syntax	cmn1 22942	Monic polynomials.
class Monic1p
Syntax	cuc1p 22943	Unitic polynomials.
class Unic1p
Syntax	cq1p 22944	Univariate polynomial quotient.
class quot1p
Syntax	cr1p 22945	Univariate polynomial remainder.
class rem1p
Syntax	cig1p 22946	Univariate polynomial ideal generator.
class idlGen1p
Definition	df-mon1 22947*	Define the set of monic univariate polynomials. (Contributed by Stefan O'Rear, 28-Mar-2015.)
|- Monic1p = ( r e. _V |-> { f e. ( Base ` (Poly1 ` r ) ) | ( f =/= ( 0g ` (Poly1 ` r ) ) /\ ( (coe1 ` f ) ` ( ( deg1 ` r ) ` f ) ) = ( 1r ` r ) ) } )
Definition	df-uc1p 22948*	Define the set of unitic univariate polynomials, as the polynomials with an invertible leading coefficient. This is not a standard concept but is useful to us as the set of polynomials which can be used as the divisor in the polynomial division theorem ply1divalg 22954. (Contributed by Stefan O'Rear, 28-Mar-2015.)
|- Unic1p = ( r e. _V |-> { f e. ( Base ` (Poly1 ` r ) ) | ( f =/= ( 0g ` (Poly1 ` r ) ) /\ ( (coe1 ` f ) ` ( ( deg1 ` r ) ` f ) ) e. (Unit ` r ) ) } )
Definition	df-q1p 22949*	Define the quotient of two univariate polynomials, which is guaranteed to exist and be unique by ply1divalg 22954. We actually use the reversed version for better harmony with our divisibility df-dvdsr 17795. (Contributed by Stefan O'Rear, 28-Mar-2015.)
|- quot1p = ( r e. _V |-> [_ (Poly1 ` r ) / p ]_ [_ ( Base ` p ) / b ]_ ( f e. b , g e. b |-> ( iota_ q e. b ( ( deg1 ` r ) ` ( f ( -g ` p ) ( q ( .r ` p ) g ) ) ) < ( ( deg1 ` r ) ` g ) ) ) )
Definition	df-r1p 22950*	Define the remainder after dividing two univariate polynomials. (Contributed by Stefan O'Rear, 28-Mar-2015.)
|- rem1p = ( r e. _V |-> [_ ( Base ` (Poly1 ` r ) ) / b ]_ ( f e. b , g e. b |-> ( f ( -g ` (Poly1 ` r ) ) ( ( f (quot1p ` r ) g ) ( .r ` (Poly1 ` r ) ) g ) ) ) )
Definition	df-ig1p 22951*	Define a choice function for generators of ideals over a division ring; this is the unique monic polynomial of minimal degree in the ideal. (Contributed by Stefan O'Rear, 29-Mar-2015.)
|- idlGen1p = ( r e. _V |-> ( i e. (LIdeal ` (Poly1 ` r ) ) |-> if ( i = { ( 0g ` (Poly1 ` r ) ) } , ( 0g ` (Poly1 ` r ) ) , ( iota_ g e. ( i i^i (Monic1p ` r ) ) ( ( deg1 ` r ) ` g ) = sup ( ( ( deg1 ` r ) " ( i \ { ( 0g ` (Poly1 ` r ) ) } ) ) , RR , `' < ) ) ) ) )
Theorem	ply1divmo 22952*	Uniqueness of a quotient in a polynomial division. For polynomials F , G such that G =/= 0 and the leading coefficient of G is not a zero divisor, there is at most one polynomial q which satisfies F = ( G x. q ) + r where the degree of r is less than the degree of G. (Contributed by Stefan O'Rear, 26-Mar-2015.) (Revised by NM, 17-Jun-2017.)
|- P = (Poly1 ` R )   &    |- D = ( deg1 ` R )   &    |- B = ( Base ` P )   &    |- .- = ( -g ` P )   &    |- .0. = ( 0g ` P )   &    |- .xb = ( .r ` P )   &    |- ( ph -> R e. Ring )   &    |- ( ph -> F e. B )   &    |- ( ph -> G e. B )   &    |- ( ph -> G =/= .0. )   &    |- ( ph -> ( (coe1 ` G ) ` ( D ` G ) ) e. E )   &    |- E = (RLReg ` R )   =>    |- ( ph -> E* q e. B ( D ` ( F .- ( G .xb q ) ) ) < ( D ` G ) )
Theorem	ply1divex 22953*	Lemma for ply1divalg 22954: existence part. (Contributed by Stefan O'Rear, 27-Mar-2015.)
|- P = (Poly1 ` R )   &    |- D = ( deg1 ` R )   &    |- B = ( Base ` P )   &    |- .- = ( -g ` P )   &    |- .0. = ( 0g ` P )   &    |- .xb = ( .r ` P )   &    |- ( ph -> R e. Ring )   &    |- ( ph -> F e. B )   &    |- ( ph -> G e. B )   &    |- ( ph -> G =/= .0. )   &    |- .1. = ( 1r ` R )   &    |- K = ( Base ` R )   &    |- .x. = ( .r ` R )   &    |- ( ph -> I e. K )   &    |- ( ph -> ( ( (coe1 ` G ) ` ( D ` G ) ) .x. I ) = .1. )   =>    |- ( ph -> E. q e. B ( D ` ( F .- ( G .xb q ) ) ) < ( D ` G ) )
Theorem	ply1divalg 22954*	The division algorithm for univariate polynomials over a ring. For polynomials F , G such that G =/= 0 and the leading coefficient of G is a unit, there are unique polynomials q and r = F - ( G x. q ) such that the degree of r is less than the degree of G. (Contributed by Stefan O'Rear, 27-Mar-2015.)
|- P = (Poly1 ` R )   &    |- D = ( deg1 ` R )   &    |- B = ( Base ` P )   &    |- .- = ( -g ` P )   &    |- .0. = ( 0g ` P )   &    |- .xb = ( .r ` P )   &    |- ( ph -> R e. Ring )   &    |- ( ph -> F e. B )   &    |- ( ph -> G e. B )   &    |- ( ph -> G =/= .0. )   &    |- ( ph -> ( (coe1 ` G ) ` ( D ` G ) ) e. U )   &    |- U = (Unit ` R )   =>    |- ( ph -> E! q e. B ( D ` ( F .- ( G .xb q ) ) ) < ( D ` G ) )
Theorem	ply1divalg2 22955*	Reverse the order of multiplication in ply1divalg 22954 via the opposite ring. (Contributed by Stefan O'Rear, 28-Mar-2015.)
|- P = (Poly1 ` R )   &    |- D = ( deg1 ` R )   &    |- B = ( Base ` P )   &    |- .- = ( -g ` P )   &    |- .0. = ( 0g ` P )   &    |- .xb = ( .r ` P )   &    |- ( ph -> R e. Ring )   &    |- ( ph -> F e. B )   &    |- ( ph -> G e. B )   &    |- ( ph -> G =/= .0. )   &    |- ( ph -> ( (coe1 ` G ) ` ( D ` G ) ) e. U )   &    |- U = (Unit ` R )   =>    |- ( ph -> E! q e. B ( D ` ( F .- ( q .xb G ) ) ) < ( D ` G ) )
Theorem	uc1pval 22956*	Value of the set of unitic polynomials. (Contributed by Stefan O'Rear, 28-Mar-2015.)
|- P = (Poly1 ` R )   &    |- B = ( Base ` P )   &    |- .0. = ( 0g ` P )   &    |- D = ( deg1 ` R )   &    |- C = (Unic1p ` R )   &    |- U = (Unit ` R )   =>    |- C = { f e. B | ( f =/= .0. /\ ( (coe1 ` f ) ` ( D ` f ) ) e. U ) }
Theorem	isuc1p 22957	Being a unitic polynomial. (Contributed by Stefan O'Rear, 28-Mar-2015.)
|- P = (Poly1 ` R )   &    |- B = ( Base ` P )   &    |- .0. = ( 0g ` P )   &    |- D = ( deg1 ` R )   &    |- C = (Unic1p ` R )   &    |- U = (Unit ` R )   =>    |- ( F e. C <-> ( F e. B /\ F =/= .0. /\ ( (coe1 ` F ) ` ( D ` F ) ) e. U ) )
Theorem	mon1pval 22958*	Value of the set of monic polynomials. (Contributed by Stefan O'Rear, 28-Mar-2015.)
|- P = (Poly1 ` R )   &    |- B = ( Base ` P )   &    |- .0. = ( 0g ` P )   &    |- D = ( deg1 ` R )   &    |- M = (Monic1p ` R )   &    |- .1. = ( 1r ` R )   =>    |- M = { f e. B | ( f =/= .0. /\ ( (coe1 ` f ) ` ( D ` f ) ) = .1. ) }
Theorem	ismon1p 22959	Being a monic polynomial. (Contributed by Stefan O'Rear, 28-Mar-2015.)
|- P = (Poly1 ` R )   &    |- B = ( Base ` P )   &    |- .0. = ( 0g ` P )   &    |- D = ( deg1 ` R )   &    |- M = (Monic1p ` R )   &    |- .1. = ( 1r ` R )   =>    |- ( F e. M <-> ( F e. B /\ F =/= .0. /\ ( (coe1 ` F ) ` ( D ` F ) ) = .1. ) )
Theorem	uc1pcl 22960	Unitic polynomials are polynomials. (Contributed by Stefan O'Rear, 28-Mar-2015.)
|- P = (Poly1 ` R )   &    |- B = ( Base ` P )   &    |- C = (Unic1p ` R )   =>    |- ( F e. C -> F e. B )
Theorem	mon1pcl 22961	Monic polynomials are polynomials. (Contributed by Stefan O'Rear, 28-Mar-2015.)
|- P = (Poly1 ` R )   &    |- B = ( Base ` P )   &    |- M = (Monic1p ` R )   =>    |- ( F e. M -> F e. B )
Theorem	uc1pn0 22962	Unitic polynomials are not zero. (Contributed by Stefan O'Rear, 28-Mar-2015.)
|- P = (Poly1 ` R )   &    |- .0. = ( 0g ` P )   &    |- C = (Unic1p ` R )   =>    |- ( F e. C -> F =/= .0. )
Theorem	mon1pn0 22963	Monic polynomials are not zero. (Contributed by Stefan O'Rear, 28-Mar-2015.)
|- P = (Poly1 ` R )   &    |- .0. = ( 0g ` P )   &    |- M = (Monic1p ` R )   =>    |- ( F e. M -> F =/= .0. )
Theorem	uc1pdeg 22964	Unitic polynomials have nonnegative degrees. (Contributed by Stefan O'Rear, 28-Mar-2015.)
|- D = ( deg1 ` R )   &    |- C = (Unic1p ` R )   =>    |- ( ( R e. Ring /\ F e. C ) -> ( D ` F ) e. NN0 )
Theorem	uc1pldg 22965	Unitic polynomials have unit leading coefficients. (Contributed by Stefan O'Rear, 28-Mar-2015.)
|- D = ( deg1 ` R )   &    |- U = (Unit ` R )   &    |- C = (Unic1p ` R )   =>    |- ( F e. C -> ( (coe1 ` F ) ` ( D ` F ) ) e. U )
Theorem	mon1pldg 22966	Unitic polynomials have one leading coefficients. (Contributed by Stefan O'Rear, 28-Mar-2015.)
|- D = ( deg1 ` R )   &    |- .1. = ( 1r ` R )   &    |- M = (Monic1p ` R )   =>    |- ( F e. M -> ( (coe1 ` F ) ` ( D ` F ) ) = .1. )
Theorem	mon1puc1p 22967	Monic polynomials are unitic. (Contributed by Stefan O'Rear, 28-Mar-2015.)
|- C = (Unic1p ` R )   &    |- M = (Monic1p ` R )   =>    |- ( ( R e. Ring /\ X e. M ) -> X e. C )
Theorem	uc1pmon1p 22968	Make a unitic polynomial monic by multiplying a factor to normalize the leading coefficient. (Contributed by Stefan O'Rear, 29-Mar-2015.)
|- C = (Unic1p ` R )   &    |- M = (Monic1p ` R )   &    |- P = (Poly1 ` R )   &    |- .x. = ( .r ` P )   &    |- A = (algSc ` P )   &    |- D = ( deg1 ` R )   &    |- I = ( invr ` R )   =>    |- ( ( R e. Ring /\ X e. C ) -> ( ( A ` ( I ` ( (coe1 ` X ) ` ( D ` X ) ) ) ) .x. X ) e. M )
Theorem	deg1submon1p 22969	The difference of two monic polynomials of the same degree is a polynomial of lesser degree. (Contributed by Stefan O'Rear, 28-Mar-2015.)
|- D = ( deg1 ` R )   &    |- O = (Monic1p ` R )   &    |- P = (Poly1 ` R )   &    |- .- = ( -g ` P )   &    |- ( ph -> R e. Ring )   &    |- ( ph -> F e. O )   &    |- ( ph -> ( D ` F ) = X )   &    |- ( ph -> G e. O )   &    |- ( ph -> ( D ` G ) = X )   =>    |- ( ph -> ( D ` ( F .- G ) ) < X )
Theorem	q1pval 22970*	Value of the univariate polynomial quotient function. (Contributed by Stefan O'Rear, 28-Mar-2015.)
|- Q = (quot1p ` R )   &    |- P = (Poly1 ` R )   &    |- B = ( Base ` P )   &    |- D = ( deg1 ` R )   &    |- .- = ( -g ` P )   &    |- .x. = ( .r ` P )   =>    |- ( ( F e. B /\ G e. B ) -> ( F Q G ) = ( iota_ q e. B ( D ` ( F .- ( q .x. G ) ) ) < ( D ` G ) ) )
Theorem	q1peqb 22971	Characterizing property of the polynomial quotient. (Contributed by Stefan O'Rear, 28-Mar-2015.)
|- Q = (quot1p ` R )   &    |- P = (Poly1 ` R )   &    |- B = ( Base ` P )   &    |- D = ( deg1 ` R )   &    |- .- = ( -g ` P )   &    |- .x. = ( .r ` P )   &    |- C = (Unic1p ` R )   =>    |- ( ( R e. Ring /\ F e. B /\ G e. C ) -> ( ( X e. B /\ ( D ` ( F .- ( X .x. G ) ) ) < ( D ` G ) ) <-> ( F Q G ) = X ) )
Theorem	q1pcl 22972	Closure of the quotient by a unitic polynomial. (Contributed by Stefan O'Rear, 28-Mar-2015.)
|- Q = (quot1p ` R )   &    |- P = (Poly1 ` R )   &    |- B = ( Base ` P )   &    |- C = (Unic1p ` R )   =>    |- ( ( R e. Ring /\ F e. B /\ G e. C ) -> ( F Q G ) e. B )
Theorem	r1pval 22973	Value of the polynomial remainder function. (Contributed by Stefan O'Rear, 28-Mar-2015.)
|- E = (rem1p ` R )   &    |- P = (Poly1 ` R )   &    |- B = ( Base ` P )   &    |- Q = (quot1p ` R )   &    |- .x. = ( .r ` P )   &    |- .- = ( -g ` P )   =>    |- ( ( F e. B /\ G e. B ) -> ( F E G ) = ( F .- ( ( F Q G ) .x. G ) ) )
Theorem	r1pcl 22974	Closure of remainder following division by a unitic polynomial. (Contributed by Stefan O'Rear, 28-Mar-2015.)
|- E = (rem1p ` R )   &    |- P = (Poly1 ` R )   &    |- B = ( Base ` P )   &    |- C = (Unic1p ` R )   =>    |- ( ( R e. Ring /\ F e. B /\ G e. C ) -> ( F E G ) e. B )
Theorem	r1pdeglt 22975	The remainder has a degree smaller than the divisor. (Contributed by Stefan O'Rear, 28-Mar-2015.)
|- E = (rem1p ` R )   &    |- P = (Poly1 ` R )   &    |- B = ( Base ` P )   &    |- C = (Unic1p ` R )   &    |- D = ( deg1 ` R )   =>    |- ( ( R e. Ring /\ F e. B /\ G e. C ) -> ( D ` ( F E G ) ) < ( D ` G ) )
Theorem	r1pid 22976	Express the original polynomial F as F = ( q x. G ) + r using the quotient and remainder functions for q and r. (Contributed by Mario Carneiro, 5-Jun-2015.)
|- P = (Poly1 ` R )   &    |- B = ( Base ` P )   &    |- C = (Unic1p ` R )   &    |- Q = (quot1p ` R )   &    |- E = (rem1p ` R )   &    |- .x. = ( .r ` P )   &    |- .+ = ( +g ` P )   =>    |- ( ( R e. Ring /\ F e. B /\ G e. C ) -> F = ( ( ( F Q G ) .x. G ) .+ ( F E G ) ) )
Theorem	dvdsq1p 22977	Divisibility in a polynomial ring is witnessed by the quotient. (Contributed by Stefan O'Rear, 28-Mar-2015.)
|- P = (Poly1 ` R )   &    |- .|| = ( ||r ` P )   &    |- B = ( Base ` P )   &    |- C = (Unic1p ` R )   &    |- .x. = ( .r ` P )   &    |- Q = (quot1p ` R )   =>    |- ( ( R e. Ring /\ F e. B /\ G e. C ) -> ( G .|| F <-> F = ( ( F Q G ) .x. G ) ) )
Theorem	dvdsr1p 22978	Divisibility in a polynomial ring in terms of the remainder. (Contributed by Stefan O'Rear, 28-Mar-2015.)
|- P = (Poly1 ` R )   &    |- .|| = ( ||r ` P )   &    |- B = ( Base ` P )   &    |- C = (Unic1p ` R )   &    |- .0. = ( 0g ` P )   &    |- E = (rem1p ` R )   =>    |- ( ( R e. Ring /\ F e. B /\ G e. C ) -> ( G .|| F <-> ( F E G ) = .0. ) )
Theorem	ply1remlem 22979	A term of the form x - N is linear, monic, and has exactly one zero. (Contributed by Mario Carneiro, 12-Jun-2015.)
|- P = (Poly1 ` R )   &    |- B = ( Base ` P )   &    |- K = ( Base ` R )   &    |- X = (var1 ` R )   &    |- .- = ( -g ` P )   &    |- A = (algSc ` P )   &    |- G = ( X .- ( A ` N ) )   &    |- O = (eval1 ` R )   &    |- ( ph -> R e. NzRing )   &    |- ( ph -> R e. CRing )   &    |- ( ph -> N e. K )   &    |- U = (Monic1p ` R )   &    |- D = ( deg1 ` R )   &    |- .0. = ( 0g ` R )   =>    |- ( ph -> ( G e. U /\ ( D ` G ) = 1 /\ ( `' ( O ` G ) " { .0. } ) = { N } ) )
Theorem	ply1rem 22980	The polynomial remainder theorem, or little Bézout's theorem (by contrast to the regular Bézout's theorem bezout 14481). If a polynomial F is divided by the linear factor x - A, the remainder is equal to F ( A ), the evaluation of the polynomial at A (interpreted as a constant polynomial). (Contributed by Mario Carneiro, 12-Jun-2015.)
|- P = (Poly1 ` R )   &    |- B = ( Base ` P )   &    |- K = ( Base ` R )   &    |- X = (var1 ` R )   &    |- .- = ( -g ` P )   &    |- A = (algSc ` P )   &    |- G = ( X .- ( A ` N ) )   &    |- O = (eval1 ` R )   &    |- ( ph -> R e. NzRing )   &    |- ( ph -> R e. CRing )   &    |- ( ph -> N e. K )   &    |- ( ph -> F e. B )   &    |- E = (rem1p ` R )   =>    |- ( ph -> ( F E G ) = ( A ` ( ( O ` F ) ` N ) ) )
Theorem	facth1 22981	The factor theorem and its converse. A polynomial F has a root at A iff G = x - A is a factor of F. (Contributed by Mario Carneiro, 12-Jun-2015.)
|- P = (Poly1 ` R )   &    |- B = ( Base ` P )   &    |- K = ( Base ` R )   &    |- X = (var1 ` R )   &    |- .- = ( -g ` P )   &    |- A = (algSc ` P )   &    |- G = ( X .- ( A ` N ) )   &    |- O = (eval1 ` R )   &    |- ( ph -> R e. NzRing )   &    |- ( ph -> R e. CRing )   &    |- ( ph -> N e. K )   &    |- ( ph -> F e. B )   &    |- .0. = ( 0g ` R )   &    |- .|| = ( ||r ` P )   =>    |- ( ph -> ( G .|| F <-> ( ( O ` F ) ` N ) = .0. ) )
Theorem	fta1glem1 22982	Lemma for fta1g 22984. (Contributed by Mario Carneiro, 7-Jun-2016.)
|- P = (Poly1 ` R )   &    |- B = ( Base ` P )   &    |- D = ( deg1 ` R )   &    |- O = (eval1 ` R )   &    |- W = ( 0g ` R )   &    |- .0. = ( 0g ` P )   &    |- ( ph -> R e. IDomn )   &    |- ( ph -> F e. B )   &    |- K = ( Base ` R )   &    |- X = (var1 ` R )   &    |- .- = ( -g ` P )   &    |- A = (algSc ` P )   &    |- G = ( X .- ( A ` T ) )   &    |- ( ph -> N e. NN0 )   &    |- ( ph -> ( D ` F ) = ( N + 1 ) )   &    |- ( ph -> T e. ( `' ( O ` F ) " { W } ) )   =>    |- ( ph -> ( D ` ( F (quot1p ` R ) G ) ) = N )
Theorem	fta1glem2 22983*	Lemma for fta1g 22984. (Contributed by Mario Carneiro, 12-Jun-2015.)
|- P = (Poly1 ` R )   &    |- B = ( Base ` P )   &    |- D = ( deg1 ` R )   &    |- O = (eval1 ` R )   &    |- W = ( 0g ` R )   &    |- .0. = ( 0g ` P )   &    |- ( ph -> R e. IDomn )   &    |- ( ph -> F e. B )   &    |- K = ( Base ` R )   &    |- X = (var1 ` R )   &    |- .- = ( -g ` P )   &    |- A = (algSc ` P )   &    |- G = ( X .- ( A ` T ) )   &    |- ( ph -> N e. NN0 )   &    |- ( ph -> ( D ` F ) = ( N + 1 ) )   &    |- ( ph -> T e. ( `' ( O ` F ) " { W } ) )   &    |- ( ph -> A. g e. B ( ( D ` g ) = N -> ( # ` ( `' ( O ` g ) " { W } ) ) <_ ( D ` g ) ) )   =>    |- ( ph -> ( # ` ( `' ( O ` F ) " { W } ) ) <_ ( D ` F ) )
Theorem	fta1g 22984	The one-sided fundamental theorem of algebra. A polynomial of degree n has at most n roots. Unlike the real fundamental theorem fta 23860, which is only true in CC and other algebraically closed fields, this is true in any integral domain. (Contributed by Mario Carneiro, 12-Jun-2015.)
|- P = (Poly1 ` R )   &    |- B = ( Base ` P )   &    |- D = ( deg1 ` R )   &    |- O = (eval1 ` R )   &    |- W = ( 0g ` R )   &    |- .0. = ( 0g ` P )   &    |- ( ph -> R e. IDomn )   &    |- ( ph -> F e. B )   &    |- ( ph -> F =/= .0. )   =>    |- ( ph -> ( # ` ( `' ( O ` F ) " { W } ) ) <_ ( D ` F ) )
Theorem	fta1blem 22985	Lemma for fta1b 22986. (Contributed by Mario Carneiro, 14-Jun-2015.)
|- P = (Poly1 ` R )   &    |- B = ( Base ` P )   &    |- D = ( deg1 ` R )   &    |- O = (eval1 ` R )   &    |- W = ( 0g ` R )   &    |- .0. = ( 0g ` P )   &    |- K = ( Base ` R )   &    |- .X. = ( .r ` R )   &    |- X = (var1 ` R )   &    |- .x. = ( .s ` P )   &    |- ( ph -> R e. CRing )   &    |- ( ph -> M e. K )   &    |- ( ph -> N e. K )   &    |- ( ph -> ( M .X. N ) = W )   &    |- ( ph -> M =/= W )   &    |- ( ph -> ( ( M .x. X ) e. ( B \ { .0. } ) -> ( # ` ( `' ( O ` ( M .x. X ) ) " { W } ) ) <_ ( D ` ( M .x. X ) ) ) )   =>    |- ( ph -> N = W )
Theorem	fta1b 22986*	The assumption that R be a domain in fta1g 22984 is necessary. Here we show that the statement is strong enough to prove that R is a domain. (Contributed by Mario Carneiro, 12-Jun-2015.)
|- P = (Poly1 ` R )   &    |- B = ( Base ` P )   &    |- D = ( deg1 ` R )   &    |- O = (eval1 ` R )   &    |- W = ( 0g ` R )   &    |- .0. = ( 0g ` P )   =>    |- ( R e. IDomn <-> ( R e. CRing /\ R e. NzRing /\ A. f e. ( B \ { .0. } ) ( # ` ( `' ( O ` f ) " { W } ) ) <_ ( D ` f ) ) )
Theorem	drnguc1p 22987	Over a division ring, all nonzero polynomials are unitic. (Contributed by Stefan O'Rear, 29-Mar-2015.)
|- P = (Poly1 ` R )   &    |- B = ( Base ` P )   &    |- .0. = ( 0g ` P )   &    |- C = (Unic1p ` R )   =>    |- ( ( R e. DivRing /\ F e. B /\ F =/= .0. ) -> F e. C )
Theorem	ig1peu 22988*	There is a unique monic polynomial of minimal degree in any nonzero ideal. (Contributed by Stefan O'Rear, 29-Mar-2015.)
|- P = (Poly1 ` R )   &    |- U = (LIdeal ` P )   &    |- .0. = ( 0g ` P )   &    |- M = (Monic1p ` R )   &    |- D = ( deg1 ` R )   =>    |- ( ( R e. DivRing /\ I e. U /\ I =/= { .0. } ) -> E! g e. ( I i^i M ) ( D ` g ) = sup ( ( D " ( I \ { .0. } ) ) , RR , `' < ) )
Theorem	ig1pval 22989*	Substitutions for the polynomial ideal generator function. (Contributed by Stefan O'Rear, 29-Mar-2015.)
|- P = (Poly1 ` R )   &    |- G = (idlGen1p ` R )   &    |- .0. = ( 0g ` P )   &    |- U = (LIdeal ` P )   &    |- D = ( deg1 ` R )   &    |- M = (Monic1p ` R )   =>    |- ( ( R e. V /\ I e. U ) -> ( G ` I ) = if ( I = { .0. } , .0. , ( iota_ g e. ( I i^i M ) ( D ` g ) = sup ( ( D " ( I \ { .0. } ) ) , RR , `' < ) ) ) )
Theorem	ig1pval2 22990	Generator of the zero ideal. (Contributed by Stefan O'Rear, 29-Mar-2015.)
|- P = (Poly1 ` R )   &    |- G = (idlGen1p ` R )   &    |- .0. = ( 0g ` P )   =>    |- ( R e. Ring -> ( G ` { .0. } ) = .0. )
Theorem	ig1pval3 22991	Characterizing properties of the monic generator of a nonzero ideal of polynomials. (Contributed by Stefan O'Rear, 29-Mar-2015.)
|- P = (Poly1 ` R )   &    |- G = (idlGen1p ` R )   &    |- .0. = ( 0g ` P )   &    |- U = (LIdeal ` P )   &    |- D = ( deg1 ` R )   &    |- M = (Monic1p ` R )   =>    |- ( ( R e. DivRing /\ I e. U /\ I =/= { .0. } ) -> ( ( G ` I ) e. I /\ ( G ` I ) e. M /\ ( D ` ( G ` I ) ) = sup ( ( D " ( I \ { .0. } ) ) , RR , `' < ) ) )
Theorem	ig1pcl 22992	The monic generator of an ideal is always in the ideal. (Contributed by Stefan O'Rear, 29-Mar-2015.)
|- P = (Poly1 ` R )   &    |- G = (idlGen1p ` R )   &    |- U = (LIdeal ` P )   =>    |- ( ( R e. DivRing /\ I e. U ) -> ( G ` I ) e. I )
Theorem	ig1pdvds 22993	The monic generator of an ideal divides all elements of the ideal. (Contributed by Stefan O'Rear, 29-Mar-2015.)
|- P = (Poly1 ` R )   &    |- G = (idlGen1p ` R )   &    |- U = (LIdeal ` P )   &    |- .|| = ( ||r ` P )   =>    |- ( ( R e. DivRing /\ I e. U /\ X e. I ) -> ( G ` I ) .|| X )
Theorem	ig1prsp 22994	Any ideal of polynomials over a division ring is generated by the ideal's canonical generator. (Contributed by Stefan O'Rear, 29-Mar-2015.)
|- P = (Poly1 ` R )   &    |- G = (idlGen1p ` R )   &    |- U = (LIdeal ` P )   &    |- K = (RSpan ` P )   =>    |- ( ( R e. DivRing /\ I e. U ) -> I = ( K ` { ( G ` I ) } ) )
Theorem	ply1lpir 22995	The ring of polynomials over a division ring has the principal ideal property. (Contributed by Stefan O'Rear, 29-Mar-2015.)
|- P = (Poly1 ` R )   =>    |- ( R e. DivRing -> P e. LPIR )
Theorem	ply1pid 22996	The polynomials over a field are a PID. (Contributed by Stefan O'Rear, 29-Mar-2015.)
|- P = (Poly1 ` R )   =>    |- ( R e. Field -> P e. PID )
14.1.3  Elementary properties of complex polynomials
Syntax	cply 22997	Extend class notation to include the set of complex polynomials.
class Poly
Syntax	cidp 22998	Extend class notation to include the identity polynomial.
class Xp
Syntax	ccoe 22999	Extend class notation to include the coefficient function on polynomials.
class coeff
Syntax	cdgr 23000	Extend class notation to include the degree function on polynomials.
class deg