HomeTheorem List (p. 333 of 491)
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. 333 of 491) | < 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-30946) |
Hilbert Space Explorer
(30947-32469) |
Users' Mathboxes
(32470-49035) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | slmdass 33201 | 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 33202 | Closure of scalar product for a semiring left module. (hvmulcl 31041 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 33203 | Distributive law for scalar product. (ax-hvdistr1 31036 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 33204 | Distributive law for scalar product. (ax-hvdistr1 31036 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 33205 | Associative law for scalar product. (ax-hvmulass 31035 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 33206 | 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 33207 | 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 33208 | Scalar product with ring unity. (ax-hvmulid 31034 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 33209 | The zero vector is a vector. (ax-hv0cl 31031 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 33210 | Left identity law for the zero vector. (hvaddlid 31051 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 33211 | Right identity law for the zero vector. (ax-hvaddid 31032 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 33212 | Zero times a vector is the zero vector. Equation 1a of [Kreyszig] p. 51. (ax-hvmul0 31038 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 33213 | Anything times the zero vector is the zero vector. Equation 1b of [Kreyszig] p. 51. (hvmul0 31052 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 33214* | 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 33215* | 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 33216 | 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 | cringmul32d 33217 | Commutative/associative law that swaps the last two factors in a triple product in a commutative ring. See also mul32 11424. (Contributed by Thierry Arnoux, 4-May-2025.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) ⇒ ⊢ (𝜑 → ((𝑋 · 𝑌) · 𝑍) = ((𝑋 · 𝑍) · 𝑌)) | ||
| Theorem | ringdid 33218 | Distributive law for the multiplication operation of a ring (left-distributivity). (Contributed by Thierry Arnoux, 4-May-2025.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ + = (+g‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝑋 · (𝑌 + 𝑍)) = ((𝑋 · 𝑌) + (𝑋 · 𝑍))) | ||
| Theorem | ringdird 33219 | Distributive law for the multiplication operation of a ring (right-distributivity). (Contributed by Thierry Arnoux, 4-May-2025.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ + = (+g‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) ⇒ ⊢ (𝜑 → ((𝑋 + 𝑌) · 𝑍) = ((𝑋 · 𝑍) + (𝑌 · 𝑍))) | ||
| Theorem | ringdi22 33220 | Expand the product of two sums in a ring. (Contributed by Thierry Arnoux, 3-Jun-2025.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ + = (+g‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) & ⊢ (𝜑 → 𝑇 ∈ 𝐵) ⇒ ⊢ (𝜑 → ((𝑋 + 𝑌) · (𝑍 + 𝑇)) = (((𝑋 · 𝑍) + (𝑌 · 𝑍)) + ((𝑋 · 𝑇) + (𝑌 · 𝑇)))) | ||
| Theorem | urpropd 33221* | Sufficient condition for ring unities to be equal. (Contributed by Thierry Arnoux, 9-Mar-2025.) |
| ⊢ 𝐵 = (Base‘𝑆) & ⊢ (𝜑 → 𝑆 ∈ 𝑉) & ⊢ (𝜑 → 𝑇 ∈ 𝑊) & ⊢ (𝜑 → 𝐵 = (Base‘𝑇)) & ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) → (𝑥(.r‘𝑆)𝑦) = (𝑥(.r‘𝑇)𝑦)) ⇒ ⊢ (𝜑 → (1r‘𝑆) = (1r‘𝑇)) | ||
| Theorem | subrgmcld 33222 | A subring is closed under multiplication. (Contributed by Thierry Arnoux, 6-Jul-2025.) |
| ⊢ · = (.r‘𝑅) & ⊢ (𝜑 → 𝐴 ∈ (SubRing‘𝑅)) & ⊢ (𝜑 → 𝑋 ∈ 𝐴) & ⊢ (𝜑 → 𝑌 ∈ 𝐴) ⇒ ⊢ (𝜑 → (𝑋 · 𝑌) ∈ 𝐴) | ||
| Theorem | ress1r 33223 | 1r is unaffected by restriction. This is a bit more generic than subrg1 20598. (Contributed by Thierry Arnoux, 6-Sep-2018.) |
| ⊢ 𝑆 = (𝑅 ↾s 𝐴) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ 1 = (1r‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 1 ∈ 𝐴 ∧ 𝐴 ⊆ 𝐵) → 1 = (1r‘𝑆)) | ||
| Theorem | ringinvval 33224* | 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 33225 | Cancellation law for common factor in ratio. (divcan5 11966 analog.) (Contributed by Thierry Arnoux, 26-Oct-2016.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝑈 = (Unit‘𝑅) & ⊢ / = (/r‘𝑅) & ⊢ · = (.r‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈 ∧ 𝑍 ∈ 𝑈)) → ((𝑋 · 𝑍) / (𝑌 · 𝑍)) = (𝑋 / 𝑌)) | ||
| Theorem | subrgchr 33226 | If 𝐴 is a subring of 𝑅, then they have the same characteristic. (Contributed by Thierry Arnoux, 24-Feb-2018.) |
| ⊢ (𝐴 ∈ (SubRing‘𝑅) → (chr‘(𝑅 ↾s 𝐴)) = (chr‘𝑅)) | ||
| Theorem | rmfsupp2 33227* | 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 33228 | In a nonzero ring, a unit cannot be zero. (Contributed by Thierry Arnoux, 25-Apr-2025.) |
| ⊢ 𝑈 = (Unit‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ NzRing) & ⊢ (𝜑 → 𝑋 ∈ 𝑈) ⇒ ⊢ (𝜑 → 𝑋 ≠ 0 ) | ||
| Theorem | isunit2 33229* | Alternate definition of being a unit. (Contributed by Thierry Arnoux, 3-Aug-2025.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝑈 = (Unit‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 1 = (1r‘𝑅) ⇒ ⊢ (𝑋 ∈ 𝑈 ↔ (𝑋 ∈ 𝐵 ∧ (∃𝑢 ∈ 𝐵 (𝑋 · 𝑢) = 1 ∧ ∃𝑣 ∈ 𝐵 (𝑣 · 𝑋) = 1 ))) | ||
| Theorem | isunit3 33230* | Alternate definition of being a unit. (Contributed by Thierry Arnoux, 3-Aug-2025.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝑈 = (Unit‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 1 = (1r‘𝑅) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑅 ∈ Ring) ⇒ ⊢ (𝜑 → (𝑋 ∈ 𝑈 ↔ ∃𝑦 ∈ 𝐵 ((𝑋 · 𝑦) = 1 ∧ (𝑦 · 𝑋) = 1 ))) | ||
| Theorem | elrgspnlem1 33231* | Lemma for elrgspn 33235. (Contributed by Thierry Arnoux, 5-Oct-2025.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝑀 = (mulGrp‘𝑅) & ⊢ · = (.g‘𝑅) & ⊢ 𝑁 = (RingSpan‘𝑅) & ⊢ 𝐹 = {𝑓 ∈ (ℤ ↑m Word 𝐴) ∣ 𝑓 finSupp 0} & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝐴 ⊆ 𝐵) & ⊢ 𝑆 = ran (𝑔 ∈ 𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) ⇒ ⊢ (𝜑 → 𝑆 ∈ (SubGrp‘𝑅)) | ||
| Theorem | elrgspnlem2 33232* | Lemma for elrgspn 33235. (Contributed by Thierry Arnoux, 5-Oct-2025.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝑀 = (mulGrp‘𝑅) & ⊢ · = (.g‘𝑅) & ⊢ 𝑁 = (RingSpan‘𝑅) & ⊢ 𝐹 = {𝑓 ∈ (ℤ ↑m Word 𝐴) ∣ 𝑓 finSupp 0} & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝐴 ⊆ 𝐵) & ⊢ 𝑆 = ran (𝑔 ∈ 𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) ⇒ ⊢ (𝜑 → 𝑆 ∈ (SubRing‘𝑅)) | ||
| Theorem | elrgspnlem3 33233* | Lemma for elrgspn 33235. (Contributed by Thierry Arnoux, 5-Oct-2025.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝑀 = (mulGrp‘𝑅) & ⊢ · = (.g‘𝑅) & ⊢ 𝑁 = (RingSpan‘𝑅) & ⊢ 𝐹 = {𝑓 ∈ (ℤ ↑m Word 𝐴) ∣ 𝑓 finSupp 0} & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝐴 ⊆ 𝐵) & ⊢ 𝑆 = ran (𝑔 ∈ 𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) ⇒ ⊢ (𝜑 → 𝐴 ⊆ 𝑆) | ||
| Theorem | elrgspnlem4 33234* | Lemma for elrgspn 33235. (Contributed by Thierry Arnoux, 5-Oct-2025.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝑀 = (mulGrp‘𝑅) & ⊢ · = (.g‘𝑅) & ⊢ 𝑁 = (RingSpan‘𝑅) & ⊢ 𝐹 = {𝑓 ∈ (ℤ ↑m Word 𝐴) ∣ 𝑓 finSupp 0} & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝐴 ⊆ 𝐵) & ⊢ 𝑆 = ran (𝑔 ∈ 𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) ⇒ ⊢ (𝜑 → (𝑁‘𝐴) = 𝑆) | ||
| Theorem | elrgspn 33235* | 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 | irrednzr 33236 | A ring with an irreducible element cannot be the zero ring. (Contributed by Thierry Arnoux, 18-May-2025.) |
| ⊢ 𝐼 = (Irred‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝑋 ∈ 𝐼) ⇒ ⊢ (𝜑 → 𝑅 ∈ NzRing) | ||
| Theorem | 0ringsubrg 33237 | A subring of a zero ring is a zero ring. (Contributed by Thierry Arnoux, 5-Feb-2025.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → (♯‘𝐵) = 1) & ⊢ (𝜑 → 𝑆 ∈ (SubRing‘𝑅)) ⇒ ⊢ (𝜑 → (♯‘𝑆) = 1) | ||
| Theorem | 0ringcring 33238 | The zero ring is commutative. (Contributed by Thierry Arnoux, 18-May-2025.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → (♯‘𝐵) = 1) ⇒ ⊢ (𝜑 → 𝑅 ∈ CRing) | ||
| Syntax | cerl 33239 | Syntax for ring localization equivalence class operation. |
| class ~RL | ||
| Syntax | crloc 33240 | Syntax for ring localization operation. |
| class RLocal | ||
| Definition | df-erl 33241* | 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 33242* | 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 33243 | Ring localization is a proper operator, so it can be used with ovprc1 7469. (Contributed by Thierry Arnoux, 10-May-2025.) |
| ⊢ Rel dom RLocal | ||
| Theorem | erlval 33244* | 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 33245* | 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 33246 | Closure for the ring localization equivalence relation. (Contributed by Thierry Arnoux, 4-May-2025.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ ∼ = (𝑅 ~RL 𝑆) & ⊢ (𝜑 → 𝑆 ⊆ 𝐵) & ⊢ (𝜑 → 𝑈 ∼ 𝑉) ⇒ ⊢ (𝜑 → 𝑈 ∈ (𝐵 × 𝑆)) | ||
| Theorem | erlcl2 33247 | Closure for the ring localization equivalence relation. (Contributed by Thierry Arnoux, 4-May-2025.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ ∼ = (𝑅 ~RL 𝑆) & ⊢ (𝜑 → 𝑆 ⊆ 𝐵) & ⊢ (𝜑 → 𝑈 ∼ 𝑉) ⇒ ⊢ (𝜑 → 𝑉 ∈ (𝐵 × 𝑆)) | ||
| Theorem | erldi 33248* | 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 33249 | 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 33250 | 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 33251 | 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 33252* | Membership in the basis of a ring localization. (Contributed by Thierry Arnoux, 4-May-2025.) |
| ⊢ (𝜑 → 𝑋 ∈ ((𝐵 × 𝑆) / ∼ )) ⇒ ⊢ (𝜑 → ∃𝑎 ∈ 𝐵 ∃𝑏 ∈ 𝑆 𝑋 = [⟨𝑎, 𝑏⟩] ∼ ) | ||
| Theorem | rlocbas 33253 | The base set of a ring localization. (Contributed by Thierry Arnoux, 4-May-2025.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ − = (-g‘𝑅) & ⊢ 𝑊 = (𝐵 × 𝑆) & ⊢ 𝐿 = (𝑅 RLocal 𝑆) & ⊢ ∼ = (𝑅 ~RL 𝑆) & ⊢ (𝜑 → 𝑅 ∈ 𝑉) & ⊢ (𝜑 → 𝑆 ⊆ 𝐵) ⇒ ⊢ (𝜑 → (𝑊 / ∼ ) = (Base‘𝐿)) | ||
| Theorem | rlocaddval 33254 | 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 33255 | 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 33256 | 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 33257 | 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 33258 | 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 33259* | 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 33260 | 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 33261 | 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 | idomrcan 33262 | 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 33263 | Obsolete version of domnlcan 20737 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 33264 | Obsolete version of domnlcanb 20736 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 33265 | Obsolete version of idomrcan 33262 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 33266 | The multiplicative identity is a left-regular element. (Contributed by Thierry Arnoux, 6-May-2025.) |
| ⊢ 1 = (1r‘𝑅) & ⊢ 𝐸 = (RLReg‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ Ring) ⇒ ⊢ (𝜑 → 1 ∈ 𝐸) | ||
| Theorem | rrgsubm 33267 | 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 33268 | A subring of a domain is a domain. (Contributed by Thierry Arnoux, 18-May-2025.) |
| ⊢ (𝜑 → 𝑅 ∈ Domn) & ⊢ (𝜑 → 𝑆 ∈ (SubRing‘𝑅)) ⇒ ⊢ (𝜑 → (𝑅 ↾s 𝑆) ∈ Domn) | ||
| Theorem | subridom 33269 | A subring of an integral domain is an integral domain. (Contributed by Thierry Arnoux, 18-May-2025.) |
| ⊢ (𝜑 → 𝑅 ∈ IDomn) & ⊢ (𝜑 → 𝑆 ∈ (SubRing‘𝑅)) ⇒ ⊢ (𝜑 → (𝑅 ↾s 𝑆) ∈ IDomn) | ||
| Theorem | subrfld 33270 | A subring of a field is an integral domain. (Contributed by Thierry Arnoux, 18-May-2025.) |
| ⊢ (𝜑 → 𝑅 ∈ Field) & ⊢ (𝜑 → 𝑆 ∈ (SubRing‘𝑅)) ⇒ ⊢ (𝜑 → (𝑅 ↾s 𝑆) ∈ IDomn) | ||
| Syntax | ceuf 33271 | Declare the syntax for the Euclidean function index extractor. |
| class EuclF | ||
| Definition | df-euf 33272 | Define the Euclidean function. (Contributed by Thierry Arnoux, 22-Mar-2025.) Use its index-independent form eufid 33274 instead. (New usage is discouraged.) |
| ⊢ EuclF = Slot ;21 | ||
| Theorem | eufndx 33273 | Index value of the Euclidean function slot. Use ndxarg 17229. (Contributed by Thierry Arnoux, 22-Mar-2025.) (New usage is discouraged.) |
| ⊢ (EuclF‘ndx) = ;21 | ||
| Theorem | eufid 33274 | Utility theorem: index-independent form of df-euf 33272. (Contributed by Thierry Arnoux, 22-Mar-2025.) |
| ⊢ EuclF = Slot (EuclF‘ndx) | ||
| Syntax | cedom 33275 | Declare the syntax for the Euclidean Domain. |
| class EDomn | ||
| Definition | df-edom 33276* | Define Euclidean Domains. (Contributed by Thierry Arnoux, 22-Mar-2025.) |
| ⊢ EDomn = {𝑑 ∈ IDomn ∣ [(EuclF‘𝑑) / 𝑒][(Base‘𝑑) / 𝑣](Fun 𝑒 ∧ (𝑒 “ (𝑣 ∖ {(0g‘𝑑)})) ⊆ (0[,)+∞) ∧ ∀𝑎 ∈ 𝑣 ∀𝑏 ∈ (𝑣 ∖ {(0g‘𝑑)})∃𝑞 ∈ 𝑣 ∃𝑟 ∈ 𝑣 (𝑎 = ((𝑏(.r‘𝑑)𝑞)(+g‘𝑑)𝑟) ∧ (𝑟 = (0g‘𝑑) ∨ (𝑒‘𝑟) < (𝑒‘𝑏))))} | ||
| Theorem | ringinveu 33277 | 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 33278* | 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 33279 | 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 | sdrgdvcl 33280 | 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 33281 | 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 33282 | 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 33283 | Syntax for the field of fractions of a given integral domain. |
| class Frac | ||
| Definition | df-frac 33284 | Define the field of fractions of a given integral domain. (Contributed by Thierry Arnoux, 26-Apr-2025.) |
| ⊢ Frac = (𝑟 ∈ V ↦ (𝑟 RLocal (RLReg‘𝑟))) | ||
| Theorem | fracval 33285 | Value of the field of fractions. (Contributed by Thierry Arnoux, 5-May-2025.) |
| ⊢ ( Frac ‘𝑅) = (𝑅 RLocal (RLReg‘𝑅)) | ||
| Theorem | fracbas 33286 | The base of the field of fractions. (Contributed by Thierry Arnoux, 10-May-2025.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝐸 = (RLReg‘𝑅) & ⊢ 𝐹 = ( Frac ‘𝑅) & ⊢ ∼ = (𝑅 ~RL 𝐸) ⇒ ⊢ ((𝐵 × 𝐸) / ∼ ) = (Base‘𝐹) | ||
| Theorem | fracerl 33287 | 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 33288* | 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 ‘𝑅)))) | ||
| Theorem | fracfld 33289 | The field of fractions of an integral domain is a field. (Contributed by Thierry Arnoux, 4-May-2025.) |
| ⊢ (𝜑 → 𝑅 ∈ IDomn) ⇒ ⊢ (𝜑 → ( Frac ‘𝑅) ∈ Field) | ||
| Theorem | idomsubr 33290* | Every integral domain is isomorphic with a subring of some field. (Proposed by Gerard Lang, 10-May-2025.) (Contributed by Thierry Arnoux, 10-May-2025.) |
| ⊢ (𝜑 → 𝑅 ∈ IDomn) ⇒ ⊢ (𝜑 → ∃𝑓 ∈ Field ∃𝑠 ∈ (SubRing‘𝑓)𝑅 ≃𝑟 (𝑓 ↾s 𝑠)) | ||
| Syntax | cfldgen 33291 | Syntax for a function generating sub-fields. |
| class fldGen | ||
| Definition | df-fldgen 33292* | Define a function generating the smallest sub-division-ring of a given ring containing a given set. If the base structure is a division ring, then this is also a division ring (see fldgensdrg 33295). If the base structure is a field, this is a subfield (see fldgenfld 33301 and fldsdrgfld 20815). In general this will be used in the context of fields, hence the name fldGen. (Contributed by Saveliy Skresanov and Thierry Arnoux, 9-Jan-2025.) |
| ⊢ fldGen = (𝑓 ∈ V, 𝑠 ∈ V ↦ ∩ {𝑎 ∈ (SubDRing‘𝑓) ∣ 𝑠 ⊆ 𝑎}) | ||
| Theorem | fldgenval 33293* | Value of the field generating function: (𝐹 fldGen 𝑆) is the smallest sub-division-ring of 𝐹 containing 𝑆. (Contributed by Thierry Arnoux, 11-Jan-2025.) |
| ⊢ 𝐵 = (Base‘𝐹) & ⊢ (𝜑 → 𝐹 ∈ DivRing) & ⊢ (𝜑 → 𝑆 ⊆ 𝐵) ⇒ ⊢ (𝜑 → (𝐹 fldGen 𝑆) = ∩ {𝑎 ∈ (SubDRing‘𝐹) ∣ 𝑆 ⊆ 𝑎}) | ||
| Theorem | fldgenssid 33294 | The field generated by a set of elements contains those elements. See lspssid 21000. (Contributed by Thierry Arnoux, 15-Jan-2025.) |
| ⊢ 𝐵 = (Base‘𝐹) & ⊢ (𝜑 → 𝐹 ∈ DivRing) & ⊢ (𝜑 → 𝑆 ⊆ 𝐵) ⇒ ⊢ (𝜑 → 𝑆 ⊆ (𝐹 fldGen 𝑆)) | ||
| Theorem | fldgensdrg 33295 | A generated subfield is a sub-division-ring. (Contributed by Thierry Arnoux, 11-Jan-2025.) |
| ⊢ 𝐵 = (Base‘𝐹) & ⊢ (𝜑 → 𝐹 ∈ DivRing) & ⊢ (𝜑 → 𝑆 ⊆ 𝐵) ⇒ ⊢ (𝜑 → (𝐹 fldGen 𝑆) ∈ (SubDRing‘𝐹)) | ||
| Theorem | fldgenssv 33296 | A generated subfield is a subset of the field's base. (Contributed by Thierry Arnoux, 25-Feb-2025.) |
| ⊢ 𝐵 = (Base‘𝐹) & ⊢ (𝜑 → 𝐹 ∈ DivRing) & ⊢ (𝜑 → 𝑆 ⊆ 𝐵) ⇒ ⊢ (𝜑 → (𝐹 fldGen 𝑆) ⊆ 𝐵) | ||
| Theorem | fldgenss 33297 | Generated subfields preserve subset ordering. ( see lspss 20999 and spanss 31376) (Contributed by Thierry Arnoux, 15-Jan-2025.) |
| ⊢ 𝐵 = (Base‘𝐹) & ⊢ (𝜑 → 𝐹 ∈ DivRing) & ⊢ (𝜑 → 𝑆 ⊆ 𝐵) & ⊢ (𝜑 → 𝑇 ⊆ 𝑆) ⇒ ⊢ (𝜑 → (𝐹 fldGen 𝑇) ⊆ (𝐹 fldGen 𝑆)) | ||
| Theorem | fldgenidfld 33298 | The subfield generated by a subfield is the subfield itself. (Contributed by Thierry Arnoux, 15-Jan-2025.) |
| ⊢ 𝐵 = (Base‘𝐹) & ⊢ (𝜑 → 𝐹 ∈ DivRing) & ⊢ (𝜑 → 𝑆 ∈ (SubDRing‘𝐹)) ⇒ ⊢ (𝜑 → (𝐹 fldGen 𝑆) = 𝑆) | ||
| Theorem | fldgenssp 33299 | The field generated by a set of elements in a division ring is contained in any sub-division-ring which contains those elements. (Contributed by Thierry Arnoux, 25-Feb-2025.) |
| ⊢ 𝐵 = (Base‘𝐹) & ⊢ (𝜑 → 𝐹 ∈ DivRing) & ⊢ (𝜑 → 𝑆 ∈ (SubDRing‘𝐹)) & ⊢ (𝜑 → 𝑇 ⊆ 𝑆) ⇒ ⊢ (𝜑 → (𝐹 fldGen 𝑇) ⊆ 𝑆) | ||
| Theorem | fldgenid 33300 | The subfield of a field 𝐹 generated by the whole base set of 𝐹 is 𝐹 itself. (Contributed by Thierry Arnoux, 11-Jan-2025.) |
| ⊢ 𝐵 = (Base‘𝐹) & ⊢ (𝜑 → 𝐹 ∈ DivRing) ⇒ ⊢ (𝜑 → (𝐹 fldGen 𝐵) = 𝐵) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |