P. 197 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 19601-19700   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	ressply1mul 19601	A restricted polynomial algebra has the same multiplication operation. (Contributed by Mario Carneiro, 3-Jul-2015.)
|- S = (Poly1 ` R )   &    |- H = ( R ↾s T )   &    |- U = (Poly1 ` H )   &    |- B = ( Base ` U )   &    |- ( ph -> T e. (SubRing ` R ) )   &    |- P = ( S ↾s B )   =>    |- ( ( ph /\ ( X e. B /\ Y e. B ) ) -> ( X ( .r ` U ) Y ) = ( X ( .r ` P ) Y ) )
Theorem	ressply1vsca 19602	A restricted power series algebra has the same scalar multiplication operation. (Contributed by Mario Carneiro, 3-Jul-2015.)
|- S = (Poly1 ` R )   &    |- H = ( R ↾s T )   &    |- U = (Poly1 ` H )   &    |- B = ( Base ` U )   &    |- ( ph -> T e. (SubRing ` R ) )   &    |- P = ( S ↾s B )   =>    |- ( ( ph /\ ( X e. T /\ Y e. B ) ) -> ( X ( .s ` U ) Y ) = ( X ( .s ` P ) Y ) )
Theorem	subrgply1 19603	A subring of the base ring induces a subring of polynomials. (Contributed by Mario Carneiro, 3-Jul-2015.)
|- S = (Poly1 ` R )   &    |- H = ( R ↾s T )   &    |- U = (Poly1 ` H )   &    |- B = ( Base ` U )   =>    |- ( T e. (SubRing ` R ) -> B e. (SubRing ` S ) )
Theorem	gsumply1subr 19604	Evaluate a group sum in a polynomial ring over a subring. (Contributed by AV, 22-Sep-2019.) (Proof shortened by AV, 31-Jan-2020.)
|- S = (Poly1 ` R )   &    |- H = ( R ↾s T )   &    |- U = (Poly1 ` H )   &    |- B = ( Base ` U )   &    |- ( ph -> T e. (SubRing ` R ) )   &    |- ( ph -> A e. V )   &    |- ( ph -> F : A --> B )   =>    |- ( ph -> ( S gsumg F ) = ( U gsumg F ) )
Theorem	psrbaspropd 19605	Property deduction for power series base set. (Contributed by Stefan O'Rear, 27-Mar-2015.)
|- ( ph -> ( Base ` R ) = ( Base ` S ) )   =>    |- ( ph -> ( Base ` ( I mPwSer R ) ) = ( Base ` ( I mPwSer S ) ) )
Theorem	psrplusgpropd 19606*	Property deduction for power series addition. (Contributed by Stefan O'Rear, 27-Mar-2015.) (Revised by Mario Carneiro, 3-Oct-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 -> ( +g ` ( I mPwSer R ) ) = ( +g ` ( I mPwSer S ) ) )
Theorem	mplbaspropd 19607*	Property deduction for polynomial base set. (Contributed by Stefan O'Rear, 27-Mar-2015.) (Proof shortened by AV, 19-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 -> ( Base ` ( I mPoly R ) ) = ( Base ` ( I mPoly S ) ) )
Theorem	psropprmul 19608	Reversing multiplication in a ring reverses multiplication in the power series ring. (Contributed by Stefan O'Rear, 27-Mar-2015.)
|- Y = ( I mPwSer R )   &    |- S = (oppr ` R )   &    |- Z = ( I mPwSer S )   &    |- .x. = ( .r ` Y )   &    |- .xb = ( .r ` Z )   &    |- B = ( Base ` Y )   =>    |- ( ( R e. Ring /\ F e. B /\ G e. B ) -> ( F .xb G ) = ( G .x. F ) )
Theorem	ply1opprmul 19609	Reversing multiplication in a ring reverses multiplication in the univariate polynomial ring. (Contributed by Stefan O'Rear, 27-Mar-2015.)
|- Y = (Poly1 ` R )   &    |- S = (oppr ` R )   &    |- Z = (Poly1 ` S )   &    |- .x. = ( .r ` Y )   &    |- .xb = ( .r ` Z )   &    |- B = ( Base ` Y )   =>    |- ( ( R e. Ring /\ F e. B /\ G e. B ) -> ( F .xb G ) = ( G .x. F ) )
Theorem	00ply1bas 19610	Lemma for ply1basfvi 19611 and deg1fvi 23845. (Contributed by Stefan O'Rear, 28-Mar-2015.)
|- (/) = ( Base ` (Poly1 ` (/) ) )
Theorem	ply1basfvi 19611	Protection compatibility of the univariate polynomial base set. (Contributed by Stefan O'Rear, 27-Mar-2015.)
|- ( Base ` (Poly1 ` R ) ) = ( Base ` (Poly1 ` ( _I ` R ) ) )
Theorem	ply1plusgfvi 19612	Protection compatibility of the univariate polynomial addition. (Contributed by Stefan O'Rear, 27-Mar-2015.)
|- ( +g ` (Poly1 ` R ) ) = ( +g ` (Poly1 ` ( _I ` R ) ) )
Theorem	ply1baspropd 19613*	Property deduction for univariate polynomial base set. (Contributed by Stefan O'Rear, 27-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 -> ( Base ` (Poly1 ` R ) ) = ( Base ` (Poly1 ` S ) ) )
Theorem	ply1plusgpropd 19614*	Property deduction for univariate polynomial addition. (Contributed by Stefan O'Rear, 27-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 -> ( +g ` (Poly1 ` R ) ) = ( +g ` (Poly1 ` S ) ) )
Theorem	opsrring 19615	Ordered power series form a ring. (Contributed by Stefan O'Rear, 22-Mar-2015.)
|- O = ( ( I ordPwSer R ) ` T )   &    |- ( ph -> I e. V )   &    |- ( ph -> R e. Ring )   &    |- ( ph -> T C_ ( I X. I ) )   =>    |- ( ph -> O e. Ring )
Theorem	opsrlmod 19616	Ordered power series form a left module. (Contributed by Stefan O'Rear, 26-Mar-2015.)
|- O = ( ( I ordPwSer R ) ` T )   &    |- ( ph -> I e. V )   &    |- ( ph -> R e. Ring )   &    |- ( ph -> T C_ ( I X. I ) )   =>    |- ( ph -> O e. LMod )
Theorem	psr1ring 19617	Univariate power series form a ring. (Contributed by Stefan O'Rear, 22-Mar-2015.)
|- S = (PwSer1 ` R )   =>    |- ( R e. Ring -> S e. Ring )
Theorem	ply1ring 19618	Univariate polynomials form a ring. (Contributed by Stefan O'Rear, 22-Mar-2015.)
|- P = (Poly1 ` R )   =>    |- ( R e. Ring -> P e. Ring )
Theorem	psr1lmod 19619	Univariate power series form a left module. (Contributed by Stefan O'Rear, 26-Mar-2015.)
|- P = (PwSer1 ` R )   =>    |- ( R e. Ring -> P e. LMod )
Theorem	psr1sca 19620	Scalars of a univariate power series ring. (Contributed by Stefan O'Rear, 4-Jul-2015.)
|- P = (PwSer1 ` R )   =>    |- ( R e. V -> R = (Scalar ` P ) )
Theorem	psr1sca2 19621	Scalars of a univariate power series ring. (Contributed by Stefan O'Rear, 26-Mar-2015.) (Revised by Mario Carneiro, 4-Jul-2015.)
|- P = (PwSer1 ` R )   =>    |- ( _I ` R ) = (Scalar ` P )
Theorem	ply1lmod 19622	Univariate polynomials form a left module. (Contributed by Stefan O'Rear, 26-Mar-2015.)
|- P = (Poly1 ` R )   =>    |- ( R e. Ring -> P e. LMod )
Theorem	ply1sca 19623	Scalars of a univariate polynomial ring. (Contributed by Stefan O'Rear, 26-Mar-2015.)
|- P = (Poly1 ` R )   =>    |- ( R e. V -> R = (Scalar ` P ) )
Theorem	ply1sca2 19624	Scalars of a univariate polynomial ring. (Contributed by Stefan O'Rear, 26-Mar-2015.)
|- P = (Poly1 ` R )   =>    |- ( _I ` R ) = (Scalar ` P )
Theorem	ply1mpl0 19625	The univariate polynomial ring has the same zero as the corresponding multivariate polynomial ring. (Contributed by Stefan O'Rear, 23-Mar-2015.) (Revised by Mario Carneiro, 3-Oct-2015.)
|- M = ( 1o mPoly R )   &    |- P = (Poly1 ` R )   &    |- .0. = ( 0g ` P )   =>    |- .0. = ( 0g ` M )
Theorem	ply10s0 19626	Zero times a univariate polynomial is the zero polynomial (lmod0vs 18896 analog.) (Contributed by AV, 2-Dec-2019.)
|- P = (Poly1 ` R )   &    |- B = ( Base ` P )   &    |- .* = ( .s ` P )   &    |- .0. = ( 0g ` R )   =>    |- ( ( R e. Ring /\ M e. B ) -> ( .0. .* M ) = ( 0g ` P ) )
Theorem	ply1mpl1 19627	The univariate polynomial ring has the same one as the corresponding multivariate polynomial ring. (Contributed by Stefan O'Rear, 23-Mar-2015.) (Revised by Mario Carneiro, 3-Oct-2015.)
|- M = ( 1o mPoly R )   &    |- P = (Poly1 ` R )   &    |- .1. = ( 1r ` P )   =>    |- .1. = ( 1r ` M )
Theorem	ply1ascl 19628	The univariate polynomial ring inherits the multivariate ring's scalar function. (Contributed by Stefan O'Rear, 28-Mar-2015.) (Proof shortened by Fan Zheng, 26-Jun-2016.)
|- P = (Poly1 ` R )   &    |- A = (algSc ` P )   =>    |- A = (algSc ` ( 1o mPoly R ) )
Theorem	subrg1ascl 19629	The scalar injection function in a subring algebra is the same up to a restriction to the subring. (Contributed by Mario Carneiro, 4-Jul-2015.)
|- P = (Poly1 ` R )   &    |- A = (algSc ` P )   &    |- H = ( R ↾s T )   &    |- U = (Poly1 ` H )   &    |- ( ph -> T e. (SubRing ` R ) )   &    |- C = (algSc ` U )   =>    |- ( ph -> C = ( A |` T ) )
Theorem	subrg1asclcl 19630	The scalars in a polynomial algebra are in the subring algebra iff the scalar value is in the subring. (Contributed by Mario Carneiro, 4-Jul-2015.)
|- P = (Poly1 ` R )   &    |- A = (algSc ` P )   &    |- H = ( R ↾s T )   &    |- U = (Poly1 ` H )   &    |- ( ph -> T e. (SubRing ` R ) )   &    |- B = ( Base ` U )   &    |- K = ( Base ` R )   &    |- ( ph -> X e. K )   =>    |- ( ph -> ( ( A ` X ) e. B <-> X e. T ) )
Theorem	subrgvr1 19631	The variables in a subring polynomial algebra are the same as the original ring. (Contributed by Mario Carneiro, 5-Jul-2015.)
|- X = (var1 ` R )   &    |- ( ph -> T e. (SubRing ` R ) )   &    |- H = ( R ↾s T )   =>    |- ( ph -> X = (var1 ` H ) )
Theorem	subrgvr1cl 19632	The variables in a polynomial algebra are contained in every subring algebra. (Contributed by Mario Carneiro, 5-Jul-2015.)
|- X = (var1 ` R )   &    |- ( ph -> T e. (SubRing ` R ) )   &    |- H = ( R ↾s T )   &    |- U = (Poly1 ` H )   &    |- B = ( Base ` U )   =>    |- ( ph -> X e. B )
Theorem	coe1z 19633	The coefficient vector of 0. (Contributed by Stefan O'Rear, 23-Mar-2015.)
|- P = (Poly1 ` R )   &    |- .0. = ( 0g ` P )   &    |- Y = ( 0g ` R )   =>    |- ( R e. Ring -> (coe1 ` .0. ) = ( NN0 X. { Y } ) )
Theorem	coe1add 19634	The coefficient vector of an addition. (Contributed by Stefan O'Rear, 24-Mar-2015.)
|- Y = (Poly1 ` R )   &    |- B = ( Base ` Y )   &    |- .+b = ( +g ` Y )   &    |- .+ = ( +g ` R )   =>    |- ( ( R e. Ring /\ F e. B /\ G e. B ) -> (coe1 ` ( F .+b G ) ) = ( (coe1 ` F ) oF .+ (coe1 ` G ) ) )
Theorem	coe1addfv 19635	A particular coefficient of an addition. (Contributed by Stefan O'Rear, 23-Mar-2015.)
|- Y = (Poly1 ` R )   &    |- B = ( Base ` Y )   &    |- .+b = ( +g ` Y )   &    |- .+ = ( +g ` R )   =>    |- ( ( ( R e. Ring /\ F e. B /\ G e. B ) /\ X e. NN0 ) -> ( (coe1 ` ( F .+b G ) ) ` X ) = ( ( (coe1 ` F ) ` X ) .+ ( (coe1 ` G ) ` X ) ) )
Theorem	coe1subfv 19636	A particular coefficient of a subtraction. (Contributed by Stefan O'Rear, 23-Mar-2015.)
|- Y = (Poly1 ` R )   &    |- B = ( Base ` Y )   &    |- .- = ( -g ` Y )   &    |- N = ( -g ` R )   =>    |- ( ( ( R e. Ring /\ F e. B /\ G e. B ) /\ X e. NN0 ) -> ( (coe1 ` ( F .- G ) ) ` X ) = ( ( (coe1 ` F ) ` X ) N ( (coe1 ` G ) ` X ) ) )
Theorem	coe1mul2lem1 19637	An equivalence for coe1mul2 19639. (Contributed by Stefan O'Rear, 25-Mar-2015.)
|- ( ( A e. NN0 /\ X e. ( NN0 ^m 1o ) ) -> ( X oR <_ ( 1o X. { A } ) <-> ( X ` (/) ) e. ( 0 ... A ) ) )
Theorem	coe1mul2lem2 19638*	An equivalence for coe1mul2 19639. (Contributed by Stefan O'Rear, 25-Mar-2015.)
|- H = { d e. ( NN0 ^m 1o ) | d oR <_ ( 1o X. { k } ) }   =>    |- ( k e. NN0 -> ( c e. H |-> ( c ` (/) ) ) : H -1-1-onto-> ( 0 ... k ) )
Theorem	coe1mul2 19639*	The coefficient vector of multiplication in the univariate power series ring. (Contributed by Stefan O'Rear, 25-Mar-2015.)
|- S = (PwSer1 ` R )   &    |- .xb = ( .r ` S )   &    |- .x. = ( .r ` R )   &    |- B = ( Base ` S )   =>    |- ( ( R e. Ring /\ F e. B /\ G e. B ) -> (coe1 ` ( F .xb G ) ) = ( k e. NN0 |-> ( R gsumg ( x e. ( 0 ... k ) |-> ( ( (coe1 ` F ) ` x ) .x. ( (coe1 ` G ) ` ( k - x ) ) ) ) ) ) )
Theorem	coe1mul 19640*	The coefficient vector of multiplication in the univariate polynomial ring. (Contributed by Stefan O'Rear, 25-Mar-2015.)
|- Y = (Poly1 ` R )   &    |- .xb = ( .r ` Y )   &    |- .x. = ( .r ` R )   &    |- B = ( Base ` Y )   =>    |- ( ( R e. Ring /\ F e. B /\ G e. B ) -> (coe1 ` ( F .xb G ) ) = ( k e. NN0 |-> ( R gsumg ( x e. ( 0 ... k ) |-> ( ( (coe1 ` F ) ` x ) .x. ( (coe1 ` G ) ` ( k - x ) ) ) ) ) ) )
Theorem	ply1moncl 19641	Closure of the expression for a univariate primitive monomial. (Contributed by AV, 14-Aug-2019.)
|- P = (Poly1 ` R )   &    |- X = (var1 ` R )   &    |- N = (mulGrp ` P )   &    |- .^ = (.g ` N )   &    |- B = ( Base ` P )   =>    |- ( ( R e. Ring /\ D e. NN0 ) -> ( D .^ X ) e. B )
Theorem	ply1tmcl 19642	Closure of the expression for a univariate polynomial term. (Contributed by Stefan O'Rear, 27-Mar-2015.) (Proof shortened by AV, 25-Nov-2019.)
|- K = ( Base ` R )   &    |- P = (Poly1 ` R )   &    |- X = (var1 ` R )   &    |- .x. = ( .s ` P )   &    |- N = (mulGrp ` P )   &    |- .^ = (.g ` N )   &    |- B = ( Base ` P )   =>    |- ( ( R e. Ring /\ C e. K /\ D e. NN0 ) -> ( C .x. ( D .^ X ) ) e. B )
Theorem	coe1tm 19643*	Coefficient vector of a polynomial term. (Contributed by Stefan O'Rear, 27-Mar-2015.)
|- .0. = ( 0g ` R )   &    |- K = ( Base ` R )   &    |- P = (Poly1 ` R )   &    |- X = (var1 ` R )   &    |- .x. = ( .s ` P )   &    |- N = (mulGrp ` P )   &    |- .^ = (.g ` N )   =>    |- ( ( R e. Ring /\ C e. K /\ D e. NN0 ) -> (coe1 ` ( C .x. ( D .^ X ) ) ) = ( x e. NN0 |-> if ( x = D , C , .0. ) ) )
Theorem	coe1tmfv1 19644	Nonzero coefficient of a polynomial term. (Contributed by Stefan O'Rear, 27-Mar-2015.)
|- .0. = ( 0g ` R )   &    |- K = ( Base ` R )   &    |- P = (Poly1 ` R )   &    |- X = (var1 ` R )   &    |- .x. = ( .s ` P )   &    |- N = (mulGrp ` P )   &    |- .^ = (.g ` N )   =>    |- ( ( R e. Ring /\ C e. K /\ D e. NN0 ) -> ( (coe1 ` ( C .x. ( D .^ X ) ) ) ` D ) = C )
Theorem	coe1tmfv2 19645	Zero coefficient of a polynomial term. (Contributed by Stefan O'Rear, 27-Mar-2015.)
|- .0. = ( 0g ` R )   &    |- K = ( Base ` R )   &    |- P = (Poly1 ` R )   &    |- X = (var1 ` R )   &    |- .x. = ( .s ` P )   &    |- N = (mulGrp ` P )   &    |- .^ = (.g ` N )   &    |- ( ph -> R e. Ring )   &    |- ( ph -> C e. K )   &    |- ( ph -> D e. NN0 )   &    |- ( ph -> F e. NN0 )   &    |- ( ph -> D =/= F )   =>    |- ( ph -> ( (coe1 ` ( C .x. ( D .^ X ) ) ) ` F ) = .0. )
Theorem	coe1tmmul2 19646*	Coefficient vector of a polynomial multiplied on the right by a term. (Contributed by Stefan O'Rear, 27-Mar-2015.)
|- .0. = ( 0g ` R )   &    |- K = ( Base ` R )   &    |- P = (Poly1 ` R )   &    |- X = (var1 ` R )   &    |- .x. = ( .s ` P )   &    |- N = (mulGrp ` P )   &    |- .^ = (.g ` N )   &    |- B = ( Base ` P )   &    |- .xb = ( .r ` P )   &    |- .X. = ( .r ` R )   &    |- ( ph -> A e. B )   &    |- ( ph -> R e. Ring )   &    |- ( ph -> C e. K )   &    |- ( ph -> D e. NN0 )   =>    |- ( ph -> (coe1 ` ( A .xb ( C .x. ( D .^ X ) ) ) ) = ( x e. NN0 |-> if ( D <_ x , ( ( (coe1 ` A ) ` ( x - D ) ) .X. C ) , .0. ) ) )
Theorem	coe1tmmul 19647*	Coefficient vector of a polynomial multiplied on the left by a term. (Contributed by Stefan O'Rear, 29-Mar-2015.)
|- .0. = ( 0g ` R )   &    |- K = ( Base ` R )   &    |- P = (Poly1 ` R )   &    |- X = (var1 ` R )   &    |- .x. = ( .s ` P )   &    |- N = (mulGrp ` P )   &    |- .^ = (.g ` N )   &    |- B = ( Base ` P )   &    |- .xb = ( .r ` P )   &    |- .X. = ( .r ` R )   &    |- ( ph -> A e. B )   &    |- ( ph -> R e. Ring )   &    |- ( ph -> C e. K )   &    |- ( ph -> D e. NN0 )   =>    |- ( ph -> (coe1 ` ( ( C .x. ( D .^ X ) ) .xb A ) ) = ( x e. NN0 |-> if ( D <_ x , ( C .X. ( (coe1 ` A ) ` ( x - D ) ) ) , .0. ) ) )
Theorem	coe1tmmul2fv 19648	Function value of a right-multiplication by a term in the shifted domain. (Contributed by Stefan O'Rear, 27-Mar-2015.)
|- .0. = ( 0g ` R )   &    |- K = ( Base ` R )   &    |- P = (Poly1 ` R )   &    |- X = (var1 ` R )   &    |- .x. = ( .s ` P )   &    |- N = (mulGrp ` P )   &    |- .^ = (.g ` N )   &    |- B = ( Base ` P )   &    |- .xb = ( .r ` P )   &    |- .X. = ( .r ` R )   &    |- ( ph -> A e. B )   &    |- ( ph -> R e. Ring )   &    |- ( ph -> C e. K )   &    |- ( ph -> D e. NN0 )   &    |- ( ph -> Y e. NN0 )   =>    |- ( ph -> ( (coe1 ` ( A .xb ( C .x. ( D .^ X ) ) ) ) ` ( D + Y ) ) = ( ( (coe1 ` A ) ` Y ) .X. C ) )
Theorem	coe1pwmul 19649*	Coefficient vector of a polynomial multiplied on the left by a variable power. (Contributed by Stefan O'Rear, 1-Apr-2015.)
|- .0. = ( 0g ` R )   &    |- P = (Poly1 ` R )   &    |- X = (var1 ` R )   &    |- N = (mulGrp ` P )   &    |- .^ = (.g ` N )   &    |- B = ( Base ` P )   &    |- .x. = ( .r ` P )   &    |- ( ph -> R e. Ring )   &    |- ( ph -> A e. B )   &    |- ( ph -> D e. NN0 )   =>    |- ( ph -> (coe1 ` ( ( D .^ X ) .x. A ) ) = ( x e. NN0 |-> if ( D <_ x , ( (coe1 ` A ) ` ( x - D ) ) , .0. ) ) )
Theorem	coe1pwmulfv 19650	Function value of a right-multiplication by a variable power in the shifted domain. (Contributed by Stefan O'Rear, 1-Apr-2015.)
|- .0. = ( 0g ` R )   &    |- P = (Poly1 ` R )   &    |- X = (var1 ` R )   &    |- N = (mulGrp ` P )   &    |- .^ = (.g ` N )   &    |- B = ( Base ` P )   &    |- .x. = ( .r ` P )   &    |- ( ph -> R e. Ring )   &    |- ( ph -> A e. B )   &    |- ( ph -> D e. NN0 )   &    |- ( ph -> Y e. NN0 )   =>    |- ( ph -> ( (coe1 ` ( ( D .^ X ) .x. A ) ) ` ( D + Y ) ) = ( (coe1 ` A ) ` Y ) )
Theorem	ply1scltm 19651	A scalar is a term with zero exponent. (Contributed by Stefan O'Rear, 29-Mar-2015.)
|- K = ( Base ` R )   &    |- P = (Poly1 ` R )   &    |- X = (var1 ` R )   &    |- .x. = ( .s ` P )   &    |- N = (mulGrp ` P )   &    |- .^ = (.g ` N )   &    |- A = (algSc ` P )   =>    |- ( ( R e. Ring /\ F e. K ) -> ( A ` F ) = ( F .x. ( 0 .^ X ) ) )
Theorem	coe1sclmul 19652	Coefficient vector of a polynomial multiplied on the left by a scalar. (Contributed by Stefan O'Rear, 29-Mar-2015.)
|- P = (Poly1 ` R )   &    |- B = ( Base ` P )   &    |- K = ( Base ` R )   &    |- A = (algSc ` P )   &    |- .xb = ( .r ` P )   &    |- .x. = ( .r ` R )   =>    |- ( ( R e. Ring /\ X e. K /\ Y e. B ) -> (coe1 ` ( ( A ` X ) .xb Y ) ) = ( ( NN0 X. { X } ) oF .x. (coe1 ` Y ) ) )
Theorem	coe1sclmulfv 19653	A single coefficient of a polynomial multiplied on the left by a scalar. (Contributed by Stefan O'Rear, 1-Apr-2015.)
|- P = (Poly1 ` R )   &    |- B = ( Base ` P )   &    |- K = ( Base ` R )   &    |- A = (algSc ` P )   &    |- .xb = ( .r ` P )   &    |- .x. = ( .r ` R )   =>    |- ( ( R e. Ring /\ ( X e. K /\ Y e. B ) /\ .0. e. NN0 ) -> ( (coe1 ` ( ( A ` X ) .xb Y ) ) ` .0. ) = ( X .x. ( (coe1 ` Y ) ` .0. ) ) )
Theorem	coe1sclmul2 19654	Coefficient vector of a polynomial multiplied on the right by a scalar. (Contributed by Stefan O'Rear, 29-Mar-2015.)
|- P = (Poly1 ` R )   &    |- B = ( Base ` P )   &    |- K = ( Base ` R )   &    |- A = (algSc ` P )   &    |- .xb = ( .r ` P )   &    |- .x. = ( .r ` R )   =>    |- ( ( R e. Ring /\ X e. K /\ Y e. B ) -> (coe1 ` ( Y .xb ( A ` X ) ) ) = ( (coe1 ` Y ) oF .x. ( NN0 X. { X } ) ) )
Theorem	ply1sclf 19655	A scalar polynomial is a polynomial. (Contributed by Stefan O'Rear, 28-Mar-2015.)
|- P = (Poly1 ` R )   &    |- A = (algSc ` P )   &    |- K = ( Base ` R )   &    |- B = ( Base ` P )   =>    |- ( R e. Ring -> A : K --> B )
Theorem	ply1sclcl 19656	The value of the algebra scalars function for (univariate) polynomials applied to a scalar results in a constant polynomial. (Contributed by AV, 27-Nov-2019.)
|- P = (Poly1 ` R )   &    |- A = (algSc ` P )   &    |- K = ( Base ` R )   &    |- B = ( Base ` P )   =>    |- ( ( R e. Ring /\ S e. K ) -> ( A ` S ) e. B )
Theorem	coe1scl 19657*	Coefficient vector of a scalar. (Contributed by Stefan O'Rear, 28-Mar-2015.)
|- P = (Poly1 ` R )   &    |- A = (algSc ` P )   &    |- K = ( Base ` R )   &    |- .0. = ( 0g ` R )   =>    |- ( ( R e. Ring /\ X e. K ) -> (coe1 ` ( A ` X ) ) = ( x e. NN0 |-> if ( x = 0 , X , .0. ) ) )
Theorem	ply1sclid 19658	Recover the base scalar from a scalar polynomial. (Contributed by Stefan O'Rear, 28-Mar-2015.)
|- P = (Poly1 ` R )   &    |- A = (algSc ` P )   &    |- K = ( Base ` R )   =>    |- ( ( R e. Ring /\ X e. K ) -> X = ( (coe1 ` ( A ` X ) ) ` 0 ) )
Theorem	ply1sclf1 19659	The polynomial scalar function is injective. (Contributed by Stefan O'Rear, 28-Mar-2015.)
|- P = (Poly1 ` R )   &    |- A = (algSc ` P )   &    |- K = ( Base ` R )   &    |- B = ( Base ` P )   =>    |- ( R e. Ring -> A : K -1-1-> B )
Theorem	ply1scl0 19660	The zero scalar is zero. (Contributed by Stefan O'Rear, 29-Mar-2015.)
|- P = (Poly1 ` R )   &    |- A = (algSc ` P )   &    |- .0. = ( 0g ` R )   &    |- Y = ( 0g ` P )   =>    |- ( R e. Ring -> ( A ` .0. ) = Y )
Theorem	ply1scln0 19661	Nonzero scalars create nonzero polynomials. (Contributed by Stefan O'Rear, 29-Mar-2015.)
|- P = (Poly1 ` R )   &    |- A = (algSc ` P )   &    |- .0. = ( 0g ` R )   &    |- Y = ( 0g ` P )   &    |- K = ( Base ` R )   =>    |- ( ( R e. Ring /\ X e. K /\ X =/= .0. ) -> ( A ` X ) =/= Y )
Theorem	ply1scl1 19662	The one scalar is the unit polynomial. (Contributed by Stefan O'Rear, 1-Apr-2015.)
|- P = (Poly1 ` R )   &    |- A = (algSc ` P )   &    |- .1. = ( 1r ` R )   &    |- N = ( 1r ` P )   =>    |- ( R e. Ring -> ( A ` .1. ) = N )
Theorem	ply1idvr1 19663	The identity of a polynomial ring expressed as power of the polynomial variable. (Contributed by AV, 14-Aug-2019.)
|- P = (Poly1 ` R )   &    |- X = (var1 ` R )   &    |- N = (mulGrp ` P )   &    |- .^ = (.g ` N )   =>    |- ( R e. Ring -> ( 0 .^ X ) = ( 1r ` P ) )
Theorem	cply1mul 19664*	The product of two constant polynomials is a constant polynomial. (Contributed by AV, 18-Nov-2019.)
|- P = (Poly1 ` R )   &    |- B = ( Base ` P )   &    |- .0. = ( 0g ` R )   &    |- .X. = ( .r ` P )   =>    |- ( ( R e. Ring /\ ( F e. B /\ G e. B ) ) -> ( A. c e. NN ( ( (coe1 ` F ) ` c ) = .0. /\ ( (coe1 ` G ) ` c ) = .0. ) -> A. c e. NN ( (coe1 ` ( F .X. G ) ) ` c ) = .0. ) )
Theorem	ply1coefsupp 19665*	The decomposition of a univariate polynomial is finitely supported. Formerly part of proof for ply1coe 19666. (Contributed by Stefan O'Rear, 21-Mar-2015.) (Revised by AV, 8-Aug-2019.)
|- P = (Poly1 ` R )   &    |- X = (var1 ` R )   &    |- B = ( Base ` P )   &    |- .x. = ( .s ` P )   &    |- M = (mulGrp ` P )   &    |- .^ = (.g ` M )   &    |- A = (coe1 ` K )   =>    |- ( ( R e. Ring /\ K e. B ) -> ( k e. NN0 |-> ( ( A ` k ) .x. ( k .^ X ) ) ) finSupp ( 0g ` P ) )
Theorem	ply1coe 19666*	Decompose a univariate polynomial as a sum of powers. (Contributed by Stefan O'Rear, 21-Mar-2015.) (Revised by AV, 7-Oct-2019.)
|- P = (Poly1 ` R )   &    |- X = (var1 ` R )   &    |- B = ( Base ` P )   &    |- .x. = ( .s ` P )   &    |- M = (mulGrp ` P )   &    |- .^ = (.g ` M )   &    |- A = (coe1 ` K )   =>    |- ( ( R e. Ring /\ K e. B ) -> K = ( P gsumg ( k e. NN0 |-> ( ( A ` k ) .x. ( k .^ X ) ) ) ) )
Theorem	eqcoe1ply1eq 19667*	Two polynomials over the same ring are equal if they have identical coefficients. (Contributed by AV, 7-Oct-2019.)
|- P = (Poly1 ` R )   &    |- B = ( Base ` P )   &    |- A = (coe1 ` K )   &    |- C = (coe1 ` L )   =>    |- ( ( R e. Ring /\ K e. B /\ L e. B ) -> ( A. k e. NN0 ( A ` k ) = ( C ` k ) -> K = L ) )
Theorem	ply1coe1eq 19668*	Two polynomials over the same ring are equal iff they have identical coefficients. (Contributed by AV, 13-Oct-2019.)
|- P = (Poly1 ` R )   &    |- B = ( Base ` P )   &    |- A = (coe1 ` K )   &    |- C = (coe1 ` L )   =>    |- ( ( R e. Ring /\ K e. B /\ L e. B ) -> ( A. k e. NN0 ( A ` k ) = ( C ` k ) <-> K = L ) )
Theorem	cply1coe0 19669*	All but the first coefficient of a constant polynomial ( i.e. a "lifted scalar") are zero. (Contributed by AV, 16-Nov-2019.)
|- K = ( Base ` R )   &    |- .0. = ( 0g ` R )   &    |- P = (Poly1 ` R )   &    |- B = ( Base ` P )   &    |- A = (algSc ` P )   =>    |- ( ( R e. Ring /\ S e. K ) -> A. n e. NN ( (coe1 ` ( A ` S ) ) ` n ) = .0. )
Theorem	cply1coe0bi 19670*	A polynomial is constant (i.e. a "lifted scalar") iff all but the first coefficient are zero. (Contributed by AV, 16-Nov-2019.)
|- K = ( Base ` R )   &    |- .0. = ( 0g ` R )   &    |- P = (Poly1 ` R )   &    |- B = ( Base ` P )   &    |- A = (algSc ` P )   =>    |- ( ( R e. Ring /\ M e. B ) -> ( E. s e. K M = ( A ` s ) <-> A. n e. NN ( (coe1 ` M ) ` n ) = .0. ) )
Theorem	coe1fzgsumdlem 19671*	Lemma for coe1fzgsumd 19672 (induction step). (Contributed by AV, 8-Oct-2019.)
|- P = (Poly1 ` R )   &    |- B = ( Base ` P )   &    |- ( ph -> R e. Ring )   &    |- ( ph -> K e. NN0 )   =>    |- ( ( m e. Fin /\ -. a e. m /\ ph ) -> ( ( A. x e. m M e. B -> ( (coe1 ` ( P gsumg ( x e. m |-> M ) ) ) ` K ) = ( R gsumg ( x e. m |-> ( (coe1 ` M ) ` K ) ) ) ) -> ( A. x e. ( m u. { a } ) M e. B -> ( (coe1 ` ( P gsumg ( x e. ( m u. { a } ) |-> M ) ) ) ` K ) = ( R gsumg ( x e. ( m u. { a } ) |-> ( (coe1 ` M ) ` K ) ) ) ) ) )
Theorem	coe1fzgsumd 19672*	Value of an evaluated coefficient in a finite group sum of polynomials. (Contributed by AV, 8-Oct-2019.)
|- P = (Poly1 ` R )   &    |- B = ( Base ` P )   &    |- ( ph -> R e. Ring )   &    |- ( ph -> K e. NN0 )   &    |- ( ph -> A. x e. N M e. B )   &    |- ( ph -> N e. Fin )   =>    |- ( ph -> ( (coe1 ` ( P gsumg ( x e. N |-> M ) ) ) ` K ) = ( R gsumg ( x e. N |-> ( (coe1 ` M ) ` K ) ) ) )
Theorem	gsumsmonply1 19673*	A finite group sum of scaled monomials is a univariate polynomial. (Contributed by AV, 8-Oct-2019.)
|- P = (Poly1 ` R )   &    |- B = ( Base ` P )   &    |- X = (var1 ` R )   &    |- .^ = (.g ` (mulGrp ` P ) )   &    |- ( ph -> R e. Ring )   &    |- K = ( Base ` R )   &    |- .* = ( .s ` P )   &    |- .0. = ( 0g ` R )   &    |- ( ph -> A. k e. NN0 A e. K )   &    |- ( ph -> ( k e. NN0 |-> A ) finSupp .0. )   =>    |- ( ph -> ( P gsumg ( k e. NN0 |-> ( A .* ( k .^ X ) ) ) ) e. B )
Theorem	gsummoncoe1 19674*	A coefficient of the polynomial represented as a sum of scaled monomials is the coefficient of the corresponding scaled monomial. (Contributed by AV, 13-Oct-2019.)
|- P = (Poly1 ` R )   &    |- B = ( Base ` P )   &    |- X = (var1 ` R )   &    |- .^ = (.g ` (mulGrp ` P ) )   &    |- ( ph -> R e. Ring )   &    |- K = ( Base ` R )   &    |- .* = ( .s ` P )   &    |- .0. = ( 0g ` R )   &    |- ( ph -> A. k e. NN0 A e. K )   &    |- ( ph -> ( k e. NN0 |-> A ) finSupp .0. )   &    |- ( ph -> L e. NN0 )   =>    |- ( ph -> ( (coe1 ` ( P gsumg ( k e. NN0 |-> ( A .* ( k .^ X ) ) ) ) ) ` L ) = [_ L / k ]_ A )
Theorem	gsumply1eq 19675*	Two univariate polynomials given as (finitely supported) sum of scaled monomials are equal iff the corresponding coefficients are equal. (Contributed by AV, 21-Nov-2019.)
|- P = (Poly1 ` R )   &    |- X = (var1 ` R )   &    |- .^ = (.g ` (mulGrp ` P ) )   &    |- ( ph -> R e. Ring )   &    |- K = ( Base ` R )   &    |- .* = ( .s ` P )   &    |- .0. = ( 0g ` R )   &    |- ( ph -> A. k e. NN0 A e. K )   &    |- ( ph -> ( k e. NN0 |-> A ) finSupp .0. )   &    |- ( ph -> A. k e. NN0 B e. K )   &    |- ( ph -> ( k e. NN0 |-> B ) finSupp .0. )   &    |- ( ph -> O = ( P gsumg ( k e. NN0 |-> ( A .* ( k .^ X ) ) ) ) )   &    |- ( ph -> Q = ( P gsumg ( k e. NN0 |-> ( B .* ( k .^ X ) ) ) ) )   =>    |- ( ph -> ( O = Q <-> A. k e. NN0 A = B ) )
Theorem	lply1binom 19676*	The binomial theorem for linear polynomials (monic polynomials of degree 1) over commutative rings: ( X + A ) ^ N is the sum from k = 0 to N of ( N _C k ) x. ( ( A ^ ( N - k ) ) x. ( X ^ k ) ). (Contributed by AV, 25-Aug-2019.)
|- P = (Poly1 ` R )   &    |- X = (var1 ` R )   &    |- .+ = ( +g ` P )   &    |- .X. = ( .r ` P )   &    |- .x. = (.g ` P )   &    |- G = (mulGrp ` P )   &    |- .^ = (.g ` G )   &    |- B = ( Base ` P )   =>    |- ( ( R e. CRing /\ N e. NN0 /\ A e. B ) -> ( N .^ ( X .+ A ) ) = ( P gsumg ( k e. ( 0 ... N ) |-> ( ( N _C k ) .x. ( ( ( N - k ) .^ A ) .X. ( k .^ X ) ) ) ) ) )
Theorem	lply1binomsc 19677*	The binomial theorem for linear polynomials (monic polynomials of degree 1) over commutative rings, expressed by an element of this ring: ( X + A ) ^ N is the sum from k = 0 to N of ( N _C k ) x. ( ( A ^ ( N - k ) ) x. ( X ^ k ) ). (Contributed by AV, 25-Aug-2019.)
|- P = (Poly1 ` R )   &    |- X = (var1 ` R )   &    |- .+ = ( +g ` P )   &    |- .X. = ( .r ` P )   &    |- .x. = (.g ` P )   &    |- G = (mulGrp ` P )   &    |- .^ = (.g ` G )   &    |- K = ( Base ` R )   &    |- S = (algSc ` P )   &    |- H = (mulGrp ` R )   &    |- E = (.g ` H )   =>    |- ( ( R e. CRing /\ N e. NN0 /\ A e. K ) -> ( N .^ ( X .+ ( S ` A ) ) ) = ( P gsumg ( k e. ( 0 ... N ) |-> ( ( N _C k ) .x. ( ( S ` ( ( N - k ) E A ) ) .X. ( k .^ X ) ) ) ) ) )
10.10.5  Univariate polynomial evaluation
Syntax	ces1 19678	Evaluation of a univariate polynomial in a subring.
class evalSub1
Syntax	ce1 19679	Evaluation of a univariate polynomial.
class eval1
Definition	df-evls1 19680*	Define the evaluation map for the univariate polynomial algebra. The function ( S evalSub1 R ) : V --> ( S ^m S ) makes sense when S is a ring and R is a subring of S, and where V is the set of polynomials in (Poly1 ` R ). This function maps an element of the formal polynomial algebra (with coefficients in R) to a function from assignments to the variable from S into an element of S formed by evaluating the polynomial with the given assignment. (Contributed by Mario Carneiro, 12-Jun-2015.)
|- evalSub1 = ( s e. _V , r e. ~P ( Base ` s ) |-> [_ ( Base ` s ) / b ]_ ( ( x e. ( b ^m ( b ^m 1o ) ) |-> ( x o. ( y e. b |-> ( 1o X. { y } ) ) ) ) o. ( ( 1o evalSub s ) ` r ) ) )
Definition	df-evl1 19681*	Define the evaluation map for the univariate polynomial algebra. The function (eval1 ` R ) : V --> ( R ^m R ) makes sense when R is a ring, and V is the set of polynomials in (Poly1 ` R ). This function maps an element of the formal polynomial algebra (with coefficients in R) to a function from assignments to the variable from R into an element of R formed by evaluating the polynomial with the given assignment. (Contributed by Mario Carneiro, 12-Jun-2015.)
|- eval1 = ( r e. _V |-> [_ ( Base ` r ) / b ]_ ( ( x e. ( b ^m ( b ^m 1o ) ) |-> ( x o. ( y e. b |-> ( 1o X. { y } ) ) ) ) o. ( 1o eval r ) ) )
Theorem	reldmevls1 19682	Well-behaved binary operation property of evalSub1. (Contributed by AV, 7-Sep-2019.)
|- Rel dom evalSub1
Theorem	ply1frcl 19683	Reverse closure for the set of univariate polynomial functions. (Contributed by AV, 9-Sep-2019.)
|- Q = ran ( S evalSub1 R )   =>    |- ( X e. Q -> ( S e. _V /\ R e. ~P ( Base ` S ) ) )
Theorem	evls1fval 19684*	Value of the univariate polynomial evaluation map function. (Contributed by AV, 7-Sep-2019.)
|- Q = ( S evalSub1 R )   &    |- E = ( 1o evalSub S )   &    |- B = ( Base ` S )   =>    |- ( ( S e. V /\ R e. ~P B ) -> Q = ( ( x e. ( B ^m ( B ^m 1o ) ) |-> ( x o. ( y e. B |-> ( 1o X. { y } ) ) ) ) o. ( E ` R ) ) )
Theorem	evls1val 19685*	Value of the univariate polynomial evaluation map. (Contributed by AV, 10-Sep-2019.)
|- Q = ( S evalSub1 R )   &    |- E = ( 1o evalSub S )   &    |- B = ( Base ` S )   &    |- M = ( 1o mPoly ( S ↾s R ) )   &    |- K = ( Base ` M )   =>    |- ( ( S e. CRing /\ R e. (SubRing ` S ) /\ A e. K ) -> ( Q ` A ) = ( ( ( E ` R ) ` A ) o. ( y e. B |-> ( 1o X. { y } ) ) ) )
Theorem	evls1rhmlem 19686*	Lemma for evl1rhm 19696 and evls1rhm 19687 (formerly part of the proof of evl1rhm 19696): The first function of the composition forming the univariate polynomial evaluation map function for a (sub)ring is a ring homomorphism. (Contributed by AV, 11-Sep-2019.)
|- B = ( Base ` R )   &    |- T = ( R ^s B )   &    |- F = ( x e. ( B ^m ( B ^m 1o ) ) |-> ( x o. ( y e. B |-> ( 1o X. { y } ) ) ) )   =>    |- ( R e. CRing -> F e. ( ( R ^s ( B ^m 1o ) ) RingHom T ) )
Theorem	evls1rhm 19687	Polynomial evaluation is a homomorphism (into the product ring). (Contributed by AV, 11-Sep-2019.)
|- Q = ( S evalSub1 R )   &    |- B = ( Base ` S )   &    |- T = ( S ^s B )   &    |- U = ( S ↾s R )   &    |- W = (Poly1 ` U )   =>    |- ( ( S e. CRing /\ R e. (SubRing ` S ) ) -> Q e. ( W RingHom T ) )
Theorem	evls1sca 19688	Univariate polynomial evaluation maps scalars to constant functions. (Contributed by AV, 8-Sep-2019.)
|- Q = ( S evalSub1 R )   &    |- W = (Poly1 ` U )   &    |- U = ( S ↾s R )   &    |- B = ( Base ` S )   &    |- A = (algSc ` W )   &    |- ( ph -> S e. CRing )   &    |- ( ph -> R e. (SubRing ` S ) )   &    |- ( ph -> X e. R )   =>    |- ( ph -> ( Q ` ( A ` X ) ) = ( B X. { X } ) )
Theorem	evls1gsumadd 19689*	Univariate polynomial evaluation maps (additive) group sums to group sums. (Contributed by AV, 14-Sep-2019.)
|- Q = ( S evalSub1 R )   &    |- K = ( Base ` S )   &    |- W = (Poly1 ` U )   &    |- .0. = ( 0g ` W )   &    |- U = ( S ↾s R )   &    |- P = ( S ^s K )   &    |- B = ( Base ` W )   &    |- ( ph -> S e. CRing )   &    |- ( ph -> R e. (SubRing ` S ) )   &    |- ( ( ph /\ x e. N ) -> Y e. B )   &    |- ( ph -> N C_ NN0 )   &    |- ( ph -> ( x e. N |-> Y ) finSupp .0. )   =>    |- ( ph -> ( Q ` ( W gsumg ( x e. N |-> Y ) ) ) = ( P gsumg ( x e. N |-> ( Q ` Y ) ) ) )
Theorem	evls1gsummul 19690*	Univariate polynomial evaluation maps (multiplicative) group sums to group sums. (Contributed by AV, 14-Sep-2019.)
|- Q = ( S evalSub1 R )   &    |- K = ( Base ` S )   &    |- W = (Poly1 ` U )   &    |- G = (mulGrp ` W )   &    |- .1. = ( 1r ` W )   &    |- U = ( S ↾s R )   &    |- P = ( S ^s K )   &    |- H = (mulGrp ` P )   &    |- B = ( Base ` W )   &    |- ( ph -> S e. CRing )   &    |- ( ph -> R e. (SubRing ` S ) )   &    |- ( ( ph /\ x e. N ) -> Y e. B )   &    |- ( ph -> N C_ NN0 )   &    |- ( ph -> ( x e. N |-> Y ) finSupp .1. )   =>    |- ( ph -> ( Q ` ( G gsumg ( x e. N |-> Y ) ) ) = ( H gsumg ( x e. N |-> ( Q ` Y ) ) ) )
Theorem	evls1varpw 19691	Univariate polynomial evaluation for subrings maps the exponentiation of a variable to the exponentiation of the evaluated variable. (Contributed by AV, 14-Sep-2019.)
|- Q = ( S evalSub1 R )   &    |- U = ( S ↾s R )   &    |- W = (Poly1 ` U )   &    |- G = (mulGrp ` W )   &    |- X = (var1 ` U )   &    |- B = ( Base ` S )   &    |- .^ = (.g ` G )   &    |- ( ph -> S e. CRing )   &    |- ( ph -> R e. (SubRing ` S ) )   &    |- ( ph -> N e. NN0 )   =>    |- ( ph -> ( Q ` ( N .^ X ) ) = ( N (.g ` (mulGrp ` ( S ^s B ) ) ) ( Q ` X ) ) )
Theorem	evl1fval 19692*	Value of the simple/same ring evaluation map. (Contributed by Mario Carneiro, 12-Jun-2015.)
|- O = (eval1 ` R )   &    |- Q = ( 1o eval R )   &    |- B = ( Base ` R )   =>    |- O = ( ( x e. ( B ^m ( B ^m 1o ) ) |-> ( x o. ( y e. B |-> ( 1o X. { y } ) ) ) ) o. Q )
Theorem	evl1val 19693*	Value of the simple/same ring evaluation map. (Contributed by Mario Carneiro, 12-Jun-2015.)
|- O = (eval1 ` R )   &    |- Q = ( 1o eval R )   &    |- B = ( Base ` R )   &    |- M = ( 1o mPoly R )   &    |- K = ( Base ` M )   =>    |- ( ( R e. CRing /\ A e. K ) -> ( O ` A ) = ( ( Q ` A ) o. ( y e. B |-> ( 1o X. { y } ) ) ) )
Theorem	evl1fval1lem 19694	Lemma for evl1fval1 19695. (Contributed by AV, 11-Sep-2019.)
|- Q = (eval1 ` R )   &    |- B = ( Base ` R )   =>    |- ( R e. V -> Q = ( R evalSub1 B ) )
Theorem	evl1fval1 19695	Value of the simple/same ring evaluation map function for univariate polynomials. (Contributed by AV, 11-Sep-2019.)
|- Q = (eval1 ` R )   &    |- B = ( Base ` R )   =>    |- Q = ( R evalSub1 B )
Theorem	evl1rhm 19696	Polynomial evaluation is a homomorphism (into the product ring). (Contributed by Mario Carneiro, 12-Jun-2015.) (Proof shortened by AV, 13-Sep-2019.)
|- O = (eval1 ` R )   &    |- P = (Poly1 ` R )   &    |- T = ( R ^s B )   &    |- B = ( Base ` R )   =>    |- ( R e. CRing -> O e. ( P RingHom T ) )
Theorem	fveval1fvcl 19697	The function value of the evaluation function of a polynomial is an element of the underlying ring. (Contributed by AV, 17-Sep-2019.)
|- O = (eval1 ` R )   &    |- P = (Poly1 ` R )   &    |- B = ( Base ` R )   &    |- U = ( Base ` P )   &    |- ( ph -> R e. CRing )   &    |- ( ph -> Y e. B )   &    |- ( ph -> M e. U )   =>    |- ( ph -> ( ( O ` M ) ` Y ) e. B )
Theorem	evl1sca 19698	Polynomial evaluation maps scalars to constant functions. (Contributed by Mario Carneiro, 12-Jun-2015.)
|- O = (eval1 ` R )   &    |- P = (Poly1 ` R )   &    |- B = ( Base ` R )   &    |- A = (algSc ` P )   =>    |- ( ( R e. CRing /\ X e. B ) -> ( O ` ( A ` X ) ) = ( B X. { X } ) )
Theorem	evl1scad 19699	Polynomial evaluation builder for scalars. (Contributed by Mario Carneiro, 4-Jul-2015.)
|- O = (eval1 ` R )   &    |- P = (Poly1 ` R )   &    |- B = ( Base ` R )   &    |- A = (algSc ` P )   &    |- U = ( Base ` P )   &    |- ( ph -> R e. CRing )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   =>    |- ( ph -> ( ( A ` X ) e. U /\ ( ( O ` ( A ` X ) ) ` Y ) = X ) )
Theorem	evl1var 19700	Polynomial evaluation maps the variable to the identity function. (Contributed by Mario Carneiro, 12-Jun-2015.)
|- O = (eval1 ` R )   &    |- X = (var1 ` R )   &    |- B = ( Base ` R )   =>    |- ( R e. CRing -> ( O ` X ) = ( _I |` B ) )