P. 196 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 19501-19600   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	mplmon2mul 19501*	Product of scaled monomials. (Contributed by Stefan O'Rear, 8-Mar-2015.)
⊢ 𝑃 = (𝐼 mPoly 𝑅)    &   ⊢ 𝐷 = {𝑓 ∈ (ℕ0 ↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝐶 = (Base‘𝑅)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ ∙ = (.r‘𝑃)    &   ⊢ · = (.r‘𝑅)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐷)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐷)    &   ⊢ (𝜑 → 𝐹 ∈ 𝐶)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐶)    ⇒   ⊢ (𝜑 → ((𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑋, 𝐹, 0 )) ∙ (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑌, 𝐺, 0 ))) = (𝑦 ∈ 𝐷 ↦ if(𝑦 = (𝑋 ∘𝑓 + 𝑌), (𝐹 · 𝐺), 0 )))
Theorem	mplind 19502*	Prove a property of polynomials by "structural" induction, under a simplified model of structure which loses the sum of products structure. The commutativity condition is stronger than strictly needed. (Contributed by Stefan O'Rear, 11-Mar-2015.)
⊢ 𝐾 = (Base‘𝑅)    &   ⊢ 𝑉 = (𝐼 mVar 𝑅)    &   ⊢ 𝑌 = (𝐼 mPoly 𝑅)    &   ⊢ + = (+g‘𝑌)    &   ⊢ · = (.r‘𝑌)    &   ⊢ 𝐶 = (algSc‘𝑌)    &   ⊢ 𝐵 = (Base‘𝑌)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐻 ∧ 𝑦 ∈ 𝐻)) → (𝑥 + 𝑦) ∈ 𝐻)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐻 ∧ 𝑦 ∈ 𝐻)) → (𝑥 · 𝑦) ∈ 𝐻)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐾) → (𝐶‘𝑥) ∈ 𝐻)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝑉‘𝑥) ∈ 𝐻)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐼 ∈ V)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    ⇒   ⊢ (𝜑 → 𝑋 ∈ 𝐻)
Theorem	mplcoe4 19503*	Decompose a polynomial into a finite sum of scaled monomials. (Contributed by Stefan O'Rear, 8-Mar-2015.)
⊢ 𝑃 = (𝐼 mPoly 𝑅)    &   ⊢ 𝐷 = {𝑓 ∈ (ℕ0 ↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → 𝑋 = (𝑃 Σg (𝑘 ∈ 𝐷 ↦ (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, (𝑋‘𝑘), 0 )))))
10.10.2  Polynomial evaluation
Syntax	ces 19504	Evaluation of a multivariate polynomial in a subring.
class evalSub
Syntax	cevl 19505	Evaluation of a multivariate polynomial.
class eval
Definition	df-evls 19506*	Define the evaluation map for the polynomial algebra. The function ((𝐼 evalSub 𝑆)‘𝑅):𝑉⟶(𝑆 ↑𝑚 (𝑆 ↑𝑚 𝐼)) makes sense when 𝐼 is an index set, 𝑆 is a ring, 𝑅 is a subring of 𝑆, and where 𝑉 is the set of polynomials in (𝐼 mPoly 𝑅). This function maps an element of the formal polynomial algebra (with coefficients in 𝑅) to a function from assignments 𝐼⟶𝑆 of the variables to elements of 𝑆 formed by evaluating the polynomial with the given assignments. (Contributed by Stefan O'Rear, 11-Mar-2015.)
⊢ evalSub = (𝑖 ∈ V, 𝑠 ∈ CRing ↦ ⦋(Base‘𝑠) / 𝑏⦌(𝑟 ∈ (SubRing‘𝑠) ↦ ⦋(𝑖 mPoly (𝑠 ↾s 𝑟)) / 𝑤⦌(℩𝑓 ∈ (𝑤 RingHom (𝑠 ↑s (𝑏 ↑𝑚 𝑖)))((𝑓 ∘ (algSc‘𝑤)) = (𝑥 ∈ 𝑟 ↦ ((𝑏 ↑𝑚 𝑖) × {𝑥})) ∧ (𝑓 ∘ (𝑖 mVar (𝑠 ↾s 𝑟))) = (𝑥 ∈ 𝑖 ↦ (𝑔 ∈ (𝑏 ↑𝑚 𝑖) ↦ (𝑔‘𝑥)))))))
Definition	df-evl 19507*	A simplification of evalSub when the evaluation ring is the same as the coefficient ring. (Contributed by Stefan O'Rear, 19-Mar-2015.)
⊢ eval = (𝑖 ∈ V, 𝑟 ∈ V ↦ ((𝑖 evalSub 𝑟)‘(Base‘𝑟)))
Theorem	evlslem4 19508*	The support of a tensor product of ring element families is contained in the product of the supports. (Contributed by Stefan O'Rear, 8-Mar-2015.) (Revised by AV, 18-Jul-2019.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝑋 ∈ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐽) → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐽 ∈ 𝑊)    ⇒   ⊢ (𝜑 → ((𝑥 ∈ 𝐼, 𝑦 ∈ 𝐽 ↦ (𝑋 · 𝑌)) supp 0 ) ⊆ (((𝑥 ∈ 𝐼 ↦ 𝑋) supp 0 ) × ((𝑦 ∈ 𝐽 ↦ 𝑌) supp 0 )))
Theorem	psrbagfsupp 19509*	Finite bags have finite nonzero-support. (Contributed by Stefan O'Rear, 9-Mar-2015.) (Revised by AV, 18-Jul-2019.)
⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑𝑚 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin}    ⇒   ⊢ ((𝑋 ∈ 𝐷 ∧ 𝐼 ∈ 𝑉) → 𝑋 finSupp 0)
Theorem	psrbagev1 19510*	A bag of multipliers provides the conditions for a valid sum. (Contributed by Stefan O'Rear, 9-Mar-2015.) (Revised by AV, 18-Jul-2019.)
⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑𝑚 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin}    &   ⊢ 𝐶 = (Base‘𝑇)    &   ⊢ · = (.g‘𝑇)    &   ⊢ 0 = (0g‘𝑇)    &   ⊢ (𝜑 → 𝑇 ∈ CMnd)    &   ⊢ (𝜑 → 𝐵 ∈ 𝐷)    &   ⊢ (𝜑 → 𝐺:𝐼⟶𝐶)    &   ⊢ (𝜑 → 𝐼 ∈ V)    ⇒   ⊢ (𝜑 → ((𝐵 ∘𝑓 · 𝐺):𝐼⟶𝐶 ∧ (𝐵 ∘𝑓 · 𝐺) finSupp 0 ))
Theorem	psrbagev2 19511*	Closure of a sum using a bag of multipliers. (Contributed by Stefan O'Rear, 9-Mar-2015.) (Proof shortened by AV, 18-Jul-2019.)
⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑𝑚 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin}    &   ⊢ 𝐶 = (Base‘𝑇)    &   ⊢ · = (.g‘𝑇)    &   ⊢ 0 = (0g‘𝑇)    &   ⊢ (𝜑 → 𝑇 ∈ CMnd)    &   ⊢ (𝜑 → 𝐵 ∈ 𝐷)    &   ⊢ (𝜑 → 𝐺:𝐼⟶𝐶)    &   ⊢ (𝜑 → 𝐼 ∈ V)    ⇒   ⊢ (𝜑 → (𝑇 Σg (𝐵 ∘𝑓 · 𝐺)) ∈ 𝐶)
Theorem	evlslem2 19512*	A linear function on the polynomial ring which is multiplicative on scaled monomials is generally multiplicative. (Contributed by Stefan O'Rear, 9-Mar-2015.)
⊢ 𝑃 = (𝐼 mPoly 𝑅)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ · = (.r‘𝑆)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑𝑚 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin}    &   ⊢ (𝜑 → 𝐼 ∈ V)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝑆 ∈ CRing)    &   ⊢ (𝜑 → 𝐸 ∈ (𝑃 GrpHom 𝑆))    &   ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑗 ∈ 𝐷 ∧ 𝑖 ∈ 𝐷))) → (𝐸‘(𝑘 ∈ 𝐷 ↦ if(𝑘 = (𝑗 ∘𝑓 + 𝑖), ((𝑥‘𝑗)(.r‘𝑅)(𝑦‘𝑖)), 0 ))) = ((𝐸‘(𝑘 ∈ 𝐷 ↦ if(𝑘 = 𝑗, (𝑥‘𝑗), 0 ))) · (𝐸‘(𝑘 ∈ 𝐷 ↦ if(𝑘 = 𝑖, (𝑦‘𝑖), 0 )))))    ⇒   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝐸‘(𝑥(.r‘𝑃)𝑦)) = ((𝐸‘𝑥) · (𝐸‘𝑦)))
Theorem	evlslem6 19513*	Lemma for evlseu 19516. Finiteness and consistency of the top-level sum. (Contributed by Stefan O'Rear, 9-Mar-2015.) (Revised by AV, 26-Jul-2019.)
⊢ 𝑃 = (𝐼 mPoly 𝑅)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 𝐶 = (Base‘𝑆)    &   ⊢ 𝐾 = (Base‘𝑅)    &   ⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑𝑚 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin}    &   ⊢ 𝑇 = (mulGrp‘𝑆)    &   ⊢ ↑ = (.g‘𝑇)    &   ⊢ · = (.r‘𝑆)    &   ⊢ 𝑉 = (𝐼 mVar 𝑅)    &   ⊢ 𝐸 = (𝑝 ∈ 𝐵 ↦ (𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑝‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓 ↑ 𝐺))))))    &   ⊢ (𝜑 → 𝐼 ∈ V)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝑆 ∈ CRing)    &   ⊢ (𝜑 → 𝐹 ∈ (𝑅 RingHom 𝑆))    &   ⊢ (𝜑 → 𝐺:𝐼⟶𝐶)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → ((𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑌‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓 ↑ 𝐺)))):𝐷⟶𝐶 ∧ (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑌‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓 ↑ 𝐺)))) finSupp (0g‘𝑆)))
Theorem	evlslem3 19514*	Lemma for evlseu 19516. Polynomial evaluation of a scaled monomial. (Contributed by Stefan O'Rear, 8-Mar-2015.)
⊢ 𝑃 = (𝐼 mPoly 𝑅)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 𝐶 = (Base‘𝑆)    &   ⊢ 𝐾 = (Base‘𝑅)    &   ⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑𝑚 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin}    &   ⊢ 𝑇 = (mulGrp‘𝑆)    &   ⊢ ↑ = (.g‘𝑇)    &   ⊢ · = (.r‘𝑆)    &   ⊢ 𝑉 = (𝐼 mVar 𝑅)    &   ⊢ 𝐸 = (𝑝 ∈ 𝐵 ↦ (𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑝‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓 ↑ 𝐺))))))    &   ⊢ (𝜑 → 𝐼 ∈ V)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝑆 ∈ CRing)    &   ⊢ (𝜑 → 𝐹 ∈ (𝑅 RingHom 𝑆))    &   ⊢ (𝜑 → 𝐺:𝐼⟶𝐶)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ (𝜑 → 𝐴 ∈ 𝐷)    &   ⊢ (𝜑 → 𝐻 ∈ 𝐾)    ⇒   ⊢ (𝜑 → (𝐸‘(𝑥 ∈ 𝐷 ↦ if(𝑥 = 𝐴, 𝐻, 0 ))) = ((𝐹‘𝐻) · (𝑇 Σg (𝐴 ∘𝑓 ↑ 𝐺))))
Theorem	evlslem1 19515*	Lemma for evlseu 19516, give a formula for (the unique) polynomial evaluation homomorphism. (Contributed by Stefan O'Rear, 9-Mar-2015.) (Proof shortened by AV, 26-Jul-2019.)
⊢ 𝑃 = (𝐼 mPoly 𝑅)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 𝐶 = (Base‘𝑆)    &   ⊢ 𝐾 = (Base‘𝑅)    &   ⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑𝑚 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin}    &   ⊢ 𝑇 = (mulGrp‘𝑆)    &   ⊢ ↑ = (.g‘𝑇)    &   ⊢ · = (.r‘𝑆)    &   ⊢ 𝑉 = (𝐼 mVar 𝑅)    &   ⊢ 𝐸 = (𝑝 ∈ 𝐵 ↦ (𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑝‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓 ↑ 𝐺))))))    &   ⊢ (𝜑 → 𝐼 ∈ V)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝑆 ∈ CRing)    &   ⊢ (𝜑 → 𝐹 ∈ (𝑅 RingHom 𝑆))    &   ⊢ (𝜑 → 𝐺:𝐼⟶𝐶)    &   ⊢ 𝐴 = (algSc‘𝑃)    ⇒   ⊢ (𝜑 → (𝐸 ∈ (𝑃 RingHom 𝑆) ∧ (𝐸 ∘ 𝐴) = 𝐹 ∧ (𝐸 ∘ 𝑉) = 𝐺))
Theorem	evlseu 19516*	For a given interpretation of the variables 𝐺 and of the scalars 𝐹, this extends to a homomorphic interpretation of the polynomial ring in exactly one way. (Contributed by Stefan O'Rear, 9-Mar-2015.)
⊢ 𝑃 = (𝐼 mPoly 𝑅)    &   ⊢ 𝐶 = (Base‘𝑆)    &   ⊢ 𝐴 = (algSc‘𝑃)    &   ⊢ 𝑉 = (𝐼 mVar 𝑅)    &   ⊢ (𝜑 → 𝐼 ∈ V)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝑆 ∈ CRing)    &   ⊢ (𝜑 → 𝐹 ∈ (𝑅 RingHom 𝑆))    &   ⊢ (𝜑 → 𝐺:𝐼⟶𝐶)    ⇒   ⊢ (𝜑 → ∃!𝑚 ∈ (𝑃 RingHom 𝑆)((𝑚 ∘ 𝐴) = 𝐹 ∧ (𝑚 ∘ 𝑉) = 𝐺))
Theorem	reldmevls 19517	Well-behaved binary operation property of evalSub. (Contributed by Stefan O'Rear, 19-Mar-2015.)
⊢ Rel dom evalSub
Theorem	mpfrcl 19518	Reverse closure for the set of polynomial functions. (Contributed by Stefan O'Rear, 19-Mar-2015.)
⊢ 𝑄 = ran ((𝐼 evalSub 𝑆)‘𝑅)    ⇒   ⊢ (𝑋 ∈ 𝑄 → (𝐼 ∈ V ∧ 𝑆 ∈ CRing ∧ 𝑅 ∈ (SubRing‘𝑆)))
Theorem	evlsval 19519*	Value of the polynomial evaluation map function. (Contributed by Stefan O'Rear, 11-Mar-2015.) (Revised by AV, 18-Sep-2021.)
⊢ 𝑄 = ((𝐼 evalSub 𝑆)‘𝑅)    &   ⊢ 𝑊 = (𝐼 mPoly 𝑈)    &   ⊢ 𝑉 = (𝐼 mVar 𝑈)    &   ⊢ 𝑈 = (𝑆 ↾s 𝑅)    &   ⊢ 𝑇 = (𝑆 ↑s (𝐵 ↑𝑚 𝐼))    &   ⊢ 𝐵 = (Base‘𝑆)    &   ⊢ 𝐴 = (algSc‘𝑊)    &   ⊢ 𝑋 = (𝑥 ∈ 𝑅 ↦ ((𝐵 ↑𝑚 𝐼) × {𝑥}))    &   ⊢ 𝑌 = (𝑥 ∈ 𝐼 ↦ (𝑔 ∈ (𝐵 ↑𝑚 𝐼) ↦ (𝑔‘𝑥)))    ⇒   ⊢ ((𝐼 ∈ 𝑍 ∧ 𝑆 ∈ CRing ∧ 𝑅 ∈ (SubRing‘𝑆)) → 𝑄 = (℩𝑓 ∈ (𝑊 RingHom 𝑇)((𝑓 ∘ 𝐴) = 𝑋 ∧ (𝑓 ∘ 𝑉) = 𝑌)))
Theorem	evlsval2 19520*	Characterizing properties of the polynomial evaluation map function. (Contributed by Stefan O'Rear, 12-Mar-2015.) (Revised by AV, 18-Sep-2021.)
⊢ 𝑄 = ((𝐼 evalSub 𝑆)‘𝑅)    &   ⊢ 𝑊 = (𝐼 mPoly 𝑈)    &   ⊢ 𝑉 = (𝐼 mVar 𝑈)    &   ⊢ 𝑈 = (𝑆 ↾s 𝑅)    &   ⊢ 𝑇 = (𝑆 ↑s (𝐵 ↑𝑚 𝐼))    &   ⊢ 𝐵 = (Base‘𝑆)    &   ⊢ 𝐴 = (algSc‘𝑊)    &   ⊢ 𝑋 = (𝑥 ∈ 𝑅 ↦ ((𝐵 ↑𝑚 𝐼) × {𝑥}))    &   ⊢ 𝑌 = (𝑥 ∈ 𝐼 ↦ (𝑔 ∈ (𝐵 ↑𝑚 𝐼) ↦ (𝑔‘𝑥)))    ⇒   ⊢ ((𝐼 ∈ 𝑍 ∧ 𝑆 ∈ CRing ∧ 𝑅 ∈ (SubRing‘𝑆)) → (𝑄 ∈ (𝑊 RingHom 𝑇) ∧ ((𝑄 ∘ 𝐴) = 𝑋 ∧ (𝑄 ∘ 𝑉) = 𝑌)))
Theorem	evlsrhm 19521	Polynomial evaluation is a homomorphism (into the product ring). (Contributed by Stefan O'Rear, 12-Mar-2015.)
⊢ 𝑄 = ((𝐼 evalSub 𝑆)‘𝑅)    &   ⊢ 𝑊 = (𝐼 mPoly 𝑈)    &   ⊢ 𝑈 = (𝑆 ↾s 𝑅)    &   ⊢ 𝑇 = (𝑆 ↑s (𝐵 ↑𝑚 𝐼))    &   ⊢ 𝐵 = (Base‘𝑆)    ⇒   ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑆 ∈ CRing ∧ 𝑅 ∈ (SubRing‘𝑆)) → 𝑄 ∈ (𝑊 RingHom 𝑇))
Theorem	evlssca 19522	Polynomial evaluation maps scalars to constant functions. (Contributed by Stefan O'Rear, 13-Mar-2015.) (Proof shortened by AV, 18-Sep-2021.)
⊢ 𝑄 = ((𝐼 evalSub 𝑆)‘𝑅)    &   ⊢ 𝑊 = (𝐼 mPoly 𝑈)    &   ⊢ 𝑈 = (𝑆 ↾s 𝑅)    &   ⊢ 𝐵 = (Base‘𝑆)    &   ⊢ 𝐴 = (algSc‘𝑊)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑆 ∈ CRing)    &   ⊢ (𝜑 → 𝑅 ∈ (SubRing‘𝑆))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑅)    ⇒   ⊢ (𝜑 → (𝑄‘(𝐴‘𝑋)) = ((𝐵 ↑𝑚 𝐼) × {𝑋}))
Theorem	evlsvar 19523*	Polynomial evaluation maps variables to projections. (Contributed by Stefan O'Rear, 12-Mar-2015.) (Proof shortened by AV, 18-Sep-2021.)
⊢ 𝑄 = ((𝐼 evalSub 𝑆)‘𝑅)    &   ⊢ 𝑉 = (𝐼 mVar 𝑈)    &   ⊢ 𝑈 = (𝑆 ↾s 𝑅)    &   ⊢ 𝐵 = (Base‘𝑆)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑆 ∈ CRing)    &   ⊢ (𝜑 → 𝑅 ∈ (SubRing‘𝑆))    &   ⊢ (𝜑 → 𝑋 ∈ 𝐼)    ⇒   ⊢ (𝜑 → (𝑄‘(𝑉‘𝑋)) = (𝑔 ∈ (𝐵 ↑𝑚 𝐼) ↦ (𝑔‘𝑋)))
Theorem	evlval 19524	Value of the simple/same ring evaluation map. (Contributed by Stefan O'Rear, 19-Mar-2015.) (Revised by Mario Carneiro, 12-Jun-2015.)
⊢ 𝑄 = (𝐼 eval 𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    ⇒   ⊢ 𝑄 = ((𝐼 evalSub 𝑅)‘𝐵)
Theorem	evlrhm 19525	The simple evaluation map is a ring homomorphism. (Contributed by Mario Carneiro, 12-Jun-2015.)
⊢ 𝑄 = (𝐼 eval 𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝑊 = (𝐼 mPoly 𝑅)    &   ⊢ 𝑇 = (𝑅 ↑s (𝐵 ↑𝑚 𝐼))    ⇒   ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑅 ∈ CRing) → 𝑄 ∈ (𝑊 RingHom 𝑇))
Theorem	evlsscasrng 19526	The evaluation of a scalar of a subring yields the same result as evaluated as a scalar over the ring itself. (Contributed by AV, 12-Sep-2019.)
⊢ 𝑄 = ((𝐼 evalSub 𝑆)‘𝑅)    &   ⊢ 𝑂 = (𝐼 eval 𝑆)    &   ⊢ 𝑊 = (𝐼 mPoly 𝑈)    &   ⊢ 𝑈 = (𝑆 ↾s 𝑅)    &   ⊢ 𝑃 = (𝐼 mPoly 𝑆)    &   ⊢ 𝐵 = (Base‘𝑆)    &   ⊢ 𝐴 = (algSc‘𝑊)    &   ⊢ 𝐶 = (algSc‘𝑃)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑆 ∈ CRing)    &   ⊢ (𝜑 → 𝑅 ∈ (SubRing‘𝑆))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑅)    ⇒   ⊢ (𝜑 → (𝑄‘(𝐴‘𝑋)) = (𝑂‘(𝐶‘𝑋)))
Theorem	evlsca 19527	Simple polynomial evaluation maps scalars to constant functions. (Contributed by AV, 12-Sep-2019.)
⊢ 𝑄 = (𝐼 eval 𝑆)    &   ⊢ 𝑊 = (𝐼 mPoly 𝑆)    &   ⊢ 𝐵 = (Base‘𝑆)    &   ⊢ 𝐴 = (algSc‘𝑊)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑆 ∈ CRing)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝑄‘(𝐴‘𝑋)) = ((𝐵 ↑𝑚 𝐼) × {𝑋}))
Theorem	evlsvarsrng 19528	The evaluation of the variable of polynomials over subring yields the same result as evaluated as variable of the polynomials over the ring itself. (Contributed by AV, 12-Sep-2019.)
⊢ 𝑄 = ((𝐼 evalSub 𝑆)‘𝑅)    &   ⊢ 𝑂 = (𝐼 eval 𝑆)    &   ⊢ 𝑉 = (𝐼 mVar 𝑈)    &   ⊢ 𝑈 = (𝑆 ↾s 𝑅)    &   ⊢ 𝐵 = (Base‘𝑆)    &   ⊢ (𝜑 → 𝐼 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑆 ∈ CRing)    &   ⊢ (𝜑 → 𝑅 ∈ (SubRing‘𝑆))    &   ⊢ (𝜑 → 𝑋 ∈ 𝐼)    ⇒   ⊢ (𝜑 → (𝑄‘(𝑉‘𝑋)) = (𝑂‘(𝑉‘𝑋)))
Theorem	evlvar 19529*	Simple polynomial evaluation maps variables to projections. (Contributed by AV, 12-Sep-2019.)
⊢ 𝑄 = (𝐼 eval 𝑆)    &   ⊢ 𝑉 = (𝐼 mVar 𝑆)    &   ⊢ 𝐵 = (Base‘𝑆)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑆 ∈ CRing)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐼)    ⇒   ⊢ (𝜑 → (𝑄‘(𝑉‘𝑋)) = (𝑔 ∈ (𝐵 ↑𝑚 𝐼) ↦ (𝑔‘𝑋)))
Theorem	mpfconst 19530	Constants are multivariate polynomial functions. (Contributed by Mario Carneiro, 19-Mar-2015.)
⊢ 𝐵 = (Base‘𝑆)    &   ⊢ 𝑄 = ran ((𝐼 evalSub 𝑆)‘𝑅)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑆 ∈ CRing)    &   ⊢ (𝜑 → 𝑅 ∈ (SubRing‘𝑆))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑅)    ⇒   ⊢ (𝜑 → ((𝐵 ↑𝑚 𝐼) × {𝑋}) ∈ 𝑄)
Theorem	mpfproj 19531*	Projections are multivariate polynomial functions. (Contributed by Mario Carneiro, 20-Mar-2015.)
⊢ 𝐵 = (Base‘𝑆)    &   ⊢ 𝑄 = ran ((𝐼 evalSub 𝑆)‘𝑅)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑆 ∈ CRing)    &   ⊢ (𝜑 → 𝑅 ∈ (SubRing‘𝑆))    &   ⊢ (𝜑 → 𝐽 ∈ 𝐼)    ⇒   ⊢ (𝜑 → (𝑓 ∈ (𝐵 ↑𝑚 𝐼) ↦ (𝑓‘𝐽)) ∈ 𝑄)
Theorem	mpfsubrg 19532	Polynomial functions are a subring. (Contributed by Mario Carneiro, 19-Mar-2015.) (Revised by Mario Carneiro, 6-May-2015.) (Revised by AV, 19-Sep-2021.)
⊢ 𝑄 = ran ((𝐼 evalSub 𝑆)‘𝑅)    ⇒   ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑆 ∈ CRing ∧ 𝑅 ∈ (SubRing‘𝑆)) → 𝑄 ∈ (SubRing‘(𝑆 ↑s ((Base‘𝑆) ↑𝑚 𝐼))))
Theorem	mpff 19533	Polynomial functions are functions. (Contributed by Mario Carneiro, 19-Mar-2015.)
⊢ 𝑄 = ran ((𝐼 evalSub 𝑆)‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑆)    ⇒   ⊢ (𝐹 ∈ 𝑄 → 𝐹:(𝐵 ↑𝑚 𝐼)⟶𝐵)
Theorem	mpfaddcl 19534	The sum of multivariate polynomial functions. (Contributed by Mario Carneiro, 19-Mar-2015.)
⊢ 𝑄 = ran ((𝐼 evalSub 𝑆)‘𝑅)    &   ⊢ + = (+g‘𝑆)    ⇒   ⊢ ((𝐹 ∈ 𝑄 ∧ 𝐺 ∈ 𝑄) → (𝐹 ∘𝑓 + 𝐺) ∈ 𝑄)
Theorem	mpfmulcl 19535	The product of multivariate polynomial functions. (Contributed by Mario Carneiro, 19-Mar-2015.)
⊢ 𝑄 = ran ((𝐼 evalSub 𝑆)‘𝑅)    &   ⊢ · = (.r‘𝑆)    ⇒   ⊢ ((𝐹 ∈ 𝑄 ∧ 𝐺 ∈ 𝑄) → (𝐹 ∘𝑓 · 𝐺) ∈ 𝑄)
Theorem	mpfind 19536*	Prove a property of polynomials by "structural" induction, under a simplified model of structure which loses the sum of products structure. (Contributed by Mario Carneiro, 19-Mar-2015.)
⊢ 𝐵 = (Base‘𝑆)    &   ⊢ + = (+g‘𝑆)    &   ⊢ · = (.r‘𝑆)    &   ⊢ 𝑄 = ran ((𝐼 evalSub 𝑆)‘𝑅)    &   ⊢ ((𝜑 ∧ ((𝑓 ∈ 𝑄 ∧ 𝜏) ∧ (𝑔 ∈ 𝑄 ∧ 𝜂))) → 𝜁)    &   ⊢ ((𝜑 ∧ ((𝑓 ∈ 𝑄 ∧ 𝜏) ∧ (𝑔 ∈ 𝑄 ∧ 𝜂))) → 𝜎)    &   ⊢ (𝑥 = ((𝐵 ↑𝑚 𝐼) × {𝑓}) → (𝜓 ↔ 𝜒))    &   ⊢ (𝑥 = (𝑔 ∈ (𝐵 ↑𝑚 𝐼) ↦ (𝑔‘𝑓)) → (𝜓 ↔ 𝜃))    &   ⊢ (𝑥 = 𝑓 → (𝜓 ↔ 𝜏))    &   ⊢ (𝑥 = 𝑔 → (𝜓 ↔ 𝜂))    &   ⊢ (𝑥 = (𝑓 ∘𝑓 + 𝑔) → (𝜓 ↔ 𝜁))    &   ⊢ (𝑥 = (𝑓 ∘𝑓 · 𝑔) → (𝜓 ↔ 𝜎))    &   ⊢ (𝑥 = 𝐴 → (𝜓 ↔ 𝜌))    &   ⊢ ((𝜑 ∧ 𝑓 ∈ 𝑅) → 𝜒)    &   ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐼) → 𝜃)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑄)    ⇒   ⊢ (𝜑 → 𝜌)
10.10.3  Additional definitions for (multivariate) polynomials Remark: There are no theorems using these definitions yet!
Syntax	cmhp 19537	Multivariate polynomials.
class mHomP
Syntax	cpsd 19538	Power series partial derivative function.
class mPSDer
Syntax	cslv 19539	Select a subset of variables in a multivariate polynomial.
class selectVars
Syntax	cai 19540	Algebraically independent.
class AlgInd
Definition	df-mhp 19541*	Define the subspaces of order- 𝑛 homogeneous polynomials. (Contributed by Mario Carneiro, 21-Mar-2015.)
⊢ mHomP = (𝑖 ∈ V, 𝑟 ∈ V ↦ (𝑛 ∈ ℕ0 ↦ {𝑓 ∈ (Base‘(𝑖 mPoly 𝑟)) ∣ (𝑓 supp (0g‘𝑟)) ⊆ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑𝑚 𝑖) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ Σ𝑗 ∈ ℕ0 (𝑔‘𝑗) = 𝑛}}))
Definition	df-psd 19542*	Define the differentiation operation on multivariate polynomials. (Contributed by Mario Carneiro, 21-Mar-2015.)
⊢ mPSDer = (𝑖 ∈ V, 𝑟 ∈ V ↦ (𝑥 ∈ 𝑖 ↦ (𝑓 ∈ (Base‘(𝑖 mPwSer 𝑟)) ↦ (𝑘 ∈ {ℎ ∈ (ℕ0 ↑𝑚 𝑖) ∣ (◡ℎ “ ℕ) ∈ Fin} ↦ (((𝑘‘𝑥) + 1)(.g‘𝑟)(𝑓‘(𝑘 ∘𝑓 + (𝑦 ∈ 𝑖 ↦ if(𝑦 = 𝑥, 1, 0)))))))))
Definition	df-selv 19543*	Define the "variable selection" function. The function ((𝐼 selectVars 𝑅)‘𝐽) maps elements of (𝐼 mPoly 𝑅) bijectively onto (𝐽 mPoly ((𝐼 ∖ 𝐽) mPoly 𝑅)) in the natural way, for example if 𝐼 = {𝑥, 𝑦} and 𝐽 = {𝑦} it would map 1 + 𝑥 + 𝑦 + 𝑥𝑦 ∈ ({𝑥, 𝑦} mPoly ℤ) to (1 + 𝑥) + (1 + 𝑥)𝑦 ∈ ({𝑦} mPoly ({𝑥} mPoly ℤ)). This, for example, allows one to treat a multivariate polynomial as a univariate polynomial with coefficients in a polynomial ring with one less variable. (Contributed by Mario Carneiro, 21-Mar-2015.)
⊢ selectVars = (𝑖 ∈ V, 𝑟 ∈ V ↦ (𝑗 ∈ 𝒫 𝑖 ↦ (𝑓 ∈ (𝑖 mPoly 𝑟) ↦ ⦋((𝑖 ∖ 𝑗) mPoly 𝑟) / 𝑠⦌⦋(𝑥 ∈ (Scalar‘𝑠) ↦ (𝑥( ·𝑠 ‘𝑠)(1r‘𝑠))) / 𝑐⦌((((𝑖 evalSub 𝑠)‘(𝑐 “s 𝑟))‘(𝑐 ∘ 𝑓))‘(𝑥 ∈ 𝑖 ↦ if(𝑥 ∈ 𝑗, ((𝑗 mVar ((𝑖 ∖ 𝑗) mPoly 𝑟))‘𝑥), (𝑐 ∘ (((𝑖 ∖ 𝑗) mVar 𝑟)‘𝑥))))))))
Definition	df-algind 19544*	Define the predicate "the set 𝑣 is algebraically independent in the algebra 𝑤". A collection of vectors is algebraically independent if no nontrivial polynomial with elements from the subset evaluates to zero. (Contributed by Mario Carneiro, 21-Mar-2015.)
⊢ AlgInd = (𝑤 ∈ V, 𝑘 ∈ 𝒫 (Base‘𝑤) ↦ {𝑣 ∈ 𝒫 (Base‘𝑤) ∣ Fun ◡(𝑓 ∈ (Base‘(𝑣 mPoly (𝑤 ↾s 𝑘))) ↦ ((((𝑣 evalSub 𝑤)‘𝑘)‘𝑓)‘( I ↾ 𝑣)))})
10.10.4  Univariate polynomials According to Wikipedia ("Polynomial", 23-Dec-2019, https://en.wikipedia.org/wiki/Polynomial) "A polynomial in one indeterminate is called a univariate polynomial, a polynomial in more than one indeterminate is called a multivariate polynomial." In this sense univariate polynomials are defined as multivariate polynomials restricted to one indeterminate/polynomial variable in the following, see ply1bascl2 19574. According to the definition in Wikipedia "a polynomial can either be zero or can be written as the sum of a finite number of nonzero terms. Each term consists of the product of a number - called the coefficient of the term - and a finite number of indeterminates, raised to nonnegative integer powers.". By this, a term of a univariate polynomial (often also called "polynomial term") is the product of a coefficient (usually a member of the underlying ring) and the variable, raised to a nonnegative integer power. A (univariate) polynomial which has only one term is called (univariate) monomial - therefore, the notions "term" and "monomial" are often used synonymously, see also the definition in [Lang] p. 102. Sometimes, however, a monomial is defined as power product, "a product of powers of variables with nonnegative integer exponents", see Wikipedia ("Monomial", 23-Dec-2019, https://en.wikipedia.org/wiki/Mononomial). In [Lang] p. 101, such terms are called "primitive monomials". To avoid any ambiguity, the notion "primitive monomial" is used for such power products ("x^i") in the following, whereas the synonym for "term" ("ai x^i") will be "scaled monomial".
Syntax	cps1 19545	Univariate power series.
class PwSer1
Syntax	cv1 19546	The base variable of a univariate power series.
class var1
Syntax	cpl1 19547	Univariate polynomials.
class Poly1
Syntax	cco1 19548	Coefficient function for a univariate polynomial.
class coe1
Syntax	ctp1 19549	Convert a univariate polynomial representation to multivariate.
class toPoly1
Definition	df-psr1 19550	Define the algebra of univariate power series. (Contributed by Mario Carneiro, 29-Dec-2014.)
⊢ PwSer1 = (𝑟 ∈ V ↦ ((1𝑜 ordPwSer 𝑟)‘∅))
Definition	df-vr1 19551	Define the base element of a univariate power series (the 𝑋 element of the set 𝑅[𝑋] of polynomials and also the 𝑋 in the set 𝑅[[𝑋]] of power series). (Contributed by Mario Carneiro, 8-Feb-2015.)
⊢ var1 = (𝑟 ∈ V ↦ ((1𝑜 mVar 𝑟)‘∅))
Definition	df-ply1 19552	Define the algebra of univariate polynomials. (Contributed by Mario Carneiro, 9-Feb-2015.)
⊢ Poly1 = (𝑟 ∈ V ↦ ((PwSer1‘𝑟) ↾s (Base‘(1𝑜 mPoly 𝑟))))
Definition	df-coe1 19553*	Define the coefficient function for a univariate polynomial. (Contributed by Stefan O'Rear, 21-Mar-2015.)
⊢ coe1 = (𝑓 ∈ V ↦ (𝑛 ∈ ℕ0 ↦ (𝑓‘(1𝑜 × {𝑛}))))
Definition	df-toply1 19554*	Define a function which maps a coefficient function for a univariate polynomial to the corresponding polynomial object. (Contributed by Mario Carneiro, 12-Jun-2015.)
⊢ toPoly1 = (𝑓 ∈ V ↦ (𝑛 ∈ (ℕ0 ↑𝑚 1𝑜) ↦ (𝑓‘(𝑛‘∅))))
Theorem	psr1baslem 19555	The set of finite bags on 1𝑜 is just the set of all functions from 1𝑜 to ℕ0. (Contributed by Mario Carneiro, 9-Feb-2015.)
⊢ (ℕ0 ↑𝑚 1𝑜) = {𝑓 ∈ (ℕ0 ↑𝑚 1𝑜) ∣ (◡𝑓 “ ℕ) ∈ Fin}
Theorem	psr1val 19556	Value of the ring of univariate power series. (Contributed by Mario Carneiro, 8-Feb-2015.)
⊢ 𝑆 = (PwSer1‘𝑅)    ⇒   ⊢ 𝑆 = ((1𝑜 ordPwSer 𝑅)‘∅)
Theorem	psr1crng 19557	The ring of univariate power series is a commutative ring. (Contributed by Mario Carneiro, 8-Feb-2015.)
⊢ 𝑆 = (PwSer1‘𝑅)    ⇒   ⊢ (𝑅 ∈ CRing → 𝑆 ∈ CRing)
Theorem	psr1assa 19558	The ring of univariate power series is an associative algebra. (Contributed by Mario Carneiro, 8-Feb-2015.)
⊢ 𝑆 = (PwSer1‘𝑅)    ⇒   ⊢ (𝑅 ∈ CRing → 𝑆 ∈ AssAlg)
Theorem	psr1tos 19559	The ordered power series structure is a totally ordered set. (Contributed by Mario Carneiro, 2-Jun-2015.)
⊢ 𝑆 = (PwSer1‘𝑅)    ⇒   ⊢ (𝑅 ∈ Toset → 𝑆 ∈ Toset)
Theorem	psr1bas2 19560	The base set of the ring of univariate power series. (Contributed by Mario Carneiro, 3-Jul-2015.)
⊢ 𝑆 = (PwSer1‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑆)    &   ⊢ 𝑂 = (1𝑜 mPwSer 𝑅)    ⇒   ⊢ 𝐵 = (Base‘𝑂)
Theorem	psr1bas 19561	The base set of the ring of univariate power series. (Contributed by Mario Carneiro, 8-Feb-2015.)
⊢ 𝑆 = (PwSer1‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑆)    &   ⊢ 𝐾 = (Base‘𝑅)    ⇒   ⊢ 𝐵 = (𝐾 ↑𝑚 (ℕ0 ↑𝑚 1𝑜))
Theorem	vr1val 19562	The value of the generator of the power series algebra (the 𝑋 in 𝑅[[𝑋]]). Since all univariate polynomial rings over a fixed base ring 𝑅 are isomorphic, we don't bother to pass this in as a parameter; internally we are actually using the empty set as this generator and 1𝑜 = {∅} is the index set (but for most purposes this choice should not be visible anyway). (Contributed by Mario Carneiro, 8-Feb-2015.) (Revised by Mario Carneiro, 12-Jun-2015.)
⊢ 𝑋 = (var1‘𝑅)    ⇒   ⊢ 𝑋 = ((1𝑜 mVar 𝑅)‘∅)
Theorem	vr1cl2 19563	The variable 𝑋 is a member of the power series algebra 𝑅[[𝑋]]. (Contributed by Mario Carneiro, 8-Feb-2015.)
⊢ 𝑋 = (var1‘𝑅)    &   ⊢ 𝑆 = (PwSer1‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑆)    ⇒   ⊢ (𝑅 ∈ Ring → 𝑋 ∈ 𝐵)
Theorem	ply1val 19564	The value of the set of univariate polynomials. (Contributed by Mario Carneiro, 9-Feb-2015.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝑆 = (PwSer1‘𝑅)    ⇒   ⊢ 𝑃 = (𝑆 ↾s (Base‘(1𝑜 mPoly 𝑅)))
Theorem	ply1bas 19565	The value of the base set of univariate polynomials. (Contributed by Mario Carneiro, 9-Feb-2015.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝑆 = (PwSer1‘𝑅)    &   ⊢ 𝑈 = (Base‘𝑃)    ⇒   ⊢ 𝑈 = (Base‘(1𝑜 mPoly 𝑅))
Theorem	ply1lss 19566	Univariate polynomials form a linear subspace of the set of univariate power series. (Contributed by Mario Carneiro, 9-Feb-2015.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝑆 = (PwSer1‘𝑅)    &   ⊢ 𝑈 = (Base‘𝑃)    ⇒   ⊢ (𝑅 ∈ Ring → 𝑈 ∈ (LSubSp‘𝑆))
Theorem	ply1subrg 19567	Univariate polynomials form a subring of the set of univariate power series. (Contributed by Mario Carneiro, 9-Feb-2015.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝑆 = (PwSer1‘𝑅)    &   ⊢ 𝑈 = (Base‘𝑃)    ⇒   ⊢ (𝑅 ∈ Ring → 𝑈 ∈ (SubRing‘𝑆))
Theorem	ply1crng 19568	The ring of univariate polynomials is a commutative ring. (Contributed by Mario Carneiro, 9-Feb-2015.)
⊢ 𝑃 = (Poly1‘𝑅)    ⇒   ⊢ (𝑅 ∈ CRing → 𝑃 ∈ CRing)
Theorem	ply1assa 19569	The ring of univariate polynomials is an associative algebra. (Contributed by Mario Carneiro, 9-Feb-2015.)
⊢ 𝑃 = (Poly1‘𝑅)    ⇒   ⊢ (𝑅 ∈ CRing → 𝑃 ∈ AssAlg)
Theorem	psr1bascl 19570	A univariate power series is a multivariate power series on one index. (Contributed by Stefan O'Rear, 25-Mar-2015.)
⊢ 𝑃 = (PwSer1‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑃)    ⇒   ⊢ (𝐹 ∈ 𝐵 → 𝐹 ∈ (Base‘(1𝑜 mPwSer 𝑅)))
Theorem	psr1basf 19571	Univariate power series base set elements are functions. (Contributed by Stefan O'Rear, 25-Mar-2015.)
⊢ 𝑃 = (PwSer1‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 𝐾 = (Base‘𝑅)    ⇒   ⊢ (𝐹 ∈ 𝐵 → 𝐹:(ℕ0 ↑𝑚 1𝑜)⟶𝐾)
Theorem	ply1basf 19572	Univariate polynomial base set elements are functions. (Contributed by Stefan O'Rear, 21-Mar-2015.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 𝐾 = (Base‘𝑅)    ⇒   ⊢ (𝐹 ∈ 𝐵 → 𝐹:(ℕ0 ↑𝑚 1𝑜)⟶𝐾)
Theorem	ply1bascl 19573	A univariate polynomial is a univariate power series. (Contributed by Stefan O'Rear, 25-Mar-2015.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑃)    ⇒   ⊢ (𝐹 ∈ 𝐵 → 𝐹 ∈ (Base‘(PwSer1‘𝑅)))
Theorem	ply1bascl2 19574	A univariate polynomial is a multivariate polynomial on one index. (Contributed by Stefan O'Rear, 25-Mar-2015.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑃)    ⇒   ⊢ (𝐹 ∈ 𝐵 → 𝐹 ∈ (Base‘(1𝑜 mPoly 𝑅)))
Theorem	coe1fval 19575*	Value of the univariate polynomial coefficient function. (Contributed by Stefan O'Rear, 21-Mar-2015.)
⊢ 𝐴 = (coe1‘𝐹)    ⇒   ⊢ (𝐹 ∈ 𝑉 → 𝐴 = (𝑛 ∈ ℕ0 ↦ (𝐹‘(1𝑜 × {𝑛}))))
Theorem	coe1fv 19576	Value of an evaluated coefficient in a polynomial coefficient vector. (Contributed by Stefan O'Rear, 21-Mar-2015.)
⊢ 𝐴 = (coe1‘𝐹)    ⇒   ⊢ ((𝐹 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) → (𝐴‘𝑁) = (𝐹‘(1𝑜 × {𝑁})))
Theorem	fvcoe1 19577	Value of a multivariate coefficient in terms of the coefficient vector. (Contributed by Stefan O'Rear, 21-Mar-2015.)
⊢ 𝐴 = (coe1‘𝐹)    ⇒   ⊢ ((𝐹 ∈ 𝑉 ∧ 𝑋 ∈ (ℕ0 ↑𝑚 1𝑜)) → (𝐹‘𝑋) = (𝐴‘(𝑋‘∅)))
Theorem	coe1fval3 19578*	Univariate power series coefficient vectors expressed as a function composition. (Contributed by Stefan O'Rear, 25-Mar-2015.)
⊢ 𝐴 = (coe1‘𝐹)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 𝑃 = (PwSer1‘𝑅)    &   ⊢ 𝐺 = (𝑦 ∈ ℕ0 ↦ (1𝑜 × {𝑦}))    ⇒   ⊢ (𝐹 ∈ 𝐵 → 𝐴 = (𝐹 ∘ 𝐺))
Theorem	coe1f2 19579	Functionality of univariate power series coefficient vectors. (Contributed by Stefan O'Rear, 25-Mar-2015.)
⊢ 𝐴 = (coe1‘𝐹)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 𝑃 = (PwSer1‘𝑅)    &   ⊢ 𝐾 = (Base‘𝑅)    ⇒   ⊢ (𝐹 ∈ 𝐵 → 𝐴:ℕ0⟶𝐾)
Theorem	coe1fval2 19580*	Univariate polynomial coefficient vectors expressed as a function composition. (Contributed by Stefan O'Rear, 21-Mar-2015.)
⊢ 𝐴 = (coe1‘𝐹)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐺 = (𝑦 ∈ ℕ0 ↦ (1𝑜 × {𝑦}))    ⇒   ⊢ (𝐹 ∈ 𝐵 → 𝐴 = (𝐹 ∘ 𝐺))
Theorem	coe1f 19581	Functionality of univariate polynomial coefficient vectors. (Contributed by Stefan O'Rear, 21-Mar-2015.)
⊢ 𝐴 = (coe1‘𝐹)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐾 = (Base‘𝑅)    ⇒   ⊢ (𝐹 ∈ 𝐵 → 𝐴:ℕ0⟶𝐾)
Theorem	coe1fvalcl 19582	A coefficient of a univariate polynomial over a class/ring is an element of this class/ring. (Contributed by AV, 9-Oct-2019.)
⊢ 𝐴 = (coe1‘𝐹)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐾 = (Base‘𝑅)    ⇒   ⊢ ((𝐹 ∈ 𝐵 ∧ 𝑁 ∈ ℕ0) → (𝐴‘𝑁) ∈ 𝐾)
Theorem	coe1sfi 19583	Finite support of univariate polynomial coefficient vectors. (Contributed by Stefan O'Rear, 21-Mar-2015.) (Revised by AV, 19-Jul-2019.)
⊢ 𝐴 = (coe1‘𝐹)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    ⇒   ⊢ (𝐹 ∈ 𝐵 → 𝐴 finSupp 0 )
Theorem	coe1fsupp 19584*	The coefficient vector of a univariate polynomial is a finitely supported mapping from the nonnegative integers to the elements of the coefficient class/ring for the polynomial. (Contributed by AV, 3-Oct-2019.)
⊢ 𝐴 = (coe1‘𝐹)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝐾 = (Base‘𝑅)    ⇒   ⊢ (𝐹 ∈ 𝐵 → 𝐴 ∈ {𝑔 ∈ (𝐾 ↑𝑚 ℕ0) ∣ 𝑔 finSupp 0 })
Theorem	mptcoe1fsupp 19585*	A mapping involving coefficients of polynomials is finitely supported. (Contributed by AV, 12-Oct-2019.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 0 = (0g‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → (𝑘 ∈ ℕ0 ↦ ((coe1‘𝑀)‘𝑘)) finSupp 0 )
Theorem	coe1ae0 19586*	The coefficient vector of a univariate polynomial is 0 almost everywhere. (Contributed by AV, 19-Oct-2019.)
⊢ 𝐴 = (coe1‘𝐹)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    ⇒   ⊢ (𝐹 ∈ 𝐵 → ∃𝑠 ∈ ℕ0 ∀𝑛 ∈ ℕ0 (𝑠 < 𝑛 → (𝐴‘𝑛) = 0 ))
Theorem	vr1cl 19587	The generator of a univariate polynomial algebra is contained in the base set. (Contributed by Stefan O'Rear, 19-Mar-2015.)
⊢ 𝑋 = (var1‘𝑅)    &   ⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑃)    ⇒   ⊢ (𝑅 ∈ Ring → 𝑋 ∈ 𝐵)
Theorem	opsr0 19588	Zero in the ordered power series ring. (Contributed by Stefan O'Rear, 23-Mar-2015.) (Revised by Mario Carneiro, 2-Oct-2015.)
⊢ 𝑆 = (𝐼 mPwSer 𝑅)    &   ⊢ 𝑂 = ((𝐼 ordPwSer 𝑅)‘𝑇)    &   ⊢ (𝜑 → 𝑇 ⊆ (𝐼 × 𝐼))    ⇒   ⊢ (𝜑 → (0g‘𝑆) = (0g‘𝑂))
Theorem	opsr1 19589	One in the ordered power series ring. (Contributed by Stefan O'Rear, 23-Mar-2015.) (Revised by Mario Carneiro, 2-Oct-2015.)
⊢ 𝑆 = (𝐼 mPwSer 𝑅)    &   ⊢ 𝑂 = ((𝐼 ordPwSer 𝑅)‘𝑇)    &   ⊢ (𝜑 → 𝑇 ⊆ (𝐼 × 𝐼))    ⇒   ⊢ (𝜑 → (1r‘𝑆) = (1r‘𝑂))
Theorem	mplplusg 19590	Value of addition in a polynomial ring. (Contributed by Stefan O'Rear, 21-Mar-2015.) (Revised by Mario Carneiro, 2-Oct-2015.)
⊢ 𝑌 = (𝐼 mPoly 𝑅)    &   ⊢ 𝑆 = (𝐼 mPwSer 𝑅)    &   ⊢ + = (+g‘𝑌)    ⇒   ⊢ + = (+g‘𝑆)
Theorem	mplmulr 19591	Value of multiplication in a polynomial ring. (Contributed by Stefan O'Rear, 21-Mar-2015.) (Revised by Mario Carneiro, 2-Oct-2015.)
⊢ 𝑌 = (𝐼 mPoly 𝑅)    &   ⊢ 𝑆 = (𝐼 mPwSer 𝑅)    &   ⊢ · = (.r‘𝑌)    ⇒   ⊢ · = (.r‘𝑆)
Theorem	psr1plusg 19592	Value of addition in a univariate power series ring. (Contributed by Stefan O'Rear, 21-Mar-2015.) (Revised by Mario Carneiro, 2-Oct-2015.)
⊢ 𝑌 = (PwSer1‘𝑅)    &   ⊢ 𝑆 = (1𝑜 mPwSer 𝑅)    &   ⊢ + = (+g‘𝑌)    ⇒   ⊢ + = (+g‘𝑆)
Theorem	psr1vsca 19593	Value of scalar multiplication in a univariate power series ring. (Contributed by Stefan O'Rear, 21-Mar-2015.) (Revised by Mario Carneiro, 2-Oct-2015.)
⊢ 𝑌 = (PwSer1‘𝑅)    &   ⊢ 𝑆 = (1𝑜 mPwSer 𝑅)    &   ⊢ · = ( ·𝑠 ‘𝑌)    ⇒   ⊢ · = ( ·𝑠 ‘𝑆)
Theorem	psr1mulr 19594	Value of multiplication in a univariate power series ring. (Contributed by Stefan O'Rear, 21-Mar-2015.) (Revised by Mario Carneiro, 2-Oct-2015.)
⊢ 𝑌 = (PwSer1‘𝑅)    &   ⊢ 𝑆 = (1𝑜 mPwSer 𝑅)    &   ⊢ · = (.r‘𝑌)    ⇒   ⊢ · = (.r‘𝑆)
Theorem	ply1plusg 19595	Value of addition in a univariate polynomial ring. (Contributed by Stefan O'Rear, 21-Mar-2015.) (Revised by Mario Carneiro, 4-Jul-2015.)
⊢ 𝑌 = (Poly1‘𝑅)    &   ⊢ 𝑆 = (1𝑜 mPoly 𝑅)    &   ⊢ + = (+g‘𝑌)    ⇒   ⊢ + = (+g‘𝑆)
Theorem	ply1vsca 19596	Value of scalar multiplication in a univariate polynomial ring. (Contributed by Stefan O'Rear, 21-Mar-2015.) (Revised by Mario Carneiro, 4-Jul-2015.)
⊢ 𝑌 = (Poly1‘𝑅)    &   ⊢ 𝑆 = (1𝑜 mPoly 𝑅)    &   ⊢ · = ( ·𝑠 ‘𝑌)    ⇒   ⊢ · = ( ·𝑠 ‘𝑆)
Theorem	ply1mulr 19597	Value of multiplication in a univariate polynomial ring. (Contributed by Stefan O'Rear, 21-Mar-2015.) (Revised by Mario Carneiro, 4-Jul-2015.)
⊢ 𝑌 = (Poly1‘𝑅)    &   ⊢ 𝑆 = (1𝑜 mPoly 𝑅)    &   ⊢ · = (.r‘𝑌)    ⇒   ⊢ · = (.r‘𝑆)
Theorem	ressply1bas2 19598	The base set of a restricted polynomial algebra consists of power series in the subring which are also polynomials (in the parent ring). (Contributed by Mario Carneiro, 3-Jul-2015.)
⊢ 𝑆 = (Poly1‘𝑅)    &   ⊢ 𝐻 = (𝑅 ↾s 𝑇)    &   ⊢ 𝑈 = (Poly1‘𝐻)    &   ⊢ 𝐵 = (Base‘𝑈)    &   ⊢ (𝜑 → 𝑇 ∈ (SubRing‘𝑅))    &   ⊢ 𝑊 = (PwSer1‘𝐻)    &   ⊢ 𝐶 = (Base‘𝑊)    &   ⊢ 𝐾 = (Base‘𝑆)    ⇒   ⊢ (𝜑 → 𝐵 = (𝐶 ∩ 𝐾))
Theorem	ressply1bas 19599	A restricted polynomial algebra has the same base set. (Contributed by Mario Carneiro, 3-Jul-2015.)
⊢ 𝑆 = (Poly1‘𝑅)    &   ⊢ 𝐻 = (𝑅 ↾s 𝑇)    &   ⊢ 𝑈 = (Poly1‘𝐻)    &   ⊢ 𝐵 = (Base‘𝑈)    &   ⊢ (𝜑 → 𝑇 ∈ (SubRing‘𝑅))    &   ⊢ 𝑃 = (𝑆 ↾s 𝐵)    ⇒   ⊢ (𝜑 → 𝐵 = (Base‘𝑃))
Theorem	ressply1add 19600	A restricted polynomial algebra has the same addition operation. (Contributed by Mario Carneiro, 3-Jul-2015.)
⊢ 𝑆 = (Poly1‘𝑅)    &   ⊢ 𝐻 = (𝑅 ↾s 𝑇)    &   ⊢ 𝑈 = (Poly1‘𝐻)    &   ⊢ 𝐵 = (Base‘𝑈)    &   ⊢ (𝜑 → 𝑇 ∈ (SubRing‘𝑅))    &   ⊢ 𝑃 = (𝑆 ↾s 𝐵)    ⇒   ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝑋(+g‘𝑈)𝑌) = (𝑋(+g‘𝑃)𝑌))