HomeTheorem List (p. 336 of 499)
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 499) | < 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-30888) |
Hilbert Space Explorer
(30889-32411) |
Users' Mathboxes
(32412-49816) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | 1arithufdlem3 33501* | Lemma for 1arithufd 33503. 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 33502* | Lemma for 1arithufd 33503. 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 33503* | 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 33492, 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 33504 | Lemma for dfufd2 33505. (Contributed by Thierry Arnoux, 6-Jun-2025.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ 𝑈 = (Unit‘𝑅) & ⊢ 𝑃 = (RPrime‘𝑅) & ⊢ 𝑀 = (mulGrp‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ IDomn) & ⊢ (𝜑 → 𝐼 ∈ (PrmIdeal‘𝑅)) & ⊢ (𝜑 → 𝐹 ∈ Word 𝑃) & ⊢ (𝜑 → (𝑀 Σg 𝐹) ∈ 𝐼) & ⊢ (𝜑 → (𝑀 Σg 𝐹) ≠ 0 ) ⇒ ⊢ (𝜑 → (𝐼 ∩ 𝑃) ≠ ∅) | ||
| Theorem | dfufd2 33505* | 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 33506 | The ring of integers is an integral domain. (Contributed by Thierry Arnoux, 4-May-2025.) |
| ⊢ ℤring ∈ IDomn | ||
| Theorem | zringpid 33507 | The ring of integers is a principal ideal domain. (Contributed by Thierry Arnoux, 18-May-2025.) |
| ⊢ ℤring ∈ PID | ||
| Theorem | dfprm3 33508 | The (positive) prime elements of the integer ring are the prime numbers. (Contributed by Thierry Arnoux, 18-May-2025.) |
| ⊢ ℙ = (ℕ ∩ (RPrime‘ℤring)) | ||
| Theorem | zringfrac 33509* | 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 33510 | There are no monic polynomials over a zero ring. (Contributed by Thierry Arnoux, 5-Feb-2025.) |
| ⊢ 𝑀 = (Monic1p‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → (♯‘𝐵) = 1) ⇒ ⊢ (𝜑 → 𝑀 = ∅) | ||
| Theorem | fply1 33511 | 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 33512 | In a division ring, the univariate polynomials form a vector space. (Contributed by Thierry Arnoux, 19-Feb-2025.) |
| ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ DivRing) ⇒ ⊢ (𝜑 → 𝑃 ∈ LVec) | ||
| Theorem | evls1fn 33513 | Functionality of the subring polynomial evaluation. (Contributed by Thierry Arnoux, 9-Feb-2025.) |
| ⊢ 𝑂 = (𝑅 evalSub1 𝑆) & ⊢ 𝑃 = (Poly1‘(𝑅 ↾s 𝑆)) & ⊢ 𝑈 = (Base‘𝑃) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝑆 ∈ (SubRing‘𝑅)) ⇒ ⊢ (𝜑 → 𝑂 Fn 𝑈) | ||
| Theorem | evls1dm 33514 | The domain of the subring polynomial evaluation function. (Contributed by Thierry Arnoux, 9-Feb-2025.) |
| ⊢ 𝑂 = (𝑅 evalSub1 𝑆) & ⊢ 𝑃 = (Poly1‘(𝑅 ↾s 𝑆)) & ⊢ 𝑈 = (Base‘𝑃) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝑆 ∈ (SubRing‘𝑅)) ⇒ ⊢ (𝜑 → dom 𝑂 = 𝑈) | ||
| Theorem | evls1fvf 33515 | 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 33516 | 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 33517* | 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 33518 | 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 33519 | 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 33520 | 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 33521 | The monic polynomials of a restricted polynomial algebra. (Contributed by Thierry Arnoux, 21-Jan-2025.) |
| ⊢ 𝑆 = (Poly1‘𝑅) & ⊢ 𝐻 = (𝑅 ↾s 𝑇) & ⊢ 𝑈 = (Poly1‘𝐻) & ⊢ 𝐵 = (Base‘𝑈) & ⊢ (𝜑 → 𝑇 ∈ (SubRing‘𝑅)) & ⊢ 𝑀 = (Monic1p‘𝑅) & ⊢ 𝑁 = (Monic1p‘𝐻) ⇒ ⊢ (𝜑 → 𝑁 = (𝐵 ∩ 𝑀)) | ||
| Theorem | ressply1invg 33522 | 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 33523 | 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 33524 | Closure of the univariate polynomial evaluation for scalars. (Contributed by Thierry Arnoux, 22-Jun-2025.) |
| ⊢ 𝑊 = (Poly1‘𝑈) & ⊢ 𝑈 = (𝑆 ↾s 𝑅) & ⊢ 𝐴 = (algSc‘𝑊) & ⊢ 𝐵 = (Base‘𝑊) & ⊢ (𝜑 → 𝑆 ∈ CRing) & ⊢ (𝜑 → 𝑅 ∈ (SubRing‘𝑆)) & ⊢ (𝜑 → 𝑋 ∈ 𝑅) ⇒ ⊢ (𝜑 → (𝐴‘𝑋) ∈ 𝐵) | ||
| Theorem | evls1subd 33525 | 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 33526 | A polynomial with nonpositive degree is the zero polynomial iff its constant term is zero. Biconditional version of deg1scl 26038. (Contributed by Thierry Arnoux, 22-Mar-2025.) |
| ⊢ 𝐷 = (deg1‘𝑅) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 𝑂 = (0g‘𝑃) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝐹 ∈ 𝐵) & ⊢ (𝜑 → (𝐷‘𝐹) ≤ 0) ⇒ ⊢ (𝜑 → (𝐹 = 𝑂 ↔ ((coe1‘𝐹)‘0) = 0 )) | ||
| Theorem | ply1asclunit 33527 | 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 33528 | In a field 𝐹, a polynomial 𝐶 is a unit iff it has degree 0. This corresponds to the nonzero scalars, see ply1asclunit 33527. (Contributed by Thierry Arnoux, 25-Apr-2025.) |
| ⊢ 𝑃 = (Poly1‘𝐹) & ⊢ 𝐴 = (algSc‘𝑃) & ⊢ 𝐵 = (Base‘𝐹) & ⊢ 0 = (0g‘𝐹) & ⊢ (𝜑 → 𝐹 ∈ Field) & ⊢ 𝐷 = (deg1‘𝐹) & ⊢ (𝜑 → 𝐶 ∈ (Base‘𝑃)) ⇒ ⊢ (𝜑 → (𝐶 ∈ (Unit‘𝑃) ↔ (𝐷‘𝐶) = 0)) | ||
| Theorem | evl1deg1 33529 | 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 33530 | 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 33531 | 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 33532 | 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 33533 | 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 33534 | 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 33535 | 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 33536 | 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 33537 | 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 33538 | 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 33539* | 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 33540 | 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 33541 | The coefficients of the zero univariate polynomial. (Contributed by Thierry Arnoux, 22-Jun-2025.) |
| ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝑍 = (0g‘𝑃) & ⊢ 0 = (0g‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) ⇒ ⊢ (𝜑 → ((coe1‘𝑍)‘𝑁) = 0 ) | ||
| Theorem | coe1vr1 33542* | 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 33543 | The degree of the variable polynomial is 1. (Contributed by Thierry Arnoux, 22-Jun-2025.) |
| ⊢ 𝐷 = (deg1‘𝑅) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝑋 = (var1‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ NzRing) ⇒ ⊢ (𝜑 → (𝐷‘𝑋) = 1) | ||
| Theorem | vr1nz 33544 | 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 33545 | 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 33546 | 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 33547 | 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 33548* | 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 33549* | 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 33550 | If both factors have degree bounded by 𝐿, then the sum of the polynomials also has degree bounded by 𝐿. See also deg1addle 26026. (Contributed by Thierry Arnoux, 2-Apr-2025.) |
| ⊢ 𝑌 = (Poly1‘𝑅) & ⊢ 𝐷 = (deg1‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ 𝐵 = (Base‘𝑌) & ⊢ + = (+g‘𝑌) & ⊢ (𝜑 → 𝐹 ∈ 𝐵) & ⊢ (𝜑 → 𝐺 ∈ 𝐵) & ⊢ (𝜑 → 𝐿 ∈ ℝ*) & ⊢ (𝜑 → (𝐷‘𝐹) < 𝐿) & ⊢ (𝜑 → (𝐷‘𝐺) < 𝐿) ⇒ ⊢ (𝜑 → (𝐷‘(𝐹 + 𝐺)) < 𝐿) | ||
| Theorem | ig1pnunit 33551 | The polynomial ideal generator is not a unit polynomial. (Contributed by Thierry Arnoux, 19-Mar-2025.) |
| ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐺 = (idlGen1p‘𝑅) & ⊢ 𝑈 = (Base‘𝑃) & ⊢ (𝜑 → 𝑅 ∈ DivRing) & ⊢ (𝜑 → 𝐼 ∈ (LIdeal‘𝑃)) & ⊢ (𝜑 → 𝐼 ≠ 𝑈) ⇒ ⊢ (𝜑 → ¬ (𝐺‘𝐼) ∈ (Unit‘𝑃)) | ||
| Theorem | ig1pmindeg 33552 | 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 33553 | Distribution of univariate polynomial quotient over addition. (Contributed by Thierry Arnoux, 2-Apr-2025.) |
| ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝑈 = (Base‘𝑃) & ⊢ 𝑁 = (Unic1p‘𝑅) & ⊢ / = (quot1p‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝐴 ∈ 𝑈) & ⊢ (𝜑 → 𝐶 ∈ 𝑁) & ⊢ (𝜑 → 𝐵 ∈ 𝑈) & ⊢ + = (+g‘𝑃) ⇒ ⊢ (𝜑 → ((𝐴 + 𝐵) / 𝐶) = ((𝐴 / 𝐶) + (𝐵 / 𝐶))) | ||
| Theorem | q1pvsca 33554 | Scalar multiplication property of the polynomial division. (Contributed by Thierry Arnoux, 2-Apr-2025.) |
| ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝑈 = (Base‘𝑃) & ⊢ 𝑁 = (Unic1p‘𝑅) & ⊢ / = (quot1p‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝐴 ∈ 𝑈) & ⊢ (𝜑 → 𝐶 ∈ 𝑁) & ⊢ × = ( ·𝑠 ‘𝑃) & ⊢ 𝐾 = (Base‘𝑅) & ⊢ (𝜑 → 𝐵 ∈ 𝐾) ⇒ ⊢ (𝜑 → ((𝐵 × 𝐴) / 𝐶) = (𝐵 × (𝐴 / 𝐶))) | ||
| Theorem | r1pvsca 33555 | Scalar multiplication property of the polynomial remainder operation. (Contributed by Thierry Arnoux, 2-Apr-2025.) |
| ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝑈 = (Base‘𝑃) & ⊢ 𝑁 = (Unic1p‘𝑅) & ⊢ 𝐸 = (rem1p‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝐴 ∈ 𝑈) & ⊢ (𝜑 → 𝐷 ∈ 𝑁) & ⊢ × = ( ·𝑠 ‘𝑃) & ⊢ 𝐾 = (Base‘𝑅) & ⊢ (𝜑 → 𝐵 ∈ 𝐾) ⇒ ⊢ (𝜑 → ((𝐵 × 𝐴)𝐸𝐷) = (𝐵 × (𝐴𝐸𝐷))) | ||
| Theorem | r1p0 33556 | 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 33557 | The polynomial remainder operation is periodic. See modcyc 13802. (Contributed by Thierry Arnoux, 2-Apr-2025.) |
| ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝑈 = (Base‘𝑃) & ⊢ 𝑁 = (Unic1p‘𝑅) & ⊢ 𝐸 = (rem1p‘𝑅) & ⊢ + = (+g‘𝑃) & ⊢ · = (.r‘𝑃) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝐴 ∈ 𝑈) & ⊢ (𝜑 → 𝐵 ∈ 𝑁) & ⊢ (𝜑 → 𝐶 ∈ 𝑈) ⇒ ⊢ (𝜑 → ((𝐴 + (𝐶 · 𝐵))𝐸𝐵) = (𝐴𝐸𝐵)) | ||
| Theorem | r1padd1 33558 | Addition property of the polynomial remainder operation, similar to modadd1 13804. (Contributed by Thierry Arnoux, 2-Apr-2025.) |
| ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝑈 = (Base‘𝑃) & ⊢ 𝑁 = (Unic1p‘𝑅) & ⊢ 𝐸 = (rem1p‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝐴 ∈ 𝑈) & ⊢ (𝜑 → 𝐷 ∈ 𝑁) & ⊢ (𝜑 → (𝐴𝐸𝐷) = (𝐵𝐸𝐷)) & ⊢ + = (+g‘𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑈) & ⊢ (𝜑 → 𝐶 ∈ 𝑈) ⇒ ⊢ (𝜑 → ((𝐴 + 𝐶)𝐸𝐷) = ((𝐵 + 𝐶)𝐸𝐷)) | ||
| Theorem | r1pid2OLD 33559 | Obsolete version of r1pid2 26087 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 33560* | 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 33561* | 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 33562 | 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 21863, but with the former expression, theorems about finite support can be used more directly. (Contributed by Thierry Arnoux, 10-Jan-2026.) |
| ⊢ 𝐷 = {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ 𝑓 finSupp 0} ⇒ ⊢ 𝐷 = {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} | ||
| Theorem | mplvrpmlem 33563* | Lemma for mplvrpmga 33565 and others. (Contributed by Thierry Arnoux, 11-Jan-2026.) |
| ⊢ 𝑆 = (SymGrp‘𝐼) & ⊢ 𝑃 = (Base‘𝑆) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ (𝜑 → 𝑋 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ⇒ ⊢ (𝜑 → (𝑋 ∘ 𝐷) ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) | ||
| Theorem | mplvrpmfgalem 33564* | 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 33565* | 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 33566* | 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 33567* | 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 𝑊)) | ||
| Syntax | csply 33568 | Extend class notation with the symmetric polynomials. |
| class SymPoly | ||
| Syntax | cesply 33569 | Extend class notation with the elementary symmetric polynomials. |
| class eSymPoly | ||
| Definition | df-sply 33570* | Define symmetric polynomials. See splyval 33572 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 33571* | Define elementary symmetric polynomials. (Contributed by Thierry Arnoux, 18-Jan-2026.) |
| ⊢ eSymPoly = (𝑖 ∈ V, 𝑟 ∈ V ↦ (𝑘 ∈ ℕ0 ↦ ((ℤRHom‘𝑟) ∘ ((𝟭‘{ℎ ∈ (ℕ0 ↑m 𝑖) ∣ ℎ finSupp 0})‘((𝟭‘𝑖) “ {𝑐 ∈ 𝒫 𝑖 ∣ (♯‘𝑐) = 𝑘}))))) | ||
| Theorem | splyval 33572* | 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 33573* | 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 33574* | Conditions for being a symmetric polynomial. (Contributed by Thierry Arnoux, 18-Jan-2026.) |
| ⊢ 𝑆 = (SymGrp‘𝐼) & ⊢ 𝑃 = (Base‘𝑆) & ⊢ 𝑀 = (Base‘(𝐼 mPoly 𝑅)) & ⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝑅 ∈ 𝑊) & ⊢ (𝜑 → 𝐹 ∈ 𝑀) & ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑃) ∧ 𝑥 ∈ 𝐷) → (𝐹‘(𝑥 ∘ 𝑝)) = (𝐹‘𝑥)) ⇒ ⊢ (𝜑 → 𝐹 ∈ (𝐼SymPoly𝑅)) | ||
| Theorem | esplyval 33575* | The elementary polynomials for a given index 𝐼 of variables and base ring 𝑅. (Contributed by Thierry Arnoux, 18-Jan-2026.) |
| ⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝑅 ∈ 𝑊) ⇒ ⊢ (𝜑 → (𝐼eSymPoly𝑅) = (𝑘 ∈ ℕ0 ↦ ((ℤRHom‘𝑅) ∘ ((𝟭‘𝐷)‘((𝟭‘𝐼) “ {𝑐 ∈ 𝒫 𝐼 ∣ (♯‘𝑐) = 𝑘}))))) | ||
| Theorem | esplyfval 33576* | The 𝐾-th elementary polynomial for a given index 𝐼 of variables and base ring 𝑅. (Contributed by Thierry Arnoux, 18-Jan-2026.) |
| ⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝑅 ∈ 𝑊) & ⊢ (𝜑 → 𝐾 ∈ ℕ0) ⇒ ⊢ (𝜑 → ((𝐼eSymPoly𝑅)‘𝐾) = ((ℤRHom‘𝑅) ∘ ((𝟭‘𝐷)‘((𝟭‘𝐼) “ {𝑐 ∈ 𝒫 𝐼 ∣ (♯‘𝑐) = 𝐾})))) | ||
| Theorem | esplylem 33577* | Lemma for esplyfv 33581 and others. (Contributed by Thierry Arnoux, 18-Jan-2026.) |
| ⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} & ⊢ (𝜑 → 𝐼 ∈ Fin) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝐾 ∈ ℕ0) ⇒ ⊢ (𝜑 → ((𝟭‘𝐼) “ {𝑐 ∈ 𝒫 𝐼 ∣ (♯‘𝑐) = 𝐾}) ⊆ 𝐷) | ||
| Theorem | esplympl 33578* | Elementary symmetric polynomials are polynomials. (Contributed by Thierry Arnoux, 18-Jan-2026.) |
| ⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} & ⊢ (𝜑 → 𝐼 ∈ Fin) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝐾 ∈ ℕ0) & ⊢ 𝑀 = (Base‘(𝐼 mPoly 𝑅)) ⇒ ⊢ (𝜑 → ((𝐼eSymPoly𝑅)‘𝐾) ∈ 𝑀) | ||
| Theorem | esplymhp 33579* | The 𝐾-th elementary symmetric polynomial is homogeneous of degree 𝐾. (Contributed by Thierry Arnoux, 18-Jan-2026.) |
| ⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} & ⊢ (𝜑 → 𝐼 ∈ Fin) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝐾 ∈ ℕ0) & ⊢ 𝐻 = (𝐼 mHomP 𝑅) ⇒ ⊢ (𝜑 → ((𝐼eSymPoly𝑅)‘𝐾) ∈ (𝐻‘𝐾)) | ||
| Theorem | esplyfv1 33580* | Coefficient for the 𝐾-th elementary symmetric polynomial and a bag of variables 𝐹 where variables are not raised to a power. (Contributed by Thierry Arnoux, 18-Jan-2026.) |
| ⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} & ⊢ (𝜑 → 𝐼 ∈ Fin) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝐾 ∈ (0...(♯‘𝐼))) & ⊢ (𝜑 → 𝐹 ∈ 𝐷) & ⊢ 0 = (0g‘𝑅) & ⊢ 1 = (1r‘𝑅) & ⊢ (𝜑 → ran 𝐹 ⊆ {0, 1}) ⇒ ⊢ (𝜑 → (((𝐼eSymPoly𝑅)‘𝐾)‘𝐹) = if((♯‘(𝐹 supp 0)) = 𝐾, 1 , 0 )) | ||
| Theorem | esplyfv 33581* | Coefficient for the 𝐾-th elementary symmetric polynomial and a bag of variables 𝐹: the coefficient is 1 for the bags of exactly 𝐾 variables, having exponent at most 1. (Contributed by Thierry Arnoux, 18-Jan-2026.) |
| ⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} & ⊢ (𝜑 → 𝐼 ∈ Fin) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝐾 ∈ (0...(♯‘𝐼))) & ⊢ (𝜑 → 𝐹 ∈ 𝐷) & ⊢ 0 = (0g‘𝑅) & ⊢ 1 = (1r‘𝑅) ⇒ ⊢ (𝜑 → (((𝐼eSymPoly𝑅)‘𝐾)‘𝐹) = if((ran 𝐹 ⊆ {0, 1} ∧ (♯‘(𝐹 supp 0)) = 𝐾), 1 , 0 )) | ||
| Theorem | esplysply 33582* | The 𝐾-th elementary symmetric polynomial is symmetric. (Contributed by Thierry Arnoux, 18-Jan-2026.) |
| ⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} & ⊢ (𝜑 → 𝐼 ∈ Fin) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝐾 ∈ (0...(♯‘𝐼))) ⇒ ⊢ (𝜑 → ((𝐼eSymPoly𝑅)‘𝐾) ∈ (𝐼SymPoly𝑅)) | ||
| Theorem | sra1r 33583 | The unity element of a subring algebra. (Contributed by Thierry Arnoux, 24-Jul-2023.) |
| ⊢ (𝜑 → 𝐴 = ((subringAlg ‘𝑊)‘𝑆)) & ⊢ (𝜑 → 1 = (1r‘𝑊)) & ⊢ (𝜑 → 𝑆 ⊆ (Base‘𝑊)) ⇒ ⊢ (𝜑 → 1 = (1r‘𝐴)) | ||
| Theorem | sradrng 33584 | Condition for a subring algebra to be a division ring. (Contributed by Thierry Arnoux, 29-Jul-2023.) |
| ⊢ 𝐴 = ((subringAlg ‘𝑅)‘𝑉) & ⊢ 𝐵 = (Base‘𝑅) ⇒ ⊢ ((𝑅 ∈ DivRing ∧ 𝑉 ⊆ 𝐵) → 𝐴 ∈ DivRing) | ||
| Theorem | sraidom 33585 | Condition for a subring algebra to be an integral domain. (Contributed by Thierry Arnoux, 13-Oct-2025.) |
| ⊢ 𝐴 = ((subringAlg ‘𝑅)‘𝑉) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ IDomn) & ⊢ (𝜑 → 𝑉 ⊆ 𝐵) ⇒ ⊢ (𝜑 → 𝐴 ∈ IDomn) | ||
| Theorem | srasubrg 33586 | 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 33587 | 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 33588 | 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 33589 | 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 33590 | A subring is a subspace of the subring algebra. (Contributed by Thierry Arnoux, 2-Apr-2025.) |
| ⊢ 𝑊 = ((subringAlg ‘𝑅)‘𝐶) & ⊢ 𝐴 = (Base‘𝑅) & ⊢ 𝑆 = (𝑅 ↾s 𝐵) & ⊢ (𝜑 → 𝐵 ∈ (SubRing‘𝑅)) & ⊢ (𝜑 → 𝐶 ∈ (SubRing‘𝑆)) ⇒ ⊢ (𝜑 → 𝐵 ∈ (LSubSp‘𝑊)) | ||
| Theorem | srapwov 33591 | The "power" operation on a subring algebra. (Contributed by Thierry Arnoux, 10-Jan-2026.) |
| ⊢ 𝐴 = ((subringAlg ‘𝑊)‘𝑆) & ⊢ (𝜑 → 𝑊 ∈ Ring) & ⊢ (𝜑 → 𝑆 ⊆ (Base‘𝑊)) ⇒ ⊢ (𝜑 → (.g‘(mulGrp‘𝑊)) = (.g‘(mulGrp‘𝐴))) | ||
| Theorem | drgext0g 33592 | The additive neutral element of a division ring extension. (Contributed by Thierry Arnoux, 17-Jul-2023.) |
| ⊢ 𝐵 = ((subringAlg ‘𝐸)‘𝑈) & ⊢ (𝜑 → 𝐸 ∈ DivRing) & ⊢ (𝜑 → 𝑈 ∈ (SubRing‘𝐸)) ⇒ ⊢ (𝜑 → (0g‘𝐸) = (0g‘𝐵)) | ||
| Theorem | drgextvsca 33593 | The scalar multiplication operation of a division ring extension. (Contributed by Thierry Arnoux, 17-Jul-2023.) |
| ⊢ 𝐵 = ((subringAlg ‘𝐸)‘𝑈) & ⊢ (𝜑 → 𝐸 ∈ DivRing) & ⊢ (𝜑 → 𝑈 ∈ (SubRing‘𝐸)) ⇒ ⊢ (𝜑 → (.r‘𝐸) = ( ·𝑠 ‘𝐵)) | ||
| Theorem | drgext0gsca 33594 | 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 33595 | 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 33596 | 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 33597* | Group sum in a division ring extension. (Contributed by Thierry Arnoux, 17-Jul-2023.) |
| ⊢ 𝐵 = ((subringAlg ‘𝐸)‘𝑈) & ⊢ (𝜑 → 𝐸 ∈ DivRing) & ⊢ (𝜑 → 𝑈 ∈ (SubRing‘𝐸)) & ⊢ 𝐹 = (𝐸 ↾s 𝑈) & ⊢ (𝜑 → 𝐹 ∈ DivRing) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) ⇒ ⊢ (𝜑 → (𝐸 Σg (𝑖 ∈ 𝑋 ↦ 𝑌)) = (𝐵 Σg (𝑖 ∈ 𝑋 ↦ 𝑌))) | ||
| Theorem | lvecdimfi 33598 | Finite version of lvecdim 21087 which does not require the axiom of choice. The axiom of choice is used in acsmapd 18452, which is required in the infinite case. Suggested by Gérard Lang. (Contributed by Thierry Arnoux, 24-May-2023.) |
| ⊢ 𝐽 = (LBasis‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝑆 ∈ 𝐽) & ⊢ (𝜑 → 𝑇 ∈ 𝐽) & ⊢ (𝜑 → 𝑆 ∈ Fin) ⇒ ⊢ (𝜑 → 𝑆 ≈ 𝑇) | ||
| Theorem | exsslsb 33599* | 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 33600 | 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) & ⊢ (𝜑 → 𝑋 ∈ 𝐽) & ⊢ (𝜑 → 𝑌 ⊆ 𝐵) & ⊢ (𝜑 → (𝐾‘𝑌) = 𝐵) ⇒ ⊢ (𝜑 → (♯‘𝑋) ≤ (♯‘𝑌)) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |