P. 337 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 33601-33700   *Has distinct variable group(s)

Type	Label	Description
Statement
Definition	df-ufd 33601*	Define the class of unique factorization domains. A unique factorization domain (UFD for short), is an integral domain such that every nonzero prime ideal contains a prime element (this is a characterization due to Irving Kaplansky). A UFD is sometimes also called a "factorial ring" following the terminology of Bourbaki. (Contributed by Mario Carneiro, 17-Feb-2015.) Exclude the 0 prime ideal. (Revised by Thierry Arnoux, 9-May-2025.) Exclude the 0 ring. (Revised by Thierry Arnoux, 14-Jun-2025.)
⊢ UFD = {𝑟 ∈ IDomn ∣ ∀𝑖 ∈ ((PrmIdeal‘𝑟) ∖ {{(0g‘𝑟)}})(𝑖 ∩ (RPrime‘𝑟)) ≠ ∅}
Theorem	isufd 33602*	The property of being a Unique Factorization Domain. (Contributed by Thierry Arnoux, 1-Jun-2024.)
⊢ 𝐼 = (PrmIdeal‘𝑅)    &   ⊢ 𝑃 = (RPrime‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    ⇒   ⊢ (𝑅 ∈ UFD ↔ (𝑅 ∈ IDomn ∧ ∀𝑖 ∈ (𝐼 ∖ {{ 0 }})(𝑖 ∩ 𝑃) ≠ ∅))
Theorem	ufdprmidl 33603*	In a unique factorization domain 𝑅, a nonzero prime ideal 𝐽 contains a prime element 𝑝. (Contributed by Thierry Arnoux, 3-Jun-2025.)
⊢ 𝐼 = (PrmIdeal‘𝑅)    &   ⊢ 𝑃 = (RPrime‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ UFD)    &   ⊢ (𝜑 → 𝐽 ∈ 𝐼)    &   ⊢ (𝜑 → 𝐽 ≠ { 0 })    ⇒   ⊢ (𝜑 → ∃𝑝 ∈ 𝑃 𝑝 ∈ 𝐽)
Theorem	ufdidom 33604	A nonzero unique factorization domain is an integral domain. (Contributed by Thierry Arnoux, 3-Jun-2025.)
⊢ (𝜑 → 𝑅 ∈ UFD)    ⇒   ⊢ (𝜑 → 𝑅 ∈ IDomn)
Theorem	pidufd 33605	Every principal ideal domain is a unique factorization domain. (Contributed by Thierry Arnoux, 3-Jun-2025.)
⊢ (𝜑 → 𝑅 ∈ PID)    ⇒   ⊢ (𝜑 → 𝑅 ∈ UFD)
Theorem	1arithufdlem1 33606*	Lemma for 1arithufd 33610. The set 𝑆 of elements which can be written as a product of primes is not empty. (Contributed by Thierry Arnoux, 3-Jun-2025.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝑈 = (Unit‘𝑅)    &   ⊢ 𝑃 = (RPrime‘𝑅)    &   ⊢ 𝑀 = (mulGrp‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ UFD)    &   ⊢ (𝜑 → ¬ 𝑅 ∈ DivRing)    &   ⊢ 𝑆 = {𝑥 ∈ 𝐵 ∣ ∃𝑓 ∈ Word 𝑃𝑥 = (𝑀 Σg 𝑓)}    ⇒   ⊢ (𝜑 → 𝑆 ≠ ∅)
Theorem	1arithufdlem2 33607*	Lemma for 1arithufd 33610. The set 𝑆 of elements which can be written as a product of primes is multiplicatively closed. (Contributed by Thierry Arnoux, 3-Jun-2025.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝑈 = (Unit‘𝑅)    &   ⊢ 𝑃 = (RPrime‘𝑅)    &   ⊢ 𝑀 = (mulGrp‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ UFD)    &   ⊢ (𝜑 → ¬ 𝑅 ∈ DivRing)    &   ⊢ 𝑆 = {𝑥 ∈ 𝐵 ∣ ∃𝑓 ∈ Word 𝑃𝑥 = (𝑀 Σg 𝑓)}    &   ⊢ · = (.r‘𝑅)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑆)    ⇒   ⊢ (𝜑 → (𝑋 · 𝑌) ∈ 𝑆)
Theorem	1arithufdlem3 33608*	Lemma for 1arithufd 33610. If a product (𝑌 · 𝑋) can be written as a product of primes, with 𝑋 non-unit, nonzero, so can 𝑋. (Contributed by Thierry Arnoux, 3-Jun-2025.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝑈 = (Unit‘𝑅)    &   ⊢ 𝑃 = (RPrime‘𝑅)    &   ⊢ 𝑀 = (mulGrp‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ UFD)    &   ⊢ (𝜑 → ¬ 𝑅 ∈ DivRing)    &   ⊢ 𝑆 = {𝑥 ∈ 𝐵 ∣ ∃𝑓 ∈ Word 𝑃𝑥 = (𝑀 Σg 𝑓)}    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → ¬ 𝑋 ∈ 𝑈)    &   ⊢ (𝜑 → 𝑋 ≠ 0 )    &   ⊢ · = (.r‘𝑅)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → (𝑌 · 𝑋) ∈ 𝑆)    ⇒   ⊢ (𝜑 → 𝑋 ∈ 𝑆)
Theorem	1arithufdlem4 33609*	Lemma for 1arithufd 33610. Nonzero ring, non-field case. Those trivial cases are handled in the final proof. (Contributed by Thierry Arnoux, 3-Jun-2025.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝑈 = (Unit‘𝑅)    &   ⊢ 𝑃 = (RPrime‘𝑅)    &   ⊢ 𝑀 = (mulGrp‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ UFD)    &   ⊢ (𝜑 → ¬ 𝑅 ∈ DivRing)    &   ⊢ 𝑆 = {𝑥 ∈ 𝐵 ∣ ∃𝑓 ∈ Word 𝑃𝑥 = (𝑀 Σg 𝑓)}    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → ¬ 𝑋 ∈ 𝑈)    &   ⊢ (𝜑 → 𝑋 ≠ 0 )    ⇒   ⊢ (𝜑 → 𝑋 ∈ 𝑆)
Theorem	1arithufd 33610*	Existence of a factorization into irreducible elements in a unique factorization domain. Any non-zero, non-unit element 𝑋 of a UFD 𝑅 can be written as a product of primes 𝑓. As shown in 1arithidom 33599, that factorization is unique, up to the order of the factors and multiplication by units. (Contributed by Thierry Arnoux, 3-Jun-2025.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝑈 = (Unit‘𝑅)    &   ⊢ 𝑃 = (RPrime‘𝑅)    &   ⊢ 𝑀 = (mulGrp‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ UFD)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → ¬ 𝑋 ∈ 𝑈)    &   ⊢ (𝜑 → 𝑋 ≠ 0 )    ⇒   ⊢ (𝜑 → ∃𝑓 ∈ Word 𝑃𝑋 = (𝑀 Σg 𝑓))
Theorem	dfufd2lem 33611	Lemma for dfufd2 33612. (Contributed by Thierry Arnoux, 6-Jun-2025.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝑈 = (Unit‘𝑅)    &   ⊢ 𝑃 = (RPrime‘𝑅)    &   ⊢ 𝑀 = (mulGrp‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ IDomn)    &   ⊢ (𝜑 → 𝐼 ∈ (PrmIdeal‘𝑅))    &   ⊢ (𝜑 → 𝐹 ∈ Word 𝑃)    &   ⊢ (𝜑 → (𝑀 Σg 𝐹) ∈ 𝐼)    &   ⊢ (𝜑 → (𝑀 Σg 𝐹) ≠ 0 )    ⇒   ⊢ (𝜑 → (𝐼 ∩ 𝑃) ≠ ∅)
Theorem	dfufd2 33612*	Alternative definition of unique factorization domain (UFD). This is often the textbook definition. Chapter VII, Paragraph 3, Section 3, Proposition 2 of [BourbakiCAlg2], p. 228. (Contributed by Thierry Arnoux, 6-Jun-2025.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝑈 = (Unit‘𝑅)    &   ⊢ 𝑃 = (RPrime‘𝑅)    &   ⊢ 𝑀 = (mulGrp‘𝑅)    ⇒   ⊢ (𝑅 ∈ UFD ↔ (𝑅 ∈ IDomn ∧ ∀𝑥 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })∃𝑓 ∈ Word 𝑃𝑥 = (𝑀 Σg 𝑓)))
21.3.10.45  The ring of integers
Theorem	zringidom 33613	The ring of integers is an integral domain. (Contributed by Thierry Arnoux, 4-May-2025.)
⊢ ℤring ∈ IDomn
Theorem	zringpid 33614	The ring of integers is a principal ideal domain. (Contributed by Thierry Arnoux, 18-May-2025.)
⊢ ℤring ∈ PID
Theorem	dfprm3 33615	The (positive) prime elements of the integer ring are the prime numbers. (Contributed by Thierry Arnoux, 18-May-2025.)
⊢ ℙ = (ℕ ∩ (RPrime‘ℤring))
Theorem	zringfrac 33616*	The field of fractions of the ring of integers is isomorphic to the field of the rational numbers. (Contributed by Thierry Arnoux, 4-May-2025.)
⊢ 𝑄 = (ℂfld ↾s ℚ)    &   ⊢ ∼ = (ℤring ~RL (ℤ ∖ {0}))    &   ⊢ 𝐹 = (𝑞 ∈ ℚ ↦ [⟨(numer‘𝑞), (denom‘𝑞)⟩] ∼ )    ⇒   ⊢ 𝐹 ∈ (𝑄 RingIso ( Frac ‘ℤring))
21.3.10.46  Associative Algebra
Theorem	assaassd 33617	Left-associative property of an associative algebra, deduction version. (Contributed by Thierry Arnoux, 15-Feb-2026.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ 𝐵 = (Base‘𝐹)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ × = (.r‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ AssAlg)    &   ⊢ (𝜑 → 𝐴 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    ⇒   ⊢ (𝜑 → ((𝐴 · 𝑋) × 𝑌) = (𝐴 · (𝑋 × 𝑌)))
Theorem	assaassrd 33618	Right-associative property of an associative algebra, deduction version. (Contributed by Thierry Arnoux, 15-Feb-2026.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ 𝐵 = (Base‘𝐹)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ × = (.r‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ AssAlg)    &   ⊢ (𝜑 → 𝐴 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (𝑋 × (𝐴 · 𝑌)) = (𝐴 · (𝑋 × 𝑌)))
21.3.10.47  Univariate Polynomials
Theorem	0ringmon1p 33619	There are no monic polynomials over a zero ring. (Contributed by Thierry Arnoux, 5-Feb-2025.)
⊢ 𝑀 = (Monic1p‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → (♯‘𝐵) = 1)    ⇒   ⊢ (𝜑 → 𝑀 = ∅)
Theorem	fply1 33620	Conditions for a function to be a univariate polynomial. (Contributed by Thierry Arnoux, 19-Aug-2023.)
⊢ 0 = (0g‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝑃 = (Base‘(Poly1‘𝑅))    &   ⊢ (𝜑 → 𝐹:(ℕ0 ↑m 1o)⟶𝐵)    &   ⊢ (𝜑 → 𝐹 finSupp 0 )    ⇒   ⊢ (𝜑 → 𝐹 ∈ 𝑃)
Theorem	ply1lvec 33621	In a division ring, the univariate polynomials form a vector space. (Contributed by Thierry Arnoux, 19-Feb-2025.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ DivRing)    ⇒   ⊢ (𝜑 → 𝑃 ∈ LVec)
Theorem	evls1fn 33622	Functionality of the subring polynomial evaluation. (Contributed by Thierry Arnoux, 9-Feb-2025.)
⊢ 𝑂 = (𝑅 evalSub1 𝑆)    &   ⊢ 𝑃 = (Poly1‘(𝑅 ↾s 𝑆))    &   ⊢ 𝑈 = (Base‘𝑃)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝑆 ∈ (SubRing‘𝑅))    ⇒   ⊢ (𝜑 → 𝑂 Fn 𝑈)
Theorem	evls1dm 33623	The domain of the subring polynomial evaluation function. (Contributed by Thierry Arnoux, 9-Feb-2025.)
⊢ 𝑂 = (𝑅 evalSub1 𝑆)    &   ⊢ 𝑃 = (Poly1‘(𝑅 ↾s 𝑆))    &   ⊢ 𝑈 = (Base‘𝑃)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝑆 ∈ (SubRing‘𝑅))    ⇒   ⊢ (𝜑 → dom 𝑂 = 𝑈)
Theorem	evls1fvf 33624	The subring evaluation function for a univariate polynomial as a function, with domain and codomain. (Contributed by Thierry Arnoux, 22-Mar-2025.)
⊢ 𝑂 = (𝑅 evalSub1 𝑆)    &   ⊢ 𝑃 = (Poly1‘(𝑅 ↾s 𝑆))    &   ⊢ 𝑈 = (Base‘𝑃)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝑆 ∈ (SubRing‘𝑅))    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ (𝜑 → 𝑄 ∈ 𝑈)    ⇒   ⊢ (𝜑 → (𝑂‘𝑄):𝐵⟶𝐵)
Theorem	evl1fvf 33625	The univariate polynomial evaluation function as a function, with domain and codomain. (Contributed by Thierry Arnoux, 8-Jun-2025.)
⊢ 𝑂 = (eval1‘𝑅)    &   ⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝑈 = (Base‘𝑃)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ (𝜑 → 𝑄 ∈ 𝑈)    ⇒   ⊢ (𝜑 → (𝑂‘𝑄):𝐵⟶𝐵)
Theorem	evl1fpws 33626*	Evaluation of a univariate polynomial as a function in a power series. (Contributed by Thierry Arnoux, 23-Jan-2025.)
⊢ 𝑂 = (eval1‘𝑅)    &   ⊢ 𝑊 = (Poly1‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝑈 = (Base‘𝑊)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝑀 ∈ 𝑈)    &   ⊢ · = (.r‘𝑅)    &   ⊢ ↑ = (.g‘(mulGrp‘𝑅))    &   ⊢ 𝐴 = (coe1‘𝑀)    ⇒   ⊢ (𝜑 → (𝑂‘𝑀) = (𝑥 ∈ 𝐵 ↦ (𝑅 Σg (𝑘 ∈ ℕ0 ↦ ((𝐴‘𝑘) · (𝑘 ↑ 𝑥))))))
Theorem	ressply1evls1 33627	Subring evaluation of a univariate polynomial is the same as the subring evaluation in the bigger ring. (Contributed by Thierry Arnoux, 14-Nov-2025.)
⊢ 𝐺 = (𝐸 ↾s 𝑅)    &   ⊢ 𝑂 = (𝐸 evalSub1 𝑆)    &   ⊢ 𝑄 = (𝐺 evalSub1 𝑆)    &   ⊢ 𝑃 = (Poly1‘𝐾)    &   ⊢ 𝐾 = (𝐸 ↾s 𝑆)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ (𝜑 → 𝐸 ∈ CRing)    &   ⊢ (𝜑 → 𝑅 ∈ (SubRing‘𝐸))    &   ⊢ (𝜑 → 𝑆 ∈ (SubRing‘𝐺))    &   ⊢ (𝜑 → 𝐹 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝑄‘𝐹) = ((𝑂‘𝐹) ↾ 𝑅))
Theorem	ressdeg1 33628	The degree of a univariate polynomial in a structure restriction. (Contributed by Thierry Arnoux, 20-Jan-2025.)
⊢ 𝐻 = (𝑅 ↾s 𝑇)    &   ⊢ 𝐷 = (deg1‘𝑅)    &   ⊢ 𝑈 = (Poly1‘𝐻)    &   ⊢ 𝐵 = (Base‘𝑈)    &   ⊢ (𝜑 → 𝑃 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑇 ∈ (SubRing‘𝑅))    ⇒   ⊢ (𝜑 → (𝐷‘𝑃) = ((deg1‘𝐻)‘𝑃))
Theorem	ressply10g 33629	A restricted polynomial algebra has the same group identity (zero polynomial). (Contributed by Thierry Arnoux, 20-Jan-2025.)
⊢ 𝑆 = (Poly1‘𝑅)    &   ⊢ 𝐻 = (𝑅 ↾s 𝑇)    &   ⊢ 𝑈 = (Poly1‘𝐻)    &   ⊢ 𝐵 = (Base‘𝑈)    &   ⊢ (𝜑 → 𝑇 ∈ (SubRing‘𝑅))    &   ⊢ 𝑍 = (0g‘𝑆)    ⇒   ⊢ (𝜑 → 𝑍 = (0g‘𝑈))
Theorem	ressply1mon1p 33630	The monic polynomials of a restricted polynomial algebra. (Contributed by Thierry Arnoux, 21-Jan-2025.)
⊢ 𝑆 = (Poly1‘𝑅)    &   ⊢ 𝐻 = (𝑅 ↾s 𝑇)    &   ⊢ 𝑈 = (Poly1‘𝐻)    &   ⊢ 𝐵 = (Base‘𝑈)    &   ⊢ (𝜑 → 𝑇 ∈ (SubRing‘𝑅))    &   ⊢ 𝑀 = (Monic1p‘𝑅)    &   ⊢ 𝑁 = (Monic1p‘𝐻)    ⇒   ⊢ (𝜑 → 𝑁 = (𝐵 ∩ 𝑀))
Theorem	ressply1invg 33631	An element of a restricted polynomial algebra has the same group inverse. (Contributed by Thierry Arnoux, 30-Jan-2025.)
⊢ 𝑆 = (Poly1‘𝑅)    &   ⊢ 𝐻 = (𝑅 ↾s 𝑇)    &   ⊢ 𝑈 = (Poly1‘𝐻)    &   ⊢ 𝐵 = (Base‘𝑈)    &   ⊢ (𝜑 → 𝑇 ∈ (SubRing‘𝑅))    &   ⊢ 𝑃 = (𝑆 ↾s 𝐵)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → ((invg‘𝑈)‘𝑋) = ((invg‘𝑃)‘𝑋))
Theorem	ressply1sub 33632	A restricted polynomial algebra has the same subtraction operation. (Contributed by Thierry Arnoux, 30-Jan-2025.)
⊢ 𝑆 = (Poly1‘𝑅)    &   ⊢ 𝐻 = (𝑅 ↾s 𝑇)    &   ⊢ 𝑈 = (Poly1‘𝐻)    &   ⊢ 𝐵 = (Base‘𝑈)    &   ⊢ (𝜑 → 𝑇 ∈ (SubRing‘𝑅))    &   ⊢ 𝑃 = (𝑆 ↾s 𝐵)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝑋(-g‘𝑈)𝑌) = (𝑋(-g‘𝑃)𝑌))
Theorem	ressasclcl 33633	Closure of the univariate polynomial evaluation for scalars. (Contributed by Thierry Arnoux, 22-Jun-2025.)
⊢ 𝑊 = (Poly1‘𝑈)    &   ⊢ 𝑈 = (𝑆 ↾s 𝑅)    &   ⊢ 𝐴 = (algSc‘𝑊)    &   ⊢ 𝐵 = (Base‘𝑊)    &   ⊢ (𝜑 → 𝑆 ∈ CRing)    &   ⊢ (𝜑 → 𝑅 ∈ (SubRing‘𝑆))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑅)    ⇒   ⊢ (𝜑 → (𝐴‘𝑋) ∈ 𝐵)
Theorem	evls1subd 33634	Univariate polynomial evaluation of a difference of polynomials. (Contributed by Thierry Arnoux, 25-Apr-2025.)
⊢ 𝑄 = (𝑆 evalSub1 𝑅)    &   ⊢ 𝐾 = (Base‘𝑆)    &   ⊢ 𝑊 = (Poly1‘𝑈)    &   ⊢ 𝑈 = (𝑆 ↾s 𝑅)    &   ⊢ 𝐵 = (Base‘𝑊)    &   ⊢ 𝐷 = (-g‘𝑊)    &   ⊢ − = (-g‘𝑆)    &   ⊢ (𝜑 → 𝑆 ∈ CRing)    &   ⊢ (𝜑 → 𝑅 ∈ (SubRing‘𝑆))    &   ⊢ (𝜑 → 𝑀 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑁 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐶 ∈ 𝐾)    ⇒   ⊢ (𝜑 → ((𝑄‘(𝑀𝐷𝑁))‘𝐶) = (((𝑄‘𝑀)‘𝐶) − ((𝑄‘𝑁)‘𝐶)))
Theorem	deg1le0eq0 33635	A polynomial with nonpositive degree is the zero polynomial iff its constant term is zero. Biconditional version of deg1scl 26078. (Contributed by Thierry Arnoux, 22-Mar-2025.)
⊢ 𝐷 = (deg1‘𝑅)    &   ⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 𝑂 = (0g‘𝑃)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝐹 ∈ 𝐵)    &   ⊢ (𝜑 → (𝐷‘𝐹) ≤ 0)    ⇒   ⊢ (𝜑 → (𝐹 = 𝑂 ↔ ((coe1‘𝐹)‘0) = 0 ))
Theorem	ply1asclunit 33636	A non-zero 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 33637	In a field 𝐹, a polynomial 𝐶 is a unit iff it has degree 0. This corresponds to the nonzero scalars, see ply1asclunit 33636. (Contributed by Thierry Arnoux, 25-Apr-2025.)
⊢ 𝑃 = (Poly1‘𝐹)    &   ⊢ 𝐴 = (algSc‘𝑃)    &   ⊢ 𝐵 = (Base‘𝐹)    &   ⊢ 0 = (0g‘𝐹)    &   ⊢ (𝜑 → 𝐹 ∈ Field)    &   ⊢ 𝐷 = (deg1‘𝐹)    &   ⊢ (𝜑 → 𝐶 ∈ (Base‘𝑃))    ⇒   ⊢ (𝜑 → (𝐶 ∈ (Unit‘𝑃) ↔ (𝐷‘𝐶) = 0))
Theorem	evl1deg1 33638	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 33639	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 33640	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 33641	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 33642	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 33643	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 33644	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 33645*	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 33646	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 33647	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 33648	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 33649*	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 33650	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 33651*	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 33652	The coefficients of the zero univariate polynomial. (Contributed by Thierry Arnoux, 22-Jun-2025.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝑍 = (0g‘𝑃)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    ⇒   ⊢ (𝜑 → ((coe1‘𝑍)‘𝑁) = 0 )
Theorem	coe1vr1 33653*	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 33654	The degree of the variable polynomial is 1. (Contributed by Thierry Arnoux, 22-Jun-2025.)
⊢ 𝐷 = (deg1‘𝑅)    &   ⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝑋 = (var1‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ NzRing)    ⇒   ⊢ (𝜑 → (𝐷‘𝑋) = 1)
Theorem	vr1nz 33655	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 33656	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 33657	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 33658	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 33659*	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 33660*	A coefficient of the polynomial represented as a sum of scaled monomials is the coefficient of the corresponding scaled monomial. See gsummoncoe1fzo 33659. (Contributed by Thierry Arnoux, 15-Feb-2026.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 𝑋 = (var1‘𝑅)    &   ⊢ ↑ = (.g‘(mulGrp‘𝑃))    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ 𝐾 = (Base‘𝑅)    &   ⊢ ∗ = ( ·𝑠 ‘𝑃)    &   ⊢ (𝜑 → 𝐷 ∈ ℕ0)    &   ⊢ (𝜑 → ∀𝑘 ∈ (0...𝐷)𝐴 ∈ 𝐾)    &   ⊢ (𝜑 → 𝐿 ∈ (0...𝐷))    &   ⊢ (𝑘 = 𝐿 → 𝐴 = 𝐶)    ⇒   ⊢ (𝜑 → ((coe1‘(𝑃 Σg (𝑘 ∈ (0...𝐷) ↦ (𝐴 ∗ (𝑘 ↑ 𝑋)))))‘𝐿) = 𝐶)
Theorem	ply1gsumz 33661*	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 33662	If both factors have degree bounded by 𝐿, then the sum of the polynomials also has degree bounded by 𝐿. See also deg1addle 26066. (Contributed by Thierry Arnoux, 2-Apr-2025.)
⊢ 𝑌 = (Poly1‘𝑅)    &   ⊢ 𝐷 = (deg1‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ 𝐵 = (Base‘𝑌)    &   ⊢ + = (+g‘𝑌)    &   ⊢ (𝜑 → 𝐹 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐿 ∈ ℝ*)    &   ⊢ (𝜑 → (𝐷‘𝐹) < 𝐿)    &   ⊢ (𝜑 → (𝐷‘𝐺) < 𝐿)    ⇒   ⊢ (𝜑 → (𝐷‘(𝐹 + 𝐺)) < 𝐿)
Theorem	ig1pnunit 33663	The polynomial ideal generator is not a unit polynomial. (Contributed by Thierry Arnoux, 19-Mar-2025.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐺 = (idlGen1p‘𝑅)    &   ⊢ 𝑈 = (Base‘𝑃)    &   ⊢ (𝜑 → 𝑅 ∈ DivRing)    &   ⊢ (𝜑 → 𝐼 ∈ (LIdeal‘𝑃))    &   ⊢ (𝜑 → 𝐼 ≠ 𝑈)    ⇒   ⊢ (𝜑 → ¬ (𝐺‘𝐼) ∈ (Unit‘𝑃))
Theorem	ig1pmindeg 33664	The polynomial ideal generator is of minimum degree. (Contributed by Thierry Arnoux, 19-Mar-2025.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐺 = (idlGen1p‘𝑅)    &   ⊢ 𝑈 = (Base‘𝑃)    &   ⊢ (𝜑 → 𝑅 ∈ DivRing)    &   ⊢ (𝜑 → 𝐼 ∈ (LIdeal‘𝑃))    &   ⊢ 𝐷 = (deg1‘𝑅)    &   ⊢ 0 = (0g‘𝑃)    &   ⊢ (𝜑 → 𝐹 ∈ 𝐼)    &   ⊢ (𝜑 → 𝐹 ≠ 0 )    ⇒   ⊢ (𝜑 → (𝐷‘(𝐺‘𝐼)) ≤ (𝐷‘𝐹))
21.3.10.48  Polynomial quotient and polynomial remainder
Theorem	q1pdir 33665	Distribution of univariate polynomial quotient over addition. (Contributed by Thierry Arnoux, 2-Apr-2025.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝑈 = (Base‘𝑃)    &   ⊢ 𝑁 = (Unic1p‘𝑅)    &   ⊢ / = (quot1p‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑁)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑈)    &   ⊢ + = (+g‘𝑃)    ⇒   ⊢ (𝜑 → ((𝐴 + 𝐵) / 𝐶) = ((𝐴 / 𝐶) + (𝐵 / 𝐶)))
Theorem	q1pvsca 33666	Scalar multiplication property of the polynomial division. (Contributed by Thierry Arnoux, 2-Apr-2025.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝑈 = (Base‘𝑃)    &   ⊢ 𝑁 = (Unic1p‘𝑅)    &   ⊢ / = (quot1p‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑁)    &   ⊢ × = ( ·𝑠 ‘𝑃)    &   ⊢ 𝐾 = (Base‘𝑅)    &   ⊢ (𝜑 → 𝐵 ∈ 𝐾)    ⇒   ⊢ (𝜑 → ((𝐵 × 𝐴) / 𝐶) = (𝐵 × (𝐴 / 𝐶)))
Theorem	r1pvsca 33667	Scalar multiplication property of the polynomial remainder operation. (Contributed by Thierry Arnoux, 2-Apr-2025.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝑈 = (Base‘𝑃)    &   ⊢ 𝑁 = (Unic1p‘𝑅)    &   ⊢ 𝐸 = (rem1p‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑁)    &   ⊢ × = ( ·𝑠 ‘𝑃)    &   ⊢ 𝐾 = (Base‘𝑅)    &   ⊢ (𝜑 → 𝐵 ∈ 𝐾)    ⇒   ⊢ (𝜑 → ((𝐵 × 𝐴)𝐸𝐷) = (𝐵 × (𝐴𝐸𝐷)))
Theorem	r1p0 33668	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 33669	The polynomial remainder operation is periodic. See modcyc 13830. (Contributed by Thierry Arnoux, 2-Apr-2025.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝑈 = (Base‘𝑃)    &   ⊢ 𝑁 = (Unic1p‘𝑅)    &   ⊢ 𝐸 = (rem1p‘𝑅)    &   ⊢ + = (+g‘𝑃)    &   ⊢ · = (.r‘𝑃)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑁)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑈)    ⇒   ⊢ (𝜑 → ((𝐴 + (𝐶 · 𝐵))𝐸𝐵) = (𝐴𝐸𝐵))
Theorem	r1padd1 33670	Addition property of the polynomial remainder operation, similar to modadd1 13832. (Contributed by Thierry Arnoux, 2-Apr-2025.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝑈 = (Base‘𝑃)    &   ⊢ 𝑁 = (Unic1p‘𝑅)    &   ⊢ 𝐸 = (rem1p‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑁)    &   ⊢ (𝜑 → (𝐴𝐸𝐷) = (𝐵𝐸𝐷))    &   ⊢ + = (+g‘𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑈)    ⇒   ⊢ (𝜑 → ((𝐴 + 𝐶)𝐸𝐷) = ((𝐵 + 𝐶)𝐸𝐷))
Theorem	r1pid2OLD 33671	Obsolete version of r1pid2 26127 as of 21-Jun-2025. (Contributed by Thierry Arnoux, 2-Apr-2025.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝑈 = (Base‘𝑃)    &   ⊢ 𝑁 = (Unic1p‘𝑅)    &   ⊢ 𝐸 = (rem1p‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ IDomn)    &   ⊢ 𝐷 = (deg1‘𝑅)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑁)    ⇒   ⊢ (𝜑 → ((𝐴𝐸𝐵) = 𝐴 ↔ (𝐷‘𝐴) < (𝐷‘𝐵)))
Theorem	r1plmhm 33672*	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 33673*	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 𝑃))
21.3.10.49  Multivariate Polynomials
Theorem	psrbasfsupp 33674	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 21893, 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}
Syntax	cextv 33675	Extend class notation with the "variable extension" function.
class extendVars
Definition	df-extv 33676*	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 33677*	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 33678*	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 33679*	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 33680*	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 33681*	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 33682*	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 33683*	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 33684*	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 33685*	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 33686	Polynomial evaluation for scalars. See evlsscaval 42846. (Contributed by Thierry Arnoux, 15-Feb-2026.)
⊢ 𝑄 = (𝐼 eval 𝑅)    &   ⊢ 𝑊 = (𝐼 mPoly 𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝐴 = (algSc‘𝑊)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐿:𝐼⟶𝐵)    ⇒   ⊢ (𝜑 → ((𝑄‘(𝐴‘𝑋))‘𝐿) = 𝑋)
Theorem	evlvarval 33687	Polynomial evaluation builder for a variable. (Contributed by Thierry Arnoux, 15-Feb-2026.)
⊢ 𝑄 = (𝐼 eval 𝑆)    &   ⊢ 𝑃 = (𝐼 mPoly 𝑆)    &   ⊢ 𝐾 = (Base‘𝑆)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ ∙ = (.r‘𝑃)    &   ⊢ · = (.r‘𝑆)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑍)    &   ⊢ (𝜑 → 𝑆 ∈ CRing)    &   ⊢ (𝜑 → 𝐴 ∈ (𝐾 ↑m 𝐼))    &   ⊢ 𝑉 = (𝐼 mVar 𝑆)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐼)    ⇒   ⊢ (𝜑 → ((𝑉‘𝑋) ∈ 𝐵 ∧ ((𝑄‘(𝑉‘𝑋))‘𝐴) = (𝐴‘𝑋)))
Theorem	evlextv 33688	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 33689*	Lemma for mplvrpmga 33691 and others. (Contributed by Thierry Arnoux, 11-Jan-2026.)
⊢ 𝑆 = (SymGrp‘𝐼)    &   ⊢ 𝑃 = (Base‘𝑆)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑋 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0})    ⇒   ⊢ (𝜑 → (𝑋 ∘ 𝐷) ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0})
Theorem	mplvrpmfgalem 33690*	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 33691*	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 33692*	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 33693*	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 𝑊))
21.3.10.50  The ring of symmetric polynomials
Syntax	csply 33694	Extend class notation with the symmetric polynomials.
class SymPoly
Syntax	cesply 33695	Extend class notation with the elementary symmetric polynomials.
class eSymPoly
Definition	df-sply 33696*	Define symmetric polynomials. See splyval 33698 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 33697*	Define elementary symmetric polynomials. (Contributed by Thierry Arnoux, 18-Jan-2026.)
⊢ eSymPoly = (𝑖 ∈ V, 𝑟 ∈ V ↦ (𝑘 ∈ ℕ0 ↦ ((ℤRHom‘𝑟) ∘ ((𝟭‘{ℎ ∈ (ℕ0 ↑m 𝑖) ∣ ℎ finSupp 0})‘((𝟭‘𝑖) “ {𝑐 ∈ 𝒫 𝑖 ∣ (♯‘𝑐) = 𝑘})))))
Theorem	splyval 33698*	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 33699*	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 33700*	Conditions for being a symmetric polynomial. (Contributed by Thierry Arnoux, 18-Jan-2026.)
⊢ 𝑆 = (SymGrp‘𝐼)    &   ⊢ 𝑃 = (Base‘𝑆)    &   ⊢ 𝑀 = (Base‘(𝐼 mPoly 𝑅))    &   ⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑀)    &   ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑃) ∧ 𝑥 ∈ 𝐷) → (𝐹‘(𝑥 ∘ 𝑝)) = (𝐹‘𝑥))    ⇒   ⊢ (𝜑 → 𝐹 ∈ (𝐼SymPoly𝑅))