P. 343 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 34201-34300   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	deg1le0eq0 34201	A polynomial with nonpositive degree is the zero polynomial iff its constant term is zero. Biconditional version of deg1scl 26475. (Contributed by Thierry Arnoux, 22-Mar-2025.)
⊢ 𝐷 = (deg1‘𝑅)    &   ⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 𝑂 = (0g‘𝑃)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝐹 ∈ 𝐵)    &   ⊢ (𝜑 → (𝐷‘𝐹) ≤ 0)    ⇒   ⊢ (𝜑 → (𝐹 = 𝑂 ↔ ((coe1‘𝐹)‘0) = 0 ))
Theorem	ply1asclunit 34202	A nonzero scalar polynomial over a field 𝐹 is a unit. (Contributed by Thierry Arnoux, 22-Mar-2025.)
⊢ 𝑃 = (Poly1‘𝐹)    &   ⊢ 𝐴 = (algSc‘𝑃)    &   ⊢ 𝐵 = (Base‘𝐹)    &   ⊢ 0 = (0g‘𝐹)    &   ⊢ (𝜑 → 𝐹 ∈ Field)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ≠ 0 )    ⇒   ⊢ (𝜑 → (𝐴‘𝑌) ∈ (Unit‘𝑃))
Theorem	ply1unit 34203	In a field 𝐹, a polynomial 𝐶 is a unit iff it has degree 0. This corresponds to the nonzero scalars, see ply1asclunit 34202. (Contributed by Thierry Arnoux, 25-Apr-2025.)
⊢ 𝑃 = (Poly1‘𝐹)    &   ⊢ 𝐴 = (algSc‘𝑃)    &   ⊢ 𝐵 = (Base‘𝐹)    &   ⊢ 0 = (0g‘𝐹)    &   ⊢ (𝜑 → 𝐹 ∈ Field)    &   ⊢ 𝐷 = (deg1‘𝐹)    &   ⊢ (𝜑 → 𝐶 ∈ (Base‘𝑃))    ⇒   ⊢ (𝜑 → (𝐶 ∈ (Unit‘𝑃) ↔ (𝐷‘𝐶) = 0))
Theorem	evl1deg1 34204	Evaluation of a univariate polynomial of degree 1. (Contributed by Thierry Arnoux, 8-Jun-2025.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝑂 = (eval1‘𝑅)    &   ⊢ 𝐾 = (Base‘𝑅)    &   ⊢ 𝑈 = (Base‘𝑃)    &   ⊢ · = (.r‘𝑅)    &   ⊢ + = (+g‘𝑅)    &   ⊢ 𝐶 = (coe1‘𝑀)    &   ⊢ 𝐷 = (deg1‘𝑅)    &   ⊢ 𝐴 = (𝐶‘1)    &   ⊢ 𝐵 = (𝐶‘0)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝑀 ∈ 𝑈)    &   ⊢ (𝜑 → (𝐷‘𝑀) = 1)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐾)    ⇒   ⊢ (𝜑 → ((𝑂‘𝑀)‘𝑋) = ((𝐴 · 𝑋) + 𝐵))
Theorem	evl1deg2 34205	Evaluation of a univariate polynomial of degree 2. (Contributed by Thierry Arnoux, 22-Jun-2025.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝑂 = (eval1‘𝑅)    &   ⊢ 𝐾 = (Base‘𝑅)    &   ⊢ 𝑈 = (Base‘𝑃)    &   ⊢ · = (.r‘𝑅)    &   ⊢ + = (+g‘𝑅)    &   ⊢ ↑ = (.g‘(mulGrp‘𝑅))    &   ⊢ 𝐹 = (coe1‘𝑀)    &   ⊢ 𝐸 = (deg1‘𝑅)    &   ⊢ 𝐴 = (𝐹‘2)    &   ⊢ 𝐵 = (𝐹‘1)    &   ⊢ 𝐶 = (𝐹‘0)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝑀 ∈ 𝑈)    &   ⊢ (𝜑 → (𝐸‘𝑀) = 2)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐾)    ⇒   ⊢ (𝜑 → ((𝑂‘𝑀)‘𝑋) = ((𝐴 · (2 ↑ 𝑋)) + ((𝐵 · 𝑋) + 𝐶)))
Theorem	evl1deg3 34206	Evaluation of a univariate polynomial of degree 3. (Contributed by Thierry Arnoux, 14-Jun-2025.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝑂 = (eval1‘𝑅)    &   ⊢ 𝐾 = (Base‘𝑅)    &   ⊢ 𝑈 = (Base‘𝑃)    &   ⊢ · = (.r‘𝑅)    &   ⊢ + = (+g‘𝑅)    &   ⊢ ↑ = (.g‘(mulGrp‘𝑅))    &   ⊢ 𝐹 = (coe1‘𝑀)    &   ⊢ 𝐸 = (deg1‘𝑅)    &   ⊢ 𝐴 = (𝐹‘3)    &   ⊢ 𝐵 = (𝐹‘2)    &   ⊢ 𝐶 = (𝐹‘1)    &   ⊢ 𝐷 = (𝐹‘0)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝑀 ∈ 𝑈)    &   ⊢ (𝜑 → (𝐸‘𝑀) = 3)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐾)    ⇒   ⊢ (𝜑 → ((𝑂‘𝑀)‘𝑋) = (((𝐴 · (3 ↑ 𝑋)) + (𝐵 · (2 ↑ 𝑋))) + ((𝐶 · 𝑋) + 𝐷)))
Theorem	evls1monply1 34207	Subring evaluation of a scaled monomial. (Contributed by Thierry Arnoux, 10-Jan-2026.)
⊢ 𝑄 = (𝑆 evalSub1 𝑅)    &   ⊢ 𝐾 = (Base‘𝑆)    &   ⊢ 𝑊 = (Poly1‘𝑈)    &   ⊢ 𝑈 = (𝑆 ↾s 𝑅)    &   ⊢ 𝑋 = (var1‘𝑈)    &   ⊢ ↑ = (.g‘(mulGrp‘𝑊))    &   ⊢ ∧ = (.g‘(mulGrp‘𝑆))    &   ⊢ ∗ = ( ·𝑠 ‘𝑊)    &   ⊢ · = (.r‘𝑆)    &   ⊢ (𝜑 → 𝑆 ∈ CRing)    &   ⊢ (𝜑 → 𝑅 ∈ (SubRing‘𝑆))    &   ⊢ (𝜑 → 𝐴 ∈ 𝑅)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐾)    ⇒   ⊢ (𝜑 → ((𝑄‘(𝐴 ∗ (𝑁 ↑ 𝑋)))‘𝑌) = (𝐴 · (𝑁 ∧ 𝑌)))
Theorem	ply1dg1rt 34208	Express the root − 𝐵 / 𝐴 of a polynomial 𝐴 · 𝑋 + 𝐵 of degree 1 over a field. (Contributed by Thierry Arnoux, 8-Jun-2025.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝑈 = (Base‘𝑃)    &   ⊢ 𝑂 = (eval1‘𝑅)    &   ⊢ 𝐷 = (deg1‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ Field)    &   ⊢ (𝜑 → 𝐺 ∈ 𝑈)    &   ⊢ (𝜑 → (𝐷‘𝐺) = 1)    &   ⊢ 𝑁 = (invg‘𝑅)    &   ⊢ / = (/r‘𝑅)    &   ⊢ 𝐶 = (coe1‘𝐺)    &   ⊢ 𝐴 = (𝐶‘1)    &   ⊢ 𝐵 = (𝐶‘0)    &   ⊢ 𝑍 = ((𝑁‘𝐵) / 𝐴)    ⇒   ⊢ (𝜑 → (◡(𝑂‘𝐺) “ { 0 }) = {𝑍})
Theorem	ply1dg1rtn0 34209	Polynomials of degree 1 over a field always have some roots. (Contributed by Thierry Arnoux, 8-Jun-2025.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝑈 = (Base‘𝑃)    &   ⊢ 𝑂 = (eval1‘𝑅)    &   ⊢ 𝐷 = (deg1‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ Field)    &   ⊢ (𝜑 → 𝐺 ∈ 𝑈)    &   ⊢ (𝜑 → (𝐷‘𝐺) = 1)    ⇒   ⊢ (𝜑 → (◡(𝑂‘𝐺) “ { 0 }) ≠ ∅)
Theorem	ply1mulrtss 34210	The roots of a factor 𝐹 are also roots of the product of polynomials (𝐹 · 𝐺). (Contributed by Thierry Arnoux, 8-Jun-2025.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝑈 = (Base‘𝑃)    &   ⊢ 𝑂 = (eval1‘𝑅)    &   ⊢ 𝐷 = (deg1‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐺 ∈ 𝑈)    &   ⊢ · = (.r‘𝑃)    ⇒   ⊢ (𝜑 → (◡(𝑂‘𝐹) “ { 0 }) ⊆ (◡(𝑂‘(𝐹 · 𝐺)) “ { 0 }))
Theorem	deg1prod 34211*	Degree of a product of polynomials. (Contributed by Thierry Arnoux, 15-Feb-2026.)
⊢ 𝐷 = (deg1‘𝑅)    &   ⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 𝑀 = (mulGrp‘𝑃)    &   ⊢ 0 = (0g‘𝑃)    &   ⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ (𝜑 → 𝑅 ∈ IDomn)    &   ⊢ (𝜑 → 𝐹:𝐴⟶(𝐵 ∖ { 0 }))    ⇒   ⊢ (𝜑 → (𝐷‘(𝑀 Σg 𝐹)) = Σ𝑘 ∈ 𝐴 (𝐷‘(𝐹‘𝑘)))
Theorem	ply1dg3rt0irred 34212	If a cubic polynomial over a field has no roots, it is irreducible. (Proposed by Saveliy Skresanov, 5-Jun-2025.) (Contributed by Thierry Arnoux, 8-Jun-2025.)
⊢ 0 = (0g‘𝐹)    &   ⊢ 𝑂 = (eval1‘𝐹)    &   ⊢ 𝐷 = (deg1‘𝐹)    &   ⊢ 𝑃 = (Poly1‘𝐹)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ (𝜑 → 𝐹 ∈ Field)    &   ⊢ (𝜑 → 𝑄 ∈ 𝐵)    &   ⊢ (𝜑 → (◡(𝑂‘𝑄) “ { 0 }) = ∅)    &   ⊢ (𝜑 → (𝐷‘𝑄) = 3)    ⇒   ⊢ (𝜑 → 𝑄 ∈ (Irred‘𝑃))
Theorem	m1pmeq 34213	If two monic polynomials 𝐼 and 𝐽 differ by a unit factor 𝐾, then they are equal. (Contributed by Thierry Arnoux, 27-Apr-2025.)
⊢ 𝑃 = (Poly1‘𝐹)    &   ⊢ 𝑀 = (Monic1p‘𝐹)    &   ⊢ 𝑈 = (Unit‘𝑃)    &   ⊢ · = (.r‘𝑃)    &   ⊢ (𝜑 → 𝐹 ∈ Field)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑀)    &   ⊢ (𝜑 → 𝐽 ∈ 𝑀)    &   ⊢ (𝜑 → 𝐾 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐼 = (𝐾 · 𝐽))    ⇒   ⊢ (𝜑 → 𝐼 = 𝐽)
Theorem	ply1fermltl 34214	Fermat's little theorem for polynomials. If 𝑃 is prime, Then (𝑋 + 𝐴)↑𝑃 = ((𝑋↑𝑃) + 𝐴) modulo 𝑃. (Contributed by Thierry Arnoux, 24-Jul-2024.)
⊢ 𝑍 = (ℤ/nℤ‘𝑃)    &   ⊢ 𝑊 = (Poly1‘𝑍)    &   ⊢ 𝑋 = (var1‘𝑍)    &   ⊢ + = (+g‘𝑊)    &   ⊢ 𝑁 = (mulGrp‘𝑊)    &   ⊢ ↑ = (.g‘𝑁)    &   ⊢ 𝐶 = (algSc‘𝑊)    &   ⊢ 𝐴 = (𝐶‘((ℤRHom‘𝑍)‘𝐸))    &   ⊢ (𝜑 → 𝑃 ∈ ℙ)    &   ⊢ (𝜑 → 𝐸 ∈ ℤ)    ⇒   ⊢ (𝜑 → (𝑃 ↑ (𝑋 + 𝐴)) = ((𝑃 ↑ 𝑋) + 𝐴))
Theorem	coe1mon 34215*	Coefficient vector of a monomial. (Contributed by Thierry Arnoux, 20-Feb-2025.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝑋 = (var1‘𝑅)    &   ⊢ ↑ = (.g‘(mulGrp‘𝑃))    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    ⇒   ⊢ (𝜑 → (coe1‘(𝑁 ↑ 𝑋)) = (𝑘 ∈ ℕ0 ↦ if(𝑘 = 𝑁, 1 , 0 )))
Theorem	ply1moneq 34216	Two monomials are equal iff their powers are equal. (Contributed by Thierry Arnoux, 20-Feb-2025.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝑋 = (var1‘𝑅)    &   ⊢ ↑ = (.g‘(mulGrp‘𝑃))    &   ⊢ (𝜑 → 𝑅 ∈ NzRing)    &   ⊢ (𝜑 → 𝑀 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    ⇒   ⊢ (𝜑 → ((𝑀 ↑ 𝑋) = (𝑁 ↑ 𝑋) ↔ 𝑀 = 𝑁))
Theorem	ply1coedeg 34217*	Decompose a univariate polynomial 𝐾 as a sum of powers, up to its degree 𝐷. (Contributed by Thierry Arnoux, 15-Feb-2026.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝑋 = (var1‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ · = ( ·𝑠 ‘𝑃)    &   ⊢ 𝑀 = (mulGrp‘𝑃)    &   ⊢ ↑ = (.g‘𝑀)    &   ⊢ 𝐴 = (coe1‘𝐾)    &   ⊢ 𝐷 = ((deg1‘𝑅)‘𝐾)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝐾 ∈ 𝐵)    ⇒   ⊢ (𝜑 → 𝐾 = (𝑃 Σg (𝑘 ∈ (0...𝐷) ↦ ((𝐴‘𝑘) · (𝑘 ↑ 𝑋)))))
Theorem	coe1zfv 34218	The coefficients of the zero univariate polynomial. (Contributed by Thierry Arnoux, 22-Jun-2025.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝑍 = (0g‘𝑃)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    ⇒   ⊢ (𝜑 → ((coe1‘𝑍)‘𝑁) = 0 )
Theorem	coe1vr1 34219*	Polynomial coefficient of the variable. (Contributed by Thierry Arnoux, 22-Jun-2025.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝑋 = (var1‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    ⇒   ⊢ (𝜑 → (coe1‘𝑋) = (𝑘 ∈ ℕ0 ↦ if(𝑘 = 1, 1 , 0 )))
Theorem	deg1vr 34220	The degree of the variable polynomial is 1. (Contributed by Thierry Arnoux, 22-Jun-2025.)
⊢ 𝐷 = (deg1‘𝑅)    &   ⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝑋 = (var1‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ NzRing)    ⇒   ⊢ (𝜑 → (𝐷‘𝑋) = 1)
Theorem	vr1nz 34221	A univariate polynomial variable cannot be the zero polynomial. (Contributed by Thierry Arnoux, 14-Nov-2025.)
⊢ 𝑋 = (var1‘𝑈)    &   ⊢ 𝑍 = (0g‘𝑃)    &   ⊢ 𝑈 = (𝑆 ↾s 𝑅)    &   ⊢ 𝑃 = (Poly1‘𝑈)    &   ⊢ (𝜑 → 𝑆 ∈ CRing)    &   ⊢ (𝜑 → 𝑆 ∈ NzRing)    &   ⊢ (𝜑 → 𝑅 ∈ (SubRing‘𝑆))    ⇒   ⊢ (𝜑 → 𝑋 ≠ 𝑍)
Theorem	ply1degltel 34222	Characterize elementhood in the set 𝑆 of polynomials of degree less than 𝑁. (Contributed by Thierry Arnoux, 20-Feb-2025.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐷 = (deg1‘𝑅)    &   ⊢ 𝑆 = (◡𝐷 “ (-∞[,)𝑁))    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ 𝐵 = (Base‘𝑃)    ⇒   ⊢ (𝜑 → (𝐹 ∈ 𝑆 ↔ (𝐹 ∈ 𝐵 ∧ (𝐷‘𝐹) ≤ (𝑁 − 1))))
Theorem	ply1degleel 34223	Characterize elementhood in the set 𝑆 of polynomials of degree less than 𝑁. (Contributed by Thierry Arnoux, 2-Apr-2025.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐷 = (deg1‘𝑅)    &   ⊢ 𝑆 = (◡𝐷 “ (-∞[,)𝑁))    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ 𝐵 = (Base‘𝑃)    ⇒   ⊢ (𝜑 → (𝐹 ∈ 𝑆 ↔ (𝐹 ∈ 𝐵 ∧ (𝐷‘𝐹) < 𝑁)))
Theorem	ply1degltlss 34224	The space 𝑆 of the univariate polynomials of degree less than 𝑁 forms a vector subspace. (Contributed by Thierry Arnoux, 20-Feb-2025.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐷 = (deg1‘𝑅)    &   ⊢ 𝑆 = (◡𝐷 “ (-∞[,)𝑁))    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    ⇒   ⊢ (𝜑 → 𝑆 ∈ (LSubSp‘𝑃))
Theorem	gsummoncoe1fzo 34225*	A coefficient of the polynomial represented as a sum of scaled monomials is the coefficient of the corresponding scaled monomial. (Contributed by Thierry Arnoux, 20-Feb-2025.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 𝑋 = (var1‘𝑅)    &   ⊢ ↑ = (.g‘(mulGrp‘𝑃))    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ 𝐾 = (Base‘𝑅)    &   ⊢ ∗ = ( ·𝑠 ‘𝑃)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ (𝜑 → ∀𝑘 ∈ (0..^𝑁)𝐴 ∈ 𝐾)    &   ⊢ (𝜑 → 𝐿 ∈ (0..^𝑁))    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝑘 = 𝐿 → 𝐴 = 𝐶)    ⇒   ⊢ (𝜑 → ((coe1‘(𝑃 Σg (𝑘 ∈ (0..^𝑁) ↦ (𝐴 ∗ (𝑘 ↑ 𝑋)))))‘𝐿) = 𝐶)
Theorem	gsummoncoe1fz 34226*	A coefficient of the polynomial represented as a sum of scaled monomials is the coefficient of the corresponding scaled monomial. See gsummoncoe1fzo 34225. (Contributed by Thierry Arnoux, 15-Feb-2026.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 𝑋 = (var1‘𝑅)    &   ⊢ ↑ = (.g‘(mulGrp‘𝑃))    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ 𝐾 = (Base‘𝑅)    &   ⊢ ∗ = ( ·𝑠 ‘𝑃)    &   ⊢ (𝜑 → 𝐷 ∈ ℕ0)    &   ⊢ (𝜑 → ∀𝑘 ∈ (0...𝐷)𝐴 ∈ 𝐾)    &   ⊢ (𝜑 → 𝐿 ∈ (0...𝐷))    &   ⊢ (𝑘 = 𝐿 → 𝐴 = 𝐶)    ⇒   ⊢ (𝜑 → ((coe1‘(𝑃 Σg (𝑘 ∈ (0...𝐷) ↦ (𝐴 ∗ (𝑘 ↑ 𝑋)))))‘𝐿) = 𝐶)
Theorem	ply1gsumz 34227*	If a polynomial given as a sum of scaled monomials by factors 𝐴 is the zero polynomial, then all factors 𝐴 are zero. (Contributed by Thierry Arnoux, 20-Feb-2025.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ 𝐹 = (𝑛 ∈ (0..^𝑁) ↦ (𝑛(.g‘(mulGrp‘𝑃))(var1‘𝑅)))    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝑍 = (0g‘𝑃)    &   ⊢ (𝜑 → 𝐴:(0..^𝑁)⟶𝐵)    &   ⊢ (𝜑 → (𝑃 Σg (𝐴 ∘f ( ·𝑠 ‘𝑃)𝐹)) = 𝑍)    ⇒   ⊢ (𝜑 → 𝐴 = ((0..^𝑁) × { 0 }))
Theorem	deg1addlt 34228	If both factors have degree bounded by 𝐿, then the sum of the polynomials also has degree bounded by 𝐿. See also deg1addle 26463. (Contributed by Thierry Arnoux, 2-Apr-2025.)
⊢ 𝑌 = (Poly1‘𝑅)    &   ⊢ 𝐷 = (deg1‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ 𝐵 = (Base‘𝑌)    &   ⊢ + = (+g‘𝑌)    &   ⊢ (𝜑 → 𝐹 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐿 ∈ ℝ*)    &   ⊢ (𝜑 → (𝐷‘𝐹) < 𝐿)    &   ⊢ (𝜑 → (𝐷‘𝐺) < 𝐿)    ⇒   ⊢ (𝜑 → (𝐷‘(𝐹 + 𝐺)) < 𝐿)
Theorem	ig1pnunit 34229	The polynomial ideal generator is not a unit polynomial. (Contributed by Thierry Arnoux, 19-Mar-2025.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐺 = (idlGen1p‘𝑅)    &   ⊢ 𝑈 = (Base‘𝑃)    &   ⊢ (𝜑 → 𝑅 ∈ DivRing)    &   ⊢ (𝜑 → 𝐼 ∈ (LIdeal‘𝑃))    &   ⊢ (𝜑 → 𝐼 ≠ 𝑈)    ⇒   ⊢ (𝜑 → ¬ (𝐺‘𝐼) ∈ (Unit‘𝑃))
Theorem	ig1pmindeg 34230	The polynomial ideal generator is of minimum degree. (Contributed by Thierry Arnoux, 19-Mar-2025.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐺 = (idlGen1p‘𝑅)    &   ⊢ 𝑈 = (Base‘𝑃)    &   ⊢ (𝜑 → 𝑅 ∈ DivRing)    &   ⊢ (𝜑 → 𝐼 ∈ (LIdeal‘𝑃))    &   ⊢ 𝐷 = (deg1‘𝑅)    &   ⊢ 0 = (0g‘𝑃)    &   ⊢ (𝜑 → 𝐹 ∈ 𝐼)    &   ⊢ (𝜑 → 𝐹 ≠ 0 )    ⇒   ⊢ (𝜑 → (𝐷‘(𝐺‘𝐼)) ≤ (𝐷‘𝐹))
Theorem	deg1le1 34231	Dichotomy for a univariate polynomial of degree at most one. (Contributed by Thierry Arnoux, 8-Nov-2026.)
⊢ 𝐷 = (deg1‘𝑅)    &   ⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ (𝜑 → 𝐹 ∈ 𝐵)    &   ⊢ (𝜑 → (𝐷‘𝐹) ≤ 1)    ⇒   ⊢ (𝜑 → ((𝐷‘𝐹) ≤ 0 ∨ (𝐷‘𝐹) = 1))
Theorem	evls1degle1 34232	Evaluation of a univariate polynomial of degree at most 1. (Contributed by Thierry Arnoux, 8-Nov-2026.)
⊢ 𝑃 = (Poly1‘(𝑅 ↾s 𝑆))    &   ⊢ 𝑄 = (𝑅 evalSub1 𝑆)    &   ⊢ 𝑉 = (Base‘𝑅)    &   ⊢ 𝑈 = (Base‘𝑃)    &   ⊢ · = (.r‘𝑅)    &   ⊢ + = (+g‘𝑅)    &   ⊢ 𝐶 = (coe1‘𝐹)    &   ⊢ 𝐷 = (deg1‘𝑅)    &   ⊢ 𝐴 = (𝐶‘1)    &   ⊢ 𝐵 = (𝐶‘0)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝑆 ∈ (SubRing‘𝑅))    &   ⊢ (𝜑 → 𝐹 ∈ 𝑈)    &   ⊢ (𝜑 → (𝐷‘𝐹) ≤ 1)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    ⇒   ⊢ (𝜑 → ((𝑄‘𝐹)‘𝑋) = ((𝐴 · 𝑋) + 𝐵))
21.4.10.48  Polynomial quotient and polynomial remainder
Theorem	q1pdir 34233	Distribution of univariate polynomial quotient over addition. (Contributed by Thierry Arnoux, 2-Apr-2025.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝑈 = (Base‘𝑃)    &   ⊢ 𝑁 = (Unic1p‘𝑅)    &   ⊢ / = (quot1p‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑁)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑈)    &   ⊢ + = (+g‘𝑃)    ⇒   ⊢ (𝜑 → ((𝐴 + 𝐵) / 𝐶) = ((𝐴 / 𝐶) + (𝐵 / 𝐶)))
Theorem	q1pvsca 34234	Scalar multiplication property of the polynomial division. (Contributed by Thierry Arnoux, 2-Apr-2025.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝑈 = (Base‘𝑃)    &   ⊢ 𝑁 = (Unic1p‘𝑅)    &   ⊢ / = (quot1p‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑁)    &   ⊢ × = ( ·𝑠 ‘𝑃)    &   ⊢ 𝐾 = (Base‘𝑅)    &   ⊢ (𝜑 → 𝐵 ∈ 𝐾)    ⇒   ⊢ (𝜑 → ((𝐵 × 𝐴) / 𝐶) = (𝐵 × (𝐴 / 𝐶)))
Theorem	r1pvsca 34235	Scalar multiplication property of the polynomial remainder operation. (Contributed by Thierry Arnoux, 2-Apr-2025.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝑈 = (Base‘𝑃)    &   ⊢ 𝑁 = (Unic1p‘𝑅)    &   ⊢ 𝐸 = (rem1p‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑁)    &   ⊢ × = ( ·𝑠 ‘𝑃)    &   ⊢ 𝐾 = (Base‘𝑅)    &   ⊢ (𝜑 → 𝐵 ∈ 𝐾)    ⇒   ⊢ (𝜑 → ((𝐵 × 𝐴)𝐸𝐷) = (𝐵 × (𝐴𝐸𝐷)))
Theorem	r1p0 34236	Polynomial remainder operation of a division of the zero polynomial. (Contributed by Thierry Arnoux, 2-Apr-2025.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝑈 = (Base‘𝑃)    &   ⊢ 𝑁 = (Unic1p‘𝑅)    &   ⊢ 𝐸 = (rem1p‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑁)    &   ⊢ 0 = (0g‘𝑃)    ⇒   ⊢ (𝜑 → ( 0 𝐸𝐷) = 0 )
Theorem	r1pcyc 34237	The polynomial remainder operation is periodic. See modcyc 14084. (Contributed by Thierry Arnoux, 2-Apr-2025.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝑈 = (Base‘𝑃)    &   ⊢ 𝑁 = (Unic1p‘𝑅)    &   ⊢ 𝐸 = (rem1p‘𝑅)    &   ⊢ + = (+g‘𝑃)    &   ⊢ · = (.r‘𝑃)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑁)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑈)    ⇒   ⊢ (𝜑 → ((𝐴 + (𝐶 · 𝐵))𝐸𝐵) = (𝐴𝐸𝐵))
Theorem	r1padd1 34238	Addition property of the polynomial remainder operation, similar to modadd1 14086. (Contributed by Thierry Arnoux, 2-Apr-2025.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝑈 = (Base‘𝑃)    &   ⊢ 𝑁 = (Unic1p‘𝑅)    &   ⊢ 𝐸 = (rem1p‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑁)    &   ⊢ (𝜑 → (𝐴𝐸𝐷) = (𝐵𝐸𝐷))    &   ⊢ + = (+g‘𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑈)    ⇒   ⊢ (𝜑 → ((𝐴 + 𝐶)𝐸𝐷) = ((𝐵 + 𝐶)𝐸𝐷))
Theorem	r1plmhm 34239*	The univariate polynomial remainder function 𝐹 is a module homomorphism. Its image (𝐹 “s 𝑃) is sometimes called the "ring of remainders". (Contributed by Thierry Arnoux, 2-Apr-2025.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝑈 = (Base‘𝑃)    &   ⊢ 𝐸 = (rem1p‘𝑅)    &   ⊢ 𝑁 = (Unic1p‘𝑅)    &   ⊢ 𝐹 = (𝑓 ∈ 𝑈 ↦ (𝑓𝐸𝑀))    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝑀 ∈ 𝑁)    ⇒   ⊢ (𝜑 → 𝐹 ∈ (𝑃 LMHom (𝐹 “s 𝑃)))
Theorem	r1pquslmic 34240*	The univariate polynomial remainder ring (𝐹 “s 𝑃) is module isomorphic with the quotient ring. (Contributed by Thierry Arnoux, 2-Apr-2025.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝑈 = (Base‘𝑃)    &   ⊢ 𝐸 = (rem1p‘𝑅)    &   ⊢ 𝑁 = (Unic1p‘𝑅)    &   ⊢ 𝐹 = (𝑓 ∈ 𝑈 ↦ (𝑓𝐸𝑀))    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝑀 ∈ 𝑁)    &   ⊢ 0 = (0g‘𝑃)    &   ⊢ 𝐾 = (◡𝐹 “ { 0 })    &   ⊢ 𝑄 = (𝑃 /s (𝑃 ~QG 𝐾))    ⇒   ⊢ (𝜑 → 𝑄 ≃𝑚 (𝐹 “s 𝑃))
Theorem	evls1rgspncl 34241	Closure of the subring polynomial evaluation in a generated ring. Generic version of cnsrplycl 26681. See also evls1fldgencl 34406. (Contributed by Thierry Arnoux, 8-Nov-2026.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝑃 = (Poly1‘(𝑅 ↾s 𝑆))    &   ⊢ 𝑈 = (Base‘𝑃)    &   ⊢ 𝑄 = (𝑅 evalSub1 𝑆)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝑆 ∈ (SubRing‘𝑅))    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ 𝑁 = (RingSpan‘𝑅)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑈)    ⇒   ⊢ (𝜑 → ((𝑄‘𝐹)‘𝑋) ∈ (𝑁‘(𝑆 ∪ {𝑋})))
Theorem	rngunsnply1 34242*	Adjoining one element to a ring results in a set of polynomial evaluations. Generalization of rngunsnply 26682. (Contributed by Thierry Arnoux, 8-Nov-2026.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝑃 = (Poly1‘(𝑅 ↾s 𝑆))    &   ⊢ 𝑈 = (Base‘𝑃)    &   ⊢ 𝑄 = (𝑅 evalSub1 𝑆)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝑆 ∈ (SubRing‘𝑅))    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ 𝑁 = (RingSpan‘𝑅)    ⇒   ⊢ (𝜑 → (𝑉 ∈ (𝑁‘(𝑆 ∪ {𝑋})) ↔ ∃𝑝 ∈ 𝑈 𝑉 = ((𝑄‘𝑝)‘𝑋)))
Theorem	rngunsnply1chr2lem1 34243	Lemma for rngunsnply1chr2 . (Contributed by Thierry Arnoux, 8-Nov-2026.)
⊢ 𝑉 = (Base‘𝑅)    &   ⊢ 𝑃 = (Poly1‘(𝑅 ↾s 𝑆))    &   ⊢ 𝑈 = (Base‘𝑃)    &   ⊢ 𝑄 = (𝑅 evalSub1 𝑆)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝑅 ∈ NzRing)    &   ⊢ (𝜑 → 𝑆 ∈ (SubRing‘𝑅))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ (𝑁‘(𝑆 ∪ {𝑋})))    &   ⊢ 𝑁 = (RingSpan‘𝑅)    &   ⊢ + = (+g‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ ↑ = (.g‘(mulGrp‘𝑅))    &   ⊢ (𝜑 → 𝐴 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑆)    &   ⊢ (𝜑 → (2 ↑ 𝑋) = ((𝐴 · 𝑋) + 𝐵))    &   ⊢ 𝐷 = (deg1‘𝑅)    &   ⊢ 𝐸 = (rem1p‘(𝑅 ↾s 𝑆))    &   ⊢ 𝐺 = ((2(.g‘(mulGrp‘𝑃))(var1‘𝑅))(-g‘𝑃)((𝐴( ·𝑠 ‘𝑃)(var1‘𝑅))(+g‘𝑃)((algSc‘𝑃)‘𝐵)))    &   ⊢ 𝐻 = (𝐹𝐸𝐺)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑈)    ⇒   ⊢ (𝜑 → (𝐷‘𝐺) = 2)
Theorem	rngunsnply1chr2lem2 34244	Lemma for rngunsnply1chr2 . (Contributed by Thierry Arnoux, 8-Nov-2026.)
⊢ 𝑉 = (Base‘𝑅)    &   ⊢ 𝑃 = (Poly1‘(𝑅 ↾s 𝑆))    &   ⊢ 𝑈 = (Base‘𝑃)    &   ⊢ 𝑄 = (𝑅 evalSub1 𝑆)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝑅 ∈ NzRing)    &   ⊢ (𝜑 → 𝑆 ∈ (SubRing‘𝑅))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ (𝑁‘(𝑆 ∪ {𝑋})))    &   ⊢ 𝑁 = (RingSpan‘𝑅)    &   ⊢ + = (+g‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ ↑ = (.g‘(mulGrp‘𝑅))    &   ⊢ (𝜑 → 𝐴 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑆)    &   ⊢ (𝜑 → (2 ↑ 𝑋) = ((𝐴 · 𝑋) + 𝐵))    &   ⊢ 𝐷 = (deg1‘𝑅)    &   ⊢ 𝐸 = (rem1p‘(𝑅 ↾s 𝑆))    &   ⊢ 𝐺 = ((2(.g‘(mulGrp‘𝑃))(var1‘𝑅))(-g‘𝑃)((𝐴( ·𝑠 ‘𝑃)(var1‘𝑅))(+g‘𝑃)((algSc‘𝑃)‘𝐵)))    &   ⊢ 𝐻 = (𝐹𝐸𝐺)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑈)    ⇒   ⊢ (𝜑 → 𝐺 ∈ (Unic1p‘(𝑅 ↾s 𝑆)))
Theorem	rngunsnply1chr2lem3 34245	Lemma for rngunsnply1chr2 . (Contributed by Thierry Arnoux, 8-Nov-2026.)
⊢ 𝑉 = (Base‘𝑅)    &   ⊢ 𝑃 = (Poly1‘(𝑅 ↾s 𝑆))    &   ⊢ 𝑈 = (Base‘𝑃)    &   ⊢ 𝑄 = (𝑅 evalSub1 𝑆)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝑅 ∈ NzRing)    &   ⊢ (𝜑 → 𝑆 ∈ (SubRing‘𝑅))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ (𝑁‘(𝑆 ∪ {𝑋})))    &   ⊢ 𝑁 = (RingSpan‘𝑅)    &   ⊢ + = (+g‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ ↑ = (.g‘(mulGrp‘𝑅))    &   ⊢ (𝜑 → 𝐴 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑆)    &   ⊢ (𝜑 → (2 ↑ 𝑋) = ((𝐴 · 𝑋) + 𝐵))    &   ⊢ 𝐷 = (deg1‘𝑅)    &   ⊢ 𝐸 = (rem1p‘(𝑅 ↾s 𝑆))    &   ⊢ 𝐺 = ((2(.g‘(mulGrp‘𝑃))(var1‘𝑅))(-g‘𝑃)((𝐴( ·𝑠 ‘𝑃)(var1‘𝑅))(+g‘𝑃)((algSc‘𝑃)‘𝐵)))    &   ⊢ 𝐻 = (𝐹𝐸𝐺)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑈)    ⇒   ⊢ (𝜑 → ((𝐷‘𝐻) ≤ 1 ∧ ((𝑄‘𝐻)‘𝑋) = ((𝑄‘𝐹)‘𝑋)))
Theorem	rngunsnply1chr2 34246*	When adjoining an element 𝑋 with characteristic polynomial of degree 2 to a subring 𝑆, the elements 𝑌 of the generated subring can be written as a linear form. (Contributed by Thierry Arnoux, 8-Nov-2026.)
⊢ 𝑉 = (Base‘𝑅)    &   ⊢ 𝑃 = (Poly1‘(𝑅 ↾s 𝑆))    &   ⊢ 𝑈 = (Base‘𝑃)    &   ⊢ 𝑄 = (𝑅 evalSub1 𝑆)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝑅 ∈ NzRing)    &   ⊢ (𝜑 → 𝑆 ∈ (SubRing‘𝑅))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ (𝑁‘(𝑆 ∪ {𝑋})))    &   ⊢ 𝑁 = (RingSpan‘𝑅)    &   ⊢ + = (+g‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ ↑ = (.g‘(mulGrp‘𝑅))    &   ⊢ (𝜑 → 𝐴 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑆)    &   ⊢ (𝜑 → (2 ↑ 𝑋) = ((𝐴 · 𝑋) + 𝐵))    ⇒   ⊢ (𝜑 → ∃𝑎 ∈ 𝑆 ∃𝑏 ∈ 𝑆 𝑌 = ((𝑎 · 𝑋) + 𝑏))
21.4.10.49  Multivariate Polynomials
Theorem	psrbasfsupp 34247	Rewrite a finite support for nonnegative integers : For functions mapping a set 𝐼 to the nonnegative integers, having finite support can also be written as having a finite preimage of the positive integers. The latter expression is used for example in psrbas 22286, but with the former expression, theorems about finite support can be used more directly. (Contributed by Thierry Arnoux, 10-Jan-2026.)
⊢ 𝐷 = {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ 𝑓 finSupp 0}    ⇒   ⊢ 𝐷 = {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}
Theorem	psrnzr 34248	The ring of power series over a nonzero ring form a nonzero ring. (Contributed by Thierry Arnoux, 4-May-2026.)
⊢ 𝑆 = (𝐼 mPwSer 𝑅)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ NzRing)    ⇒   ⊢ (𝜑 → 𝑆 ∈ NzRing)
Theorem	mplnzr 34249	The multivariate polynomials over a nonzero ring form a nonzero ring. (Contributed by Thierry Arnoux, 4-May-2026.)
⊢ 𝑃 = (𝐼 mPoly 𝑅)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ NzRing)    ⇒   ⊢ (𝜑 → 𝑃 ∈ NzRing)
Theorem	0mplrim 34250*	Build a ring isomorphism between multivariate polynomials with no variables and the underlying ring. (Contributed by Thierry Arnoux, 4-May-2026.)
⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 𝑃 = (∅ mPoly 𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ 𝐹 = (𝑝 ∈ 𝐵 ↦ (𝑝‘∅))    ⇒   ⊢ (𝜑 → 𝐹 ∈ (𝑃 RingIso 𝑅))
Theorem	0mplric 34251	Multivariate polynomials with no variables are isomorphic with the underlying ring. (Contributed by Thierry Arnoux, 4-May-2026.)
⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 𝑃 = (∅ mPoly 𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    ⇒   ⊢ (𝜑 → 𝑃 ≃𝑟 𝑅)
Theorem	mplasclco 34252*	Case where composing an algebra scalar lifting functions with a scalar leads to a scalar. This is useful when working with selectVars. (Contributed by Thierry Arnoux, 4-May-2026.)
⊢ 𝑆 = (Base‘𝑅)    &   ⊢ 𝑂 = (𝐽 mPoly 𝑅)    &   ⊢ 𝑃 = (𝐼 mPoly 𝑅)    &   ⊢ 𝑄 = (𝐼 mPoly 𝑂)    &   ⊢ 𝐴 = (algSc‘𝑂)    &   ⊢ 𝐵 = (algSc‘𝑃)    &   ⊢ 𝐶 = (algSc‘𝑄)    &   ⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin}    &   ⊢ 𝐸 = {𝑗 ∈ (ℕ0 ↑m 𝐽) ∣ (◡𝑗 “ ℕ) ∈ Fin}    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐽 ⊆ 𝐼)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑆)    ⇒   ⊢ (𝜑 → (𝐴 ∘ (𝐵‘𝑋)) = (𝐶‘(𝐴‘𝑋)))
Theorem	selvascl 34253	The "variable selection" function evaluated at a scalar. (Contributed by Thierry Arnoux, 4-May-2026.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝑃 = (𝐼 mPoly 𝑅)    &   ⊢ 𝐴 = (algSc‘𝑃)    &   ⊢ 𝐶 = (algSc‘𝑇)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ 𝑈 = ((𝐼 ∖ 𝐽) mPoly 𝑅)    &   ⊢ 𝑇 = (𝐽 mPoly 𝑈)    &   ⊢ 𝐷 = (𝐶 ∘ (algSc‘𝑈))    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝐽 ⊆ 𝐼)    ⇒   ⊢ (𝜑 → (((𝐼 selectVars 𝑅)‘𝐽)‘(𝐴‘𝑋)) = (𝐷‘𝑋))
Theorem	selvply1rhmlema 34254*	Lemma for selvply1rhm 34261. (Contributed by Thierry Arnoux, 4-May-2026.)
⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 𝑃 = ({𝑋} mPoly 𝑅)    &   ⊢ · = (.r‘𝑃)    &   ⊢ × = (.r‘𝑄)    &   ⊢ 𝑄 = (Poly1‘𝑅)    &   ⊢ 𝑀 = (𝑓 ∈ 𝐵 ↦ (𝑛 ∈ (ℕ0 ↑m 1o) ↦ (𝑓‘{⟨𝑋, (𝑛‘∅)⟩})))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝐹 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝑀‘𝐹) ∈ (Base‘𝑄))
Theorem	selvply1rhmlemb 34255*	Lemma for selvply1rhm 34261. (Contributed by Thierry Arnoux, 4-May-2026.)
⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 𝑃 = ({𝑋} mPoly 𝑅)    &   ⊢ · = (.r‘𝑃)    &   ⊢ × = (.r‘𝑄)    &   ⊢ 𝑄 = (Poly1‘𝑅)    &   ⊢ 𝑀 = (𝑓 ∈ 𝐵 ↦ (𝑛 ∈ (ℕ0 ↑m 1o) ↦ (𝑓‘{⟨𝑋, (𝑛‘∅)⟩})))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝐹 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝑀‘(𝐹 · 𝐺)) = ((𝑀‘𝐹) × (𝑀‘𝐺)))
Theorem	selvply1rhmlem1 34256*	Lemma for selvply1rhm 34261. (Contributed by Thierry Arnoux, 4-May-2026.)
⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 𝑃 = (𝐼 mPoly 𝑅)    &   ⊢ 𝑈 = ((𝐼 ∖ {𝑋}) mPoly 𝑅)    &   ⊢ 𝑄 = (Poly1‘𝑈)    &   ⊢ 𝐻 = (𝑓 ∈ 𝐵 ↦ (𝑛 ∈ (ℕ0 ↑m 1o) ↦ ((((𝐼 selectVars 𝑅)‘{𝑋})‘𝑓)‘{⟨𝑋, (𝑛‘∅)⟩})))    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐼)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    ⇒   ⊢ (𝜑 → 𝐻:𝐵⟶(Base‘𝑄))
Theorem	selvply1rhmlem2 34257*	Lemma for selvply1rhm 34261: Image of the ring unit by the mapping 𝐻 (Contributed by Thierry Arnoux, 4-May-2026.)
⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 𝑃 = (𝐼 mPoly 𝑅)    &   ⊢ 𝑈 = ((𝐼 ∖ {𝑋}) mPoly 𝑅)    &   ⊢ 𝑄 = (Poly1‘𝑈)    &   ⊢ 𝐻 = (𝑓 ∈ 𝐵 ↦ (𝑛 ∈ (ℕ0 ↑m 1o) ↦ ((((𝐼 selectVars 𝑅)‘{𝑋})‘𝑓)‘{⟨𝑋, (𝑛‘∅)⟩})))    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐼)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    ⇒   ⊢ (𝜑 → (𝐻‘(1r‘𝑃)) = (1r‘𝑄))
Theorem	selvply1rhmlem3 34258*	Lemma for selvply1rhm 34261. (Contributed by Thierry Arnoux, 4-May-2026.)
⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 𝑃 = (𝐼 mPoly 𝑅)    &   ⊢ 𝑈 = ((𝐼 ∖ {𝑋}) mPoly 𝑅)    &   ⊢ 𝑄 = (Poly1‘𝑈)    &   ⊢ 𝐻 = (𝑓 ∈ 𝐵 ↦ (𝑛 ∈ (ℕ0 ↑m 1o) ↦ ((((𝐼 selectVars 𝑅)‘{𝑋})‘𝑓)‘{⟨𝑋, (𝑛‘∅)⟩})))    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐼)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝐹 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑁 ∈ (ℕ0 ↑m 1o))    ⇒   ⊢ (𝜑 → ((𝐻‘𝐹)‘𝑁) = ((((𝐼 selectVars 𝑅)‘{𝑋})‘𝐹)‘{⟨𝑋, (𝑁‘∅)⟩}))
Theorem	selvply1rhmlem4 34259*	Lemma for selvply1rhm 34261: The mapping 𝐻 is linear. (Contributed by Thierry Arnoux, 4-May-2026.)
⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 𝑃 = (𝐼 mPoly 𝑅)    &   ⊢ 𝑈 = ((𝐼 ∖ {𝑋}) mPoly 𝑅)    &   ⊢ 𝑄 = (Poly1‘𝑈)    &   ⊢ 𝐻 = (𝑓 ∈ 𝐵 ↦ (𝑛 ∈ (ℕ0 ↑m 1o) ↦ ((((𝐼 selectVars 𝑅)‘{𝑋})‘𝑓)‘{⟨𝑋, (𝑛‘∅)⟩})))    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐼)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝐹 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝐻‘(𝐹(+g‘𝑃)𝐺)) = ((𝐻‘𝐹)(+g‘𝑄)(𝐻‘𝐺)))
Theorem	selvply1rhmlem5 34260*	Lemma for selvply1rhm 34261. (Contributed by Thierry Arnoux, 4-May-2026.)
⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 𝑃 = (𝐼 mPoly 𝑅)    &   ⊢ 𝑈 = ((𝐼 ∖ {𝑋}) mPoly 𝑅)    &   ⊢ 𝑄 = (Poly1‘𝑈)    &   ⊢ 𝐻 = (𝑓 ∈ 𝐵 ↦ (𝑛 ∈ (ℕ0 ↑m 1o) ↦ ((((𝐼 selectVars 𝑅)‘{𝑋})‘𝑓)‘{⟨𝑋, (𝑛‘∅)⟩})))    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐼)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝐹 ∈ 𝐵)    &   ⊢ 𝑀 = (𝑞 ∈ (Base‘({𝑋} mPoly 𝑈)) ↦ (𝑠 ∈ (ℕ0 ↑m 1o) ↦ (𝑞‘{⟨𝑋, (𝑠‘∅)⟩})))    ⇒   ⊢ (𝜑 → (𝐻‘𝐹) = (𝑀‘(((𝐼 selectVars 𝑅)‘{𝑋})‘𝐹)))
Theorem	selvply1rhm 34261*	Build a ring homomorphism 𝐻 between the multivariate polynomials 𝑃 with variables in 𝐼 and the univariate polynomials 𝑄 in a single variable 𝑋 element of 𝐼. (Contributed by Thierry Arnoux, 4-May-2026.)
⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 𝑃 = (𝐼 mPoly 𝑅)    &   ⊢ 𝑈 = ((𝐼 ∖ {𝑋}) mPoly 𝑅)    &   ⊢ 𝑄 = (Poly1‘𝑈)    &   ⊢ 𝐻 = (𝑓 ∈ 𝐵 ↦ (𝑛 ∈ (ℕ0 ↑m 1o) ↦ ((((𝐼 selectVars 𝑅)‘{𝑋})‘𝑓)‘{⟨𝑋, (𝑛‘∅)⟩})))    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐼)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    ⇒   ⊢ (𝜑 → 𝐻 ∈ (𝑃 RingHom 𝑄))
Theorem	selvply1rhm0 34262*	The ring homomorphism 𝐻 built in selvply1rhm 34261 is injective. (Contributed by Thierry Arnoux, 4-May-2026.)
⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 𝑃 = (𝐼 mPoly 𝑅)    &   ⊢ 𝑈 = ((𝐼 ∖ {𝑋}) mPoly 𝑅)    &   ⊢ 𝑄 = (Poly1‘𝑈)    &   ⊢ 𝐻 = (𝑓 ∈ 𝐵 ↦ (𝑛 ∈ (ℕ0 ↑m 1o) ↦ ((((𝐼 selectVars 𝑅)‘{𝑋})‘𝑓)‘{⟨𝑋, (𝑛‘∅)⟩})))    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐼)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ 0 = (0g‘𝑄)    &   ⊢ 𝑍 = (0g‘𝑃)    &   ⊢ (𝜑 → 𝐹 ∈ 𝐵)    &   ⊢ (𝜑 → (𝐻‘𝐹) = 0 )    ⇒   ⊢ (𝜑 → 𝐹 = 𝑍)
Theorem	mplidomlem 34263*	Lemma for mplidom 34264. (Contributed by Thierry Arnoux, 4-May-2026.)
⊢ 𝑃 = (𝐼 mPoly 𝑅)    &   ⊢ (𝜑 → 𝐼 ∈ Fin)    &   ⊢ (𝜑 → 𝑅 ∈ IDomn)    &   ⊢ 𝐻 = (𝑓 ∈ 𝐶 ↦ (𝑛 ∈ (ℕ0 ↑m 1o) ↦ (((((𝑗 ∪ {𝑥}) selectVars 𝑅)‘{𝑥})‘𝑓)‘{⟨𝑥, (𝑛‘∅)⟩})))    &   ⊢ 𝐶 = (Base‘𝑆)    &   ⊢ 𝑆 = ((𝑗 ∪ {𝑥}) mPoly 𝑅)    &   ⊢ 𝑈 = (((𝑗 ∪ {𝑥}) ∖ {𝑥}) mPoly 𝑅)    &   ⊢ 𝑄 = (Poly1‘𝑈)    ⇒   ⊢ (𝜑 → 𝑃 ∈ IDomn)
Theorem	mplidom 34264	The multivariate polynomials over an integral domain form an integral domain. See ply1idom 26487. (Contributed by Thierry Arnoux, 4-May-2026.)
⊢ 𝑃 = (𝐼 mPoly 𝑅)    &   ⊢ (𝜑 → 𝐼 ∈ Fin)    &   ⊢ (𝜑 → 𝑅 ∈ IDomn)    ⇒   ⊢ (𝜑 → 𝑃 ∈ IDomn)
Syntax	cextv 34265	Extend class notation with the "variable extension" function.
class extendVars
Definition	df-extv 34266*	Define the "variable extension" function. The function ((𝐼extendVars𝑅)‘𝐴) converts polynomials with variables indexed by (𝐼 ∖ {𝐴}) into polynomials indexed by 𝐼, and therefore maps elements of ((𝐼 ∖ {𝐴}) mPoly 𝑅) onto (𝐼 mPoly 𝑅). (Contributed by Thierry Arnoux, 20-Jan-2026.)
⊢ extendVars = (𝑖 ∈ V, 𝑟 ∈ V ↦ (𝑎 ∈ 𝑖 ↦ (𝑓 ∈ (Base‘((𝑖 ∖ {𝑎}) mPoly 𝑟)) ↦ (𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝑖) ∣ ℎ finSupp 0} ↦ if((𝑥‘𝑎) = 0, (𝑓‘(𝑥 ↾ (𝑖 ∖ {𝑎}))), (0g‘𝑟))))))
Theorem	extvval 34267*	Value of the "variable extension" function. (Contributed by Thierry Arnoux, 25-Jan-2026.)
⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑊)    &   ⊢ 𝐽 = (𝐼 ∖ {𝑎})    &   ⊢ 𝑀 = (Base‘(𝐽 mPoly 𝑅))    ⇒   ⊢ (𝜑 → (𝐼extendVars𝑅) = (𝑎 ∈ 𝐼 ↦ (𝑓 ∈ 𝑀 ↦ (𝑥 ∈ 𝐷 ↦ if((𝑥‘𝑎) = 0, (𝑓‘(𝑥 ↾ (𝐼 ∖ {𝑎}))), 0 )))))
Theorem	extvfval 34268*	The "variable extension" function evaluated for adding a variable with index 𝐴. (Contributed by Thierry Arnoux, 25-Jan-2026.)
⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐴 ∈ 𝐼)    &   ⊢ 𝐽 = (𝐼 ∖ {𝐴})    &   ⊢ 𝑀 = (Base‘(𝐽 mPoly 𝑅))    ⇒   ⊢ (𝜑 → ((𝐼extendVars𝑅)‘𝐴) = (𝑓 ∈ 𝑀 ↦ (𝑥 ∈ 𝐷 ↦ if((𝑥‘𝐴) = 0, (𝑓‘(𝑥 ↾ 𝐽)), 0 ))))
Theorem	extvfv 34269*	The "variable extension" function evaluated for converting a given polynomial 𝐹 by adding a variable with index 𝐴. (Contributed by Thierry Arnoux, 25-Jan-2026.)
⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐴 ∈ 𝐼)    &   ⊢ 𝐽 = (𝐼 ∖ {𝐴})    &   ⊢ 𝑀 = (Base‘(𝐽 mPoly 𝑅))    &   ⊢ (𝜑 → 𝐹 ∈ 𝑀)    ⇒   ⊢ (𝜑 → (((𝐼extendVars𝑅)‘𝐴)‘𝐹) = (𝑥 ∈ 𝐷 ↦ if((𝑥‘𝐴) = 0, (𝐹‘(𝑥 ↾ 𝐽)), 0 )))
Theorem	extvfvv 34270*	The "variable extension" function evaluated for converting a given polynomial 𝐹 by adding a variable with index 𝐴. (Contributed by Thierry Arnoux, 25-Jan-2026.)
⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐴 ∈ 𝐼)    &   ⊢ 𝐽 = (𝐼 ∖ {𝐴})    &   ⊢ 𝑀 = (Base‘(𝐽 mPoly 𝑅))    &   ⊢ (𝜑 → 𝐹 ∈ 𝑀)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐷)    ⇒   ⊢ (𝜑 → ((((𝐼extendVars𝑅)‘𝐴)‘𝐹)‘𝑋) = if((𝑋‘𝐴) = 0, (𝐹‘(𝑋 ↾ 𝐽)), 0 ))
Theorem	extvfvvcl 34271*	Closure for the "variable extension" function evaluated for converting a given polynomial 𝐹 by adding a variable with index 𝐴. (Contributed by Thierry Arnoux, 25-Jan-2026.)
⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝐽 = (𝐼 ∖ {𝐴})    &   ⊢ 𝑀 = (Base‘(𝐽 mPoly 𝑅))    &   ⊢ (𝜑 → 𝐴 ∈ 𝐼)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑀)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐷)    ⇒   ⊢ (𝜑 → ((((𝐼extendVars𝑅)‘𝐴)‘𝐹)‘𝑋) ∈ 𝐵)
Theorem	extvfvcl 34272*	Closure for the "variable extension" function evaluated for converting a given polynomial 𝐹 by adding a variable with index 𝐴. (Contributed by Thierry Arnoux, 25-Jan-2026.)
⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝐽 = (𝐼 ∖ {𝐴})    &   ⊢ 𝑀 = (Base‘(𝐽 mPoly 𝑅))    &   ⊢ (𝜑 → 𝐴 ∈ 𝐼)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑀)    &   ⊢ 𝑁 = (Base‘(𝐼 mPoly 𝑅))    ⇒   ⊢ (𝜑 → (((𝐼extendVars𝑅)‘𝐴)‘𝐹) ∈ 𝑁)
Theorem	extvfvalf 34273*	The "variable extension" function maps polynomials with variables indexed in 𝐽 to polynomials with variables indexed in 𝐼. (Contributed by Thierry Arnoux, 25-Jan-2026.)
⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝐽 = (𝐼 ∖ {𝐴})    &   ⊢ 𝑀 = (Base‘(𝐽 mPoly 𝑅))    &   ⊢ (𝜑 → 𝐴 ∈ 𝐼)    &   ⊢ 𝑁 = (Base‘(𝐼 mPoly 𝑅))    ⇒   ⊢ (𝜑 → ((𝐼extendVars𝑅)‘𝐴):𝑀⟶𝑁)
Theorem	mvrvalind 34274*	Value of the generating elements of the power series structure, expressed using the indicator function. (Contributed by Thierry Arnoux, 25-Jan-2026.)
⊢ 𝑉 = (𝐼 mVar 𝑅)    &   ⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin}    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑌)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐼)    &   ⊢ (𝜑 → 𝐹 ∈ 𝐷)    &   ⊢ 𝐴 = ((𝟭‘𝐼)‘{𝑋})    ⇒   ⊢ (𝜑 → ((𝑉‘𝑋)‘𝐹) = if(𝐹 = 𝐴, 1 , 0 ))
Theorem	mplmulmvr 34275*	Multiply a polynomial 𝐹 with a variable 𝑋 (i.e. with a monic monomial). (Contributed by Thierry Arnoux, 25-Jan-2026.)
⊢ 𝑃 = (𝐼 mPoly 𝑅)    &   ⊢ 𝑋 = ((𝐼 mVar 𝑅)‘𝑌)    &   ⊢ 𝑀 = (Base‘𝑃)    &   ⊢ · = (.r‘𝑃)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}    &   ⊢ 𝐴 = ((𝟭‘𝐼)‘{𝑌})    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐼)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑀)    ⇒   ⊢ (𝜑 → (𝑋 · 𝐹) = (𝑏 ∈ 𝐷 ↦ if((𝑏‘𝑌) = 0, 0 , (𝐹‘(𝑏 ∘f − 𝐴)))))
Theorem	evlscaval 34276	Polynomial evaluation for scalars. See evlsscaval 22479. (Contributed by Thierry Arnoux, 15-Feb-2026.)
⊢ 𝑄 = (𝐼 eval 𝑅)    &   ⊢ 𝑊 = (𝐼 mPoly 𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝐴 = (algSc‘𝑊)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐿:𝐼⟶𝐵)    ⇒   ⊢ (𝜑 → ((𝑄‘(𝐴‘𝑋))‘𝐿) = 𝑋)
Theorem	evlvarval 34277	Polynomial evaluation builder for a variable. (Contributed by Thierry Arnoux, 15-Feb-2026.)
⊢ 𝑄 = (𝐼 eval 𝑆)    &   ⊢ 𝑃 = (𝐼 mPoly 𝑆)    &   ⊢ 𝐾 = (Base‘𝑆)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ ∙ = (.r‘𝑃)    &   ⊢ · = (.r‘𝑆)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑍)    &   ⊢ (𝜑 → 𝑆 ∈ CRing)    &   ⊢ (𝜑 → 𝐴 ∈ (𝐾 ↑m 𝐼))    &   ⊢ 𝑉 = (𝐼 mVar 𝑆)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐼)    ⇒   ⊢ (𝜑 → ((𝑉‘𝑋) ∈ 𝐵 ∧ ((𝑄‘(𝑉‘𝑋))‘𝐴) = (𝐴‘𝑋)))
Theorem	evlextv 34278	Evaluating a variable-extended polynomial is the same as evaluating the polynomial in the original set of variables (in both cases, the additionial variable is ignored). (Contributed by Thierry Arnoux, 15-Feb-2026.)
⊢ 𝑄 = (𝐼 eval 𝑅)    &   ⊢ 𝑂 = (𝐽 eval 𝑅)    &   ⊢ 𝐽 = (𝐼 ∖ {𝑌})    &   ⊢ 𝑀 = (Base‘(𝐽 mPoly 𝑅))    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝐸 = (𝐼extendVars𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐼)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑀)    &   ⊢ (𝜑 → 𝐴:𝐼⟶𝐵)    ⇒   ⊢ (𝜑 → ((𝑄‘((𝐸‘𝑌)‘𝐹))‘𝐴) = ((𝑂‘𝐹)‘(𝐴 ↾ 𝐽)))
Theorem	mplvrpmlem 34279*	Lemma for mplvrpmga 34281 and others. (Contributed by Thierry Arnoux, 11-Jan-2026.)
⊢ 𝑆 = (SymGrp‘𝐼)    &   ⊢ 𝑃 = (Base‘𝑆)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑋 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0})    ⇒   ⊢ (𝜑 → (𝑋 ∘ 𝐷) ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0})
Theorem	mplvrpmfgalem 34280*	Permuting variables in a multivariate polynomial conserves finite support. (Contributed by Thierry Arnoux, 10-Jan-2026.)
⊢ 𝑆 = (SymGrp‘𝐼)    &   ⊢ 𝑃 = (Base‘𝑆)    &   ⊢ 𝑀 = (Base‘(𝐼 mPoly 𝑅))    &   ⊢ 𝐴 = (𝑑 ∈ 𝑃, 𝑓 ∈ 𝑀 ↦ (𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑓‘(𝑥 ∘ 𝑑))))    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑀)    &   ⊢ (𝜑 → 𝑄 ∈ 𝑃)    ⇒   ⊢ (𝜑 → (𝑄𝐴𝐹) finSupp 0 )
Theorem	mplvrpmga 34281*	The action of permuting variables in a multivariate polynomial is a group action. (Contributed by Thierry Arnoux, 10-Jan-2026.)
⊢ 𝑆 = (SymGrp‘𝐼)    &   ⊢ 𝑃 = (Base‘𝑆)    &   ⊢ 𝑀 = (Base‘(𝐼 mPoly 𝑅))    &   ⊢ 𝐴 = (𝑑 ∈ 𝑃, 𝑓 ∈ 𝑀 ↦ (𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑓‘(𝑥 ∘ 𝑑))))    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    ⇒   ⊢ (𝜑 → 𝐴 ∈ (𝑆 GrpAct 𝑀))
Theorem	mplvrpmmhm 34282*	The action of permuting variables in a multivariate polynomial is a monoid homomorphism. (Contributed by Thierry Arnoux, 11-Jan-2026.)
⊢ 𝑆 = (SymGrp‘𝐼)    &   ⊢ 𝑃 = (Base‘𝑆)    &   ⊢ 𝑀 = (Base‘(𝐼 mPoly 𝑅))    &   ⊢ 𝐴 = (𝑑 ∈ 𝑃, 𝑓 ∈ 𝑀 ↦ (𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑓‘(𝑥 ∘ 𝑑))))    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ 𝐹 = (𝑓 ∈ 𝑀 ↦ (𝐷𝐴𝑓))    &   ⊢ 𝑊 = (𝐼 mPoly 𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑃)    ⇒   ⊢ (𝜑 → 𝐹 ∈ (𝑊 MndHom 𝑊))
Theorem	mplvrpmrhm 34283*	The action of permuting variables in a multivariate polynomial is a ring homomorphism. (Contributed by Thierry Arnoux, 15-Jan-2026.)
⊢ 𝑆 = (SymGrp‘𝐼)    &   ⊢ 𝑃 = (Base‘𝑆)    &   ⊢ 𝑀 = (Base‘(𝐼 mPoly 𝑅))    &   ⊢ 𝐴 = (𝑑 ∈ 𝑃, 𝑓 ∈ 𝑀 ↦ (𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑓‘(𝑥 ∘ 𝑑))))    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ 𝐹 = (𝑓 ∈ 𝑀 ↦ (𝐷𝐴𝑓))    &   ⊢ 𝑊 = (𝐼 mPoly 𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑃)    ⇒   ⊢ (𝜑 → 𝐹 ∈ (𝑊 RingHom 𝑊))
Theorem	psrgsum 34284*	Finite commutative sums of power series are taken componentwise. (Contributed by Thierry Arnoux, 16-Mar-2026.)
⊢ 𝑆 = (𝐼 mPwSer 𝑅)    &   ⊢ 𝐵 = (Base‘𝑆)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}    &   ⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ (𝜑 → 𝐹:𝐴⟶𝐵)    ⇒   ⊢ (𝜑 → (𝑆 Σg 𝐹) = (𝑦 ∈ 𝐷 ↦ (𝑅 Σg (𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘)‘𝑦)))))
Theorem	psrmon 34285*	A monomial is a power series. (Contributed by Thierry Arnoux, 16-Mar-2026.)
⊢ 𝑆 = (𝐼 mPwSer 𝑅)    &   ⊢ 𝐵 = (Base‘𝑆)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    &   ⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}    &   ⊢ (𝜑 → 𝐼 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐷)    ⇒   ⊢ (𝜑 → (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑋, 1 , 0 )) ∈ 𝐵)
Theorem	psrmonmul 34286*	The product of two power series monomials adds the exponent vectors together. For example, the product of (𝑥↑2)(𝑦↑2) with (𝑦↑1)(𝑧↑3) is (𝑥↑2)(𝑦↑3)(𝑧↑3), where the exponent vectors ⟨2, 2, 0⟩ and ⟨0, 1, 3⟩ are added to give ⟨2, 3, 3⟩. (Contributed by Thierry Arnoux, 16-Mar-2026.)
⊢ 𝑆 = (𝐼 mPwSer 𝑅)    &   ⊢ 𝐵 = (Base‘𝑆)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    &   ⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}    &   ⊢ (𝜑 → 𝐼 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐷)    &   ⊢ · = (.r‘𝑆)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐷)    ⇒   ⊢ (𝜑 → ((𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑋, 1 , 0 )) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑌, 1 , 0 ))) = (𝑦 ∈ 𝐷 ↦ if(𝑦 = (𝑋 ∘f + 𝑌), 1 , 0 )))
Theorem	psrmonmul2 34287*	The product of two power series monomials adds the exponent vectors together. Here, the function 𝐺 is a monomial builder, which maps a bag of variables with the monic monomial with only those variables. (Contributed by Thierry Arnoux, 16-Mar-2026.)
⊢ 𝑆 = (𝐼 mPwSer 𝑅)    &   ⊢ 𝐵 = (Base‘𝑆)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    &   ⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}    &   ⊢ (𝜑 → 𝐼 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐷)    &   ⊢ · = (.r‘𝑆)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐷)    &   ⊢ 𝐺 = (𝑦 ∈ 𝐷 ↦ (𝑧 ∈ 𝐷 ↦ if(𝑧 = 𝑦, 1 , 0 )))    ⇒   ⊢ (𝜑 → ((𝐺‘𝑋) · (𝐺‘𝑌)) = (𝐺‘(𝑋 ∘f + 𝑌)))
Theorem	psrmonprod 34288*	Finite product of bags of variables in a power series. Here the function 𝐺 maps a bag of variables to the corresponding monomial. (Contributed by Thierry Arnoux, 16-Mar-2026.)
⊢ 𝑆 = (𝐼 mPwSer 𝑅)    &   ⊢ 𝐵 = (Base‘𝑆)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}    &   ⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ (𝜑 → 𝐹:𝐴⟶𝐷)    &   ⊢ 1 = (1r‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝑀 = (mulGrp‘𝑆)    &   ⊢ 𝐺 = (𝑦 ∈ 𝐷 ↦ (𝑧 ∈ 𝐷 ↦ if(𝑧 = 𝑦, 1 , 0 )))    ⇒   ⊢ (𝜑 → (𝑀 Σg (𝐺 ∘ 𝐹)) = (𝐺‘(𝑖 ∈ 𝐼 ↦ (ℂfld Σg (𝑥 ∈ 𝐴 ↦ ((𝐹‘𝑥)‘𝑖))))))
Theorem	mplgsum 34289*	Finite commutative sums of polynomials are taken componentwise. (Contributed by Thierry Arnoux, 16-Mar-2026.)
⊢ 𝑃 = (𝐼 mPoly 𝑅)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}    &   ⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ (𝜑 → 𝐹:𝐴⟶𝐵)    ⇒   ⊢ (𝜑 → (𝑃 Σg 𝐹) = (𝑦 ∈ 𝐷 ↦ (𝑅 Σg (𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘)‘𝑦)))))
Theorem	mplmonprod 34290*	Finite product of monomials. Here the function 𝐺 maps a bag of variables to the corresponding monomial. (Contributed by Thierry Arnoux, 16-Mar-2026.)
⊢ 𝑃 = (𝐼 mPoly 𝑅)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}    &   ⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ (𝜑 → 𝐹:𝐴⟶𝐷)    &   ⊢ 1 = (1r‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝑀 = (mulGrp‘𝑃)    &   ⊢ 𝐺 = (𝑦 ∈ 𝐷 ↦ (𝑧 ∈ 𝐷 ↦ if(𝑧 = 𝑦, 1 , 0 )))    ⇒   ⊢ (𝜑 → (𝑀 Σg (𝐺 ∘ 𝐹)) = (𝐺‘(𝑖 ∈ 𝐼 ↦ (ℂfld Σg (𝑥 ∈ 𝐴 ↦ ((𝐹‘𝑥)‘𝑖))))))
21.4.10.50  The ring of symmetric polynomials
Syntax	csply 34291	Extend class notation with the symmetric polynomials.
class SymPoly
Syntax	cesply 34292	Extend class notation with the elementary symmetric polynomials.
class eSymPoly
Definition	df-sply 34293*	Define symmetric polynomials. See splyval 34295 for a more readable expression. (Contributed by Thierry Arnoux, 11-Jan-2026.)
⊢ SymPoly = (𝑖 ∈ V, 𝑟 ∈ V ↦ ((Base‘(𝑖 mPoly 𝑟))FixPts(𝑑 ∈ (Base‘(SymGrp‘𝑖)), 𝑓 ∈ (Base‘(𝑖 mPoly 𝑟)) ↦ (𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝑖) ∣ ℎ finSupp 0} ↦ (𝑓‘(𝑥 ∘ 𝑑))))))
Definition	df-esply 34294*	Define elementary symmetric polynomials. (Contributed by Thierry Arnoux, 18-Jan-2026.)
⊢ eSymPoly = (𝑖 ∈ V, 𝑟 ∈ V ↦ (𝑘 ∈ ℕ0 ↦ ((ℤRHom‘𝑟) ∘ ((𝟭‘{ℎ ∈ (ℕ0 ↑m 𝑖) ∣ ℎ finSupp 0})‘((𝟭‘𝑖) “ {𝑐 ∈ 𝒫 𝑖 ∣ (♯‘𝑐) = 𝑘})))))
Theorem	splyval 34295*	The symmetric polynomials for a given index 𝐼 of variables and base ring 𝑅. These are the fixed points of the action 𝐴 which permutes variables. (Contributed by Thierry Arnoux, 11-Jan-2026.)
⊢ 𝑆 = (SymGrp‘𝐼)    &   ⊢ 𝑃 = (Base‘𝑆)    &   ⊢ 𝑀 = (Base‘(𝐼 mPoly 𝑅))    &   ⊢ 𝐴 = (𝑑 ∈ 𝑃, 𝑓 ∈ 𝑀 ↦ (𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑓‘(𝑥 ∘ 𝑑))))    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑊)    ⇒   ⊢ (𝜑 → (𝐼SymPoly𝑅) = (𝑀FixPts𝐴))
Theorem	splysubrg 34296*	The symmetric polynomials form a subring of the ring of polynomials. (Contributed by Thierry Arnoux, 15-Jan-2026.)
⊢ 𝑆 = (SymGrp‘𝐼)    &   ⊢ 𝑃 = (Base‘𝑆)    &   ⊢ 𝑀 = (Base‘(𝐼 mPoly 𝑅))    &   ⊢ 𝐴 = (𝑑 ∈ 𝑃, 𝑓 ∈ 𝑀 ↦ (𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑓‘(𝑥 ∘ 𝑑))))    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    ⇒   ⊢ (𝜑 → (𝐼SymPoly𝑅) ∈ (SubRing‘(𝐼 mPoly 𝑅)))
Theorem	issply 34297*	Conditions for being a symmetric polynomial. (Contributed by Thierry Arnoux, 18-Jan-2026.)
⊢ 𝑆 = (SymGrp‘𝐼)    &   ⊢ 𝑃 = (Base‘𝑆)    &   ⊢ 𝑀 = (Base‘(𝐼 mPoly 𝑅))    &   ⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑀)    &   ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑃) ∧ 𝑥 ∈ 𝐷) → (𝐹‘(𝑥 ∘ 𝑝)) = (𝐹‘𝑥))    ⇒   ⊢ (𝜑 → 𝐹 ∈ (𝐼SymPoly𝑅))
Theorem	esplyval 34298*	The elementary polynomials for a given index 𝐼 of variables and base ring 𝑅. (Contributed by Thierry Arnoux, 18-Jan-2026.)
⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑊)    ⇒   ⊢ (𝜑 → (𝐼eSymPoly𝑅) = (𝑘 ∈ ℕ0 ↦ ((ℤRHom‘𝑅) ∘ ((𝟭‘𝐷)‘((𝟭‘𝐼) “ {𝑐 ∈ 𝒫 𝐼 ∣ (♯‘𝑐) = 𝑘})))))
Theorem	esplyfval 34299*	The 𝐾-th elementary polynomial for a given index 𝐼 of variables and base ring 𝑅. (Contributed by Thierry Arnoux, 18-Jan-2026.)
⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐾 ∈ ℕ0)    ⇒   ⊢ (𝜑 → ((𝐼eSymPoly𝑅)‘𝐾) = ((ℤRHom‘𝑅) ∘ ((𝟭‘𝐷)‘((𝟭‘𝐼) “ {𝑐 ∈ 𝒫 𝐼 ∣ (♯‘𝑐) = 𝐾}))))
Theorem	esplyfval0 34300	The 0-th elementary symmetric polynomial is the constant 1. (Contributed by Thierry Arnoux, 15-Feb-2026.)
⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ 𝑈 = (1r‘(𝐼 mPoly 𝑅))    ⇒   ⊢ (𝜑 → ((𝐼eSymPoly𝑅)‘0) = 𝑈)