HomeTheorem List (p. 336 of 497)
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. 336 of 497) | < 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-30845) |
Hilbert Space Explorer
(30846-32368) |
Users' Mathboxes
(32369-49617) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | isufd 33501* | The property of being a Unique Factorization Domain. (Contributed by Thierry Arnoux, 1-Jun-2024.) |
| ⊢ 𝐼 = (PrmIdeal‘𝑅) & ⊢ 𝑃 = (RPrime‘𝑅) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ (𝑅 ∈ UFD ↔ (𝑅 ∈ IDomn ∧ ∀𝑖 ∈ (𝐼 ∖ {{ 0 }})(𝑖 ∩ 𝑃) ≠ ∅)) | ||
| Theorem | ufdprmidl 33502* | 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 33503 | A nonzero unique factorization domain is an integral domain. (Contributed by Thierry Arnoux, 3-Jun-2025.) |
| ⊢ (𝜑 → 𝑅 ∈ UFD) ⇒ ⊢ (𝜑 → 𝑅 ∈ IDomn) | ||
| Theorem | pidufd 33504 | Every principal ideal domain is a unique factorization domain. (Contributed by Thierry Arnoux, 3-Jun-2025.) |
| ⊢ (𝜑 → 𝑅 ∈ PID) ⇒ ⊢ (𝜑 → 𝑅 ∈ UFD) | ||
| Theorem | 1arithufdlem1 33505* | Lemma for 1arithufd 33509. 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 33506* | Lemma for 1arithufd 33509. 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 33507* | Lemma for 1arithufd 33509. 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 33508* | Lemma for 1arithufd 33509. 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 33509* | 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 33498, 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 33510 | Lemma for dfufd2 33511. (Contributed by Thierry Arnoux, 6-Jun-2025.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ 𝑈 = (Unit‘𝑅) & ⊢ 𝑃 = (RPrime‘𝑅) & ⊢ 𝑀 = (mulGrp‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ IDomn) & ⊢ (𝜑 → 𝐼 ∈ (PrmIdeal‘𝑅)) & ⊢ (𝜑 → 𝐹 ∈ Word 𝑃) & ⊢ (𝜑 → (𝑀 Σg 𝐹) ∈ 𝐼) & ⊢ (𝜑 → (𝑀 Σg 𝐹) ≠ 0 ) ⇒ ⊢ (𝜑 → (𝐼 ∩ 𝑃) ≠ ∅) | ||
| Theorem | dfufd2 33511* | 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 33512 | The ring of integers is an integral domain. (Contributed by Thierry Arnoux, 4-May-2025.) |
| ⊢ ℤring ∈ IDomn | ||
| Theorem | zringpid 33513 | The ring of integers is a principal ideal domain. (Contributed by Thierry Arnoux, 18-May-2025.) |
| ⊢ ℤring ∈ PID | ||
| Theorem | dfprm3 33514 | The (positive) prime elements of the integer ring are the prime numbers. (Contributed by Thierry Arnoux, 18-May-2025.) |
| ⊢ ℙ = (ℕ ∩ (RPrime‘ℤring)) | ||
| Theorem | zringfrac 33515* | 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 | 0ringmon1p 33516 | There are no monic polynomials over a zero ring. (Contributed by Thierry Arnoux, 5-Feb-2025.) |
| ⊢ 𝑀 = (Monic1p‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → (♯‘𝐵) = 1) ⇒ ⊢ (𝜑 → 𝑀 = ∅) | ||
| Theorem | fply1 33517 | 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 33518 | In a division ring, the univariate polynomials form a vector space. (Contributed by Thierry Arnoux, 19-Feb-2025.) |
| ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ DivRing) ⇒ ⊢ (𝜑 → 𝑃 ∈ LVec) | ||
| Theorem | evls1fn 33519 | Functionality of the subring polynomial evaluation. (Contributed by Thierry Arnoux, 9-Feb-2025.) |
| ⊢ 𝑂 = (𝑅 evalSub1 𝑆) & ⊢ 𝑃 = (Poly1‘(𝑅 ↾s 𝑆)) & ⊢ 𝑈 = (Base‘𝑃) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝑆 ∈ (SubRing‘𝑅)) ⇒ ⊢ (𝜑 → 𝑂 Fn 𝑈) | ||
| Theorem | evls1dm 33520 | The domain of the subring polynomial evaluation function. (Contributed by Thierry Arnoux, 9-Feb-2025.) |
| ⊢ 𝑂 = (𝑅 evalSub1 𝑆) & ⊢ 𝑃 = (Poly1‘(𝑅 ↾s 𝑆)) & ⊢ 𝑈 = (Base‘𝑃) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝑆 ∈ (SubRing‘𝑅)) ⇒ ⊢ (𝜑 → dom 𝑂 = 𝑈) | ||
| Theorem | evls1fvf 33521 | 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 33522 | 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 33523* | 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 33524 | 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 33525 | 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 33526 | 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 33527 | The monic polynomials of a restricted polynomial algebra. (Contributed by Thierry Arnoux, 21-Jan-2025.) |
| ⊢ 𝑆 = (Poly1‘𝑅) & ⊢ 𝐻 = (𝑅 ↾s 𝑇) & ⊢ 𝑈 = (Poly1‘𝐻) & ⊢ 𝐵 = (Base‘𝑈) & ⊢ (𝜑 → 𝑇 ∈ (SubRing‘𝑅)) & ⊢ 𝑀 = (Monic1p‘𝑅) & ⊢ 𝑁 = (Monic1p‘𝐻) ⇒ ⊢ (𝜑 → 𝑁 = (𝐵 ∩ 𝑀)) | ||
| Theorem | ressply1invg 33528 | 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 33529 | 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 33530 | Closure of the univariate polynomial evaluation for scalars. (Contributed by Thierry Arnoux, 22-Jun-2025.) |
| ⊢ 𝑊 = (Poly1‘𝑈) & ⊢ 𝑈 = (𝑆 ↾s 𝑅) & ⊢ 𝐴 = (algSc‘𝑊) & ⊢ 𝐵 = (Base‘𝑊) & ⊢ (𝜑 → 𝑆 ∈ CRing) & ⊢ (𝜑 → 𝑅 ∈ (SubRing‘𝑆)) & ⊢ (𝜑 → 𝑋 ∈ 𝑅) ⇒ ⊢ (𝜑 → (𝐴‘𝑋) ∈ 𝐵) | ||
| Theorem | evls1subd 33531 | 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 33532 | A polynomial with nonpositive degree is the zero polynomial iff its constant term is zero. Biconditional version of deg1scl 26068. (Contributed by Thierry Arnoux, 22-Mar-2025.) |
| ⊢ 𝐷 = (deg1‘𝑅) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 𝑂 = (0g‘𝑃) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝐹 ∈ 𝐵) & ⊢ (𝜑 → (𝐷‘𝐹) ≤ 0) ⇒ ⊢ (𝜑 → (𝐹 = 𝑂 ↔ ((coe1‘𝐹)‘0) = 0 )) | ||
| Theorem | ply1asclunit 33533 | 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 33534 | In a field 𝐹, a polynomial 𝐶 is a unit iff it has degree 0. This corresponds to the nonzero scalars, see ply1asclunit 33533. (Contributed by Thierry Arnoux, 25-Apr-2025.) |
| ⊢ 𝑃 = (Poly1‘𝐹) & ⊢ 𝐴 = (algSc‘𝑃) & ⊢ 𝐵 = (Base‘𝐹) & ⊢ 0 = (0g‘𝐹) & ⊢ (𝜑 → 𝐹 ∈ Field) & ⊢ 𝐷 = (deg1‘𝐹) & ⊢ (𝜑 → 𝐶 ∈ (Base‘𝑃)) ⇒ ⊢ (𝜑 → (𝐶 ∈ (Unit‘𝑃) ↔ (𝐷‘𝐶) = 0)) | ||
| Theorem | evl1deg1 33535 | 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 33536 | 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 33537 | 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 | ply1dg1rt 33538 | 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 33539 | 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 33540 | 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 | ply1dg3rt0irred 33541 | 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 33542 | 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 33543 | 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 33544* | 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 33545 | Two monomials are equal iff their powers are equal. (Contributed by Thierry Arnoux, 20-Feb-2025.) |
| ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝑋 = (var1‘𝑅) & ⊢ ↑ = (.g‘(mulGrp‘𝑃)) & ⊢ (𝜑 → 𝑅 ∈ NzRing) & ⊢ (𝜑 → 𝑀 ∈ ℕ0) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) ⇒ ⊢ (𝜑 → ((𝑀 ↑ 𝑋) = (𝑁 ↑ 𝑋) ↔ 𝑀 = 𝑁)) | ||
| Theorem | coe1zfv 33546 | The coefficients of the zero univariate polynomial. (Contributed by Thierry Arnoux, 22-Jun-2025.) |
| ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝑍 = (0g‘𝑃) & ⊢ 0 = (0g‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) ⇒ ⊢ (𝜑 → ((coe1‘𝑍)‘𝑁) = 0 ) | ||
| Theorem | coe1vr1 33547* | 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 33548 | The degree of the variable polynomial is 1. (Contributed by Thierry Arnoux, 22-Jun-2025.) |
| ⊢ 𝐷 = (deg1‘𝑅) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝑋 = (var1‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ NzRing) ⇒ ⊢ (𝜑 → (𝐷‘𝑋) = 1) | ||
| Theorem | vr1nz 33549 | 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 33550 | 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 33551 | 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 33552 | 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 33553* | 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 | ply1gsumz 33554* | 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 33555 | If both factors have degree bounded by 𝐿, then the sum of the polynomials also has degree bounded by 𝐿. See also deg1addle 26056. (Contributed by Thierry Arnoux, 2-Apr-2025.) |
| ⊢ 𝑌 = (Poly1‘𝑅) & ⊢ 𝐷 = (deg1‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ 𝐵 = (Base‘𝑌) & ⊢ + = (+g‘𝑌) & ⊢ (𝜑 → 𝐹 ∈ 𝐵) & ⊢ (𝜑 → 𝐺 ∈ 𝐵) & ⊢ (𝜑 → 𝐿 ∈ ℝ*) & ⊢ (𝜑 → (𝐷‘𝐹) < 𝐿) & ⊢ (𝜑 → (𝐷‘𝐺) < 𝐿) ⇒ ⊢ (𝜑 → (𝐷‘(𝐹 + 𝐺)) < 𝐿) | ||
| Theorem | ig1pnunit 33556 | The polynomial ideal generator is not a unit polynomial. (Contributed by Thierry Arnoux, 19-Mar-2025.) |
| ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐺 = (idlGen1p‘𝑅) & ⊢ 𝑈 = (Base‘𝑃) & ⊢ (𝜑 → 𝑅 ∈ DivRing) & ⊢ (𝜑 → 𝐼 ∈ (LIdeal‘𝑃)) & ⊢ (𝜑 → 𝐼 ≠ 𝑈) ⇒ ⊢ (𝜑 → ¬ (𝐺‘𝐼) ∈ (Unit‘𝑃)) | ||
| Theorem | ig1pmindeg 33557 | 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 33558 | Distribution of univariate polynomial quotient over addition. (Contributed by Thierry Arnoux, 2-Apr-2025.) |
| ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝑈 = (Base‘𝑃) & ⊢ 𝑁 = (Unic1p‘𝑅) & ⊢ / = (quot1p‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝐴 ∈ 𝑈) & ⊢ (𝜑 → 𝐶 ∈ 𝑁) & ⊢ (𝜑 → 𝐵 ∈ 𝑈) & ⊢ + = (+g‘𝑃) ⇒ ⊢ (𝜑 → ((𝐴 + 𝐵) / 𝐶) = ((𝐴 / 𝐶) + (𝐵 / 𝐶))) | ||
| Theorem | q1pvsca 33559 | Scalar multiplication property of the polynomial division. (Contributed by Thierry Arnoux, 2-Apr-2025.) |
| ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝑈 = (Base‘𝑃) & ⊢ 𝑁 = (Unic1p‘𝑅) & ⊢ / = (quot1p‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝐴 ∈ 𝑈) & ⊢ (𝜑 → 𝐶 ∈ 𝑁) & ⊢ × = ( ·𝑠 ‘𝑃) & ⊢ 𝐾 = (Base‘𝑅) & ⊢ (𝜑 → 𝐵 ∈ 𝐾) ⇒ ⊢ (𝜑 → ((𝐵 × 𝐴) / 𝐶) = (𝐵 × (𝐴 / 𝐶))) | ||
| Theorem | r1pvsca 33560 | Scalar multiplication property of the polynomial remainder operation. (Contributed by Thierry Arnoux, 2-Apr-2025.) |
| ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝑈 = (Base‘𝑃) & ⊢ 𝑁 = (Unic1p‘𝑅) & ⊢ 𝐸 = (rem1p‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝐴 ∈ 𝑈) & ⊢ (𝜑 → 𝐷 ∈ 𝑁) & ⊢ × = ( ·𝑠 ‘𝑃) & ⊢ 𝐾 = (Base‘𝑅) & ⊢ (𝜑 → 𝐵 ∈ 𝐾) ⇒ ⊢ (𝜑 → ((𝐵 × 𝐴)𝐸𝐷) = (𝐵 × (𝐴𝐸𝐷))) | ||
| Theorem | r1p0 33561 | 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 33562 | The polynomial remainder operation is periodic. See modcyc 13921. (Contributed by Thierry Arnoux, 2-Apr-2025.) |
| ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝑈 = (Base‘𝑃) & ⊢ 𝑁 = (Unic1p‘𝑅) & ⊢ 𝐸 = (rem1p‘𝑅) & ⊢ + = (+g‘𝑃) & ⊢ · = (.r‘𝑃) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝐴 ∈ 𝑈) & ⊢ (𝜑 → 𝐵 ∈ 𝑁) & ⊢ (𝜑 → 𝐶 ∈ 𝑈) ⇒ ⊢ (𝜑 → ((𝐴 + (𝐶 · 𝐵))𝐸𝐵) = (𝐴𝐸𝐵)) | ||
| Theorem | r1padd1 33563 | Addition property of the polynomial remainder operation, similar to modadd1 13923. (Contributed by Thierry Arnoux, 2-Apr-2025.) |
| ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝑈 = (Base‘𝑃) & ⊢ 𝑁 = (Unic1p‘𝑅) & ⊢ 𝐸 = (rem1p‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝐴 ∈ 𝑈) & ⊢ (𝜑 → 𝐷 ∈ 𝑁) & ⊢ (𝜑 → (𝐴𝐸𝐷) = (𝐵𝐸𝐷)) & ⊢ + = (+g‘𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑈) & ⊢ (𝜑 → 𝐶 ∈ 𝑈) ⇒ ⊢ (𝜑 → ((𝐴 + 𝐶)𝐸𝐷) = ((𝐵 + 𝐶)𝐸𝐷)) | ||
| Theorem | r1pid2OLD 33564 | Obsolete version of r1pid2 26117 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 33565* | 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 33566* | 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 | sra1r 33567 | The unity element of a subring algebra. (Contributed by Thierry Arnoux, 24-Jul-2023.) |
| ⊢ (𝜑 → 𝐴 = ((subringAlg ‘𝑊)‘𝑆)) & ⊢ (𝜑 → 1 = (1r‘𝑊)) & ⊢ (𝜑 → 𝑆 ⊆ (Base‘𝑊)) ⇒ ⊢ (𝜑 → 1 = (1r‘𝐴)) | ||
| Theorem | sradrng 33568 | Condition for a subring algebra to be a division ring. (Contributed by Thierry Arnoux, 29-Jul-2023.) |
| ⊢ 𝐴 = ((subringAlg ‘𝑅)‘𝑉) & ⊢ 𝐵 = (Base‘𝑅) ⇒ ⊢ ((𝑅 ∈ DivRing ∧ 𝑉 ⊆ 𝐵) → 𝐴 ∈ DivRing) | ||
| Theorem | sraidom 33569 | Condition for a subring algebra to be an integral domain. (Contributed by Thierry Arnoux, 13-Oct-2025.) |
| ⊢ 𝐴 = ((subringAlg ‘𝑅)‘𝑉) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ IDomn) & ⊢ (𝜑 → 𝑉 ⊆ 𝐵) ⇒ ⊢ (𝜑 → 𝐴 ∈ IDomn) | ||
| Theorem | srasubrg 33570 | A subring of the original structure is also a subring of the constructed subring algebra. (Contributed by Thierry Arnoux, 24-Jul-2023.) |
| ⊢ (𝜑 → 𝐴 = ((subringAlg ‘𝑊)‘𝑆)) & ⊢ (𝜑 → 𝑈 ∈ (SubRing‘𝑊)) & ⊢ (𝜑 → 𝑆 ⊆ (Base‘𝑊)) ⇒ ⊢ (𝜑 → 𝑈 ∈ (SubRing‘𝐴)) | ||
| Theorem | sralvec 33571 | Given a sub division ring 𝐹 of a division ring 𝐸, 𝐸 may be considered as a vector space over 𝐹, which becomes the field of scalars. (Contributed by Thierry Arnoux, 24-May-2023.) |
| ⊢ 𝐴 = ((subringAlg ‘𝐸)‘𝑈) & ⊢ 𝐹 = (𝐸 ↾s 𝑈) ⇒ ⊢ ((𝐸 ∈ DivRing ∧ 𝐹 ∈ DivRing ∧ 𝑈 ∈ (SubRing‘𝐸)) → 𝐴 ∈ LVec) | ||
| Theorem | srafldlvec 33572 | Given a subfield 𝐹 of a field 𝐸, 𝐸 may be considered as a vector space over 𝐹, which becomes the field of scalars. (Contributed by Thierry Arnoux, 24-May-2023.) |
| ⊢ 𝐴 = ((subringAlg ‘𝐸)‘𝑈) & ⊢ 𝐹 = (𝐸 ↾s 𝑈) ⇒ ⊢ ((𝐸 ∈ Field ∧ 𝐹 ∈ Field ∧ 𝑈 ∈ (SubRing‘𝐸)) → 𝐴 ∈ LVec) | ||
| Theorem | resssra 33573 | The subring algebra of a restricted structure is the restriction of the subring algebra. (Contributed by Thierry Arnoux, 2-Apr-2025.) |
| ⊢ 𝐴 = (Base‘𝑅) & ⊢ 𝑆 = (𝑅 ↾s 𝐵) & ⊢ (𝜑 → 𝐵 ⊆ 𝐴) & ⊢ (𝜑 → 𝐶 ⊆ 𝐵) & ⊢ (𝜑 → 𝑅 ∈ 𝑉) ⇒ ⊢ (𝜑 → ((subringAlg ‘𝑆)‘𝐶) = (((subringAlg ‘𝑅)‘𝐶) ↾s 𝐵)) | ||
| Theorem | lsssra 33574 | A subring is a subspace of the subring algebra. (Contributed by Thierry Arnoux, 2-Apr-2025.) |
| ⊢ 𝑊 = ((subringAlg ‘𝑅)‘𝐶) & ⊢ 𝐴 = (Base‘𝑅) & ⊢ 𝑆 = (𝑅 ↾s 𝐵) & ⊢ (𝜑 → 𝐵 ∈ (SubRing‘𝑅)) & ⊢ (𝜑 → 𝐶 ∈ (SubRing‘𝑆)) ⇒ ⊢ (𝜑 → 𝐵 ∈ (LSubSp‘𝑊)) | ||
| Theorem | drgext0g 33575 | The additive neutral element of a division ring extension. (Contributed by Thierry Arnoux, 17-Jul-2023.) |
| ⊢ 𝐵 = ((subringAlg ‘𝐸)‘𝑈) & ⊢ (𝜑 → 𝐸 ∈ DivRing) & ⊢ (𝜑 → 𝑈 ∈ (SubRing‘𝐸)) ⇒ ⊢ (𝜑 → (0g‘𝐸) = (0g‘𝐵)) | ||
| Theorem | drgextvsca 33576 | The scalar multiplication operation of a division ring extension. (Contributed by Thierry Arnoux, 17-Jul-2023.) |
| ⊢ 𝐵 = ((subringAlg ‘𝐸)‘𝑈) & ⊢ (𝜑 → 𝐸 ∈ DivRing) & ⊢ (𝜑 → 𝑈 ∈ (SubRing‘𝐸)) ⇒ ⊢ (𝜑 → (.r‘𝐸) = ( ·𝑠 ‘𝐵)) | ||
| Theorem | drgext0gsca 33577 | The additive neutral element of the scalar field of a division ring extension. (Contributed by Thierry Arnoux, 17-Jul-2023.) |
| ⊢ 𝐵 = ((subringAlg ‘𝐸)‘𝑈) & ⊢ (𝜑 → 𝐸 ∈ DivRing) & ⊢ (𝜑 → 𝑈 ∈ (SubRing‘𝐸)) ⇒ ⊢ (𝜑 → (0g‘𝐵) = (0g‘(Scalar‘𝐵))) | ||
| Theorem | drgextsubrg 33578 | The scalar field is a subring of a division ring extension. (Contributed by Thierry Arnoux, 17-Jul-2023.) |
| ⊢ 𝐵 = ((subringAlg ‘𝐸)‘𝑈) & ⊢ (𝜑 → 𝐸 ∈ DivRing) & ⊢ (𝜑 → 𝑈 ∈ (SubRing‘𝐸)) & ⊢ 𝐹 = (𝐸 ↾s 𝑈) & ⊢ (𝜑 → 𝐹 ∈ DivRing) ⇒ ⊢ (𝜑 → 𝑈 ∈ (SubRing‘𝐵)) | ||
| Theorem | drgextlsp 33579 | The scalar field is a subspace of a subring algebra. (Contributed by Thierry Arnoux, 17-Jul-2023.) |
| ⊢ 𝐵 = ((subringAlg ‘𝐸)‘𝑈) & ⊢ (𝜑 → 𝐸 ∈ DivRing) & ⊢ (𝜑 → 𝑈 ∈ (SubRing‘𝐸)) & ⊢ 𝐹 = (𝐸 ↾s 𝑈) & ⊢ (𝜑 → 𝐹 ∈ DivRing) ⇒ ⊢ (𝜑 → 𝑈 ∈ (LSubSp‘𝐵)) | ||
| Theorem | drgextgsum 33580* | Group sum in a division ring extension. (Contributed by Thierry Arnoux, 17-Jul-2023.) |
| ⊢ 𝐵 = ((subringAlg ‘𝐸)‘𝑈) & ⊢ (𝜑 → 𝐸 ∈ DivRing) & ⊢ (𝜑 → 𝑈 ∈ (SubRing‘𝐸)) & ⊢ 𝐹 = (𝐸 ↾s 𝑈) & ⊢ (𝜑 → 𝐹 ∈ DivRing) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) ⇒ ⊢ (𝜑 → (𝐸 Σg (𝑖 ∈ 𝑋 ↦ 𝑌)) = (𝐵 Σg (𝑖 ∈ 𝑋 ↦ 𝑌))) | ||
| Theorem | lvecdimfi 33581 | Finite version of lvecdim 21116 which does not require the axiom of choice. The axiom of choice is used in acsmapd 18562, which is required in the infinite case. Suggested by Gérard Lang. (Contributed by Thierry Arnoux, 24-May-2023.) |
| ⊢ 𝐽 = (LBasis‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝑆 ∈ 𝐽) & ⊢ (𝜑 → 𝑇 ∈ 𝐽) & ⊢ (𝜑 → 𝑆 ∈ Fin) ⇒ ⊢ (𝜑 → 𝑆 ≈ 𝑇) | ||
| Theorem | exsslsb 33582* | Any finite generating set 𝑆 of a vector space 𝑊 contains a basis. (Contributed by Thierry Arnoux, 13-Oct-2025.) |
| ⊢ 𝐵 = (Base‘𝑊) & ⊢ 𝐽 = (LBasis‘𝑊) & ⊢ 𝐾 = (LSpan‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝑆 ∈ Fin) & ⊢ (𝜑 → 𝑆 ⊆ 𝐵) & ⊢ (𝜑 → (𝐾‘𝑆) = 𝐵) ⇒ ⊢ (𝜑 → ∃𝑠 ∈ 𝐽 𝑠 ⊆ 𝑆) | ||
| Theorem | lbslelsp 33583 | The size of a basis 𝑋 of a vector space 𝑊 is less than the size of a generating set 𝑌. (Contributed by Thierry Arnoux, 13-Oct-2025.) |
| ⊢ 𝐵 = (Base‘𝑊) & ⊢ 𝐽 = (LBasis‘𝑊) & ⊢ 𝐾 = (LSpan‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝑋 ∈ 𝐽) & ⊢ (𝜑 → 𝑌 ⊆ 𝐵) & ⊢ (𝜑 → (𝐾‘𝑌) = 𝐵) ⇒ ⊢ (𝜑 → (♯‘𝑋) ≤ (♯‘𝑌)) | ||
| Syntax | cldim 33584 | Extend class notation with the dimension of a vector space. |
| class dim | ||
| Definition | df-dim 33585 | Define the dimension of a vector space as the cardinality of its bases. Note that by lvecdim 21116, all bases are equinumerous. (Contributed by Thierry Arnoux, 6-May-2023.) |
| ⊢ dim = (𝑓 ∈ V ↦ ∪ (♯ “ (LBasis‘𝑓))) | ||
| Theorem | dimval 33586 | The dimension of a vector space 𝐹 is the cardinality of one of its bases. (Contributed by Thierry Arnoux, 6-May-2023.) |
| ⊢ 𝐽 = (LBasis‘𝐹) ⇒ ⊢ ((𝐹 ∈ LVec ∧ 𝑆 ∈ 𝐽) → (dim‘𝐹) = (♯‘𝑆)) | ||
| Theorem | dimvalfi 33587 | The dimension of a vector space 𝐹 is the cardinality of one of its bases. This version of dimval 33586 does not depend on the axiom of choice, but it is limited to the case where the base 𝑆 is finite. (Contributed by Thierry Arnoux, 24-May-2023.) |
| ⊢ 𝐽 = (LBasis‘𝐹) ⇒ ⊢ ((𝐹 ∈ LVec ∧ 𝑆 ∈ 𝐽 ∧ 𝑆 ∈ Fin) → (dim‘𝐹) = (♯‘𝑆)) | ||
| Theorem | dimcl 33588 | Closure of the vector space dimension. (Contributed by Thierry Arnoux, 18-May-2023.) |
| ⊢ (𝑉 ∈ LVec → (dim‘𝑉) ∈ ℕ0*) | ||
| Theorem | lmimdim 33589 | Module isomorphisms preserve vector space dimensions. (Contributed by Thierry Arnoux, 25-Feb-2025.) |
| ⊢ (𝜑 → 𝐹 ∈ (𝑆 LMIso 𝑇)) & ⊢ (𝜑 → 𝑆 ∈ LVec) ⇒ ⊢ (𝜑 → (dim‘𝑆) = (dim‘𝑇)) | ||
| Theorem | lmicdim 33590 | Module isomorphisms preserve vector space dimensions. (Contributed by Thierry Arnoux, 25-Mar-2025.) |
| ⊢ (𝜑 → 𝑆 ≃𝑚 𝑇) & ⊢ (𝜑 → 𝑆 ∈ LVec) ⇒ ⊢ (𝜑 → (dim‘𝑆) = (dim‘𝑇)) | ||
| Theorem | lvecdim0i 33591 | A vector space of dimension zero is reduced to its identity element. (Contributed by Thierry Arnoux, 31-Jul-2023.) |
| ⊢ 0 = (0g‘𝑉) ⇒ ⊢ ((𝑉 ∈ LVec ∧ (dim‘𝑉) = 0) → (Base‘𝑉) = { 0 }) | ||
| Theorem | lvecdim0 33592 | A vector space of dimension zero is reduced to its identity element, biconditional version. (Contributed by Thierry Arnoux, 31-Jul-2023.) |
| ⊢ 0 = (0g‘𝑉) ⇒ ⊢ (𝑉 ∈ LVec → ((dim‘𝑉) = 0 ↔ (Base‘𝑉) = { 0 })) | ||
| Theorem | lssdimle 33593 | The dimension of a linear subspace is less than or equal to the dimension of the parent vector space. This is corollary 5.4 of [Lang] p. 141. (Contributed by Thierry Arnoux, 20-May-2023.) |
| ⊢ 𝑋 = (𝑊 ↾s 𝑈) ⇒ ⊢ ((𝑊 ∈ LVec ∧ 𝑈 ∈ (LSubSp‘𝑊)) → (dim‘𝑋) ≤ (dim‘𝑊)) | ||
| Theorem | dimpropd 33594* | If two structures have the same components (properties), they have the same dimension. (Contributed by Thierry Arnoux, 18-May-2023.) |
| ⊢ (𝜑 → 𝐵 = (Base‘𝐾)) & ⊢ (𝜑 → 𝐵 = (Base‘𝐿)) & ⊢ (𝜑 → 𝐵 ⊆ 𝑊) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊)) → (𝑥(+g‘𝐾)𝑦) = (𝑥(+g‘𝐿)𝑦)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝐵)) → (𝑥( ·𝑠 ‘𝐾)𝑦) ∈ 𝑊) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝐵)) → (𝑥( ·𝑠 ‘𝐾)𝑦) = (𝑥( ·𝑠 ‘𝐿)𝑦)) & ⊢ 𝐹 = (Scalar‘𝐾) & ⊢ 𝐺 = (Scalar‘𝐿) & ⊢ (𝜑 → 𝑃 = (Base‘𝐹)) & ⊢ (𝜑 → 𝑃 = (Base‘𝐺)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑃)) → (𝑥(+g‘𝐹)𝑦) = (𝑥(+g‘𝐺)𝑦)) & ⊢ (𝜑 → 𝐾 ∈ LVec) & ⊢ (𝜑 → 𝐿 ∈ LVec) ⇒ ⊢ (𝜑 → (dim‘𝐾) = (dim‘𝐿)) | ||
| Theorem | rlmdim 33595 | The left vector space induced by a ring over itself has dimension 1. (Contributed by Thierry Arnoux, 5-Aug-2023.) Generalize to division rings. (Revised by SN, 22-Mar-2025.) |
| ⊢ 𝑉 = (ringLMod‘𝐹) ⇒ ⊢ (𝐹 ∈ DivRing → (dim‘𝑉) = 1) | ||
| Theorem | rgmoddimOLD 33596 | Obsolete version of rlmdim 33595 as of 21-Mar-2025. (Contributed by Thierry Arnoux, 5-Aug-2023.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ 𝑉 = (ringLMod‘𝐹) ⇒ ⊢ (𝐹 ∈ Field → (dim‘𝑉) = 1) | ||
| Theorem | frlmdim 33597 | Dimension of a free left module. (Contributed by Thierry Arnoux, 20-May-2023.) |
| ⊢ 𝐹 = (𝑅 freeLMod 𝐼) ⇒ ⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑉) → (dim‘𝐹) = (♯‘𝐼)) | ||
| Theorem | tnglvec 33598 | Augmenting a structure with a norm conserves left vector spaces. (Contributed by Thierry Arnoux, 20-May-2023.) |
| ⊢ 𝑇 = (𝐺 toNrmGrp 𝑁) ⇒ ⊢ (𝑁 ∈ 𝑉 → (𝐺 ∈ LVec ↔ 𝑇 ∈ LVec)) | ||
| Theorem | tngdim 33599 | Dimension of a left vector space augmented with a norm. (Contributed by Thierry Arnoux, 20-May-2023.) |
| ⊢ 𝑇 = (𝐺 toNrmGrp 𝑁) ⇒ ⊢ ((𝐺 ∈ LVec ∧ 𝑁 ∈ 𝑉) → (dim‘𝐺) = (dim‘𝑇)) | ||
| Theorem | rrxdim 33600 | Dimension of the generalized Euclidean space. (Contributed by Thierry Arnoux, 20-May-2023.) |
| ⊢ 𝐻 = (ℝ^‘𝐼) ⇒ ⊢ (𝐼 ∈ 𝑉 → (dim‘𝐻) = (♯‘𝐼)) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |