HomeTheorem List (p. 337 of 503)
GIF version.
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List
| Home |
Metamath
Proof Explorer Theorem List (p. 337 of 503) | < Previous Next > |
| Bad symbols? Try the
GIF version. |
||
|
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
||
| Color key: | Metamath Proof Explorer
(1-30989) |
Hilbert Space Explorer
(30990-32512) |
Users' Mathboxes
(32513-50274) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | ufdprmidl 33601* | 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 33602 | A nonzero unique factorization domain is an integral domain. (Contributed by Thierry Arnoux, 3-Jun-2025.) |
| ⊢ (𝜑 → 𝑅 ∈ UFD) ⇒ ⊢ (𝜑 → 𝑅 ∈ IDomn) | ||
| Theorem | pidufd 33603 | Every principal ideal domain is a unique factorization domain. (Contributed by Thierry Arnoux, 3-Jun-2025.) |
| ⊢ (𝜑 → 𝑅 ∈ PID) ⇒ ⊢ (𝜑 → 𝑅 ∈ UFD) | ||
| Theorem | 1arithufdlem1 33604* | Lemma for 1arithufd 33608. 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 33605* | Lemma for 1arithufd 33608. 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 33606* | Lemma for 1arithufd 33608. 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 33607* | Lemma for 1arithufd 33608. 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 33608* | Existence of a factorization into irreducible elements in a unique factorization domain. Any nonzero, non-unit element 𝑋 of a UFD 𝑅 can be written as a product of primes 𝑓. As shown in 1arithidom 33597, 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 33609 | Lemma for dfufd2 33610. (Contributed by Thierry Arnoux, 6-Jun-2025.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ 𝑈 = (Unit‘𝑅) & ⊢ 𝑃 = (RPrime‘𝑅) & ⊢ 𝑀 = (mulGrp‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ IDomn) & ⊢ (𝜑 → 𝐼 ∈ (PrmIdeal‘𝑅)) & ⊢ (𝜑 → 𝐹 ∈ Word 𝑃) & ⊢ (𝜑 → (𝑀 Σg 𝐹) ∈ 𝐼) & ⊢ (𝜑 → (𝑀 Σg 𝐹) ≠ 0 ) ⇒ ⊢ (𝜑 → (𝐼 ∩ 𝑃) ≠ ∅) | ||
| Theorem | dfufd2 33610* | 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 𝑓))) | ||
| Theorem | zringidom 33611 | The ring of integers is an integral domain. (Contributed by Thierry Arnoux, 4-May-2025.) |
| ⊢ ℤring ∈ IDomn | ||
| Theorem | zringpid 33612 | The ring of integers is a principal ideal domain. (Contributed by Thierry Arnoux, 18-May-2025.) |
| ⊢ ℤring ∈ PID | ||
| Theorem | dfprm3 33613 | The (positive) prime elements of the integer ring are the prime numbers. (Contributed by Thierry Arnoux, 18-May-2025.) |
| ⊢ ℙ = (ℕ ∩ (RPrime‘ℤring)) | ||
| Theorem | zringfrac 33614* | 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)) | ||
| Theorem | assaassd 33615 | Left-associative property of an associative algebra, deduction version. (Contributed by Thierry Arnoux, 15-Feb-2026.) |
| ⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐵 = (Base‘𝐹) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ × = (.r‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ AssAlg) & ⊢ (𝜑 → 𝐴 ∈ 𝐵) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) ⇒ ⊢ (𝜑 → ((𝐴 · 𝑋) × 𝑌) = (𝐴 · (𝑋 × 𝑌))) | ||
| Theorem | assaassrd 33616 | Right-associative property of an associative algebra, deduction version. (Contributed by Thierry Arnoux, 15-Feb-2026.) |
| ⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐵 = (Base‘𝐹) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ × = (.r‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ AssAlg) & ⊢ (𝜑 → 𝐴 ∈ 𝐵) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) ⇒ ⊢ (𝜑 → (𝑋 × (𝐴 · 𝑌)) = (𝐴 · (𝑋 × 𝑌))) | ||
| Theorem | 0ringmon1p 33617 | There are no monic polynomials over a zero ring. (Contributed by Thierry Arnoux, 5-Feb-2025.) |
| ⊢ 𝑀 = (Monic1p‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → (♯‘𝐵) = 1) ⇒ ⊢ (𝜑 → 𝑀 = ∅) | ||
| Theorem | fply1 33618 | 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 33619 | In a division ring, the univariate polynomials form a vector space. (Contributed by Thierry Arnoux, 19-Feb-2025.) |
| ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ DivRing) ⇒ ⊢ (𝜑 → 𝑃 ∈ LVec) | ||
| Theorem | evls1fn 33620 | Functionality of the subring polynomial evaluation. (Contributed by Thierry Arnoux, 9-Feb-2025.) |
| ⊢ 𝑂 = (𝑅 evalSub1 𝑆) & ⊢ 𝑃 = (Poly1‘(𝑅 ↾s 𝑆)) & ⊢ 𝑈 = (Base‘𝑃) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝑆 ∈ (SubRing‘𝑅)) ⇒ ⊢ (𝜑 → 𝑂 Fn 𝑈) | ||
| Theorem | evls1dm 33621 | The domain of the subring polynomial evaluation function. (Contributed by Thierry Arnoux, 9-Feb-2025.) |
| ⊢ 𝑂 = (𝑅 evalSub1 𝑆) & ⊢ 𝑃 = (Poly1‘(𝑅 ↾s 𝑆)) & ⊢ 𝑈 = (Base‘𝑃) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝑆 ∈ (SubRing‘𝑅)) ⇒ ⊢ (𝜑 → dom 𝑂 = 𝑈) | ||
| Theorem | evls1fvf 33622 | 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 33623 | 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 33624* | 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 33625 | 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 33626 | 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 33627 | 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 33628 | The monic polynomials of a restricted polynomial algebra. (Contributed by Thierry Arnoux, 21-Jan-2025.) |
| ⊢ 𝑆 = (Poly1‘𝑅) & ⊢ 𝐻 = (𝑅 ↾s 𝑇) & ⊢ 𝑈 = (Poly1‘𝐻) & ⊢ 𝐵 = (Base‘𝑈) & ⊢ (𝜑 → 𝑇 ∈ (SubRing‘𝑅)) & ⊢ 𝑀 = (Monic1p‘𝑅) & ⊢ 𝑁 = (Monic1p‘𝐻) ⇒ ⊢ (𝜑 → 𝑁 = (𝐵 ∩ 𝑀)) | ||
| Theorem | ressply1invg 33629 | 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 33630 | 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 33631 | Closure of the univariate polynomial evaluation for scalars. (Contributed by Thierry Arnoux, 22-Jun-2025.) |
| ⊢ 𝑊 = (Poly1‘𝑈) & ⊢ 𝑈 = (𝑆 ↾s 𝑅) & ⊢ 𝐴 = (algSc‘𝑊) & ⊢ 𝐵 = (Base‘𝑊) & ⊢ (𝜑 → 𝑆 ∈ CRing) & ⊢ (𝜑 → 𝑅 ∈ (SubRing‘𝑆)) & ⊢ (𝜑 → 𝑋 ∈ 𝑅) ⇒ ⊢ (𝜑 → (𝐴‘𝑋) ∈ 𝐵) | ||
| Theorem | evls1subd 33632 | 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 33633 | 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 33634 | 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 33635 | In a field 𝐹, a polynomial 𝐶 is a unit iff it has degree 0. This corresponds to the nonzero scalars, see ply1asclunit 33634. (Contributed by Thierry Arnoux, 25-Apr-2025.) |
| ⊢ 𝑃 = (Poly1‘𝐹) & ⊢ 𝐴 = (algSc‘𝑃) & ⊢ 𝐵 = (Base‘𝐹) & ⊢ 0 = (0g‘𝐹) & ⊢ (𝜑 → 𝐹 ∈ Field) & ⊢ 𝐷 = (deg1‘𝐹) & ⊢ (𝜑 → 𝐶 ∈ (Base‘𝑃)) ⇒ ⊢ (𝜑 → (𝐶 ∈ (Unit‘𝑃) ↔ (𝐷‘𝐶) = 0)) | ||
| Theorem | evl1deg1 33636 | 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 33637 | 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 33638 | 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 33639 | 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 33640 | 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 33641 | 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 33642 | 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 33643* | 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 33644 | 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 33645 | 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 33646 | 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 33647* | 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 33648 | 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 33649* | 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 33650 | The coefficients of the zero univariate polynomial. (Contributed by Thierry Arnoux, 22-Jun-2025.) |
| ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝑍 = (0g‘𝑃) & ⊢ 0 = (0g‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) ⇒ ⊢ (𝜑 → ((coe1‘𝑍)‘𝑁) = 0 ) | ||
| Theorem | coe1vr1 33651* | 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 33652 | The degree of the variable polynomial is 1. (Contributed by Thierry Arnoux, 22-Jun-2025.) |
| ⊢ 𝐷 = (deg1‘𝑅) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝑋 = (var1‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ NzRing) ⇒ ⊢ (𝜑 → (𝐷‘𝑋) = 1) | ||
| Theorem | vr1nz 33653 | 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 33654 | 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 33655 | 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 33656 | 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 33657* | 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 33658* | A coefficient of the polynomial represented as a sum of scaled monomials is the coefficient of the corresponding scaled monomial. See gsummoncoe1fzo 33657. (Contributed by Thierry Arnoux, 15-Feb-2026.) |
| ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 𝑋 = (var1‘𝑅) & ⊢ ↑ = (.g‘(mulGrp‘𝑃)) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ 𝐾 = (Base‘𝑅) & ⊢ ∗ = ( ·𝑠 ‘𝑃) & ⊢ (𝜑 → 𝐷 ∈ ℕ0) & ⊢ (𝜑 → ∀𝑘 ∈ (0...𝐷)𝐴 ∈ 𝐾) & ⊢ (𝜑 → 𝐿 ∈ (0...𝐷)) & ⊢ (𝑘 = 𝐿 → 𝐴 = 𝐶) ⇒ ⊢ (𝜑 → ((coe1‘(𝑃 Σg (𝑘 ∈ (0...𝐷) ↦ (𝐴 ∗ (𝑘 ↑ 𝑋)))))‘𝐿) = 𝐶) | ||
| Theorem | ply1gsumz 33659* | 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 33660 | 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 33661 | The polynomial ideal generator is not a unit polynomial. (Contributed by Thierry Arnoux, 19-Mar-2025.) |
| ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐺 = (idlGen1p‘𝑅) & ⊢ 𝑈 = (Base‘𝑃) & ⊢ (𝜑 → 𝑅 ∈ DivRing) & ⊢ (𝜑 → 𝐼 ∈ (LIdeal‘𝑃)) & ⊢ (𝜑 → 𝐼 ≠ 𝑈) ⇒ ⊢ (𝜑 → ¬ (𝐺‘𝐼) ∈ (Unit‘𝑃)) | ||
| Theorem | ig1pmindeg 33662 | 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 | q1pdir 33663 | Distribution of univariate polynomial quotient over addition. (Contributed by Thierry Arnoux, 2-Apr-2025.) |
| ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝑈 = (Base‘𝑃) & ⊢ 𝑁 = (Unic1p‘𝑅) & ⊢ / = (quot1p‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝐴 ∈ 𝑈) & ⊢ (𝜑 → 𝐶 ∈ 𝑁) & ⊢ (𝜑 → 𝐵 ∈ 𝑈) & ⊢ + = (+g‘𝑃) ⇒ ⊢ (𝜑 → ((𝐴 + 𝐵) / 𝐶) = ((𝐴 / 𝐶) + (𝐵 / 𝐶))) | ||
| Theorem | q1pvsca 33664 | Scalar multiplication property of the polynomial division. (Contributed by Thierry Arnoux, 2-Apr-2025.) |
| ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝑈 = (Base‘𝑃) & ⊢ 𝑁 = (Unic1p‘𝑅) & ⊢ / = (quot1p‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝐴 ∈ 𝑈) & ⊢ (𝜑 → 𝐶 ∈ 𝑁) & ⊢ × = ( ·𝑠 ‘𝑃) & ⊢ 𝐾 = (Base‘𝑅) & ⊢ (𝜑 → 𝐵 ∈ 𝐾) ⇒ ⊢ (𝜑 → ((𝐵 × 𝐴) / 𝐶) = (𝐵 × (𝐴 / 𝐶))) | ||
| Theorem | r1pvsca 33665 | Scalar multiplication property of the polynomial remainder operation. (Contributed by Thierry Arnoux, 2-Apr-2025.) |
| ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝑈 = (Base‘𝑃) & ⊢ 𝑁 = (Unic1p‘𝑅) & ⊢ 𝐸 = (rem1p‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝐴 ∈ 𝑈) & ⊢ (𝜑 → 𝐷 ∈ 𝑁) & ⊢ × = ( ·𝑠 ‘𝑃) & ⊢ 𝐾 = (Base‘𝑅) & ⊢ (𝜑 → 𝐵 ∈ 𝐾) ⇒ ⊢ (𝜑 → ((𝐵 × 𝐴)𝐸𝐷) = (𝐵 × (𝐴𝐸𝐷))) | ||
| Theorem | r1p0 33666 | 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 33667 | The polynomial remainder operation is periodic. See modcyc 13865. (Contributed by Thierry Arnoux, 2-Apr-2025.) |
| ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝑈 = (Base‘𝑃) & ⊢ 𝑁 = (Unic1p‘𝑅) & ⊢ 𝐸 = (rem1p‘𝑅) & ⊢ + = (+g‘𝑃) & ⊢ · = (.r‘𝑃) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝐴 ∈ 𝑈) & ⊢ (𝜑 → 𝐵 ∈ 𝑁) & ⊢ (𝜑 → 𝐶 ∈ 𝑈) ⇒ ⊢ (𝜑 → ((𝐴 + (𝐶 · 𝐵))𝐸𝐵) = (𝐴𝐸𝐵)) | ||
| Theorem | r1padd1 33668 | Addition property of the polynomial remainder operation, similar to modadd1 13867. (Contributed by Thierry Arnoux, 2-Apr-2025.) |
| ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝑈 = (Base‘𝑃) & ⊢ 𝑁 = (Unic1p‘𝑅) & ⊢ 𝐸 = (rem1p‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝐴 ∈ 𝑈) & ⊢ (𝜑 → 𝐷 ∈ 𝑁) & ⊢ (𝜑 → (𝐴𝐸𝐷) = (𝐵𝐸𝐷)) & ⊢ + = (+g‘𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑈) & ⊢ (𝜑 → 𝐶 ∈ 𝑈) ⇒ ⊢ (𝜑 → ((𝐴 + 𝐶)𝐸𝐷) = ((𝐵 + 𝐶)𝐸𝐷)) | ||
| Theorem | r1pid2OLD 33669 | 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 33670* | 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 33671* | 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 | psrbasfsupp 33672 | 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 21913, 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 33673 | Extend class notation with the "variable extension" function. |
| class extendVars | ||
| Definition | df-extv 33674* | 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 33675* | 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 33676* | 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 33677* | 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 33678* | 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 33679* | 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 33680* | 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 33681* | 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 33682* | 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 33683* | 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 33684 | Polynomial evaluation for scalars. See evlsscaval 43000. (Contributed by Thierry Arnoux, 15-Feb-2026.) |
| ⊢ 𝑄 = (𝐼 eval 𝑅) & ⊢ 𝑊 = (𝐼 mPoly 𝑅) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝐴 = (algSc‘𝑊) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝐿:𝐼⟶𝐵) ⇒ ⊢ (𝜑 → ((𝑄‘(𝐴‘𝑋))‘𝐿) = 𝑋) | ||
| Theorem | evlvarval 33685 | Polynomial evaluation builder for a variable. (Contributed by Thierry Arnoux, 15-Feb-2026.) |
| ⊢ 𝑄 = (𝐼 eval 𝑆) & ⊢ 𝑃 = (𝐼 mPoly 𝑆) & ⊢ 𝐾 = (Base‘𝑆) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ ∙ = (.r‘𝑃) & ⊢ · = (.r‘𝑆) & ⊢ (𝜑 → 𝐼 ∈ 𝑍) & ⊢ (𝜑 → 𝑆 ∈ CRing) & ⊢ (𝜑 → 𝐴 ∈ (𝐾 ↑m 𝐼)) & ⊢ 𝑉 = (𝐼 mVar 𝑆) & ⊢ (𝜑 → 𝑋 ∈ 𝐼) ⇒ ⊢ (𝜑 → ((𝑉‘𝑋) ∈ 𝐵 ∧ ((𝑄‘(𝑉‘𝑋))‘𝐴) = (𝐴‘𝑋))) | ||
| Theorem | evlextv 33686 | 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 33687* | Lemma for mplvrpmga 33689 and others. (Contributed by Thierry Arnoux, 11-Jan-2026.) |
| ⊢ 𝑆 = (SymGrp‘𝐼) & ⊢ 𝑃 = (Base‘𝑆) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ (𝜑 → 𝑋 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ⇒ ⊢ (𝜑 → (𝑋 ∘ 𝐷) ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) | ||
| Theorem | mplvrpmfgalem 33688* | 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 33689* | 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 33690* | 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 33691* | 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 33692* | 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 33693* | 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 33694* | 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 33695* | 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 33696* | 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 33697* | 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 33698* | 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 (𝑥 ∈ 𝐴 ↦ ((𝐹‘𝑥)‘𝑖)))))) | ||
| Syntax | csply 33699 | Extend class notation with the symmetric polynomials. |
| class SymPoly | ||
| Syntax | cesply 33700 | Extend class notation with the elementary symmetric polynomials. |
| class eSymPoly | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |