P. 225 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 22401-22500   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	mpff 22401	Polynomial functions are functions. (Contributed by Mario Carneiro, 19-Mar-2015.)
⊢ 𝑄 = ran ((𝐼 evalSub 𝑆)‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑆)    ⇒   ⊢ (𝐹 ∈ 𝑄 → 𝐹:(𝐵 ↑m 𝐼)⟶𝐵)
Theorem	mpfaddcl 22402	The sum of multivariate polynomial functions. (Contributed by Mario Carneiro, 19-Mar-2015.)
⊢ 𝑄 = ran ((𝐼 evalSub 𝑆)‘𝑅)    &   ⊢ + = (+g‘𝑆)    ⇒   ⊢ ((𝐹 ∈ 𝑄 ∧ 𝐺 ∈ 𝑄) → (𝐹 ∘f + 𝐺) ∈ 𝑄)
Theorem	mpfmulcl 22403	The product of multivariate polynomial functions. (Contributed by Mario Carneiro, 19-Mar-2015.)
⊢ 𝑄 = ran ((𝐼 evalSub 𝑆)‘𝑅)    &   ⊢ · = (.r‘𝑆)    ⇒   ⊢ ((𝐹 ∈ 𝑄 ∧ 𝐺 ∈ 𝑄) → (𝐹 ∘f · 𝐺) ∈ 𝑄)
Theorem	mpfind 22404*	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 𝑆)‘𝑅)    &   ⊢ ((𝜑 ∧ ((𝑓 ∈ 𝑄 ∧ 𝜏) ∧ (𝑔 ∈ 𝑄 ∧ 𝜂))) → 𝜁)    &   ⊢ ((𝜑 ∧ ((𝑓 ∈ 𝑄 ∧ 𝜏) ∧ (𝑔 ∈ 𝑄 ∧ 𝜂))) → 𝜎)    &   ⊢ (𝑥 = ((𝐵 ↑m 𝐼) × {𝑓}) → (𝜓 ↔ 𝜒))    &   ⊢ (𝑥 = (𝑔 ∈ (𝐵 ↑m 𝐼) ↦ (𝑔‘𝑓)) → (𝜓 ↔ 𝜃))    &   ⊢ (𝑥 = 𝑓 → (𝜓 ↔ 𝜏))    &   ⊢ (𝑥 = 𝑔 → (𝜓 ↔ 𝜂))    &   ⊢ (𝑥 = (𝑓 ∘f + 𝑔) → (𝜓 ↔ 𝜁))    &   ⊢ (𝑥 = (𝑓 ∘f · 𝑔) → (𝜓 ↔ 𝜎))    &   ⊢ (𝑥 = 𝐴 → (𝜓 ↔ 𝜌))    &   ⊢ ((𝜑 ∧ 𝑓 ∈ 𝑅) → 𝜒)    &   ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐼) → 𝜃)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑄)    ⇒   ⊢ (𝜑 → 𝜌)
11.3.3  The "variable selection" function
Syntax	cslv 22405	Select a subset of variables in a multivariate polynomial.
class selectVars
Definition	df-selv 22406*	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 ↦ (𝑗 ∈ 𝒫 𝑖 ↦ (𝑓 ∈ (Base‘(𝑖 mPoly 𝑟)) ↦ ⦋((𝑖 ∖ 𝑗) mPoly 𝑟) / 𝑢⦌⦋(𝑗 mPoly 𝑢) / 𝑡⦌⦋(algSc‘𝑡) / 𝑐⦌⦋(𝑐 ∘ (algSc‘𝑢)) / 𝑑⦌((((𝑖 evalSub 𝑡)‘ran 𝑑)‘(𝑑 ∘ 𝑓))‘(𝑥 ∈ 𝑖 ↦ if(𝑥 ∈ 𝑗, ((𝑗 mVar 𝑢)‘𝑥), (𝑐‘(((𝑖 ∖ 𝑗) mVar 𝑟)‘𝑥))))))))
Theorem	selvffval 22407*	Value of the "variable selection" function. (Contributed by SN, 4-Nov-2023.)
⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑊)    ⇒   ⊢ (𝜑 → (𝐼 selectVars 𝑅) = (𝑗 ∈ 𝒫 𝐼 ↦ (𝑓 ∈ (Base‘(𝐼 mPoly 𝑅)) ↦ ⦋((𝐼 ∖ 𝑗) mPoly 𝑅) / 𝑢⦌⦋(𝑗 mPoly 𝑢) / 𝑡⦌⦋(algSc‘𝑡) / 𝑐⦌⦋(𝑐 ∘ (algSc‘𝑢)) / 𝑑⦌((((𝐼 evalSub 𝑡)‘ran 𝑑)‘(𝑑 ∘ 𝑓))‘(𝑥 ∈ 𝐼 ↦ if(𝑥 ∈ 𝑗, ((𝑗 mVar 𝑢)‘𝑥), (𝑐‘(((𝐼 ∖ 𝑗) mVar 𝑅)‘𝑥))))))))
Theorem	selvfval 22408*	Value of the "variable selection" function. (Contributed by SN, 4-Nov-2023.)
⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐽 ⊆ 𝐼)    ⇒   ⊢ (𝜑 → ((𝐼 selectVars 𝑅)‘𝐽) = (𝑓 ∈ (Base‘(𝐼 mPoly 𝑅)) ↦ ⦋((𝐼 ∖ 𝐽) mPoly 𝑅) / 𝑢⦌⦋(𝐽 mPoly 𝑢) / 𝑡⦌⦋(algSc‘𝑡) / 𝑐⦌⦋(𝑐 ∘ (algSc‘𝑢)) / 𝑑⦌((((𝐼 evalSub 𝑡)‘ran 𝑑)‘(𝑑 ∘ 𝑓))‘(𝑥 ∈ 𝐼 ↦ if(𝑥 ∈ 𝐽, ((𝐽 mVar 𝑢)‘𝑥), (𝑐‘(((𝐼 ∖ 𝐽) mVar 𝑅)‘𝑥)))))))
Theorem	selvval 22409*	Value of the "variable selection" function. (Contributed by SN, 4-Nov-2023.)
⊢ 𝑃 = (𝐼 mPoly 𝑅)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 𝑈 = ((𝐼 ∖ 𝐽) mPoly 𝑅)    &   ⊢ 𝑇 = (𝐽 mPoly 𝑈)    &   ⊢ 𝐶 = (algSc‘𝑇)    &   ⊢ 𝐷 = (𝐶 ∘ (algSc‘𝑈))    &   ⊢ (𝜑 → 𝐽 ⊆ 𝐼)    &   ⊢ (𝜑 → 𝐹 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (((𝐼 selectVars 𝑅)‘𝐽)‘𝐹) = ((((𝐼 evalSub 𝑇)‘ran 𝐷)‘(𝐷 ∘ 𝐹))‘(𝑥 ∈ 𝐼 ↦ if(𝑥 ∈ 𝐽, ((𝐽 mVar 𝑈)‘𝑥), (𝐶‘(((𝐼 ∖ 𝐽) mVar 𝑅)‘𝑥))))))
Theorem	mhmcompl 22410	The composition of a monoid homomorphism and a polynomial is a polynomial. (Contributed by SN, 7-Feb-2025.)
⊢ 𝑃 = (𝐼 mPoly 𝑅)    &   ⊢ 𝑄 = (𝐼 mPoly 𝑆)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 𝐶 = (Base‘𝑄)    &   ⊢ (𝜑 → 𝐻 ∈ (𝑅 MndHom 𝑆))    &   ⊢ (𝜑 → 𝐹 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝐻 ∘ 𝐹) ∈ 𝐶)
Theorem	mplmapghm 22411*	The function 𝐻 mapping polynomials 𝑝 to their coefficient given a bag of variables 𝐹 is a group homomorphism. (Contributed by SN, 15-Mar-2025.)
⊢ 𝑃 = (𝐼 mPoly 𝑅)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 𝐷 = {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}    &   ⊢ 𝐻 = (𝑝 ∈ 𝐵 ↦ (𝑝‘𝐹))    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ Grp)    &   ⊢ (𝜑 → 𝐹 ∈ 𝐷)    ⇒   ⊢ (𝜑 → 𝐻 ∈ (𝑃 GrpHom 𝑅))
Theorem	mhmcoaddmpl 22412	Show that the ring homomorphism in rhmmpl 22678 preserves addition. (Contributed by SN, 8-Feb-2025.)
⊢ 𝑃 = (𝐼 mPoly 𝑅)    &   ⊢ 𝑄 = (𝐼 mPoly 𝑆)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 𝐶 = (Base‘𝑄)    &   ⊢ + = (+g‘𝑃)    &   ⊢ ✚ = (+g‘𝑄)    &   ⊢ (𝜑 → 𝐻 ∈ (𝑅 MndHom 𝑆))    &   ⊢ (𝜑 → 𝐹 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝐻 ∘ (𝐹 + 𝐺)) = ((𝐻 ∘ 𝐹) ✚ (𝐻 ∘ 𝐺)))
Theorem	rhmcomulmpl 22413	Show that the ring homomorphism in rhmmpl 22678 preserves multiplication. (Contributed by SN, 8-Feb-2025.)
⊢ 𝑃 = (𝐼 mPoly 𝑅)    &   ⊢ 𝑄 = (𝐼 mPoly 𝑆)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 𝐶 = (Base‘𝑄)    &   ⊢ · = (.r‘𝑃)    &   ⊢ ∙ = (.r‘𝑄)    &   ⊢ (𝜑 → 𝐻 ∈ (𝑅 RingHom 𝑆))    &   ⊢ (𝜑 → 𝐹 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝐻 ∘ (𝐹 · 𝐺)) = ((𝐻 ∘ 𝐹) ∙ (𝐻 ∘ 𝐺)))
Theorem	evlscl 22414	A polynomial over the ring 𝑅 evaluates to an element in 𝑅. (Contributed by SN, 12-Mar-2025.)
⊢ 𝑄 = ((𝐼 evalSub 𝑅)‘𝑆)    &   ⊢ 𝑃 = (𝐼 mPoly 𝑈)    &   ⊢ 𝑈 = (𝑅 ↾s 𝑆)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 𝐾 = (Base‘𝑅)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝑆 ∈ (SubRing‘𝑅))    &   ⊢ (𝜑 → 𝐹 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐴 ∈ (𝐾 ↑m 𝐼))    ⇒   ⊢ (𝜑 → ((𝑄‘𝐹)‘𝐴) ∈ 𝐾)
Theorem	evlsscaval 22415	Polynomial evaluation builder for a scalar. Compare evl1scad 22633. Note that scalar multiplication by 𝑋 is the same as vector multiplication by (𝐴‘𝑋) by asclmul1 22174. (Contributed by SN, 27-Jul-2024.)
⊢ 𝑄 = ((𝐼 evalSub 𝑆)‘𝑅)    &   ⊢ 𝑃 = (𝐼 mPoly 𝑈)    &   ⊢ 𝑈 = (𝑆 ↾s 𝑅)    &   ⊢ 𝐾 = (Base‘𝑆)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 𝐴 = (algSc‘𝑃)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑆 ∈ CRing)    &   ⊢ (𝜑 → 𝑅 ∈ (SubRing‘𝑆))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑅)    &   ⊢ (𝜑 → 𝐿 ∈ (𝐾 ↑m 𝐼))    ⇒   ⊢ (𝜑 → ((𝐴‘𝑋) ∈ 𝐵 ∧ ((𝑄‘(𝐴‘𝑋))‘𝐿) = 𝑋))
Theorem	evlsvarval 22416	Polynomial evaluation builder for a variable. (Contributed by SN, 27-Jul-2024.)
⊢ 𝑄 = ((𝐼 evalSub 𝑆)‘𝑅)    &   ⊢ 𝑃 = (𝐼 mPoly 𝑈)    &   ⊢ 𝑉 = (𝐼 mVar 𝑈)    &   ⊢ 𝑈 = (𝑆 ↾s 𝑅)    &   ⊢ 𝐾 = (Base‘𝑆)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑆 ∈ CRing)    &   ⊢ (𝜑 → 𝑅 ∈ (SubRing‘𝑆))    &   ⊢ (𝜑 → 𝑋 ∈ 𝐼)    &   ⊢ (𝜑 → 𝐴 ∈ (𝐾 ↑m 𝐼))    ⇒   ⊢ (𝜑 → ((𝑉‘𝑋) ∈ 𝐵 ∧ ((𝑄‘(𝑉‘𝑋))‘𝐴) = (𝐴‘𝑋)))
Theorem	evlsexpval 22417	Polynomial evaluation builder for exponentiation. (Contributed by SN, 27-Jul-2024.)
⊢ 𝑄 = ((𝐼 evalSub 𝑆)‘𝑅)    &   ⊢ 𝑃 = (𝐼 mPoly 𝑈)    &   ⊢ 𝑈 = (𝑆 ↾s 𝑅)    &   ⊢ 𝐾 = (Base‘𝑆)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑍)    &   ⊢ (𝜑 → 𝑆 ∈ CRing)    &   ⊢ (𝜑 → 𝑅 ∈ (SubRing‘𝑆))    &   ⊢ (𝜑 → 𝐴 ∈ (𝐾 ↑m 𝐼))    &   ⊢ (𝜑 → (𝑀 ∈ 𝐵 ∧ ((𝑄‘𝑀)‘𝐴) = 𝑉))    &   ⊢ ∙ = (.g‘(mulGrp‘𝑃))    &   ⊢ ↑ = (.g‘(mulGrp‘𝑆))    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    ⇒   ⊢ (𝜑 → ((𝑁 ∙ 𝑀) ∈ 𝐵 ∧ ((𝑄‘(𝑁 ∙ 𝑀))‘𝐴) = (𝑁 ↑ 𝑉)))
Theorem	evlsaddval 22418	Polynomial evaluation builder for addition. (Contributed by SN, 27-Jul-2024.)
⊢ 𝑄 = ((𝐼 evalSub 𝑆)‘𝑅)    &   ⊢ 𝑃 = (𝐼 mPoly 𝑈)    &   ⊢ 𝑈 = (𝑆 ↾s 𝑅)    &   ⊢ 𝐾 = (Base‘𝑆)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑍)    &   ⊢ (𝜑 → 𝑆 ∈ CRing)    &   ⊢ (𝜑 → 𝑅 ∈ (SubRing‘𝑆))    &   ⊢ (𝜑 → 𝐴 ∈ (𝐾 ↑m 𝐼))    &   ⊢ (𝜑 → (𝑀 ∈ 𝐵 ∧ ((𝑄‘𝑀)‘𝐴) = 𝑉))    &   ⊢ (𝜑 → (𝑁 ∈ 𝐵 ∧ ((𝑄‘𝑁)‘𝐴) = 𝑊))    &   ⊢ ✚ = (+g‘𝑃)    &   ⊢ + = (+g‘𝑆)    ⇒   ⊢ (𝜑 → ((𝑀 ✚ 𝑁) ∈ 𝐵 ∧ ((𝑄‘(𝑀 ✚ 𝑁))‘𝐴) = (𝑉 + 𝑊)))
Theorem	evlsmulval 22419	Polynomial evaluation builder for multiplication. (Contributed by SN, 27-Jul-2024.)
⊢ 𝑄 = ((𝐼 evalSub 𝑆)‘𝑅)    &   ⊢ 𝑃 = (𝐼 mPoly 𝑈)    &   ⊢ 𝑈 = (𝑆 ↾s 𝑅)    &   ⊢ 𝐾 = (Base‘𝑆)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑍)    &   ⊢ (𝜑 → 𝑆 ∈ CRing)    &   ⊢ (𝜑 → 𝑅 ∈ (SubRing‘𝑆))    &   ⊢ (𝜑 → 𝐴 ∈ (𝐾 ↑m 𝐼))    &   ⊢ (𝜑 → (𝑀 ∈ 𝐵 ∧ ((𝑄‘𝑀)‘𝐴) = 𝑉))    &   ⊢ (𝜑 → (𝑁 ∈ 𝐵 ∧ ((𝑄‘𝑁)‘𝐴) = 𝑊))    &   ⊢ ∙ = (.r‘𝑃)    &   ⊢ · = (.r‘𝑆)    ⇒   ⊢ (𝜑 → ((𝑀 ∙ 𝑁) ∈ 𝐵 ∧ ((𝑄‘(𝑀 ∙ 𝑁))‘𝐴) = (𝑉 · 𝑊)))
Theorem	evlsmaprhm 22420*	The function 𝐹 mapping polynomials 𝑝 to their subring evaluation at a given point 𝑋 is a ring homomorphism. Compare evls1maprhm 22674. (Contributed by SN, 12-Mar-2025.)
⊢ 𝑄 = ((𝐼 evalSub 𝑅)‘𝑆)    &   ⊢ 𝑃 = (𝐼 mPoly 𝑈)    &   ⊢ 𝑈 = (𝑅 ↾s 𝑆)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 𝐾 = (Base‘𝑅)    &   ⊢ 𝐹 = (𝑝 ∈ 𝐵 ↦ ((𝑄‘𝑝)‘𝐴))    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝑆 ∈ (SubRing‘𝑅))    &   ⊢ (𝜑 → 𝐴 ∈ (𝐾 ↑m 𝐼))    ⇒   ⊢ (𝜑 → 𝐹 ∈ (𝑃 RingHom 𝑅))
Theorem	evlsevl 22421	Evaluation in a subring is the same as evaluation in the ring itself. (Contributed by SN, 9-Feb-2025.)
⊢ 𝑄 = ((𝐼 evalSub 𝑆)‘𝑅)    &   ⊢ 𝑂 = (𝐼 eval 𝑆)    &   ⊢ 𝑊 = (𝐼 mPoly 𝑈)    &   ⊢ 𝑈 = (𝑆 ↾s 𝑅)    &   ⊢ 𝐵 = (Base‘𝑊)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑆 ∈ CRing)    &   ⊢ (𝜑 → 𝑅 ∈ (SubRing‘𝑆))    &   ⊢ (𝜑 → 𝐹 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝑄‘𝐹) = (𝑂‘𝐹))
Theorem	evlvvval 22422*	Give a formula for the evaluation of a polynomial given assignments from variables to values. (Contributed by SN, 5-Mar-2025.)
⊢ 𝑄 = (𝐼 eval 𝑅)    &   ⊢ 𝑃 = (𝐼 mPoly 𝑅)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin}    &   ⊢ 𝐾 = (Base‘𝑅)    &   ⊢ 𝑀 = (mulGrp‘𝑅)    &   ⊢ ↑ = (.g‘𝑀)    &   ⊢ · = (.r‘𝑅)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝐹 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐴 ∈ (𝐾 ↑m 𝐼))    ⇒   ⊢ (𝜑 → ((𝑄‘𝐹)‘𝐴) = (𝑅 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘𝑏) · (𝑀 Σg (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (𝐴‘𝑖))))))))
Theorem	selvcllem1 22423	𝑇 is an associative algebra. For simplicity, 𝐼 stands for (𝐼 ∖ 𝐽) and we have 𝐽 ∈ 𝑊 instead of 𝐽 ⊆ 𝐼. (Contributed by SN, 15-Dec-2023.)
⊢ 𝑈 = (𝐼 mPoly 𝑅)    &   ⊢ 𝑇 = (𝐽 mPoly 𝑈)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐽 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    ⇒   ⊢ (𝜑 → 𝑇 ∈ AssAlg)
Theorem	selvcllem2 22424	𝐷 is a ring homomorphism. (Contributed by SN, 15-Dec-2023.)
⊢ 𝑈 = (𝐼 mPoly 𝑅)    &   ⊢ 𝑇 = (𝐽 mPoly 𝑈)    &   ⊢ 𝐶 = (algSc‘𝑇)    &   ⊢ 𝐷 = (𝐶 ∘ (algSc‘𝑈))    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐽 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    ⇒   ⊢ (𝜑 → 𝐷 ∈ (𝑅 RingHom 𝑇))
Theorem	selvcllem3 22425	The third argument passed to evalSub is in the domain. (Contributed by SN, 15-Dec-2023.)
⊢ 𝑈 = (𝐼 mPoly 𝑅)    &   ⊢ 𝑇 = (𝐽 mPoly 𝑈)    &   ⊢ 𝐶 = (algSc‘𝑇)    &   ⊢ 𝐷 = (𝐶 ∘ (algSc‘𝑈))    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐽 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    ⇒   ⊢ (𝜑 → ran 𝐷 ∈ (SubRing‘𝑇))
Theorem	selvcllemh 22426	Apply the third argument (selvcllem3 22425) to show that 𝑄 is a (ring) homomorphism. (Contributed by SN, 5-Nov-2023.)
⊢ 𝑈 = ((𝐼 ∖ 𝐽) mPoly 𝑅)    &   ⊢ 𝑇 = (𝐽 mPoly 𝑈)    &   ⊢ 𝐶 = (algSc‘𝑇)    &   ⊢ 𝐷 = (𝐶 ∘ (algSc‘𝑈))    &   ⊢ 𝑄 = ((𝐼 evalSub 𝑇)‘ran 𝐷)    &   ⊢ 𝑊 = (𝐼 mPoly 𝑆)    &   ⊢ 𝑆 = (𝑇 ↾s ran 𝐷)    &   ⊢ 𝑋 = (𝑇 ↑s (𝐵 ↑m 𝐼))    &   ⊢ 𝐵 = (Base‘𝑇)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝐽 ⊆ 𝐼)    ⇒   ⊢ (𝜑 → 𝑄 ∈ (𝑊 RingHom 𝑋))
Theorem	selvcllem4 22427	The fourth argument passed to evalSub is in the domain (a polynomial in (𝐼 mPoly (𝐽 mPoly ((𝐼 ∖ 𝐽) mPoly 𝑅)))). (Contributed by SN, 5-Nov-2023.)
⊢ 𝑃 = (𝐼 mPoly 𝑅)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 𝑈 = ((𝐼 ∖ 𝐽) mPoly 𝑅)    &   ⊢ 𝑇 = (𝐽 mPoly 𝑈)    &   ⊢ 𝐶 = (algSc‘𝑇)    &   ⊢ 𝐷 = (𝐶 ∘ (algSc‘𝑈))    &   ⊢ 𝑆 = (𝑇 ↾s ran 𝐷)    &   ⊢ 𝑊 = (𝐼 mPoly 𝑆)    &   ⊢ 𝑋 = (Base‘𝑊)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝐽 ⊆ 𝐼)    &   ⊢ (𝜑 → 𝐹 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝐷 ∘ 𝐹) ∈ 𝑋)
Theorem	selvcllem5 22428*	The fifth argument passed to evalSub is in the domain (a function 𝐼⟶𝐸). (Contributed by SN, 22-Feb-2024.)
⊢ 𝑈 = ((𝐼 ∖ 𝐽) mPoly 𝑅)    &   ⊢ 𝑇 = (𝐽 mPoly 𝑈)    &   ⊢ 𝐶 = (algSc‘𝑇)    &   ⊢ 𝐸 = (Base‘𝑇)    &   ⊢ 𝐹 = (𝑥 ∈ 𝐼 ↦ if(𝑥 ∈ 𝐽, ((𝐽 mVar 𝑈)‘𝑥), (𝐶‘(((𝐼 ∖ 𝐽) mVar 𝑅)‘𝑥))))    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝐽 ⊆ 𝐼)    ⇒   ⊢ (𝜑 → 𝐹 ∈ (𝐸 ↑m 𝐼))
Theorem	selvcl 22429	Closure of the "variable selection" function. (Contributed by SN, 22-Feb-2024.)
⊢ 𝑃 = (𝐼 mPoly 𝑅)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 𝑈 = ((𝐼 ∖ 𝐽) mPoly 𝑅)    &   ⊢ 𝑇 = (𝐽 mPoly 𝑈)    &   ⊢ 𝐸 = (Base‘𝑇)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝐽 ⊆ 𝐼)    &   ⊢ (𝜑 → 𝐹 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (((𝐼 selectVars 𝑅)‘𝐽)‘𝐹) ∈ 𝐸)
Theorem	selvval2 22430*	Value of the "variable selection" function. Convert selvval 22409 into a simpler form by using evlsevl 22421. (Contributed by SN, 9-Feb-2025.)
⊢ 𝑃 = (𝐼 mPoly 𝑅)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 𝑈 = ((𝐼 ∖ 𝐽) mPoly 𝑅)    &   ⊢ 𝑇 = (𝐽 mPoly 𝑈)    &   ⊢ 𝐶 = (algSc‘𝑇)    &   ⊢ 𝐷 = (𝐶 ∘ (algSc‘𝑈))    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝐽 ⊆ 𝐼)    &   ⊢ (𝜑 → 𝐹 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (((𝐼 selectVars 𝑅)‘𝐽)‘𝐹) = (((𝐼 eval 𝑇)‘(𝐷 ∘ 𝐹))‘(𝑥 ∈ 𝐼 ↦ if(𝑥 ∈ 𝐽, ((𝐽 mVar 𝑈)‘𝑥), (𝐶‘(((𝐼 ∖ 𝐽) mVar 𝑅)‘𝑥))))))
Theorem	selvvvval 22431*	Recover the original polynomial from a selectVars application. (Contributed by SN, 15-Mar-2025.)
⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin}    &   ⊢ 𝑃 = (𝐼 mPoly 𝑅)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝐽 ⊆ 𝐼)    &   ⊢ (𝜑 → 𝐹 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐷)    ⇒   ⊢ (𝜑 → (((((𝐼 selectVars 𝑅)‘𝐽)‘𝐹)‘(𝑌 ↾ 𝐽))‘(𝑌 ↾ (𝐼 ∖ 𝐽))) = (𝐹‘𝑌))
Theorem	selvadd 22432	The "variable selection" function is additive. (Contributed by SN, 7-Feb-2025.)
⊢ 𝑃 = (𝐼 mPoly 𝑅)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ + = (+g‘𝑃)    &   ⊢ 𝑈 = ((𝐼 ∖ 𝐽) mPoly 𝑅)    &   ⊢ 𝑇 = (𝐽 mPoly 𝑈)    &   ⊢ ✚ = (+g‘𝑇)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝐽 ⊆ 𝐼)    &   ⊢ (𝜑 → 𝐹 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (((𝐼 selectVars 𝑅)‘𝐽)‘(𝐹 + 𝐺)) = ((((𝐼 selectVars 𝑅)‘𝐽)‘𝐹) ✚ (((𝐼 selectVars 𝑅)‘𝐽)‘𝐺)))
Theorem	selvmul 22433	The "variable selection" function is multiplicative. (Contributed by SN, 18-Feb-2025.)
⊢ 𝑃 = (𝐼 mPoly 𝑅)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ · = (.r‘𝑃)    &   ⊢ 𝑈 = ((𝐼 ∖ 𝐽) mPoly 𝑅)    &   ⊢ 𝑇 = (𝐽 mPoly 𝑈)    &   ⊢ ∙ = (.r‘𝑇)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝐽 ⊆ 𝐼)    &   ⊢ (𝜑 → 𝐹 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (((𝐼 selectVars 𝑅)‘𝐽)‘(𝐹 · 𝐺)) = ((((𝐼 selectVars 𝑅)‘𝐽)‘𝐹) ∙ (((𝐼 selectVars 𝑅)‘𝐽)‘𝐺)))
11.3.4  Additional definitions for (multivariate) polynomials
Syntax	cmhp 22434	Multivariate polynomials.
class mHomP
Syntax	cpsd 22435	Power series partial derivative function.
class mPSDer
Syntax	cai 22436	Algebraically independent.
class AlgInd
Definition	df-mhp 22437*	Define the subspaces of order- 𝑛 homogeneous polynomials. (Contributed by Mario Carneiro, 21-Mar-2015.)
⊢ mHomP = (𝑖 ∈ V, 𝑟 ∈ V ↦ (𝑛 ∈ ℕ0 ↦ {𝑓 ∈ (Base‘(𝑖 mPoly 𝑟)) ∣ (𝑓 supp (0g‘𝑟)) ⊆ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝑖) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑛}}))
Theorem	reldmmhp 22438	The domain of the homogeneous polynomial operator is a relation. (Contributed by SN, 18-May-2025.)
⊢ Rel dom mHomP
Theorem	mhpfval 22439*	Value of the "homogeneous polynomial" operator. (Contributed by Steven Nguyen, 25-Aug-2023.)
⊢ 𝐻 = (𝐼 mHomP 𝑅)    &   ⊢ 𝑃 = (𝐼 mPoly 𝑅)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin}    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑊)    ⇒   ⊢ (𝜑 → 𝐻 = (𝑛 ∈ ℕ0 ↦ {𝑓 ∈ 𝐵 ∣ (𝑓 supp 0 ) ⊆ {𝑔 ∈ 𝐷 ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑛}}))
Theorem	mhpval 22440*	Value of the "homogeneous polynomial" function. (Contributed by Steven Nguyen, 25-Aug-2023.)
⊢ 𝐻 = (𝐼 mHomP 𝑅)    &   ⊢ 𝑃 = (𝐼 mPoly 𝑅)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin}    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    ⇒   ⊢ (𝜑 → (𝐻‘𝑁) = {𝑓 ∈ 𝐵 ∣ (𝑓 supp 0 ) ⊆ {𝑔 ∈ 𝐷 ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁}})
Theorem	ismhp 22441*	Property of being a homogeneous polynomial. (Contributed by Steven Nguyen, 25-Aug-2023.)
⊢ 𝐻 = (𝐼 mHomP 𝑅)    &   ⊢ 𝑃 = (𝐼 mPoly 𝑅)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin}    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    ⇒   ⊢ (𝜑 → (𝑋 ∈ (𝐻‘𝑁) ↔ (𝑋 ∈ 𝐵 ∧ (𝑋 supp 0 ) ⊆ {𝑔 ∈ 𝐷 ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁})))
Theorem	ismhp2 22442*	Deduce a homogeneous polynomial from its properties. (Contributed by SN, 25-May-2024.)
⊢ 𝐻 = (𝐼 mHomP 𝑅)    &   ⊢ 𝑃 = (𝐼 mPoly 𝑅)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin}    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → (𝑋 supp 0 ) ⊆ {𝑔 ∈ 𝐷 ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁})    ⇒   ⊢ (𝜑 → 𝑋 ∈ (𝐻‘𝑁))
Theorem	ismhp3 22443*	A polynomial is homogeneous iff the degree of every nonzero term is the same. (Contributed by SN, 22-Jul-2024.)
⊢ 𝐻 = (𝐼 mHomP 𝑅)    &   ⊢ 𝑃 = (𝐼 mPoly 𝑅)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin}    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝑋 ∈ (𝐻‘𝑁) ↔ ∀𝑑 ∈ 𝐷 ((𝑋‘𝑑) ≠ 0 → ((ℂfld ↾s ℕ0) Σg 𝑑) = 𝑁)))
Theorem	mhprcl 22444	Reverse closure for homogeneous polynomials, use elfvov1 7454 and elfvov2 7455 with reldmmhp 22438 for the reverse closure of 𝐼 and 𝑅. (Contributed by SN, 4-Aug-2025.)
⊢ 𝐻 = (𝐼 mHomP 𝑅)    &   ⊢ (𝜑 → 𝑋 ∈ (𝐻‘𝑁))    ⇒   ⊢ (𝜑 → 𝑁 ∈ ℕ0)
Theorem	mhpmpl 22445	A homogeneous polynomial is a polynomial. (Contributed by Steven Nguyen, 25-Aug-2023.)
⊢ 𝐻 = (𝐼 mHomP 𝑅)    &   ⊢ 𝑃 = (𝐼 mPoly 𝑅)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ (𝜑 → 𝑋 ∈ (𝐻‘𝑁))    ⇒   ⊢ (𝜑 → 𝑋 ∈ 𝐵)
Theorem	mhpdeg 22446*	All nonzero terms of a homogeneous polynomial have degree 𝑁. (Contributed by Steven Nguyen, 25-Aug-2023.)
⊢ 𝐻 = (𝐼 mHomP 𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin}    &   ⊢ (𝜑 → 𝑋 ∈ (𝐻‘𝑁))    ⇒   ⊢ (𝜑 → (𝑋 supp 0 ) ⊆ {𝑔 ∈ 𝐷 ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁})
Theorem	mhp0cl 22447*	The zero polynomial is homogeneous. Under df-mhp 22437, it has any (nonnegative integer) degree which loosely corresponds to the value "undefined". The values -∞ and 0 are also used in Metamath (by df-mdeg 26353 and df-dgr 26489 respectively) and the literature: https://math.stackexchange.com/a/1796314/593843 26489. (Contributed by SN, 12-Sep-2023.)
⊢ 𝐻 = (𝐼 mHomP 𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin}    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ Grp)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    ⇒   ⊢ (𝜑 → (𝐷 × { 0 }) ∈ (𝐻‘𝑁))
Theorem	mhpsclcl 22448	A scalar (or constant) polynomial has degree 0. Compare deg1scl 26411. In other contexts, there may be an exception for the zero polynomial, but under df-mhp 22437 the zero polynomial can be any degree (see mhp0cl 22447) so there is no exception. (Contributed by SN, 25-May-2024.)
⊢ 𝐻 = (𝐼 mHomP 𝑅)    &   ⊢ 𝑃 = (𝐼 mPoly 𝑅)    &   ⊢ 𝐴 = (algSc‘𝑃)    &   ⊢ 𝐾 = (Base‘𝑅)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝐶 ∈ 𝐾)    ⇒   ⊢ (𝜑 → (𝐴‘𝐶) ∈ (𝐻‘0))
Theorem	mhpvarcl 22449	A power series variable is a polynomial of degree 1. (Contributed by SN, 25-May-2024.)
⊢ 𝐻 = (𝐼 mHomP 𝑅)    &   ⊢ 𝑉 = (𝐼 mVar 𝑅)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐼)    ⇒   ⊢ (𝜑 → (𝑉‘𝑋) ∈ (𝐻‘1))
Theorem	mhpmulcl 22450	A product of homogeneous polynomials is a homogeneous polynomial whose degree is the sum of the degrees of the factors. Compare mdegmulle2 26377 (which shows less-than-or-equal instead of equal). (Contributed by SN, 22-Jul-2024.) Remove closure hypotheses. (Revised by SN, 4-Sep-2025.)
⊢ 𝐻 = (𝐼 mHomP 𝑅)    &   ⊢ 𝑌 = (𝐼 mPoly 𝑅)    &   ⊢ · = (.r‘𝑌)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝑃 ∈ (𝐻‘𝑀))    &   ⊢ (𝜑 → 𝑄 ∈ (𝐻‘𝑁))    ⇒   ⊢ (𝜑 → (𝑃 · 𝑄) ∈ (𝐻‘(𝑀 + 𝑁)))
Theorem	mhppwdeg 22451	Degree of a homogeneous polynomial raised to a power. General version of deg1pw 26419. (Contributed by SN, 26-Jul-2024.) Remove closure hypotheses. (Revised by SN, 4-Sep-2025.)
⊢ 𝐻 = (𝐼 mHomP 𝑅)    &   ⊢ 𝑃 = (𝐼 mPoly 𝑅)    &   ⊢ 𝑇 = (mulGrp‘𝑃)    &   ⊢ ↑ = (.g‘𝑇)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑋 ∈ (𝐻‘𝑀))    ⇒   ⊢ (𝜑 → (𝑁 ↑ 𝑋) ∈ (𝐻‘(𝑀 · 𝑁)))
Theorem	mhpaddcl 22452	Homogeneous polynomials are closed under addition. (Contributed by SN, 26-Aug-2023.) Remove closure hypotheses. (Revised by SN, 4-Sep-2025.)
⊢ 𝐻 = (𝐼 mHomP 𝑅)    &   ⊢ 𝑃 = (𝐼 mPoly 𝑅)    &   ⊢ + = (+g‘𝑃)    &   ⊢ (𝜑 → 𝑅 ∈ Grp)    &   ⊢ (𝜑 → 𝑋 ∈ (𝐻‘𝑁))    &   ⊢ (𝜑 → 𝑌 ∈ (𝐻‘𝑁))    ⇒   ⊢ (𝜑 → (𝑋 + 𝑌) ∈ (𝐻‘𝑁))
Theorem	mhpinvcl 22453	Homogeneous polynomials are closed under taking the opposite. (Contributed by SN, 12-Sep-2023.) Remove closure hypotheses. (Revised by SN, 4-Sep-2025.)
⊢ 𝐻 = (𝐼 mHomP 𝑅)    &   ⊢ 𝑃 = (𝐼 mPoly 𝑅)    &   ⊢ 𝑀 = (invg‘𝑃)    &   ⊢ (𝜑 → 𝑅 ∈ Grp)    &   ⊢ (𝜑 → 𝑋 ∈ (𝐻‘𝑁))    ⇒   ⊢ (𝜑 → (𝑀‘𝑋) ∈ (𝐻‘𝑁))
Theorem	mhpsubg 22454	Homogeneous polynomials form a subgroup of the polynomials. (Contributed by SN, 25-Sep-2023.)
⊢ 𝐻 = (𝐼 mHomP 𝑅)    &   ⊢ 𝑃 = (𝐼 mPoly 𝑅)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ Grp)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    ⇒   ⊢ (𝜑 → (𝐻‘𝑁) ∈ (SubGrp‘𝑃))
Theorem	mhpvscacl 22455	Homogeneous polynomials are closed under scalar multiplication. (Contributed by SN, 25-Sep-2023.) Remove closure hypotheses. (Revised by SN, 4-Sep-2025.)
⊢ 𝐻 = (𝐼 mHomP 𝑅)    &   ⊢ 𝑃 = (𝐼 mPoly 𝑅)    &   ⊢ · = ( ·𝑠 ‘𝑃)    &   ⊢ 𝐾 = (Base‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐾)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐻‘𝑁))    ⇒   ⊢ (𝜑 → (𝑋 · 𝐹) ∈ (𝐻‘𝑁))
Theorem	mhplss 22456	Homogeneous polynomials form a linear subspace of the polynomials. (Contributed by SN, 25-Sep-2023.)
⊢ 𝐻 = (𝐼 mHomP 𝑅)    &   ⊢ 𝑃 = (𝐼 mPoly 𝑅)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    ⇒   ⊢ (𝜑 → (𝐻‘𝑁) ∈ (LSubSp‘𝑃))
Definition	df-psd 22457*	Define the differentiation operation on multivariate polynomials. (((𝐼 mPSDer 𝑅)‘𝑋)‘𝐹) is the partial derivative of the polynomial 𝐹 with respect to 𝑋. (Contributed by Mario Carneiro, 21-Mar-2015.)
⊢ mPSDer = (𝑖 ∈ V, 𝑟 ∈ V ↦ (𝑥 ∈ 𝑖 ↦ (𝑓 ∈ (Base‘(𝑖 mPwSer 𝑟)) ↦ (𝑘 ∈ {ℎ ∈ (ℕ0 ↑m 𝑖) ∣ (◡ℎ “ ℕ) ∈ Fin} ↦ (((𝑘‘𝑥) + 1)(.g‘𝑟)(𝑓‘(𝑘 ∘f + (𝑦 ∈ 𝑖 ↦ if(𝑦 = 𝑥, 1, 0)))))))))
Theorem	psdffval 22458*	Value of the power series differentiation operation. (Contributed by SN, 11-Apr-2025.)
⊢ 𝑆 = (𝐼 mPwSer 𝑅)    &   ⊢ 𝐵 = (Base‘𝑆)    &   ⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin}    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑊)    ⇒   ⊢ (𝜑 → (𝐼 mPSDer 𝑅) = (𝑥 ∈ 𝐼 ↦ (𝑓 ∈ 𝐵 ↦ (𝑘 ∈ 𝐷 ↦ (((𝑘‘𝑥) + 1)(.g‘𝑅)(𝑓‘(𝑘 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑥, 1, 0)))))))))
Theorem	psdfval 22459*	Give a map between power series and their partial derivatives with respect to a given variable 𝑋. (Contributed by SN, 11-Apr-2025.)
⊢ 𝑆 = (𝐼 mPwSer 𝑅)    &   ⊢ 𝐵 = (Base‘𝑆)    &   ⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin}    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐼)    ⇒   ⊢ (𝜑 → ((𝐼 mPSDer 𝑅)‘𝑋) = (𝑓 ∈ 𝐵 ↦ (𝑘 ∈ 𝐷 ↦ (((𝑘‘𝑋) + 1)(.g‘𝑅)(𝑓‘(𝑘 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0))))))))
Theorem	psdval 22460*	Evaluate the partial derivative of a power series 𝐹 with respect to 𝑋. (Contributed by SN, 11-Apr-2025.)
⊢ 𝑆 = (𝐼 mPwSer 𝑅)    &   ⊢ 𝐵 = (Base‘𝑆)    &   ⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin}    &   ⊢ (𝜑 → 𝑋 ∈ 𝐼)    &   ⊢ (𝜑 → 𝐹 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (((𝐼 mPSDer 𝑅)‘𝑋)‘𝐹) = (𝑘 ∈ 𝐷 ↦ (((𝑘‘𝑋) + 1)(.g‘𝑅)(𝐹‘(𝑘 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0)))))))
Theorem	psdcoef 22461*	Coefficient of a term of the derivative of a power series. (Contributed by SN, 12-Apr-2025.)
⊢ 𝑆 = (𝐼 mPwSer 𝑅)    &   ⊢ 𝐵 = (Base‘𝑆)    &   ⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin}    &   ⊢ (𝜑 → 𝑋 ∈ 𝐼)    &   ⊢ (𝜑 → 𝐹 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐾 ∈ 𝐷)    ⇒   ⊢ (𝜑 → ((((𝐼 mPSDer 𝑅)‘𝑋)‘𝐹)‘𝐾) = (((𝐾‘𝑋) + 1)(.g‘𝑅)(𝐹‘(𝐾 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0))))))
Theorem	psdcl 22462	The derivative of a power series is a power series. (Contributed by SN, 11-Apr-2025.)
⊢ 𝑆 = (𝐼 mPwSer 𝑅)    &   ⊢ 𝐵 = (Base‘𝑆)    &   ⊢ (𝜑 → 𝑅 ∈ Mgm)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐼)    &   ⊢ (𝜑 → 𝐹 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (((𝐼 mPSDer 𝑅)‘𝑋)‘𝐹) ∈ 𝐵)
Theorem	psdmplcl 22463	The derivative of a polynomial is a polynomial. (Contributed by SN, 12-Apr-2025.)
⊢ 𝑃 = (𝐼 mPoly 𝑅)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ (𝜑 → 𝑅 ∈ Mnd)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐼)    &   ⊢ (𝜑 → 𝐹 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (((𝐼 mPSDer 𝑅)‘𝑋)‘𝐹) ∈ 𝐵)
Theorem	psdadd 22464	The derivative of a sum is the sum of the derivatives. (Contributed by SN, 12-Apr-2025.)
⊢ 𝑆 = (𝐼 mPwSer 𝑅)    &   ⊢ 𝐵 = (Base‘𝑆)    &   ⊢ + = (+g‘𝑆)    &   ⊢ (𝜑 → 𝑅 ∈ CMnd)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐼)    &   ⊢ (𝜑 → 𝐹 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (((𝐼 mPSDer 𝑅)‘𝑋)‘(𝐹 + 𝐺)) = ((((𝐼 mPSDer 𝑅)‘𝑋)‘𝐹) + (((𝐼 mPSDer 𝑅)‘𝑋)‘𝐺)))
Theorem	psdvsca 22465	The derivative of a scaled power series is the scaled derivative. (Contributed by SN, 12-Apr-2025.)
⊢ 𝑆 = (𝐼 mPwSer 𝑅)    &   ⊢ 𝐵 = (Base‘𝑆)    &   ⊢ · = ( ·𝑠 ‘𝑆)    &   ⊢ 𝐾 = (Base‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐼)    &   ⊢ (𝜑 → 𝐹 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐶 ∈ 𝐾)    ⇒   ⊢ (𝜑 → (((𝐼 mPSDer 𝑅)‘𝑋)‘(𝐶 · 𝐹)) = (𝐶 · (((𝐼 mPSDer 𝑅)‘𝑋)‘𝐹)))
Theorem	psdmullem 22466	Lemma for psdmul 22467. Transitive law for union of class difference. (Contributed by SN, 5-May-2025.)
⊢ (𝜑 → 𝐶 ⊆ 𝐵)    &   ⊢ (𝜑 → 𝐵 ⊆ 𝐴)    ⇒   ⊢ (𝜑 → ((𝐴 ∖ 𝐵) ∪ (𝐵 ∖ 𝐶)) = (𝐴 ∖ 𝐶))
Theorem	psdmul 22467	Product rule for power series. An outline is available at https://github.com/icecream17/Stuff/blob/main/math/psdmul.pdf. (Contributed by SN, 25-Apr-2025.)
⊢ 𝑆 = (𝐼 mPwSer 𝑅)    &   ⊢ 𝐵 = (Base‘𝑆)    &   ⊢ + = (+g‘𝑆)    &   ⊢ · = (.r‘𝑆)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐼)    &   ⊢ (𝜑 → 𝐹 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (((𝐼 mPSDer 𝑅)‘𝑋)‘(𝐹 · 𝐺)) = (((((𝐼 mPSDer 𝑅)‘𝑋)‘𝐹) · 𝐺) + (𝐹 · (((𝐼 mPSDer 𝑅)‘𝑋)‘𝐺))))
Theorem	psd1 22468	The derivative of one is zero. (Contributed by SN, 25-Apr-2025.)
⊢ 𝑆 = (𝐼 mPwSer 𝑅)    &   ⊢ 1 = (1r‘𝑆)    &   ⊢ 0 = (0g‘𝑆)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐼)    ⇒   ⊢ (𝜑 → (((𝐼 mPSDer 𝑅)‘𝑋)‘ 1 ) = 0 )
Theorem	psdascl 22469	The derivative of a constant polynomial is zero. (Contributed by SN, 25-Apr-2025.)
⊢ 𝑆 = (𝐼 mPwSer 𝑅)    &   ⊢ 0 = (0g‘𝑆)    &   ⊢ 𝐴 = (algSc‘𝑆)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐼)    &   ⊢ (𝜑 → 𝐶 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (((𝐼 mPSDer 𝑅)‘𝑋)‘(𝐴‘𝐶)) = 0 )
Theorem	psdmvr 22470	The partial derivative of a variable is the Kronecker delta if(𝑋 = 𝑌, 1 , 0 ). (Contributed by SN, 16-Oct-2025.)
⊢ 𝑆 = (𝐼 mPwSer 𝑅)    &   ⊢ 0 = (0g‘𝑆)    &   ⊢ 1 = (1r‘𝑆)    &   ⊢ 𝑉 = (𝐼 mVar 𝑅)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐼)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐼)    ⇒   ⊢ (𝜑 → (((𝐼 mPSDer 𝑅)‘𝑋)‘(𝑉‘𝑌)) = if(𝑋 = 𝑌, 1 , 0 ))
Theorem	psdpw 22471	Power rule for partial derivative of power series. (Contributed by SN, 25-Apr-2025.)
⊢ 𝑆 = (𝐼 mPwSer 𝑅)    &   ⊢ 𝐵 = (Base‘𝑆)    &   ⊢ · = (.g‘𝑆)    &   ⊢ ∙ = (.r‘𝑆)    &   ⊢ 𝑀 = (mulGrp‘𝑆)    &   ⊢ ↑ = (.g‘𝑀)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐼)    &   ⊢ (𝜑 → 𝐹 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    ⇒   ⊢ (𝜑 → (((𝐼 mPSDer 𝑅)‘𝑋)‘(𝑁 ↑ 𝐹)) = ((𝑁 · ((𝑁 − 1) ↑ 𝐹)) ∙ (((𝐼 mPSDer 𝑅)‘𝑋)‘𝐹)))
Definition	df-algind 22472*	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 ↾ 𝑣)))})
11.3.5  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 22502. 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 22502). 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 22473	Univariate power series.
class PwSer1
Syntax	cv1 22474	The base variable of a univariate power series.
class var1
Syntax	cpl1 22475	Univariate polynomials.
class Poly1
Syntax	cco1 22476	Coefficient function for a univariate polynomial.
class coe1
Syntax	ctp1 22477	Convert a univariate polynomial representation to multivariate.
class toPoly1
Definition	df-psr1 22478	Define the algebra of univariate power series. (Contributed by Mario Carneiro, 29-Dec-2014.)
⊢ PwSer1 = (𝑟 ∈ V ↦ ((1o ordPwSer 𝑟)‘∅))
Definition	df-vr1 22479	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 ↦ ((1o mVar 𝑟)‘∅))
Definition	df-ply1 22480	Define the algebra of univariate polynomials. (Contributed by Mario Carneiro, 9-Feb-2015.)
⊢ Poly1 = (𝑟 ∈ V ↦ ((PwSer1‘𝑟) ↾s (Base‘(1o mPoly 𝑟))))
Definition	df-coe1 22481*	Define the coefficient function for a univariate polynomial. (Contributed by Stefan O'Rear, 21-Mar-2015.)
⊢ coe1 = (𝑓 ∈ V ↦ (𝑛 ∈ ℕ0 ↦ (𝑓‘(1o × {𝑛}))))
Definition	df-toply1 22482*	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 ↑m 1o) ↦ (𝑓‘(𝑛‘∅))))
Theorem	psr1baslem 22483	The set of finite bags on 1o is just the set of all functions from 1o to ℕ0. (Contributed by Mario Carneiro, 9-Feb-2015.)
⊢ (ℕ0 ↑m 1o) = {𝑓 ∈ (ℕ0 ↑m 1o) ∣ (◡𝑓 “ ℕ) ∈ Fin}
Theorem	psr1val 22484	Value of the ring of univariate power series. (Contributed by Mario Carneiro, 8-Feb-2015.)
⊢ 𝑆 = (PwSer1‘𝑅)    ⇒   ⊢ 𝑆 = ((1o ordPwSer 𝑅)‘∅)
Theorem	psr1crng 22485	The ring of univariate power series is a commutative ring. (Contributed by Mario Carneiro, 8-Feb-2015.)
⊢ 𝑆 = (PwSer1‘𝑅)    ⇒   ⊢ (𝑅 ∈ CRing → 𝑆 ∈ CRing)
Theorem	psr1assa 22486	The ring of univariate power series is an associative algebra. (Contributed by Mario Carneiro, 8-Feb-2015.)
⊢ 𝑆 = (PwSer1‘𝑅)    ⇒   ⊢ (𝑅 ∈ CRing → 𝑆 ∈ AssAlg)
Theorem	psr1tos 22487	The ordered power series structure is a totally ordered set. (Contributed by Mario Carneiro, 2-Jun-2015.)
⊢ 𝑆 = (PwSer1‘𝑅)    ⇒   ⊢ (𝑅 ∈ Toset → 𝑆 ∈ Toset)
Theorem	psr1bas2 22488	The base set of the ring of univariate power series. (Contributed by Mario Carneiro, 3-Jul-2015.)
⊢ 𝑆 = (PwSer1‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑆)    &   ⊢ 𝑂 = (1o mPwSer 𝑅)    ⇒   ⊢ 𝐵 = (Base‘𝑂)
Theorem	psr1bas 22489	The base set of the ring of univariate power series. (Contributed by Mario Carneiro, 8-Feb-2015.)
⊢ 𝑆 = (PwSer1‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑆)    &   ⊢ 𝐾 = (Base‘𝑅)    ⇒   ⊢ 𝐵 = (𝐾 ↑m (ℕ0 ↑m 1o))
Theorem	vr1val 22490	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 1o = {∅} 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‘𝑅)    ⇒   ⊢ 𝑋 = ((1o mVar 𝑅)‘∅)
Theorem	vr1cl2 22491	The variable 𝑋 is a member of the power series algebra 𝑅[[𝑋]]. (Contributed by Mario Carneiro, 8-Feb-2015.)
⊢ 𝑋 = (var1‘𝑅)    &   ⊢ 𝑆 = (PwSer1‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑆)    ⇒   ⊢ (𝑅 ∈ Ring → 𝑋 ∈ 𝐵)
Theorem	ply1val 22492	The value of the set of univariate polynomials. (Contributed by Mario Carneiro, 9-Feb-2015.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝑆 = (PwSer1‘𝑅)    ⇒   ⊢ 𝑃 = (𝑆 ↾s (Base‘(1o mPoly 𝑅)))
Theorem	ply1bas 22493	The value of the base set of univariate polynomials. (Contributed by Mario Carneiro, 9-Feb-2015.) Remove hypothesis. (Revised by SN, 20-May-2025.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝑈 = (Base‘𝑃)    ⇒   ⊢ 𝑈 = (Base‘(1o mPoly 𝑅))
Theorem	ply1lss 22494	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 22495	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 22496	The ring of univariate polynomials is a commutative ring. (Contributed by Mario Carneiro, 9-Feb-2015.)
⊢ 𝑃 = (Poly1‘𝑅)    ⇒   ⊢ (𝑅 ∈ CRing → 𝑃 ∈ CRing)
Theorem	ply1assa 22497	The ring of univariate polynomials is an associative algebra. (Contributed by Mario Carneiro, 9-Feb-2015.)
⊢ 𝑃 = (Poly1‘𝑅)    ⇒   ⊢ (𝑅 ∈ CRing → 𝑃 ∈ AssAlg)
Theorem	psr1bascl 22498	A univariate power series is a multivariate power series on one index. (Contributed by Stefan O'Rear, 25-Mar-2015.)
⊢ 𝑃 = (PwSer1‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑃)    ⇒   ⊢ (𝐹 ∈ 𝐵 → 𝐹 ∈ (Base‘(1o mPwSer 𝑅)))
Theorem	psr1basf 22499	Univariate power series base set elements are functions. (Contributed by Stefan O'Rear, 25-Mar-2015.)
⊢ 𝑃 = (PwSer1‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 𝐾 = (Base‘𝑅)    ⇒   ⊢ (𝐹 ∈ 𝐵 → 𝐹:(ℕ0 ↑m 1o)⟶𝐾)
Theorem	ply1basf 22500	Univariate polynomial base set elements are functions. (Contributed by Stefan O'Rear, 21-Mar-2015.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 𝐾 = (Base‘𝑅)    ⇒   ⊢ (𝐹 ∈ 𝐵 → 𝐹:(ℕ0 ↑m 1o)⟶𝐾)