HomeTheorem List (p. 334 of 502)
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. 334 of 502) | < 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-31005) |
Hilbert Space Explorer
(31006-32528) |
Users' Mathboxes
(32529-50153) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | slmdbn0 33301 | The base set of a semimodule is nonempty. (Contributed by Thierry Arnoux, 1-Apr-2018.) (Proof shortened by AV, 10-Jan-2023.) |
| ⊢ 𝐵 = (Base‘𝑊) ⇒ ⊢ (𝑊 ∈ SLMod → 𝐵 ≠ ∅) | ||
| Theorem | slmdacl 33302 | Closure of ring addition for a semimodule. (Contributed by Thierry Arnoux, 1-Apr-2018.) |
| ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) & ⊢ + = (+g‘𝐹) ⇒ ⊢ ((𝑊 ∈ SLMod ∧ 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐾) → (𝑋 + 𝑌) ∈ 𝐾) | ||
| Theorem | slmdmcl 33303 | Closure of ring multiplication for a semimodule. (Contributed by NM, 14-Jan-2014.) (Revised by Mario Carneiro, 19-Jun-2014.) (Revised by Thierry Arnoux, 1-Apr-2018.) |
| ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) & ⊢ · = (.r‘𝐹) ⇒ ⊢ ((𝑊 ∈ SLMod ∧ 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐾) → (𝑋 · 𝑌) ∈ 𝐾) | ||
| Theorem | slmdsn0 33304 | The set of scalars in a semimodule is nonempty. (Contributed by Thierry Arnoux, 1-Apr-2018.) (Proof shortened by AV, 10-Jan-2023.) |
| ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐵 = (Base‘𝐹) ⇒ ⊢ (𝑊 ∈ SLMod → 𝐵 ≠ ∅) | ||
| Theorem | slmdvacl 33305 | Closure of vector addition for a semiring left module. (Contributed by NM, 8-Dec-2013.) (Revised by Mario Carneiro, 19-Jun-2014.) (Revised by Thierry Arnoux, 1-Apr-2018.) |
| ⊢ 𝑉 = (Base‘𝑊) & ⊢ + = (+g‘𝑊) ⇒ ⊢ ((𝑊 ∈ SLMod ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → (𝑋 + 𝑌) ∈ 𝑉) | ||
| Theorem | slmdass 33306 | Semiring left module vector sum is associative. (Contributed by NM, 10-Jan-2014.) (Revised by Mario Carneiro, 19-Jun-2014.) (Revised by Thierry Arnoux, 1-Apr-2018.) |
| ⊢ 𝑉 = (Base‘𝑊) & ⊢ + = (+g‘𝑊) ⇒ ⊢ ((𝑊 ∈ SLMod ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑉)) → ((𝑋 + 𝑌) + 𝑍) = (𝑋 + (𝑌 + 𝑍))) | ||
| Theorem | slmdvscl 33307 | Closure of scalar product for a semiring left module. (hvmulcl 31100 analog.) (Contributed by NM, 8-Dec-2013.) (Revised by Mario Carneiro, 19-Jun-2014.) (Revised by Thierry Arnoux, 1-Apr-2018.) |
| ⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) ⇒ ⊢ ((𝑊 ∈ SLMod ∧ 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) → (𝑅 · 𝑋) ∈ 𝑉) | ||
| Theorem | slmdvsdi 33308 | Distributive law for scalar product. (ax-hvdistr1 31095 analog.) (Contributed by NM, 10-Jan-2014.) (Revised by Mario Carneiro, 22-Sep-2015.) (Revised by Thierry Arnoux, 1-Apr-2018.) |
| ⊢ 𝑉 = (Base‘𝑊) & ⊢ + = (+g‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) ⇒ ⊢ ((𝑊 ∈ SLMod ∧ (𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉)) → (𝑅 · (𝑋 + 𝑌)) = ((𝑅 · 𝑋) + (𝑅 · 𝑌))) | ||
| Theorem | slmdvsdir 33309 | Distributive law for scalar product. (ax-hvdistr1 31095 analog.) (Contributed by NM, 10-Jan-2014.) (Revised by Mario Carneiro, 22-Sep-2015.) (Revised by Thierry Arnoux, 1-Apr-2018.) |
| ⊢ 𝑉 = (Base‘𝑊) & ⊢ + = (+g‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) & ⊢ ⨣ = (+g‘𝐹) ⇒ ⊢ ((𝑊 ∈ SLMod ∧ (𝑄 ∈ 𝐾 ∧ 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉)) → ((𝑄 ⨣ 𝑅) · 𝑋) = ((𝑄 · 𝑋) + (𝑅 · 𝑋))) | ||
| Theorem | slmdvsass 33310 | Associative law for scalar product. (ax-hvmulass 31094 analog.) (Contributed by NM, 10-Jan-2014.) (Revised by Mario Carneiro, 22-Sep-2015.) (Revised by Thierry Arnoux, 1-Apr-2018.) |
| ⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) & ⊢ × = (.r‘𝐹) ⇒ ⊢ ((𝑊 ∈ SLMod ∧ (𝑄 ∈ 𝐾 ∧ 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉)) → ((𝑄 × 𝑅) · 𝑋) = (𝑄 · (𝑅 · 𝑋))) | ||
| Theorem | slmd0cl 33311 | The ring zero in a semimodule belongs to the ring base set. (Contributed by NM, 11-Jan-2014.) (Revised by Mario Carneiro, 19-Jun-2014.) (Revised by Thierry Arnoux, 1-Apr-2018.) |
| ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) & ⊢ 0 = (0g‘𝐹) ⇒ ⊢ (𝑊 ∈ SLMod → 0 ∈ 𝐾) | ||
| Theorem | slmd1cl 33312 | The ring unity in a semiring left module belongs to the ring base set. (Contributed by NM, 11-Jan-2014.) (Revised by Mario Carneiro, 19-Jun-2014.) (Revised by Thierry Arnoux, 1-Apr-2018.) |
| ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) & ⊢ 1 = (1r‘𝐹) ⇒ ⊢ (𝑊 ∈ SLMod → 1 ∈ 𝐾) | ||
| Theorem | slmdvs1 33313 | Scalar product with ring unity. (ax-hvmulid 31093 analog.) (Contributed by NM, 10-Jan-2014.) (Revised by Mario Carneiro, 19-Jun-2014.) (Revised by Thierry Arnoux, 1-Apr-2018.) |
| ⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 1 = (1r‘𝐹) ⇒ ⊢ ((𝑊 ∈ SLMod ∧ 𝑋 ∈ 𝑉) → ( 1 · 𝑋) = 𝑋) | ||
| Theorem | slmd0vcl 33314 | The zero vector is a vector. (ax-hv0cl 31090 analog.) (Contributed by NM, 10-Jan-2014.) (Revised by Mario Carneiro, 19-Jun-2014.) (Revised by Thierry Arnoux, 1-Apr-2018.) |
| ⊢ 𝑉 = (Base‘𝑊) & ⊢ 0 = (0g‘𝑊) ⇒ ⊢ (𝑊 ∈ SLMod → 0 ∈ 𝑉) | ||
| Theorem | slmd0vlid 33315 | Left identity law for the zero vector. (hvaddlid 31110 analog.) (Contributed by NM, 10-Jan-2014.) (Revised by Mario Carneiro, 19-Jun-2014.) (Revised by Thierry Arnoux, 1-Apr-2018.) |
| ⊢ 𝑉 = (Base‘𝑊) & ⊢ + = (+g‘𝑊) & ⊢ 0 = (0g‘𝑊) ⇒ ⊢ ((𝑊 ∈ SLMod ∧ 𝑋 ∈ 𝑉) → ( 0 + 𝑋) = 𝑋) | ||
| Theorem | slmd0vrid 33316 | Right identity law for the zero vector. (ax-hvaddid 31091 analog.) (Contributed by NM, 10-Jan-2014.) (Revised by Mario Carneiro, 19-Jun-2014.) (Revised by Thierry Arnoux, 1-Apr-2018.) |
| ⊢ 𝑉 = (Base‘𝑊) & ⊢ + = (+g‘𝑊) & ⊢ 0 = (0g‘𝑊) ⇒ ⊢ ((𝑊 ∈ SLMod ∧ 𝑋 ∈ 𝑉) → (𝑋 + 0 ) = 𝑋) | ||
| Theorem | slmd0vs 33317 | Zero times a vector is the zero vector. Equation 1a of [Kreyszig] p. 51. (ax-hvmul0 31097 analog.) (Contributed by NM, 12-Jan-2014.) (Revised by Mario Carneiro, 19-Jun-2014.) (Revised by Thierry Arnoux, 1-Apr-2018.) |
| ⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝑂 = (0g‘𝐹) & ⊢ 0 = (0g‘𝑊) ⇒ ⊢ ((𝑊 ∈ SLMod ∧ 𝑋 ∈ 𝑉) → (𝑂 · 𝑋) = 0 ) | ||
| Theorem | slmdvs0 33318 | Anything times the zero vector is the zero vector. Equation 1b of [Kreyszig] p. 51. (hvmul0 31111 analog.) (Contributed by NM, 12-Jan-2014.) (Revised by Mario Carneiro, 19-Jun-2014.) (Revised by Thierry Arnoux, 1-Apr-2018.) |
| ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) & ⊢ 0 = (0g‘𝑊) ⇒ ⊢ ((𝑊 ∈ SLMod ∧ 𝑋 ∈ 𝐾) → (𝑋 · 0 ) = 0 ) | ||
| Theorem | gsumvsca1 33319* | Scalar product of a finite group sum for a left module over a semiring. (Contributed by Thierry Arnoux, 16-Mar-2018.) |
| ⊢ 𝐵 = (Base‘𝑊) & ⊢ 𝐺 = (Scalar‘𝑊) & ⊢ 0 = (0g‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ + = (+g‘𝑊) & ⊢ (𝜑 → 𝐾 ⊆ (Base‘𝐺)) & ⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ (𝜑 → 𝑊 ∈ SLMod) & ⊢ (𝜑 → 𝑃 ∈ 𝐾) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝑄 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝑊 Σg (𝑘 ∈ 𝐴 ↦ (𝑃 · 𝑄))) = (𝑃 · (𝑊 Σg (𝑘 ∈ 𝐴 ↦ 𝑄)))) | ||
| Theorem | gsumvsca2 33320* | Scalar product of a finite group sum for a left module over a semiring. (Contributed by Thierry Arnoux, 16-Mar-2018.) (Proof shortened by AV, 12-Dec-2019.) |
| ⊢ 𝐵 = (Base‘𝑊) & ⊢ 𝐺 = (Scalar‘𝑊) & ⊢ 0 = (0g‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ + = (+g‘𝑊) & ⊢ (𝜑 → 𝐾 ⊆ (Base‘𝐺)) & ⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ (𝜑 → 𝑊 ∈ SLMod) & ⊢ (𝜑 → 𝑄 ∈ 𝐵) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝑃 ∈ 𝐾) ⇒ ⊢ (𝜑 → (𝑊 Σg (𝑘 ∈ 𝐴 ↦ (𝑃 · 𝑄))) = ((𝐺 Σg (𝑘 ∈ 𝐴 ↦ 𝑃)) · 𝑄)) | ||
| Theorem | prmsimpcyc 33321 | A group of prime order is cyclic if and only if it is simple. This is the first family of finite simple groups. (Contributed by Thierry Arnoux, 21-Sep-2023.) |
| ⊢ 𝐵 = (Base‘𝐺) ⇒ ⊢ ((♯‘𝐵) ∈ ℙ → (𝐺 ∈ SimpGrp ↔ 𝐺 ∈ CycGrp)) | ||
| Theorem | ringrngd 33322 | A unital ring is a non-unital ring, deduction version. (Contributed by Thierry Arnoux, 15-Feb-2026.) |
| ⊢ (𝜑 → 𝑅 ∈ Ring) ⇒ ⊢ (𝜑 → 𝑅 ∈ Rng) | ||
| Theorem | ringdi22 33323 | Expand the product of two sums in a ring. (Contributed by Thierry Arnoux, 3-Jun-2025.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ + = (+g‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) & ⊢ (𝜑 → 𝑇 ∈ 𝐵) ⇒ ⊢ (𝜑 → ((𝑋 + 𝑌) · (𝑍 + 𝑇)) = (((𝑋 · 𝑍) + (𝑌 · 𝑍)) + ((𝑋 · 𝑇) + (𝑌 · 𝑇)))) | ||
| Theorem | urpropd 33324* | Sufficient condition for ring unities to be equal. (Contributed by Thierry Arnoux, 9-Mar-2025.) |
| ⊢ 𝐵 = (Base‘𝑆) & ⊢ (𝜑 → 𝑆 ∈ 𝑉) & ⊢ (𝜑 → 𝑇 ∈ 𝑊) & ⊢ (𝜑 → 𝐵 = (Base‘𝑇)) & ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) → (𝑥(.r‘𝑆)𝑦) = (𝑥(.r‘𝑇)𝑦)) ⇒ ⊢ (𝜑 → (1r‘𝑆) = (1r‘𝑇)) | ||
| Theorem | subrgmcld 33325 | A subring is closed under multiplication. (Contributed by Thierry Arnoux, 6-Jul-2025.) |
| ⊢ · = (.r‘𝑅) & ⊢ (𝜑 → 𝐴 ∈ (SubRing‘𝑅)) & ⊢ (𝜑 → 𝑋 ∈ 𝐴) & ⊢ (𝜑 → 𝑌 ∈ 𝐴) ⇒ ⊢ (𝜑 → (𝑋 · 𝑌) ∈ 𝐴) | ||
| Theorem | ress1r 33326 | 1r is unaffected by restriction. This is a bit more generic than subrg1 20527. (Contributed by Thierry Arnoux, 6-Sep-2018.) |
| ⊢ 𝑆 = (𝑅 ↾s 𝐴) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ 1 = (1r‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 1 ∈ 𝐴 ∧ 𝐴 ⊆ 𝐵) → 1 = (1r‘𝑆)) | ||
| Theorem | ringm1expp1 33327 | Ring exponentiation of minus one: Adding one to the exponent is the same as taking the additive inverse. (Contributed by Thierry Arnoux, 15-Feb-2026.) |
| ⊢ 1 = (1r‘𝑅) & ⊢ 𝑁 = (invg‘𝑅) & ⊢ ↑ = (.g‘(mulGrp‘𝑅)) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝐾 ∈ ℕ0) ⇒ ⊢ (𝜑 → ((𝐾 + 1) ↑ (𝑁‘ 1 )) = (𝑁‘(𝐾 ↑ (𝑁‘ 1 )))) | ||
| Theorem | ringinvval 33328* | The ring inverse expressed in terms of multiplication. (Contributed by Thierry Arnoux, 23-Oct-2017.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ ∗ = (.r‘𝑅) & ⊢ 1 = (1r‘𝑅) & ⊢ 𝑁 = (invr‘𝑅) & ⊢ 𝑈 = (Unit‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈) → (𝑁‘𝑋) = (℩𝑦 ∈ 𝑈 (𝑦 ∗ 𝑋) = 1 )) | ||
| Theorem | dvrcan5 33329 | Cancellation law for common factor in ratio. (divcan5 11855 analog.) (Contributed by Thierry Arnoux, 26-Oct-2016.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝑈 = (Unit‘𝑅) & ⊢ / = (/r‘𝑅) & ⊢ · = (.r‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈 ∧ 𝑍 ∈ 𝑈)) → ((𝑋 · 𝑍) / (𝑌 · 𝑍)) = (𝑋 / 𝑌)) | ||
| Theorem | subrgchr 33330 | If 𝐴 is a subring of 𝑅, then they have the same characteristic. (Contributed by Thierry Arnoux, 24-Feb-2018.) |
| ⊢ (𝐴 ∈ (SubRing‘𝑅) → (chr‘(𝑅 ↾s 𝐴)) = (chr‘𝑅)) | ||
| Theorem | rmfsupp2 33331* | A mapping of a multiplication of a constant with a function into a ring is finitely supported if the function is finitely supported. (Contributed by Thierry Arnoux, 3-Jun-2023.) |
| ⊢ 𝑅 = (Base‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ Ring) & ⊢ (𝜑 → 𝑉 ∈ 𝑋) & ⊢ ((𝜑 ∧ 𝑣 ∈ 𝑉) → 𝐶 ∈ 𝑅) & ⊢ (𝜑 → 𝐴:𝑉⟶𝑅) & ⊢ (𝜑 → 𝐴 finSupp (0g‘𝑀)) ⇒ ⊢ (𝜑 → (𝑣 ∈ 𝑉 ↦ ((𝐴‘𝑣)(.r‘𝑀)𝐶)) finSupp (0g‘𝑀)) | ||
| Theorem | unitnz 33332 | In a nonzero ring, a unit cannot be zero. (Contributed by Thierry Arnoux, 25-Apr-2025.) |
| ⊢ 𝑈 = (Unit‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ NzRing) & ⊢ (𝜑 → 𝑋 ∈ 𝑈) ⇒ ⊢ (𝜑 → 𝑋 ≠ 0 ) | ||
| Theorem | isunit2 33333* | Alternate definition of being a unit. (Contributed by Thierry Arnoux, 3-Aug-2025.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝑈 = (Unit‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 1 = (1r‘𝑅) ⇒ ⊢ (𝑋 ∈ 𝑈 ↔ (𝑋 ∈ 𝐵 ∧ (∃𝑢 ∈ 𝐵 (𝑋 · 𝑢) = 1 ∧ ∃𝑣 ∈ 𝐵 (𝑣 · 𝑋) = 1 ))) | ||
| Theorem | isunit3 33334* | Alternate definition of being a unit. (Contributed by Thierry Arnoux, 3-Aug-2025.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝑈 = (Unit‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 1 = (1r‘𝑅) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑅 ∈ Ring) ⇒ ⊢ (𝜑 → (𝑋 ∈ 𝑈 ↔ ∃𝑦 ∈ 𝐵 ((𝑋 · 𝑦) = 1 ∧ (𝑦 · 𝑋) = 1 ))) | ||
| Theorem | elrgspnlem1 33335* | Lemma for elrgspn 33339. (Contributed by Thierry Arnoux, 5-Oct-2025.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝑀 = (mulGrp‘𝑅) & ⊢ · = (.g‘𝑅) & ⊢ 𝑁 = (RingSpan‘𝑅) & ⊢ 𝐹 = {𝑓 ∈ (ℤ ↑m Word 𝐴) ∣ 𝑓 finSupp 0} & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝐴 ⊆ 𝐵) & ⊢ 𝑆 = ran (𝑔 ∈ 𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) ⇒ ⊢ (𝜑 → 𝑆 ∈ (SubGrp‘𝑅)) | ||
| Theorem | elrgspnlem2 33336* | Lemma for elrgspn 33339. (Contributed by Thierry Arnoux, 5-Oct-2025.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝑀 = (mulGrp‘𝑅) & ⊢ · = (.g‘𝑅) & ⊢ 𝑁 = (RingSpan‘𝑅) & ⊢ 𝐹 = {𝑓 ∈ (ℤ ↑m Word 𝐴) ∣ 𝑓 finSupp 0} & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝐴 ⊆ 𝐵) & ⊢ 𝑆 = ran (𝑔 ∈ 𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) ⇒ ⊢ (𝜑 → 𝑆 ∈ (SubRing‘𝑅)) | ||
| Theorem | elrgspnlem3 33337* | Lemma for elrgspn 33339. (Contributed by Thierry Arnoux, 5-Oct-2025.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝑀 = (mulGrp‘𝑅) & ⊢ · = (.g‘𝑅) & ⊢ 𝑁 = (RingSpan‘𝑅) & ⊢ 𝐹 = {𝑓 ∈ (ℤ ↑m Word 𝐴) ∣ 𝑓 finSupp 0} & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝐴 ⊆ 𝐵) & ⊢ 𝑆 = ran (𝑔 ∈ 𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) ⇒ ⊢ (𝜑 → 𝐴 ⊆ 𝑆) | ||
| Theorem | elrgspnlem4 33338* | Lemma for elrgspn 33339. (Contributed by Thierry Arnoux, 5-Oct-2025.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝑀 = (mulGrp‘𝑅) & ⊢ · = (.g‘𝑅) & ⊢ 𝑁 = (RingSpan‘𝑅) & ⊢ 𝐹 = {𝑓 ∈ (ℤ ↑m Word 𝐴) ∣ 𝑓 finSupp 0} & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝐴 ⊆ 𝐵) & ⊢ 𝑆 = ran (𝑔 ∈ 𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) ⇒ ⊢ (𝜑 → (𝑁‘𝐴) = 𝑆) | ||
| Theorem | elrgspn 33339* | Membership in the subring generated by the subset 𝐴. An element 𝑋 lies in that subring if and only if 𝑋 is a linear combination with integer coefficients of products of elements of 𝐴. (Contributed by Thierry Arnoux, 5-Oct-2025.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝑀 = (mulGrp‘𝑅) & ⊢ · = (.g‘𝑅) & ⊢ 𝑁 = (RingSpan‘𝑅) & ⊢ 𝐹 = {𝑓 ∈ (ℤ ↑m Word 𝐴) ∣ 𝑓 finSupp 0} & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝐴 ⊆ 𝐵) ⇒ ⊢ (𝜑 → (𝑋 ∈ (𝑁‘𝐴) ↔ ∃𝑔 ∈ 𝐹 𝑋 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤)))))) | ||
| Theorem | elrgspnsubrunlem1 33340* | Lemma for elrgspnsubrun 33342, first direction. (Contributed by Thierry Arnoux, 13-Oct-2025.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ 𝑁 = (RingSpan‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝐸 ∈ (SubRing‘𝑅)) & ⊢ (𝜑 → 𝐹 ∈ (SubRing‘𝑅)) & ⊢ (𝜑 → 𝑃:𝐹⟶𝐸) & ⊢ (𝜑 → 𝑃 finSupp 0 ) & ⊢ (𝜑 → 𝑋 = (𝑅 Σg (𝑒 ∈ 𝐹 ↦ ((𝑃‘𝑒) · 𝑒)))) & ⊢ 𝑇 = ran (𝑓 ∈ (𝑃 supp 0 ) ↦ ⟨“(𝑃‘𝑓)𝑓”⟩) ⇒ ⊢ (𝜑 → 𝑋 ∈ (𝑁‘(𝐸 ∪ 𝐹))) | ||
| Theorem | elrgspnsubrunlem2 33341* | Lemma for elrgspnsubrun 33342, second direction. (Contributed by Thierry Arnoux, 13-Oct-2025.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ 𝑁 = (RingSpan‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝐸 ∈ (SubRing‘𝑅)) & ⊢ (𝜑 → 𝐹 ∈ (SubRing‘𝑅)) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝐺:Word (𝐸 ∪ 𝐹)⟶ℤ) & ⊢ (𝜑 → 𝐺 finSupp 0) & ⊢ (𝜑 → 𝑋 = (𝑅 Σg (𝑤 ∈ Word (𝐸 ∪ 𝐹) ↦ ((𝐺‘𝑤)(.g‘𝑅)((mulGrp‘𝑅) Σg 𝑤))))) ⇒ ⊢ (𝜑 → ∃𝑝 ∈ (𝐸 ↑m 𝐹)(𝑝 finSupp 0 ∧ 𝑋 = (𝑅 Σg (𝑓 ∈ 𝐹 ↦ ((𝑝‘𝑓) · 𝑓))))) | ||
| Theorem | elrgspnsubrun 33342* | Membership in the ring span of the union of two subrings of a commutative ring. (Contributed by Thierry Arnoux, 13-Oct-2025.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ 𝑁 = (RingSpan‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝐸 ∈ (SubRing‘𝑅)) & ⊢ (𝜑 → 𝐹 ∈ (SubRing‘𝑅)) ⇒ ⊢ (𝜑 → (𝑋 ∈ (𝑁‘(𝐸 ∪ 𝐹)) ↔ ∃𝑝 ∈ (𝐸 ↑m 𝐹)(𝑝 finSupp 0 ∧ 𝑋 = (𝑅 Σg (𝑓 ∈ 𝐹 ↦ ((𝑝‘𝑓) · 𝑓)))))) | ||
| Theorem | irrednzr 33343 | A ring with an irreducible element cannot be the zero ring. (Contributed by Thierry Arnoux, 18-May-2025.) |
| ⊢ 𝐼 = (Irred‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝑋 ∈ 𝐼) ⇒ ⊢ (𝜑 → 𝑅 ∈ NzRing) | ||
| Theorem | 0ringsubrg 33344 | A subring of a zero ring is a zero ring. (Contributed by Thierry Arnoux, 5-Feb-2025.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → (♯‘𝐵) = 1) & ⊢ (𝜑 → 𝑆 ∈ (SubRing‘𝑅)) ⇒ ⊢ (𝜑 → (♯‘𝑆) = 1) | ||
| Theorem | 0ringcring 33345 | The zero ring is commutative. (Contributed by Thierry Arnoux, 18-May-2025.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → (♯‘𝐵) = 1) ⇒ ⊢ (𝜑 → 𝑅 ∈ CRing) | ||
| Syntax | cerl 33346 | Syntax for ring localization equivalence class operation. |
| class ~RL | ||
| Syntax | crloc 33347 | Syntax for ring localization operation. |
| class RLocal | ||
| Definition | df-erl 33348* | Define the operation giving the equivalence relation used in the localization of a ring 𝑟 by a set 𝑠. Two pairs 𝑎 = ⟨𝑥, 𝑦⟩ and 𝑏 = ⟨𝑧, 𝑤⟩ are equivalent if there exists 𝑡 ∈ 𝑠 such that 𝑡 · (𝑥 · 𝑤 − 𝑧 · 𝑦) = 0. This corresponds to the usual comparison of fractions 𝑥 / 𝑦 and 𝑧 / 𝑤. (Contributed by Thierry Arnoux, 28-Apr-2025.) |
| ⊢ ~RL = (𝑟 ∈ V, 𝑠 ∈ V ↦ ⦋(.r‘𝑟) / 𝑥⦌⦋((Base‘𝑟) × 𝑠) / 𝑤⦌{⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ 𝑤 ∧ 𝑏 ∈ 𝑤) ∧ ∃𝑡 ∈ 𝑠 (𝑡𝑥(((1st ‘𝑎)𝑥(2nd ‘𝑏))(-g‘𝑟)((1st ‘𝑏)𝑥(2nd ‘𝑎)))) = (0g‘𝑟))}) | ||
| Definition | df-rloc 33349* | Define the operation giving the localization of a ring 𝑟 by a given set 𝑠. The localized ring 𝑟 RLocal 𝑠 is the set of equivalence classes of pairs of elements in 𝑟 over the relation 𝑟 ~RL 𝑠 with addition and multiplication defined naturally. (Contributed by Thierry Arnoux, 27-Apr-2025.) |
| ⊢ RLocal = (𝑟 ∈ V, 𝑠 ∈ V ↦ ⦋(.r‘𝑟) / 𝑥⦌⦋((Base‘𝑟) × 𝑠) / 𝑤⦌((({⟨(Base‘ndx), 𝑤⟩, ⟨(+g‘ndx), (𝑎 ∈ 𝑤, 𝑏 ∈ 𝑤 ↦ ⟨(((1st ‘𝑎)𝑥(2nd ‘𝑏))(+g‘𝑟)((1st ‘𝑏)𝑥(2nd ‘𝑎))), ((2nd ‘𝑎)𝑥(2nd ‘𝑏))⟩)⟩, ⟨(.r‘ndx), (𝑎 ∈ 𝑤, 𝑏 ∈ 𝑤 ↦ ⟨((1st ‘𝑎)𝑥(1st ‘𝑏)), ((2nd ‘𝑎)𝑥(2nd ‘𝑏))⟩)⟩} ∪ {⟨(Scalar‘ndx), (Scalar‘𝑟)⟩, ⟨( ·𝑠 ‘ndx), (𝑘 ∈ (Base‘(Scalar‘𝑟)), 𝑎 ∈ 𝑤 ↦ ⟨(𝑘( ·𝑠 ‘𝑟)(1st ‘𝑎)), (2nd ‘𝑎)⟩)⟩, ⟨(·𝑖‘ndx), ∅⟩}) ∪ {⟨(TopSet‘ndx), ((TopSet‘𝑟) ×t ((TopSet‘𝑟) ↾t 𝑠))⟩, ⟨(le‘ndx), {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ 𝑤 ∧ 𝑏 ∈ 𝑤) ∧ ((1st ‘𝑎)𝑥(2nd ‘𝑏))(le‘𝑟)((1st ‘𝑏)𝑥(2nd ‘𝑎)))}⟩, ⟨(dist‘ndx), (𝑎 ∈ 𝑤, 𝑏 ∈ 𝑤 ↦ (((1st ‘𝑎)𝑥(2nd ‘𝑏))(dist‘𝑟)((1st ‘𝑏)𝑥(2nd ‘𝑎))))⟩}) /s (𝑟 ~RL 𝑠))) | ||
| Theorem | reldmrloc 33350 | Ring localization is a proper operator, so it can be used with ovprc1 7407. (Contributed by Thierry Arnoux, 10-May-2025.) |
| ⊢ Rel dom RLocal | ||
| Theorem | erlval 33351* | Value of the ring localization equivalence relation. (Contributed by Thierry Arnoux, 4-May-2025.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ − = (-g‘𝑅) & ⊢ 𝑊 = (𝐵 × 𝑆) & ⊢ ∼ = {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ 𝑊 ∧ 𝑏 ∈ 𝑊) ∧ ∃𝑡 ∈ 𝑆 (𝑡 · (((1st ‘𝑎) · (2nd ‘𝑏)) − ((1st ‘𝑏) · (2nd ‘𝑎)))) = 0 )} & ⊢ (𝜑 → 𝑆 ⊆ 𝐵) ⇒ ⊢ (𝜑 → (𝑅 ~RL 𝑆) = ∼ ) | ||
| Theorem | rlocval 33352* | Expand the value of the ring localization operation. (Contributed by Thierry Arnoux, 4-May-2025.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ − = (-g‘𝑅) & ⊢ + = (+g‘𝑅) & ⊢ ≤ = (le‘𝑅) & ⊢ 𝐹 = (Scalar‘𝑅) & ⊢ 𝐾 = (Base‘𝐹) & ⊢ 𝐶 = ( ·𝑠 ‘𝑅) & ⊢ 𝑊 = (𝐵 × 𝑆) & ⊢ ∼ = (𝑅 ~RL 𝑆) & ⊢ 𝐽 = (TopSet‘𝑅) & ⊢ 𝐷 = (dist‘𝑅) & ⊢ ⊕ = (𝑎 ∈ 𝑊, 𝑏 ∈ 𝑊 ↦ ⟨(((1st ‘𝑎) · (2nd ‘𝑏)) + ((1st ‘𝑏) · (2nd ‘𝑎))), ((2nd ‘𝑎) · (2nd ‘𝑏))⟩) & ⊢ ⊗ = (𝑎 ∈ 𝑊, 𝑏 ∈ 𝑊 ↦ ⟨((1st ‘𝑎) · (1st ‘𝑏)), ((2nd ‘𝑎) · (2nd ‘𝑏))⟩) & ⊢ × = (𝑘 ∈ 𝐾, 𝑎 ∈ 𝑊 ↦ ⟨(𝑘𝐶(1st ‘𝑎)), (2nd ‘𝑎)⟩) & ⊢ ≲ = {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ 𝑊 ∧ 𝑏 ∈ 𝑊) ∧ ((1st ‘𝑎) · (2nd ‘𝑏)) ≤ ((1st ‘𝑏) · (2nd ‘𝑎)))} & ⊢ 𝐸 = (𝑎 ∈ 𝑊, 𝑏 ∈ 𝑊 ↦ (((1st ‘𝑎) · (2nd ‘𝑏))𝐷((1st ‘𝑏) · (2nd ‘𝑎)))) & ⊢ (𝜑 → 𝑅 ∈ 𝑉) & ⊢ (𝜑 → 𝑆 ⊆ 𝐵) ⇒ ⊢ (𝜑 → (𝑅 RLocal 𝑆) = ((({⟨(Base‘ndx), 𝑊⟩, ⟨(+g‘ndx), ⊕ ⟩, ⟨(.r‘ndx), ⊗ ⟩} ∪ {⟨(Scalar‘ndx), 𝐹⟩, ⟨( ·𝑠 ‘ndx), × ⟩, ⟨(·𝑖‘ndx), ∅⟩}) ∪ {⟨(TopSet‘ndx), (𝐽 ×t (𝐽 ↾t 𝑆))⟩, ⟨(le‘ndx), ≲ ⟩, ⟨(dist‘ndx), 𝐸⟩}) /s ∼ )) | ||
| Theorem | erlcl1 33353 | Closure for the ring localization equivalence relation. (Contributed by Thierry Arnoux, 4-May-2025.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ ∼ = (𝑅 ~RL 𝑆) & ⊢ (𝜑 → 𝑆 ⊆ 𝐵) & ⊢ (𝜑 → 𝑈 ∼ 𝑉) ⇒ ⊢ (𝜑 → 𝑈 ∈ (𝐵 × 𝑆)) | ||
| Theorem | erlcl2 33354 | Closure for the ring localization equivalence relation. (Contributed by Thierry Arnoux, 4-May-2025.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ ∼ = (𝑅 ~RL 𝑆) & ⊢ (𝜑 → 𝑆 ⊆ 𝐵) & ⊢ (𝜑 → 𝑈 ∼ 𝑉) ⇒ ⊢ (𝜑 → 𝑉 ∈ (𝐵 × 𝑆)) | ||
| Theorem | erldi 33355* | Main property of the ring localization equivalence relation. (Contributed by Thierry Arnoux, 4-May-2025.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ ∼ = (𝑅 ~RL 𝑆) & ⊢ (𝜑 → 𝑆 ⊆ 𝐵) & ⊢ 0 = (0g‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ − = (-g‘𝑅) & ⊢ (𝜑 → 𝑈 ∼ 𝑉) ⇒ ⊢ (𝜑 → ∃𝑡 ∈ 𝑆 (𝑡 · (((1st ‘𝑈) · (2nd ‘𝑉)) − ((1st ‘𝑉) · (2nd ‘𝑈)))) = 0 ) | ||
| Theorem | erlbrd 33356 | Deduce the ring localization equivalence relation. If for some 𝑇 ∈ 𝑆 we have 𝑇 · (𝐸 · 𝐻 − 𝐹 · 𝐺) = 0, then pairs ⟨𝐸, 𝐺⟩ and ⟨𝐹, 𝐻⟩ are equivalent under the localization relation. (Contributed by Thierry Arnoux, 4-May-2025.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ ∼ = (𝑅 ~RL 𝑆) & ⊢ (𝜑 → 𝑆 ⊆ 𝐵) & ⊢ 0 = (0g‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ − = (-g‘𝑅) & ⊢ (𝜑 → 𝑈 = ⟨𝐸, 𝐺⟩) & ⊢ (𝜑 → 𝑉 = ⟨𝐹, 𝐻⟩) & ⊢ (𝜑 → 𝐸 ∈ 𝐵) & ⊢ (𝜑 → 𝐹 ∈ 𝐵) & ⊢ (𝜑 → 𝐺 ∈ 𝑆) & ⊢ (𝜑 → 𝐻 ∈ 𝑆) & ⊢ (𝜑 → 𝑇 ∈ 𝑆) & ⊢ (𝜑 → (𝑇 · ((𝐸 · 𝐻) − (𝐹 · 𝐺))) = 0 ) ⇒ ⊢ (𝜑 → 𝑈 ∼ 𝑉) | ||
| Theorem | erlbr2d 33357 | Deduce the ring localization equivalence relation. Pairs ⟨𝐸, 𝐺⟩ and ⟨𝑇 · 𝐸, 𝑇 · 𝐺⟩ for 𝑇 ∈ 𝑆 are equivalent under the localization relation. (Contributed by Thierry Arnoux, 4-May-2025.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ ∼ = (𝑅 ~RL 𝑆) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝑆 ∈ (SubMnd‘(mulGrp‘𝑅))) & ⊢ · = (.r‘𝑅) & ⊢ (𝜑 → 𝑈 = ⟨𝐸, 𝐺⟩) & ⊢ (𝜑 → 𝑉 = ⟨𝐹, 𝐻⟩) & ⊢ (𝜑 → 𝐸 ∈ 𝐵) & ⊢ (𝜑 → 𝐹 ∈ 𝐵) & ⊢ (𝜑 → 𝐺 ∈ 𝑆) & ⊢ (𝜑 → 𝐻 ∈ 𝑆) & ⊢ (𝜑 → 𝑇 ∈ 𝑆) & ⊢ (𝜑 → 𝐹 = (𝑇 · 𝐸)) & ⊢ (𝜑 → 𝐻 = (𝑇 · 𝐺)) ⇒ ⊢ (𝜑 → 𝑈 ∼ 𝑉) | ||
| Theorem | erler 33358 | The relation used to build the ring localization is an equivalence relation. (Contributed by Thierry Arnoux, 4-May-2025.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ 1 = (1r‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ − = (-g‘𝑅) & ⊢ 𝑊 = (𝐵 × 𝑆) & ⊢ ∼ = (𝑅 ~RL 𝑆) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝑆 ∈ (SubMnd‘(mulGrp‘𝑅))) ⇒ ⊢ (𝜑 → ∼ Er 𝑊) | ||
| Theorem | elrlocbasi 33359* | Membership in the basis of a ring localization. (Contributed by Thierry Arnoux, 4-May-2025.) |
| ⊢ (𝜑 → 𝑋 ∈ ((𝐵 × 𝑆) / ∼ )) ⇒ ⊢ (𝜑 → ∃𝑎 ∈ 𝐵 ∃𝑏 ∈ 𝑆 𝑋 = [⟨𝑎, 𝑏⟩] ∼ ) | ||
| Theorem | rlocbas 33360 | The base set of a ring localization. (Contributed by Thierry Arnoux, 4-May-2025.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ − = (-g‘𝑅) & ⊢ 𝑊 = (𝐵 × 𝑆) & ⊢ 𝐿 = (𝑅 RLocal 𝑆) & ⊢ ∼ = (𝑅 ~RL 𝑆) & ⊢ (𝜑 → 𝑅 ∈ 𝑉) & ⊢ (𝜑 → 𝑆 ⊆ 𝐵) ⇒ ⊢ (𝜑 → (𝑊 / ∼ ) = (Base‘𝐿)) | ||
| Theorem | rlocaddval 33361 | Value of the addition in the ring localization, given two representatives. (Contributed by Thierry Arnoux, 4-May-2025.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ + = (+g‘𝑅) & ⊢ 𝐿 = (𝑅 RLocal 𝑆) & ⊢ ∼ = (𝑅 ~RL 𝑆) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝑆 ∈ (SubMnd‘(mulGrp‘𝑅))) & ⊢ (𝜑 → 𝐸 ∈ 𝐵) & ⊢ (𝜑 → 𝐹 ∈ 𝐵) & ⊢ (𝜑 → 𝐺 ∈ 𝑆) & ⊢ (𝜑 → 𝐻 ∈ 𝑆) & ⊢ ⊕ = (+g‘𝐿) ⇒ ⊢ (𝜑 → ([⟨𝐸, 𝐺⟩] ∼ ⊕ [⟨𝐹, 𝐻⟩] ∼ ) = [⟨((𝐸 · 𝐻) + (𝐹 · 𝐺)), (𝐺 · 𝐻)⟩] ∼ ) | ||
| Theorem | rlocmulval 33362 | Value of the addition in the ring localization, given two representatives. (Contributed by Thierry Arnoux, 4-May-2025.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ + = (+g‘𝑅) & ⊢ 𝐿 = (𝑅 RLocal 𝑆) & ⊢ ∼ = (𝑅 ~RL 𝑆) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝑆 ∈ (SubMnd‘(mulGrp‘𝑅))) & ⊢ (𝜑 → 𝐸 ∈ 𝐵) & ⊢ (𝜑 → 𝐹 ∈ 𝐵) & ⊢ (𝜑 → 𝐺 ∈ 𝑆) & ⊢ (𝜑 → 𝐻 ∈ 𝑆) & ⊢ ⊗ = (.r‘𝐿) ⇒ ⊢ (𝜑 → ([⟨𝐸, 𝐺⟩] ∼ ⊗ [⟨𝐹, 𝐻⟩] ∼ ) = [⟨(𝐸 · 𝐹), (𝐺 · 𝐻)⟩] ∼ ) | ||
| Theorem | rloccring 33363 | The ring localization 𝐿 of a commutative ring 𝑅 by a multiplicatively closed set 𝑆 is itself a commutative ring. (Contributed by Thierry Arnoux, 4-May-2025.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ + = (+g‘𝑅) & ⊢ 𝐿 = (𝑅 RLocal 𝑆) & ⊢ ∼ = (𝑅 ~RL 𝑆) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝑆 ∈ (SubMnd‘(mulGrp‘𝑅))) ⇒ ⊢ (𝜑 → 𝐿 ∈ CRing) | ||
| Theorem | rloc0g 33364 | The zero of a ring localization. (Contributed by Thierry Arnoux, 4-May-2025.) |
| ⊢ 0 = (0g‘𝑅) & ⊢ 1 = (1r‘𝑅) & ⊢ 𝐿 = (𝑅 RLocal 𝑆) & ⊢ ∼ = (𝑅 ~RL 𝑆) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝑆 ∈ (SubMnd‘(mulGrp‘𝑅))) & ⊢ 𝑂 = [⟨ 0 , 1 ⟩] ∼ ⇒ ⊢ (𝜑 → 𝑂 = (0g‘𝐿)) | ||
| Theorem | rloc1r 33365 | The multiplicative identity of a ring localization. (Contributed by Thierry Arnoux, 4-May-2025.) |
| ⊢ 0 = (0g‘𝑅) & ⊢ 1 = (1r‘𝑅) & ⊢ 𝐿 = (𝑅 RLocal 𝑆) & ⊢ ∼ = (𝑅 ~RL 𝑆) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝑆 ∈ (SubMnd‘(mulGrp‘𝑅))) & ⊢ 𝐼 = [⟨ 1 , 1 ⟩] ∼ ⇒ ⊢ (𝜑 → 𝐼 = (1r‘𝐿)) | ||
| Theorem | rlocf1 33366* | The embedding 𝐹 of a ring 𝑅 into its localization 𝐿. (Contributed by Thierry Arnoux, 4-May-2025.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ 1 = (1r‘𝑅) & ⊢ 𝐿 = (𝑅 RLocal 𝑆) & ⊢ ∼ = (𝑅 ~RL 𝑆) & ⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ [⟨𝑥, 1 ⟩] ∼ ) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝑆 ∈ (SubMnd‘(mulGrp‘𝑅))) & ⊢ (𝜑 → 𝑆 ⊆ (RLReg‘𝑅)) ⇒ ⊢ (𝜑 → (𝐹:𝐵–1-1→((𝐵 × 𝑆) / ∼ ) ∧ 𝐹 ∈ (𝑅 RingHom 𝐿))) | ||
| Theorem | domnmuln0rd 33367 | In a domain, factors of a nonzero product are nonzero. (Contributed by Thierry Arnoux, 8-Jun-2025.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ Domn) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → (𝑋 · 𝑌) ≠ 0 ) ⇒ ⊢ (𝜑 → (𝑋 ≠ 0 ∧ 𝑌 ≠ 0 )) | ||
| Theorem | domnprodn0 33368 | In a domain, a finite product of nonzero terms is nonzero. (Contributed by Thierry Arnoux, 6-Jun-2025.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝑀 = (mulGrp‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ Domn) & ⊢ (𝜑 → 𝐹 ∈ Word (𝐵 ∖ { 0 })) ⇒ ⊢ (𝜑 → (𝑀 Σg 𝐹) ≠ 0 ) | ||
| Theorem | domnprodeq0 33369 | A product over a domain is zero exactly when one of the factors is zero. Generalization of domneq0 20653 for any number of factors. See also domnprodn0 33368. (Contributed by Thierry Arnoux, 15-Feb-2026.) |
| ⊢ 𝑀 = (mulGrp‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ IDomn) & ⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ (𝜑 → 𝐹:𝐴⟶𝐵) ⇒ ⊢ (𝜑 → ((𝑀 Σg 𝐹) = 0 ↔ 0 ∈ ran 𝐹)) | ||
| Theorem | domnpropd 33370* | If two structures have the same components (properties), one is a domain iff the other one is. (Contributed by Thierry Arnoux, 13-Oct-2025.) |
| ⊢ (𝜑 → 𝐵 = (Base‘𝐾)) & ⊢ (𝜑 → 𝐵 = (Base‘𝐿)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(+g‘𝐾)𝑦) = (𝑥(+g‘𝐿)𝑦)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(.r‘𝐾)𝑦) = (𝑥(.r‘𝐿)𝑦)) ⇒ ⊢ (𝜑 → (𝐾 ∈ Domn ↔ 𝐿 ∈ Domn)) | ||
| Theorem | idompropd 33371* | If two structures have the same components (properties), one is a integral domain iff the other one is. See also domnpropd 33370. (Contributed by Thierry Arnoux, 13-Oct-2025.) |
| ⊢ (𝜑 → 𝐵 = (Base‘𝐾)) & ⊢ (𝜑 → 𝐵 = (Base‘𝐿)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(+g‘𝐾)𝑦) = (𝑥(+g‘𝐿)𝑦)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(.r‘𝐾)𝑦) = (𝑥(.r‘𝐿)𝑦)) ⇒ ⊢ (𝜑 → (𝐾 ∈ IDomn ↔ 𝐿 ∈ IDomn)) | ||
| Theorem | idomrcan 33372 | Right-cancellation law for integral domains. (Contributed by Thierry Arnoux, 22-Mar-2025.) (Proof shortened by SN, 21-Jun-2025.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑍 ∈ (𝐵 ∖ { 0 })) & ⊢ (𝜑 → 𝑅 ∈ IDomn) & ⊢ (𝜑 → (𝑋 · 𝑍) = (𝑌 · 𝑍)) ⇒ ⊢ (𝜑 → 𝑋 = 𝑌) | ||
| Theorem | domnlcanOLD 33373 | Obsolete version of domnlcan 20666 as of 21-Jun-2025. (Contributed by Thierry Arnoux, 22-Mar-2025.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ (𝜑 → 𝑋 ∈ (𝐵 ∖ { 0 })) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) & ⊢ (𝜑 → 𝑅 ∈ Domn) & ⊢ (𝜑 → (𝑋 · 𝑌) = (𝑋 · 𝑍)) ⇒ ⊢ (𝜑 → 𝑌 = 𝑍) | ||
| Theorem | domnlcanbOLD 33374 | Obsolete version of domnlcanb 20665 as of 21-Jun-2025. (Contributed by Thierry Arnoux, 8-Jun-2025.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ (𝜑 → 𝑋 ∈ (𝐵 ∖ { 0 })) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) & ⊢ (𝜑 → 𝑅 ∈ Domn) ⇒ ⊢ (𝜑 → ((𝑋 · 𝑌) = (𝑋 · 𝑍) ↔ 𝑌 = 𝑍)) | ||
| Theorem | idomrcanOLD 33375 | Obsolete version of idomrcan 33372 as of 21-Jun-2025. (Contributed by Thierry Arnoux, 22-Mar-2025.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ (𝜑 → 𝑋 ∈ (𝐵 ∖ { 0 })) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) & ⊢ (𝜑 → 𝑅 ∈ IDomn) & ⊢ (𝜑 → (𝑌 · 𝑋) = (𝑍 · 𝑋)) ⇒ ⊢ (𝜑 → 𝑌 = 𝑍) | ||
| Theorem | 1rrg 33376 | The multiplicative identity is a left-regular element. (Contributed by Thierry Arnoux, 6-May-2025.) |
| ⊢ 1 = (1r‘𝑅) & ⊢ 𝐸 = (RLReg‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ Ring) ⇒ ⊢ (𝜑 → 1 ∈ 𝐸) | ||
| Theorem | rrgsubm 33377 | The left regular elements of a ring form a submonoid of the multiplicative group. (Contributed by Thierry Arnoux, 10-May-2025.) |
| ⊢ 𝐸 = (RLReg‘𝑅) & ⊢ 𝑀 = (mulGrp‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ Ring) ⇒ ⊢ (𝜑 → 𝐸 ∈ (SubMnd‘𝑀)) | ||
| Theorem | subrdom 33378 | A subring of a domain is a domain. (Contributed by Thierry Arnoux, 18-May-2025.) |
| ⊢ (𝜑 → 𝑅 ∈ Domn) & ⊢ (𝜑 → 𝑆 ∈ (SubRing‘𝑅)) ⇒ ⊢ (𝜑 → (𝑅 ↾s 𝑆) ∈ Domn) | ||
| Theorem | subridom 33379 | A subring of an integral domain is an integral domain. (Contributed by Thierry Arnoux, 18-May-2025.) |
| ⊢ (𝜑 → 𝑅 ∈ IDomn) & ⊢ (𝜑 → 𝑆 ∈ (SubRing‘𝑅)) ⇒ ⊢ (𝜑 → (𝑅 ↾s 𝑆) ∈ IDomn) | ||
| Theorem | subrfld 33380 | A subring of a field is an integral domain. (Contributed by Thierry Arnoux, 18-May-2025.) |
| ⊢ (𝜑 → 𝑅 ∈ Field) & ⊢ (𝜑 → 𝑆 ∈ (SubRing‘𝑅)) ⇒ ⊢ (𝜑 → (𝑅 ↾s 𝑆) ∈ IDomn) | ||
| Syntax | ceuf 33381 | Declare the syntax for the Euclidean function index extractor. |
| class EuclF | ||
| Definition | df-euf 33382 | Define the Euclidean function. (Contributed by Thierry Arnoux, 22-Mar-2025.) Use its index-independent form eufid 33384 instead. (New usage is discouraged.) |
| ⊢ EuclF = Slot ;21 | ||
| Theorem | eufndx 33383 | Index value of the Euclidean function slot. Use ndxarg 17135. (Contributed by Thierry Arnoux, 22-Mar-2025.) (New usage is discouraged.) |
| ⊢ (EuclF‘ndx) = ;21 | ||
| Theorem | eufid 33384 | Utility theorem: index-independent form of df-euf 33382. (Contributed by Thierry Arnoux, 22-Mar-2025.) |
| ⊢ EuclF = Slot (EuclF‘ndx) | ||
| Syntax | cedom 33385 | Declare the syntax for the Euclidean Domain. |
| class EDomn | ||
| Definition | df-edom 33386* | Define Euclidean Domains. (Contributed by Thierry Arnoux, 22-Mar-2025.) |
| ⊢ EDomn = {𝑑 ∈ IDomn ∣ [(EuclF‘𝑑) / 𝑒][(Base‘𝑑) / 𝑣](Fun 𝑒 ∧ (𝑒 “ (𝑣 ∖ {(0g‘𝑑)})) ⊆ (0[,)+∞) ∧ ∀𝑎 ∈ 𝑣 ∀𝑏 ∈ (𝑣 ∖ {(0g‘𝑑)})∃𝑞 ∈ 𝑣 ∃𝑟 ∈ 𝑣 (𝑎 = ((𝑏(.r‘𝑑)𝑞)(+g‘𝑑)𝑟) ∧ (𝑟 = (0g‘𝑑) ∨ (𝑒‘𝑟) < (𝑒‘𝑏))))} | ||
| Theorem | ringinveu 33387 | If a ring unit element 𝑋 admits both a left inverse 𝑌 and a right inverse 𝑍, they are equal. (Contributed by Thierry Arnoux, 9-Mar-2025.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ 1 = (1r‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 𝑈 = (Unit‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) & ⊢ (𝜑 → (𝑌 · 𝑋) = 1 ) & ⊢ (𝜑 → (𝑋 · 𝑍) = 1 ) ⇒ ⊢ (𝜑 → 𝑍 = 𝑌) | ||
| Theorem | isdrng4 33388* | A division ring is a ring in which 1 ≠ 0 and every nonzero element has a left and right inverse. (Contributed by Thierry Arnoux, 2-Mar-2025.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ 1 = (1r‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 𝑈 = (Unit‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ Ring) ⇒ ⊢ (𝜑 → (𝑅 ∈ DivRing ↔ ( 1 ≠ 0 ∧ ∀𝑥 ∈ (𝐵 ∖ { 0 })∃𝑦 ∈ 𝐵 ((𝑥 · 𝑦) = 1 ∧ (𝑦 · 𝑥) = 1 )))) | ||
| Theorem | rndrhmcl 33389 | The image of a division ring by a ring homomorphism is a division ring. (Contributed by Thierry Arnoux, 25-Feb-2025.) |
| ⊢ 𝑅 = (𝑁 ↾s ran 𝐹) & ⊢ 0 = (0g‘𝑁) & ⊢ (𝜑 → 𝐹 ∈ (𝑀 RingHom 𝑁)) & ⊢ (𝜑 → ran 𝐹 ≠ { 0 }) & ⊢ (𝜑 → 𝑀 ∈ DivRing) ⇒ ⊢ (𝜑 → 𝑅 ∈ DivRing) | ||
| Theorem | qfld 33390 | The field of rational numbers is a field. (Contributed by Thierry Arnoux, 19-Oct-2025.) |
| ⊢ 𝑄 = (ℂfld ↾s ℚ) ⇒ ⊢ 𝑄 ∈ Field | ||
| Theorem | subsdrg 33391 | A subring of a sub-division-ring is a sub-division-ring. See also subsubrg 20543. (Contributed by Thierry Arnoux, 26-Oct-2025.) |
| ⊢ 𝑆 = (𝑅 ↾s 𝐴) & ⊢ (𝜑 → 𝐴 ∈ (SubDRing‘𝑅)) ⇒ ⊢ (𝜑 → (𝐵 ∈ (SubDRing‘𝑆) ↔ (𝐵 ∈ (SubDRing‘𝑅) ∧ 𝐵 ⊆ 𝐴))) | ||
| Theorem | sdrgdvcl 33392 | A sub-division-ring is closed under the ring division operation. (Contributed by Thierry Arnoux, 15-Jan-2025.) |
| ⊢ / = (/r‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ (𝜑 → 𝐴 ∈ (SubDRing‘𝑅)) & ⊢ (𝜑 → 𝑋 ∈ 𝐴) & ⊢ (𝜑 → 𝑌 ∈ 𝐴) & ⊢ (𝜑 → 𝑌 ≠ 0 ) ⇒ ⊢ (𝜑 → (𝑋 / 𝑌) ∈ 𝐴) | ||
| Theorem | sdrginvcl 33393 | A sub-division-ring is closed under the ring inverse operation. (Contributed by Thierry Arnoux, 15-Jan-2025.) |
| ⊢ 𝐼 = (invr‘𝑅) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ ((𝐴 ∈ (SubDRing‘𝑅) ∧ 𝑋 ∈ 𝐴 ∧ 𝑋 ≠ 0 ) → (𝐼‘𝑋) ∈ 𝐴) | ||
| Theorem | primefldchr 33394 | The characteristic of a prime field is the same as the characteristic of the main field. (Contributed by Thierry Arnoux, 21-Aug-2023.) |
| ⊢ 𝑃 = (𝑅 ↾s ∩ (SubDRing‘𝑅)) ⇒ ⊢ (𝑅 ∈ DivRing → (chr‘𝑃) = (chr‘𝑅)) | ||
| Syntax | cfrac 33395 | Syntax for the field of fractions of a given integral domain. |
| class Frac | ||
| Definition | df-frac 33396 | Define the field of fractions of a given integral domain. (Contributed by Thierry Arnoux, 26-Apr-2025.) |
| ⊢ Frac = (𝑟 ∈ V ↦ (𝑟 RLocal (RLReg‘𝑟))) | ||
| Theorem | fracval 33397 | Value of the field of fractions. (Contributed by Thierry Arnoux, 5-May-2025.) |
| ⊢ ( Frac ‘𝑅) = (𝑅 RLocal (RLReg‘𝑅)) | ||
| Theorem | fracbas 33398 | The base of the field of fractions. (Contributed by Thierry Arnoux, 10-May-2025.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝐸 = (RLReg‘𝑅) & ⊢ 𝐹 = ( Frac ‘𝑅) & ⊢ ∼ = (𝑅 ~RL 𝐸) ⇒ ⊢ ((𝐵 × 𝐸) / ∼ ) = (Base‘𝐹) | ||
| Theorem | fracerl 33399 | Rewrite the ring localization equivalence relation in the case of a field of fractions. (Contributed by Thierry Arnoux, 5-May-2025.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ ∼ = (𝑅 ~RL (RLReg‘𝑅)) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝐸 ∈ 𝐵) & ⊢ (𝜑 → 𝐺 ∈ 𝐵) & ⊢ (𝜑 → 𝐹 ∈ (RLReg‘𝑅)) & ⊢ (𝜑 → 𝐻 ∈ (RLReg‘𝑅)) ⇒ ⊢ (𝜑 → (⟨𝐸, 𝐹⟩ ∼ ⟨𝐺, 𝐻⟩ ↔ (𝐸 · 𝐻) = (𝐺 · 𝐹))) | ||
| Theorem | fracf1 33400* | The embedding of a commutative ring 𝑅 into its field of fractions. (Contributed by Thierry Arnoux, 10-May-2025.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝐸 = (RLReg‘𝑅) & ⊢ 1 = (1r‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ ∼ = (𝑅 ~RL 𝐸) & ⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ [⟨𝑥, 1 ⟩] ∼ ) ⇒ ⊢ (𝜑 → (𝐹:𝐵–1-1→((𝐵 × 𝐸) / ∼ ) ∧ 𝐹 ∈ (𝑅 RingHom ( Frac ‘𝑅)))) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |