P. 214 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 21301-21400   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	evlslem1 21301*	Lemma for evlseu 21302, give a formula for (the unique) polynomial evaluation homomorphism. (Contributed by Stefan O'Rear, 9-Mar-2015.) (Proof shortened by AV, 26-Jul-2019.) (Revised by AV, 11-Apr-2024.)
⊢ 𝑃 = (𝐼 mPoly 𝑅)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 𝐶 = (Base‘𝑆)    &   ⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin}    &   ⊢ 𝑇 = (mulGrp‘𝑆)    &   ⊢ ↑ = (.g‘𝑇)    &   ⊢ · = (.r‘𝑆)    &   ⊢ 𝑉 = (𝐼 mVar 𝑅)    &   ⊢ 𝐸 = (𝑝 ∈ 𝐵 ↦ (𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑝‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))))))    &   ⊢ (𝜑 → 𝐼 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝑆 ∈ CRing)    &   ⊢ (𝜑 → 𝐹 ∈ (𝑅 RingHom 𝑆))    &   ⊢ (𝜑 → 𝐺:𝐼⟶𝐶)    &   ⊢ 𝐴 = (algSc‘𝑃)    ⇒   ⊢ (𝜑 → (𝐸 ∈ (𝑃 RingHom 𝑆) ∧ (𝐸 ∘ 𝐴) = 𝐹 ∧ (𝐸 ∘ 𝑉) = 𝐺))
Theorem	evlseu 21302*	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.) (Revised by AV, 11-Apr-2024.)
⊢ 𝑃 = (𝐼 mPoly 𝑅)    &   ⊢ 𝐶 = (Base‘𝑆)    &   ⊢ 𝐴 = (algSc‘𝑃)    &   ⊢ 𝑉 = (𝐼 mVar 𝑅)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝑆 ∈ CRing)    &   ⊢ (𝜑 → 𝐹 ∈ (𝑅 RingHom 𝑆))    &   ⊢ (𝜑 → 𝐺:𝐼⟶𝐶)    ⇒   ⊢ (𝜑 → ∃!𝑚 ∈ (𝑃 RingHom 𝑆)((𝑚 ∘ 𝐴) = 𝐹 ∧ (𝑚 ∘ 𝑉) = 𝐺))
Theorem	reldmevls 21303	Well-behaved binary operation property of evalSub. (Contributed by Stefan O'Rear, 19-Mar-2015.)
⊢ Rel dom evalSub
Theorem	mpfrcl 21304	Reverse closure for the set of polynomial functions. (Contributed by Stefan O'Rear, 19-Mar-2015.)
⊢ 𝑄 = ran ((𝐼 evalSub 𝑆)‘𝑅)    ⇒   ⊢ (𝑋 ∈ 𝑄 → (𝐼 ∈ V ∧ 𝑆 ∈ CRing ∧ 𝑅 ∈ (SubRing‘𝑆)))
Theorem	evlsval 21305*	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 (𝐵 ↑m 𝐼))    &   ⊢ 𝐵 = (Base‘𝑆)    &   ⊢ 𝐴 = (algSc‘𝑊)    &   ⊢ 𝑋 = (𝑥 ∈ 𝑅 ↦ ((𝐵 ↑m 𝐼) × {𝑥}))    &   ⊢ 𝑌 = (𝑥 ∈ 𝐼 ↦ (𝑔 ∈ (𝐵 ↑m 𝐼) ↦ (𝑔‘𝑥)))    ⇒   ⊢ ((𝐼 ∈ 𝑍 ∧ 𝑆 ∈ CRing ∧ 𝑅 ∈ (SubRing‘𝑆)) → 𝑄 = (℩𝑓 ∈ (𝑊 RingHom 𝑇)((𝑓 ∘ 𝐴) = 𝑋 ∧ (𝑓 ∘ 𝑉) = 𝑌)))
Theorem	evlsval2 21306*	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 (𝐵 ↑m 𝐼))    &   ⊢ 𝐵 = (Base‘𝑆)    &   ⊢ 𝐴 = (algSc‘𝑊)    &   ⊢ 𝑋 = (𝑥 ∈ 𝑅 ↦ ((𝐵 ↑m 𝐼) × {𝑥}))    &   ⊢ 𝑌 = (𝑥 ∈ 𝐼 ↦ (𝑔 ∈ (𝐵 ↑m 𝐼) ↦ (𝑔‘𝑥)))    ⇒   ⊢ ((𝐼 ∈ 𝑍 ∧ 𝑆 ∈ CRing ∧ 𝑅 ∈ (SubRing‘𝑆)) → (𝑄 ∈ (𝑊 RingHom 𝑇) ∧ ((𝑄 ∘ 𝐴) = 𝑋 ∧ (𝑄 ∘ 𝑉) = 𝑌)))
Theorem	evlsrhm 21307	Polynomial evaluation is a homomorphism (into the product ring). (Contributed by Stefan O'Rear, 12-Mar-2015.)
⊢ 𝑄 = ((𝐼 evalSub 𝑆)‘𝑅)    &   ⊢ 𝑊 = (𝐼 mPoly 𝑈)    &   ⊢ 𝑈 = (𝑆 ↾s 𝑅)    &   ⊢ 𝑇 = (𝑆 ↑s (𝐵 ↑m 𝐼))    &   ⊢ 𝐵 = (Base‘𝑆)    ⇒   ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑆 ∈ CRing ∧ 𝑅 ∈ (SubRing‘𝑆)) → 𝑄 ∈ (𝑊 RingHom 𝑇))
Theorem	evlssca 21308	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‘𝑆))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑅)    ⇒   ⊢ (𝜑 → (𝑄‘(𝐴‘𝑋)) = ((𝐵 ↑m 𝐼) × {𝑋}))
Theorem	evlsvar 21309*	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‘𝑆))    &   ⊢ (𝜑 → 𝑋 ∈ 𝐼)    ⇒   ⊢ (𝜑 → (𝑄‘(𝑉‘𝑋)) = (𝑔 ∈ (𝐵 ↑m 𝐼) ↦ (𝑔‘𝑋)))
Theorem	evlsgsumadd 21310*	Polynomial evaluation maps (additive) group sums to group sums. (Contributed by SN, 13-Feb-2024.)
⊢ 𝑄 = ((𝐼 evalSub 𝑆)‘𝑅)    &   ⊢ 𝑊 = (𝐼 mPoly 𝑈)    &   ⊢ 0 = (0g‘𝑊)    &   ⊢ 𝑈 = (𝑆 ↾s 𝑅)    &   ⊢ 𝑃 = (𝑆 ↑s (𝐾 ↑m 𝐼))    &   ⊢ 𝐾 = (Base‘𝑆)    &   ⊢ 𝐵 = (Base‘𝑊)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑆 ∈ CRing)    &   ⊢ (𝜑 → 𝑅 ∈ (SubRing‘𝑆))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑁) → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑁 ⊆ ℕ0)    &   ⊢ (𝜑 → (𝑥 ∈ 𝑁 ↦ 𝑌) finSupp 0 )    ⇒   ⊢ (𝜑 → (𝑄‘(𝑊 Σg (𝑥 ∈ 𝑁 ↦ 𝑌))) = (𝑃 Σg (𝑥 ∈ 𝑁 ↦ (𝑄‘𝑌))))
Theorem	evlsgsummul 21311*	Polynomial evaluation maps (multiplicative) group sums to group sums. (Contributed by SN, 13-Feb-2024.)
⊢ 𝑄 = ((𝐼 evalSub 𝑆)‘𝑅)    &   ⊢ 𝑊 = (𝐼 mPoly 𝑈)    &   ⊢ 𝐺 = (mulGrp‘𝑊)    &   ⊢ 1 = (1r‘𝑊)    &   ⊢ 𝑈 = (𝑆 ↾s 𝑅)    &   ⊢ 𝑃 = (𝑆 ↑s (𝐾 ↑m 𝐼))    &   ⊢ 𝐻 = (mulGrp‘𝑃)    &   ⊢ 𝐾 = (Base‘𝑆)    &   ⊢ 𝐵 = (Base‘𝑊)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑆 ∈ CRing)    &   ⊢ (𝜑 → 𝑅 ∈ (SubRing‘𝑆))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑁) → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑁 ⊆ ℕ0)    &   ⊢ (𝜑 → (𝑥 ∈ 𝑁 ↦ 𝑌) finSupp 1 )    ⇒   ⊢ (𝜑 → (𝑄‘(𝐺 Σg (𝑥 ∈ 𝑁 ↦ 𝑌))) = (𝐻 Σg (𝑥 ∈ 𝑁 ↦ (𝑄‘𝑌))))
Theorem	evlspw 21312	Polynomial evaluation for subrings maps the exponentiation of a polynomial to the exponentiation of the evaluated polynomial. (Contributed by SN, 29-Feb-2024.)
⊢ 𝑄 = ((𝐼 evalSub 𝑆)‘𝑅)    &   ⊢ 𝑊 = (𝐼 mPoly 𝑈)    &   ⊢ 𝐺 = (mulGrp‘𝑊)    &   ⊢ ↑ = (.g‘𝐺)    &   ⊢ 𝑈 = (𝑆 ↾s 𝑅)    &   ⊢ 𝑃 = (𝑆 ↑s (𝐾 ↑m 𝐼))    &   ⊢ 𝐻 = (mulGrp‘𝑃)    &   ⊢ 𝐾 = (Base‘𝑆)    &   ⊢ 𝐵 = (Base‘𝑊)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑆 ∈ CRing)    &   ⊢ (𝜑 → 𝑅 ∈ (SubRing‘𝑆))    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝑄‘(𝑁 ↑ 𝑋)) = (𝑁(.g‘𝐻)(𝑄‘𝑋)))
Theorem	evlsvarpw 21313	Polynomial evaluation for subrings maps the exponentiation of a variable to the exponentiation of the evaluated variable. (Contributed by SN, 21-Feb-2024.)
⊢ 𝑄 = ((𝐼 evalSub 𝑆)‘𝑅)    &   ⊢ 𝑊 = (𝐼 mPoly 𝑈)    &   ⊢ 𝐺 = (mulGrp‘𝑊)    &   ⊢ ↑ = (.g‘𝐺)    &   ⊢ 𝑋 = ((𝐼 mVar 𝑈)‘𝑌)    &   ⊢ 𝑈 = (𝑆 ↾s 𝑅)    &   ⊢ 𝑃 = (𝑆 ↑s (𝐵 ↑m 𝐼))    &   ⊢ 𝐻 = (mulGrp‘𝑃)    &   ⊢ 𝐵 = (Base‘𝑆)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐼)    &   ⊢ (𝜑 → 𝑆 ∈ CRing)    &   ⊢ (𝜑 → 𝑅 ∈ (SubRing‘𝑆))    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    ⇒   ⊢ (𝜑 → (𝑄‘(𝑁 ↑ 𝑋)) = (𝑁(.g‘𝐻)(𝑄‘𝑋)))
Theorem	evlval 21314	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 21315	The simple evaluation map is a ring homomorphism. (Contributed by Mario Carneiro, 12-Jun-2015.)
⊢ 𝑄 = (𝐼 eval 𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝑊 = (𝐼 mPoly 𝑅)    &   ⊢ 𝑇 = (𝑅 ↑s (𝐵 ↑m 𝐼))    ⇒   ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑅 ∈ CRing) → 𝑄 ∈ (𝑊 RingHom 𝑇))
Theorem	evlsscasrng 21316	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 21317	Simple polynomial evaluation maps scalars to constant functions. (Contributed by AV, 12-Sep-2019.)
⊢ 𝑄 = (𝐼 eval 𝑆)    &   ⊢ 𝑊 = (𝐼 mPoly 𝑆)    &   ⊢ 𝐵 = (Base‘𝑆)    &   ⊢ 𝐴 = (algSc‘𝑊)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑆 ∈ CRing)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝑄‘(𝐴‘𝑋)) = ((𝐵 ↑m 𝐼) × {𝑋}))
Theorem	evlsvarsrng 21318	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 21319*	Simple polynomial evaluation maps variables to projections. (Contributed by AV, 12-Sep-2019.)
⊢ 𝑄 = (𝐼 eval 𝑆)    &   ⊢ 𝑉 = (𝐼 mVar 𝑆)    &   ⊢ 𝐵 = (Base‘𝑆)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑆 ∈ CRing)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐼)    ⇒   ⊢ (𝜑 → (𝑄‘(𝑉‘𝑋)) = (𝑔 ∈ (𝐵 ↑m 𝐼) ↦ (𝑔‘𝑋)))
Theorem	mpfconst 21320	Constants are multivariate polynomial functions. (Contributed by Mario Carneiro, 19-Mar-2015.)
⊢ 𝐵 = (Base‘𝑆)    &   ⊢ 𝑄 = ran ((𝐼 evalSub 𝑆)‘𝑅)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑆 ∈ CRing)    &   ⊢ (𝜑 → 𝑅 ∈ (SubRing‘𝑆))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑅)    ⇒   ⊢ (𝜑 → ((𝐵 ↑m 𝐼) × {𝑋}) ∈ 𝑄)
Theorem	mpfproj 21321*	Projections are multivariate polynomial functions. (Contributed by Mario Carneiro, 20-Mar-2015.)
⊢ 𝐵 = (Base‘𝑆)    &   ⊢ 𝑄 = ran ((𝐼 evalSub 𝑆)‘𝑅)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑆 ∈ CRing)    &   ⊢ (𝜑 → 𝑅 ∈ (SubRing‘𝑆))    &   ⊢ (𝜑 → 𝐽 ∈ 𝐼)    ⇒   ⊢ (𝜑 → (𝑓 ∈ (𝐵 ↑m 𝐼) ↦ (𝑓‘𝐽)) ∈ 𝑄)
Theorem	mpfsubrg 21322	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‘𝑆) ↑m 𝐼))))
Theorem	mpff 21323	Polynomial functions are functions. (Contributed by Mario Carneiro, 19-Mar-2015.)
⊢ 𝑄 = ran ((𝐼 evalSub 𝑆)‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑆)    ⇒   ⊢ (𝐹 ∈ 𝑄 → 𝐹:(𝐵 ↑m 𝐼)⟶𝐵)
Theorem	mpfaddcl 21324	The sum of multivariate polynomial functions. (Contributed by Mario Carneiro, 19-Mar-2015.)
⊢ 𝑄 = ran ((𝐼 evalSub 𝑆)‘𝑅)    &   ⊢ + = (+g‘𝑆)    ⇒   ⊢ ((𝐹 ∈ 𝑄 ∧ 𝐺 ∈ 𝑄) → (𝐹 ∘f + 𝐺) ∈ 𝑄)
Theorem	mpfmulcl 21325	The product of multivariate polynomial functions. (Contributed by Mario Carneiro, 19-Mar-2015.)
⊢ 𝑄 = ran ((𝐼 evalSub 𝑆)‘𝑅)    &   ⊢ · = (.r‘𝑆)    ⇒   ⊢ ((𝐹 ∈ 𝑄 ∧ 𝐺 ∈ 𝑄) → (𝐹 ∘f · 𝐺) ∈ 𝑄)
Theorem	mpfind 21326*	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  Additional definitions for (multivariate) polynomials
Syntax	cslv 21327	Select a subset of variables in a multivariate polynomial.
class selectVars
Syntax	cmhp 21328	Multivariate polynomials.
class mHomP
Syntax	cpsd 21329	Power series partial derivative function.
class mPSDer
Syntax	cai 21330	Algebraically independent.
class AlgInd
Definition	df-selv 21331*	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 𝑟)‘𝑥))))))))
Definition	df-mhp 21332*	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 𝑔) = 𝑛}}))
Definition	df-psd 21333*	Define the differentiation operation on multivariate polynomials. (Contributed by Mario Carneiro, 21-Mar-2015.)
⊢ mPSDer = (𝑖 ∈ V, 𝑟 ∈ V ↦ (𝑥 ∈ 𝑖 ↦ (𝑓 ∈ (Base‘(𝑖 mPwSer 𝑟)) ↦ (𝑘 ∈ {ℎ ∈ (ℕ0 ↑m 𝑖) ∣ (◡ℎ “ ℕ) ∈ Fin} ↦ (((𝑘‘𝑥) + 1)(.g‘𝑟)(𝑓‘(𝑘 ∘f + (𝑦 ∈ 𝑖 ↦ if(𝑦 = 𝑥, 1, 0)))))))))
Definition	df-algind 21334*	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 ↾ 𝑣)))})
Theorem	selvffval 21335*	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 21336*	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 21337*	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	mhpfval 21338*	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	mhpval 21339*	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 21340*	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 21341*	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 21342*	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	mhpmpl 21343	A homogeneous polynomial is a polynomial. (Contributed by Steven Nguyen, 25-Aug-2023.)
⊢ 𝐻 = (𝐼 mHomP 𝑅)    &   ⊢ 𝑃 = (𝐼 mPoly 𝑅)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑋 ∈ (𝐻‘𝑁))    ⇒   ⊢ (𝜑 → 𝑋 ∈ 𝐵)
Theorem	mhpdeg 21344*	All nonzero terms of a homogeneous polynomial have degree 𝑁. (Contributed by Steven Nguyen, 25-Aug-2023.)
⊢ 𝐻 = (𝐼 mHomP 𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin}    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑋 ∈ (𝐻‘𝑁))    ⇒   ⊢ (𝜑 → (𝑋 supp 0 ) ⊆ {𝑔 ∈ 𝐷 ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁})
Theorem	mhp0cl 21345*	The zero polynomial is homogeneous. Under df-mhp 21332, 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 25226 and df-dgr 25361 respectively) and the literature: https://math.stackexchange.com/a/1796314/593843 25361. (Contributed by SN, 12-Sep-2023.)
⊢ 𝐻 = (𝐼 mHomP 𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin}    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ Grp)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    ⇒   ⊢ (𝜑 → (𝐷 × { 0 }) ∈ (𝐻‘𝑁))
Theorem	mhpsclcl 21346	A scalar (or constant) polynomial has degree 0. Compare deg1scl 25287. In other contexts, there may be an exception for the zero polynomial, but under df-mhp 21332 the zero polynomial can be any degree (see mhp0cl 21345) so there is no exception. (Contributed by SN, 25-May-2024.)
⊢ 𝐻 = (𝐼 mHomP 𝑅)    &   ⊢ 𝑃 = (𝐼 mPoly 𝑅)    &   ⊢ 𝐴 = (algSc‘𝑃)    &   ⊢ 𝐾 = (Base‘𝑅)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝐶 ∈ 𝐾)    ⇒   ⊢ (𝜑 → (𝐴‘𝐶) ∈ (𝐻‘0))
Theorem	mhpvarcl 21347	A power series variable is a polynomial of degree 1. (Contributed by SN, 25-May-2024.)
⊢ 𝐻 = (𝐼 mHomP 𝑅)    &   ⊢ 𝑉 = (𝐼 mVar 𝑅)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐼)    ⇒   ⊢ (𝜑 → (𝑉‘𝑋) ∈ (𝐻‘1))
Theorem	mhpmulcl 21348	A product of homogeneous polynomials is a homogeneous polynomial whose degree is the sum of the degrees of the factors. Compare mdegmulle2 25253 (which shows less-than-or-equal instead of equal). (Contributed by SN, 22-Jul-2024.)
⊢ 𝐻 = (𝐼 mHomP 𝑅)    &   ⊢ 𝑌 = (𝐼 mPoly 𝑅)    &   ⊢ · = (.r‘𝑌)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝑀 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑃 ∈ (𝐻‘𝑀))    &   ⊢ (𝜑 → 𝑄 ∈ (𝐻‘𝑁))    ⇒   ⊢ (𝜑 → (𝑃 · 𝑄) ∈ (𝐻‘(𝑀 + 𝑁)))
Theorem	mhppwdeg 21349	Degree of a homogeneous polynomial raised to a power. General version of deg1pw 25294. (Contributed by SN, 26-Jul-2024.)
⊢ 𝐻 = (𝐼 mHomP 𝑅)    &   ⊢ 𝑃 = (𝐼 mPoly 𝑅)    &   ⊢ 𝑇 = (mulGrp‘𝑃)    &   ⊢ ↑ = (.g‘𝑇)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝑀 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑋 ∈ (𝐻‘𝑀))    ⇒   ⊢ (𝜑 → (𝑁 ↑ 𝑋) ∈ (𝐻‘(𝑀 · 𝑁)))
Theorem	mhpaddcl 21350	Homogeneous polynomials are closed under addition. (Contributed by SN, 26-Aug-2023.)
⊢ 𝐻 = (𝐼 mHomP 𝑅)    &   ⊢ 𝑃 = (𝐼 mPoly 𝑅)    &   ⊢ + = (+g‘𝑃)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ Grp)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑋 ∈ (𝐻‘𝑁))    &   ⊢ (𝜑 → 𝑌 ∈ (𝐻‘𝑁))    ⇒   ⊢ (𝜑 → (𝑋 + 𝑌) ∈ (𝐻‘𝑁))
Theorem	mhpinvcl 21351	Homogeneous polynomials are closed under taking the opposite. (Contributed by SN, 12-Sep-2023.)
⊢ 𝐻 = (𝐼 mHomP 𝑅)    &   ⊢ 𝑃 = (𝐼 mPoly 𝑅)    &   ⊢ 𝑀 = (invg‘𝑃)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ Grp)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑋 ∈ (𝐻‘𝑁))    ⇒   ⊢ (𝜑 → (𝑀‘𝑋) ∈ (𝐻‘𝑁))
Theorem	mhpsubg 21352	Homogeneous polynomials form a subgroup of the polynomials. (Contributed by SN, 25-Sep-2023.)
⊢ 𝐻 = (𝐼 mHomP 𝑅)    &   ⊢ 𝑃 = (𝐼 mPoly 𝑅)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ Grp)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    ⇒   ⊢ (𝜑 → (𝐻‘𝑁) ∈ (SubGrp‘𝑃))
Theorem	mhpvscacl 21353	Homogeneous polynomials are closed under scalar multiplication. (Contributed by SN, 25-Sep-2023.)
⊢ 𝐻 = (𝐼 mHomP 𝑅)    &   ⊢ 𝑃 = (𝐼 mPoly 𝑅)    &   ⊢ · = ( ·𝑠 ‘𝑃)    &   ⊢ 𝐾 = (Base‘𝑅)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐾)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐻‘𝑁))    ⇒   ⊢ (𝜑 → (𝑋 · 𝐹) ∈ (𝐻‘𝑁))
Theorem	mhplss 21354	Homogeneous polynomials form a linear subspace of the polynomials. (Contributed by SN, 25-Sep-2023.)
⊢ 𝐻 = (𝐼 mHomP 𝑅)    &   ⊢ 𝑃 = (𝐼 mPoly 𝑅)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    ⇒   ⊢ (𝜑 → (𝐻‘𝑁) ∈ (LSubSp‘𝑃))
11.3.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 21384. 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 21384). 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 21355	Univariate power series.
class PwSer1
Syntax	cv1 21356	The base variable of a univariate power series.
class var1
Syntax	cpl1 21357	Univariate polynomials.
class Poly1
Syntax	cco1 21358	Coefficient function for a univariate polynomial.
class coe1
Syntax	ctp1 21359	Convert a univariate polynomial representation to multivariate.
class toPoly1
Definition	df-psr1 21360	Define the algebra of univariate power series. (Contributed by Mario Carneiro, 29-Dec-2014.)
⊢ PwSer1 = (𝑟 ∈ V ↦ ((1o ordPwSer 𝑟)‘∅))
Definition	df-vr1 21361	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 21362	Define the algebra of univariate polynomials. (Contributed by Mario Carneiro, 9-Feb-2015.)
⊢ Poly1 = (𝑟 ∈ V ↦ ((PwSer1‘𝑟) ↾s (Base‘(1o mPoly 𝑟))))
Definition	df-coe1 21363*	Define the coefficient function for a univariate polynomial. (Contributed by Stefan O'Rear, 21-Mar-2015.)
⊢ coe1 = (𝑓 ∈ V ↦ (𝑛 ∈ ℕ0 ↦ (𝑓‘(1o × {𝑛}))))
Definition	df-toply1 21364*	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 21365	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 21366	Value of the ring of univariate power series. (Contributed by Mario Carneiro, 8-Feb-2015.)
⊢ 𝑆 = (PwSer1‘𝑅)    ⇒   ⊢ 𝑆 = ((1o ordPwSer 𝑅)‘∅)
Theorem	psr1crng 21367	The ring of univariate power series is a commutative ring. (Contributed by Mario Carneiro, 8-Feb-2015.)
⊢ 𝑆 = (PwSer1‘𝑅)    ⇒   ⊢ (𝑅 ∈ CRing → 𝑆 ∈ CRing)
Theorem	psr1assa 21368	The ring of univariate power series is an associative algebra. (Contributed by Mario Carneiro, 8-Feb-2015.)
⊢ 𝑆 = (PwSer1‘𝑅)    ⇒   ⊢ (𝑅 ∈ CRing → 𝑆 ∈ AssAlg)
Theorem	psr1tos 21369	The ordered power series structure is a totally ordered set. (Contributed by Mario Carneiro, 2-Jun-2015.)
⊢ 𝑆 = (PwSer1‘𝑅)    ⇒   ⊢ (𝑅 ∈ Toset → 𝑆 ∈ Toset)
Theorem	psr1bas2 21370	The base set of the ring of univariate power series. (Contributed by Mario Carneiro, 3-Jul-2015.)
⊢ 𝑆 = (PwSer1‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑆)    &   ⊢ 𝑂 = (1o mPwSer 𝑅)    ⇒   ⊢ 𝐵 = (Base‘𝑂)
Theorem	psr1bas 21371	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 21372	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 21373	The variable 𝑋 is a member of the power series algebra 𝑅[[𝑋]]. (Contributed by Mario Carneiro, 8-Feb-2015.)
⊢ 𝑋 = (var1‘𝑅)    &   ⊢ 𝑆 = (PwSer1‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑆)    ⇒   ⊢ (𝑅 ∈ Ring → 𝑋 ∈ 𝐵)
Theorem	ply1val 21374	The value of the set of univariate polynomials. (Contributed by Mario Carneiro, 9-Feb-2015.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝑆 = (PwSer1‘𝑅)    ⇒   ⊢ 𝑃 = (𝑆 ↾s (Base‘(1o mPoly 𝑅)))
Theorem	ply1bas 21375	The value of the base set of univariate polynomials. (Contributed by Mario Carneiro, 9-Feb-2015.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝑆 = (PwSer1‘𝑅)    &   ⊢ 𝑈 = (Base‘𝑃)    ⇒   ⊢ 𝑈 = (Base‘(1o mPoly 𝑅))
Theorem	ply1lss 21376	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 21377	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 21378	The ring of univariate polynomials is a commutative ring. (Contributed by Mario Carneiro, 9-Feb-2015.)
⊢ 𝑃 = (Poly1‘𝑅)    ⇒   ⊢ (𝑅 ∈ CRing → 𝑃 ∈ CRing)
Theorem	ply1assa 21379	The ring of univariate polynomials is an associative algebra. (Contributed by Mario Carneiro, 9-Feb-2015.)
⊢ 𝑃 = (Poly1‘𝑅)    ⇒   ⊢ (𝑅 ∈ CRing → 𝑃 ∈ AssAlg)
Theorem	psr1bascl 21380	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 21381	Univariate power series base set elements are functions. (Contributed by Stefan O'Rear, 25-Mar-2015.)
⊢ 𝑃 = (PwSer1‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 𝐾 = (Base‘𝑅)    ⇒   ⊢ (𝐹 ∈ 𝐵 → 𝐹:(ℕ0 ↑m 1o)⟶𝐾)
Theorem	ply1basf 21382	Univariate polynomial base set elements are functions. (Contributed by Stefan O'Rear, 21-Mar-2015.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 𝐾 = (Base‘𝑅)    ⇒   ⊢ (𝐹 ∈ 𝐵 → 𝐹:(ℕ0 ↑m 1o)⟶𝐾)
Theorem	ply1bascl 21383	A univariate polynomial is a univariate power series. (Contributed by Stefan O'Rear, 25-Mar-2015.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑃)    ⇒   ⊢ (𝐹 ∈ 𝐵 → 𝐹 ∈ (Base‘(PwSer1‘𝑅)))
Theorem	ply1bascl2 21384	A univariate polynomial is a multivariate polynomial on one index. (Contributed by Stefan O'Rear, 25-Mar-2015.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑃)    ⇒   ⊢ (𝐹 ∈ 𝐵 → 𝐹 ∈ (Base‘(1o mPoly 𝑅)))
Theorem	coe1fval 21385*	Value of the univariate polynomial coefficient function. (Contributed by Stefan O'Rear, 21-Mar-2015.)
⊢ 𝐴 = (coe1‘𝐹)    ⇒   ⊢ (𝐹 ∈ 𝑉 → 𝐴 = (𝑛 ∈ ℕ0 ↦ (𝐹‘(1o × {𝑛}))))
Theorem	coe1fv 21386	Value of an evaluated coefficient in a polynomial coefficient vector. (Contributed by Stefan O'Rear, 21-Mar-2015.)
⊢ 𝐴 = (coe1‘𝐹)    ⇒   ⊢ ((𝐹 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) → (𝐴‘𝑁) = (𝐹‘(1o × {𝑁})))
Theorem	fvcoe1 21387	Value of a multivariate coefficient in terms of the coefficient vector. (Contributed by Stefan O'Rear, 21-Mar-2015.)
⊢ 𝐴 = (coe1‘𝐹)    ⇒   ⊢ ((𝐹 ∈ 𝑉 ∧ 𝑋 ∈ (ℕ0 ↑m 1o)) → (𝐹‘𝑋) = (𝐴‘(𝑋‘∅)))
Theorem	coe1fval3 21388*	Univariate power series coefficient vectors expressed as a function composition. (Contributed by Stefan O'Rear, 25-Mar-2015.)
⊢ 𝐴 = (coe1‘𝐹)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 𝑃 = (PwSer1‘𝑅)    &   ⊢ 𝐺 = (𝑦 ∈ ℕ0 ↦ (1o × {𝑦}))    ⇒   ⊢ (𝐹 ∈ 𝐵 → 𝐴 = (𝐹 ∘ 𝐺))
Theorem	coe1f2 21389	Functionality of univariate power series coefficient vectors. (Contributed by Stefan O'Rear, 25-Mar-2015.)
⊢ 𝐴 = (coe1‘𝐹)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 𝑃 = (PwSer1‘𝑅)    &   ⊢ 𝐾 = (Base‘𝑅)    ⇒   ⊢ (𝐹 ∈ 𝐵 → 𝐴:ℕ0⟶𝐾)
Theorem	coe1fval2 21390*	Univariate polynomial coefficient vectors expressed as a function composition. (Contributed by Stefan O'Rear, 21-Mar-2015.)
⊢ 𝐴 = (coe1‘𝐹)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐺 = (𝑦 ∈ ℕ0 ↦ (1o × {𝑦}))    ⇒   ⊢ (𝐹 ∈ 𝐵 → 𝐴 = (𝐹 ∘ 𝐺))
Theorem	coe1f 21391	Functionality of univariate polynomial coefficient vectors. (Contributed by Stefan O'Rear, 21-Mar-2015.)
⊢ 𝐴 = (coe1‘𝐹)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐾 = (Base‘𝑅)    ⇒   ⊢ (𝐹 ∈ 𝐵 → 𝐴:ℕ0⟶𝐾)
Theorem	coe1fvalcl 21392	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 21393	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 21394*	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‘𝑅)    ⇒   ⊢ (𝐹 ∈ 𝐵 → 𝐴 ∈ {𝑔 ∈ (𝐾 ↑m ℕ0) ∣ 𝑔 finSupp 0 })
Theorem	mptcoe1fsupp 21395*	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 21396*	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 21397	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 21398	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 21399	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 21400	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‘𝑆)