HomeTheorem List (p. 339 of 510)
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. 339 of 510) | < 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-31513) |
Hilbert Space Explorer
(31514-33036) |
Users' Mathboxes
(33037-50959) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | elrgspnsubrunlem1 33801* | Lemma for elrgspnsubrun 33803, 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 33802* | Lemma for elrgspnsubrun 33803, 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 33803* | 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 33804 | A ring with an irreducible element cannot be the zero ring. (Contributed by Thierry Arnoux, 18-May-2025.) |
| ⊢ 𝐼 = (Irred‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝑋 ∈ 𝐼) ⇒ ⊢ (𝜑 → 𝑅 ∈ NzRing) | ||
| Theorem | 0ringsubrg 33805 | A subring of a zero ring is a zero ring. (Contributed by Thierry Arnoux, 5-Feb-2025.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → (♯‘𝐵) = 1) & ⊢ (𝜑 → 𝑆 ∈ (SubRing‘𝑅)) ⇒ ⊢ (𝜑 → (♯‘𝑆) = 1) | ||
| Theorem | 0ringcring 33806 | The zero ring is commutative. (Contributed by Thierry Arnoux, 18-May-2025.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → (♯‘𝐵) = 1) ⇒ ⊢ (𝜑 → 𝑅 ∈ CRing) | ||
| Syntax | cerl 33807 | Syntax for ring localization equivalence class operation. |
| class ~RL | ||
| Syntax | crloc 33808 | Syntax for ring localization operation. |
| class RLocal | ||
| Definition | df-erl 33809* | 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 33810* | 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 33811 | Ring localization is a proper operator, so it can be used with ovprc1 7457. (Contributed by Thierry Arnoux, 10-May-2025.) |
| ⊢ Rel dom RLocal | ||
| Theorem | erlval 33812* | 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 33813* | 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 33814 | Closure for the ring localization equivalence relation. (Contributed by Thierry Arnoux, 4-May-2025.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ ∼ = (𝑅 ~RL 𝑆) & ⊢ (𝜑 → 𝑆 ⊆ 𝐵) & ⊢ (𝜑 → 𝑈 ∼ 𝑉) ⇒ ⊢ (𝜑 → 𝑈 ∈ (𝐵 × 𝑆)) | ||
| Theorem | erlcl2 33815 | Closure for the ring localization equivalence relation. (Contributed by Thierry Arnoux, 4-May-2025.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ ∼ = (𝑅 ~RL 𝑆) & ⊢ (𝜑 → 𝑆 ⊆ 𝐵) & ⊢ (𝜑 → 𝑈 ∼ 𝑉) ⇒ ⊢ (𝜑 → 𝑉 ∈ (𝐵 × 𝑆)) | ||
| Theorem | erldi 33816* | 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 33817 | 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 33818 | 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 33819 | 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 | erld2 33820* | Main property of the ring localization equivalence relation. (Contributed by Thierry Arnoux, 4-May-2025.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ ∼ = (𝑅 ~RL 𝑆) & ⊢ · = (.r‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝑆 ∈ (SubMnd‘(mulGrp‘𝑅))) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝑆) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) & ⊢ (𝜑 → 𝑊 ∈ 𝑆) & ⊢ (𝜑 → [⟨𝑋, 𝑌⟩] ∼ = [⟨𝑍, 𝑊⟩] ∼ ) ⇒ ⊢ (𝜑 → ∃𝑡 ∈ 𝑆 (𝑡 · (𝑋 · 𝑊)) = (𝑡 · (𝑍 · 𝑌))) | ||
| Theorem | elrlocbasi 33821* | Membership in the basis of a ring localization. (Contributed by Thierry Arnoux, 4-May-2025.) |
| ⊢ (𝜑 → 𝑋 ∈ ((𝐵 × 𝑆) / ∼ )) ⇒ ⊢ (𝜑 → ∃𝑎 ∈ 𝐵 ∃𝑏 ∈ 𝑆 𝑋 = [⟨𝑎, 𝑏⟩] ∼ ) | ||
| Theorem | rlocbas 33822 | The base set of a ring localization. (Contributed by Thierry Arnoux, 4-May-2025.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ − = (-g‘𝑅) & ⊢ 𝑊 = (𝐵 × 𝑆) & ⊢ 𝐿 = (𝑅 RLocal 𝑆) & ⊢ ∼ = (𝑅 ~RL 𝑆) & ⊢ (𝜑 → 𝑅 ∈ 𝑉) & ⊢ (𝜑 → 𝑆 ⊆ 𝐵) ⇒ ⊢ (𝜑 → (𝑊 / ∼ ) = (Base‘𝐿)) | ||
| Theorem | rlocaddval 33823 | 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 33824 | 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 33825 | 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 33826 | 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 33827 | 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 33828* | 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 | rlocinvunit 33829 | In the localization of a ring 𝑅 at 𝑆, inverses of elements of 𝑆 are units. (Contributed by Thierry Arnoux, 6-Jun-2026.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ 1 = (1r‘𝑅) & ⊢ ∼ = (𝑅 ~RL 𝑆) & ⊢ 𝐿 = (𝑅 RLocal 𝑆) & ⊢ 𝑊 = (Unit‘𝐿) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝑆 ∈ (SubMnd‘(mulGrp‘𝑅))) & ⊢ (𝜑 → 𝑄 ∈ 𝑆) ⇒ ⊢ (𝜑 → [⟨ 1 , 𝑄⟩] ∼ ∈ 𝑊) | ||
| Theorem | rlocisunit 33830* | Characterize the units of the localization 𝐿 of a ring 𝑅 at 𝑆 as the elements with a "numerator" 𝑃 in the saturation 𝑇 of 𝑆. (Contributed by Thierry Arnoux, 6-Jun-2026.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 𝐿 = (𝑅 RLocal 𝑆) & ⊢ 𝑊 = (Unit‘𝐿) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝑆 ∈ (SubMnd‘(mulGrp‘𝑅))) & ⊢ ∼ = (𝑅 ~RL 𝑆) & ⊢ (𝜑 → 𝑃 ∈ 𝐵) & ⊢ (𝜑 → 𝑄 ∈ 𝑆) & ⊢ 𝑇 = {𝑟 ∈ 𝐵 ∣ ∃𝑠 ∈ 𝐵 (𝑟 · 𝑠) ∈ 𝑆} ⇒ ⊢ (𝜑 → ([⟨𝑃, 𝑄⟩] ∼ ∈ 𝑊 ↔ 𝑃 ∈ 𝑇)) | ||
| Theorem | domnmuln0rd 33831 | 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 33832 | 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 33833 | A product over a domain is zero exactly when one of the factors is zero. Generalization of domneq0 20953 for any number of factors. See also domnprodn0 33832. (Contributed by Thierry Arnoux, 15-Feb-2026.) |
| ⊢ 𝑀 = (mulGrp‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ IDomn) & ⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ (𝜑 → 𝐹:𝐴⟶𝐵) ⇒ ⊢ (𝜑 → ((𝑀 Σg 𝐹) = 0 ↔ 0 ∈ ran 𝐹)) | ||
| Theorem | domnpropd 33834* | 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 33835* | If two structures have the same components (properties), one is a integral domain iff the other one is. See also domnpropd 33834. (Contributed by Thierry Arnoux, 13-Oct-2025.) |
| ⊢ (𝜑 → 𝐵 = (Base‘𝐾)) & ⊢ (𝜑 → 𝐵 = (Base‘𝐿)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(+g‘𝐾)𝑦) = (𝑥(+g‘𝐿)𝑦)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(.r‘𝐾)𝑦) = (𝑥(.r‘𝐿)𝑦)) ⇒ ⊢ (𝜑 → (𝐾 ∈ IDomn ↔ 𝐿 ∈ IDomn)) | ||
| Theorem | idomrcan 33836 | 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 | 1rrg 33837 | The multiplicative identity is a left-regular element. (Contributed by Thierry Arnoux, 6-May-2025.) |
| ⊢ 1 = (1r‘𝑅) & ⊢ 𝐸 = (RLReg‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ Ring) ⇒ ⊢ (𝜑 → 1 ∈ 𝐸) | ||
| Theorem | rrgsubm 33838 | 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 33839 | A subring of a domain is a domain. (Contributed by Thierry Arnoux, 18-May-2025.) |
| ⊢ (𝜑 → 𝑅 ∈ Domn) & ⊢ (𝜑 → 𝑆 ∈ (SubRing‘𝑅)) ⇒ ⊢ (𝜑 → (𝑅 ↾s 𝑆) ∈ Domn) | ||
| Theorem | subridom 33840 | A subring of an integral domain is an integral domain. (Contributed by Thierry Arnoux, 18-May-2025.) |
| ⊢ (𝜑 → 𝑅 ∈ IDomn) & ⊢ (𝜑 → 𝑆 ∈ (SubRing‘𝑅)) ⇒ ⊢ (𝜑 → (𝑅 ↾s 𝑆) ∈ IDomn) | ||
| Theorem | subrfld 33841 | A subring of a field is an integral domain. (Contributed by Thierry Arnoux, 18-May-2025.) |
| ⊢ (𝜑 → 𝑅 ∈ Field) & ⊢ (𝜑 → 𝑆 ∈ (SubRing‘𝑅)) ⇒ ⊢ (𝜑 → (𝑅 ↾s 𝑆) ∈ IDomn) | ||
| Theorem | ricnzr1 33842 | A ring isomorphism maps a nonzero ring to a nonzero ring. (Contributed by Thierry Arnoux, 4-May-2026.) |
| ⊢ ((𝑅 ≃𝑟 𝑆 ∧ 𝑅 ∈ NzRing) → 𝑆 ∈ NzRing) | ||
| Theorem | ricdomn1 33843 | A ring isomorphism maps a domain to a domain. (Contributed by Thierry Arnoux, 4-May-2026.) |
| ⊢ ((𝑅 ≃𝑟 𝑆 ∧ 𝑅 ∈ Domn) → 𝑆 ∈ Domn) | ||
| Theorem | ricdomn 33844 | A ring is a domain if and only if an isomorphic ring is a domain. (Contributed by Thierry Arnoux, 4-May-2026.) |
| ⊢ (𝑅 ≃𝑟 𝑆 → (𝑅 ∈ Domn ↔ 𝑆 ∈ Domn)) | ||
| Syntax | ceuf 33845 | Declare the syntax for the Euclidean function index extractor. |
| class EuclF | ||
| Definition | df-euf 33846 | Define the Euclidean function. (Contributed by Thierry Arnoux, 22-Mar-2025.) Use its index-independent form eufid 33848 instead. (New usage is discouraged.) |
| ⊢ EuclF = Slot ;21 | ||
| Theorem | eufndx 33847 | Index value of the Euclidean function slot. Use ndxarg 17367. (Contributed by Thierry Arnoux, 22-Mar-2025.) (New usage is discouraged.) |
| ⊢ (EuclF‘ndx) = ;21 | ||
| Theorem | eufid 33848 | Utility theorem: index-independent form of df-euf 33846. (Contributed by Thierry Arnoux, 22-Mar-2025.) |
| ⊢ EuclF = Slot (EuclF‘ndx) | ||
| Syntax | cedom 33849 | Declare the syntax for the Euclidean Domain. |
| class EDomn | ||
| Definition | df-edom 33850* | Define Euclidean Domains. (Contributed by Thierry Arnoux, 22-Mar-2025.) |
| ⊢ EDomn = {𝑑 ∈ IDomn ∣ [(EuclF‘𝑑) / 𝑒][(Base‘𝑑) / 𝑣](Fun 𝑒 ∧ (𝑒 “ (𝑣 ∖ {(0g‘𝑑)})) ⊆ (0[,)+∞) ∧ ∀𝑎 ∈ 𝑣 ∀𝑏 ∈ (𝑣 ∖ {(0g‘𝑑)})∃𝑞 ∈ 𝑣 ∃𝑟 ∈ 𝑣 (𝑎 = ((𝑏(.r‘𝑑)𝑞)(+g‘𝑑)𝑟) ∧ (𝑟 = (0g‘𝑑) ∨ (𝑒‘𝑟) < (𝑒‘𝑏))))} | ||
| Theorem | rndrhmcl 33851 | 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 33852 | The field of rational numbers is a field. (Contributed by Thierry Arnoux, 19-Oct-2025.) |
| ⊢ 𝑄 = (ℂfld ↾s ℚ) ⇒ ⊢ 𝑄 ∈ Field | ||
| Theorem | subsdrg 33853 | A subring of a sub-division-ring is a sub-division-ring. See also subsubrg 20843. (Contributed by Thierry Arnoux, 26-Oct-2025.) |
| ⊢ 𝑆 = (𝑅 ↾s 𝐴) & ⊢ (𝜑 → 𝐴 ∈ (SubDRing‘𝑅)) ⇒ ⊢ (𝜑 → (𝐵 ∈ (SubDRing‘𝑆) ↔ (𝐵 ∈ (SubDRing‘𝑅) ∧ 𝐵 ⊆ 𝐴))) | ||
| Theorem | sdrgdvcl 33854 | 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 33855 | 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 33856 | 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 33857 | Syntax for the field of fractions of a given integral domain. |
| class Frac | ||
| Definition | df-frac 33858 | Define the field of fractions of a given integral domain. (Contributed by Thierry Arnoux, 26-Apr-2025.) |
| ⊢ Frac = (𝑟 ∈ V ↦ (𝑟 RLocal (RLReg‘𝑟))) | ||
| Theorem | fracval 33859 | Value of the field of fractions. (Contributed by Thierry Arnoux, 5-May-2025.) |
| ⊢ ( Frac ‘𝑅) = (𝑅 RLocal (RLReg‘𝑅)) | ||
| Theorem | fracbas 33860 | The base of the field of fractions. (Contributed by Thierry Arnoux, 10-May-2025.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝐸 = (RLReg‘𝑅) & ⊢ 𝐹 = ( Frac ‘𝑅) & ⊢ ∼ = (𝑅 ~RL 𝐸) ⇒ ⊢ ((𝐵 × 𝐸) / ∼ ) = (Base‘𝐹) | ||
| Theorem | fracerl 33861 | 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 33862* | 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 33863 | The field of fractions of an integral domain is a field. (Contributed by Thierry Arnoux, 4-May-2025.) |
| ⊢ (𝜑 → 𝑅 ∈ IDomn) ⇒ ⊢ (𝜑 → ( Frac ‘𝑅) ∈ Field) | ||
| Theorem | idomsubr 33864* | 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 33865 | Syntax for a function generating sub-fields. |
| class fldGen | ||
| Definition | df-fldgen 33866* | 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 33869). If the base structure is a field, this is a subfield (see fldgenfld 33875 and fldsdrgfld 21048). 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 33867* | 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 33868 | The field generated by a set of elements contains those elements. See lspssid 21253. (Contributed by Thierry Arnoux, 15-Jan-2025.) |
| ⊢ 𝐵 = (Base‘𝐹) & ⊢ (𝜑 → 𝐹 ∈ DivRing) & ⊢ (𝜑 → 𝑆 ⊆ 𝐵) ⇒ ⊢ (𝜑 → 𝑆 ⊆ (𝐹 fldGen 𝑆)) | ||
| Theorem | fldgensdrg 33869 | A generated subfield is a sub-division-ring. (Contributed by Thierry Arnoux, 11-Jan-2025.) |
| ⊢ 𝐵 = (Base‘𝐹) & ⊢ (𝜑 → 𝐹 ∈ DivRing) & ⊢ (𝜑 → 𝑆 ⊆ 𝐵) ⇒ ⊢ (𝜑 → (𝐹 fldGen 𝑆) ∈ (SubDRing‘𝐹)) | ||
| Theorem | fldgenssv 33870 | A generated subfield is a subset of the field's base. (Contributed by Thierry Arnoux, 25-Feb-2025.) |
| ⊢ 𝐵 = (Base‘𝐹) & ⊢ (𝜑 → 𝐹 ∈ DivRing) & ⊢ (𝜑 → 𝑆 ⊆ 𝐵) ⇒ ⊢ (𝜑 → (𝐹 fldGen 𝑆) ⊆ 𝐵) | ||
| Theorem | fldgenss 33871 | Generated subfields preserve subset ordering. ( see lspss 21252 and spanss 31943) (Contributed by Thierry Arnoux, 15-Jan-2025.) |
| ⊢ 𝐵 = (Base‘𝐹) & ⊢ (𝜑 → 𝐹 ∈ DivRing) & ⊢ (𝜑 → 𝑆 ⊆ 𝐵) & ⊢ (𝜑 → 𝑇 ⊆ 𝑆) ⇒ ⊢ (𝜑 → (𝐹 fldGen 𝑇) ⊆ (𝐹 fldGen 𝑆)) | ||
| Theorem | fldgenidfld 33872 | The subfield generated by a subfield is the subfield itself. (Contributed by Thierry Arnoux, 15-Jan-2025.) |
| ⊢ 𝐵 = (Base‘𝐹) & ⊢ (𝜑 → 𝐹 ∈ DivRing) & ⊢ (𝜑 → 𝑆 ∈ (SubDRing‘𝐹)) ⇒ ⊢ (𝜑 → (𝐹 fldGen 𝑆) = 𝑆) | ||
| Theorem | fldgenssp 33873 | 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 33874 | The subfield of a field 𝐹 generated by the whole base set of 𝐹 is 𝐹 itself. (Contributed by Thierry Arnoux, 11-Jan-2025.) |
| ⊢ 𝐵 = (Base‘𝐹) & ⊢ (𝜑 → 𝐹 ∈ DivRing) ⇒ ⊢ (𝜑 → (𝐹 fldGen 𝐵) = 𝐵) | ||
| Theorem | fldgenfld 33875 | A generated subfield is a field. (Contributed by Thierry Arnoux, 11-Jan-2025.) |
| ⊢ 𝐵 = (Base‘𝐹) & ⊢ (𝜑 → 𝐹 ∈ Field) & ⊢ (𝜑 → 𝑆 ⊆ 𝐵) ⇒ ⊢ (𝜑 → (𝐹 ↾s (𝐹 fldGen 𝑆)) ∈ Field) | ||
| Theorem | primefldgen1 33876 | The prime field of a division ring is the subfield generated by the multiplicative identity element. In general, we should write "prime division ring", but since most later usages are in the case where the ambient ring is commutative, we keep the term "prime field". (Contributed by Thierry Arnoux, 11-Jan-2025.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ 1 = (1r‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ DivRing) ⇒ ⊢ (𝜑 → ∩ (SubDRing‘𝑅) = (𝑅 fldGen { 1 })) | ||
| Theorem | 1fldgenq 33877 | The field of rational numbers ℚ is generated by 1 in ℂfld, that is, ℚ is the prime field of ℂfld. (Contributed by Thierry Arnoux, 15-Jan-2025.) |
| ⊢ (ℂfld fldGen {1}) = ℚ | ||
| Theorem | rhmdvd 33878 | A ring homomorphism preserves ratios. (Contributed by Thierry Arnoux, 22-Oct-2017.) |
| ⊢ 𝑈 = (Unit‘𝑆) & ⊢ 𝑋 = (Base‘𝑅) & ⊢ / = (/r‘𝑆) & ⊢ · = (.r‘𝑅) ⇒ ⊢ ((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋) ∧ ((𝐹‘𝐵) ∈ 𝑈 ∧ (𝐹‘𝐶) ∈ 𝑈)) → ((𝐹‘𝐴) / (𝐹‘𝐵)) = ((𝐹‘(𝐴 · 𝐶)) / (𝐹‘(𝐵 · 𝐶)))) | ||
| Theorem | kerunit 33879 | If a unit element lies in the kernel of a ring homomorphism, then 0 = 1, i.e. the target ring is the zero ring. (Contributed by Thierry Arnoux, 24-Oct-2017.) |
| ⊢ 𝑈 = (Unit‘𝑅) & ⊢ 0 = (0g‘𝑆) & ⊢ 1 = (1r‘𝑆) ⇒ ⊢ ((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ (𝑈 ∩ (◡𝐹 “ { 0 })) ≠ ∅) → 1 = 0 ) | ||
| Syntax | cresv 33880 | Extend class notation with the scalar restriction operation. |
| class ↾v | ||
| Definition | df-resv 33881* | Define an operator to restrict the scalar field component of an extended structure. (Contributed by Thierry Arnoux, 5-Sep-2018.) |
| ⊢ ↾v = (𝑤 ∈ V, 𝑥 ∈ V ↦ if((Base‘(Scalar‘𝑤)) ⊆ 𝑥, 𝑤, (𝑤 sSet ⟨(Scalar‘ndx), ((Scalar‘𝑤) ↾s 𝑥)⟩))) | ||
| Theorem | reldmresv 33882 | The scalar restriction is a proper operator, so it can be used with ovprc1 7457. (Contributed by Thierry Arnoux, 6-Sep-2018.) |
| ⊢ Rel dom ↾v | ||
| Theorem | resvval 33883 | Value of structure restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.) |
| ⊢ 𝑅 = (𝑊 ↾v 𝐴) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐵 = (Base‘𝐹) ⇒ ⊢ ((𝑊 ∈ 𝑋 ∧ 𝐴 ∈ 𝑌) → 𝑅 = if(𝐵 ⊆ 𝐴, 𝑊, (𝑊 sSet ⟨(Scalar‘ndx), (𝐹 ↾s 𝐴)⟩))) | ||
| Theorem | resvid2 33884 | General behavior of trivial restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.) |
| ⊢ 𝑅 = (𝑊 ↾v 𝐴) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐵 = (Base‘𝐹) ⇒ ⊢ ((𝐵 ⊆ 𝐴 ∧ 𝑊 ∈ 𝑋 ∧ 𝐴 ∈ 𝑌) → 𝑅 = 𝑊) | ||
| Theorem | resvval2 33885 | Value of nontrivial structure restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.) |
| ⊢ 𝑅 = (𝑊 ↾v 𝐴) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐵 = (Base‘𝐹) ⇒ ⊢ ((¬ 𝐵 ⊆ 𝐴 ∧ 𝑊 ∈ 𝑋 ∧ 𝐴 ∈ 𝑌) → 𝑅 = (𝑊 sSet ⟨(Scalar‘ndx), (𝐹 ↾s 𝐴)⟩)) | ||
| Theorem | resvsca 33886 | Base set of a structure restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.) |
| ⊢ 𝑅 = (𝑊 ↾v 𝐴) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐵 = (Base‘𝐹) ⇒ ⊢ (𝐴 ∈ 𝑉 → (𝐹 ↾s 𝐴) = (Scalar‘𝑅)) | ||
| Theorem | resvlem 33887 | Other elements of a scalar restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.) (Revised by AV, 31-Oct-2024.) |
| ⊢ 𝑅 = (𝑊 ↾v 𝐴) & ⊢ 𝐶 = (𝐸‘𝑊) & ⊢ 𝐸 = Slot (𝐸‘ndx) & ⊢ (𝐸‘ndx) ≠ (Scalar‘ndx) ⇒ ⊢ (𝐴 ∈ 𝑉 → 𝐶 = (𝐸‘𝑅)) | ||
| Theorem | resvbas 33888 | Base is unaffected by scalar restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.) (Revised by AV, 31-Oct-2024.) |
| ⊢ 𝐻 = (𝐺 ↾v 𝐴) & ⊢ 𝐵 = (Base‘𝐺) ⇒ ⊢ (𝐴 ∈ 𝑉 → 𝐵 = (Base‘𝐻)) | ||
| Theorem | resvplusg 33889 | +g is unaffected by scalar restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.) (Revised by AV, 31-Oct-2024.) |
| ⊢ 𝐻 = (𝐺 ↾v 𝐴) & ⊢ + = (+g‘𝐺) ⇒ ⊢ (𝐴 ∈ 𝑉 → + = (+g‘𝐻)) | ||
| Theorem | resvvsca 33890 | ·𝑠 is unaffected by scalar restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.) (Proof shortened by AV, 31-Oct-2024.) |
| ⊢ 𝐻 = (𝐺 ↾v 𝐴) & ⊢ · = ( ·𝑠 ‘𝐺) ⇒ ⊢ (𝐴 ∈ 𝑉 → · = ( ·𝑠 ‘𝐻)) | ||
| Theorem | resvmulr 33891 | .r is unaffected by scalar restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.) (Revised by AV, 31-Oct-2024.) |
| ⊢ 𝐻 = (𝐺 ↾v 𝐴) & ⊢ · = (.r‘𝐺) ⇒ ⊢ (𝐴 ∈ 𝑉 → · = (.r‘𝐻)) | ||
| Theorem | resv0g 33892 | 0g is unaffected by scalar restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.) |
| ⊢ 𝐻 = (𝐺 ↾v 𝐴) & ⊢ 0 = (0g‘𝐺) ⇒ ⊢ (𝐴 ∈ 𝑉 → 0 = (0g‘𝐻)) | ||
| Theorem | resv1r 33893 | 1r is unaffected by scalar restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.) |
| ⊢ 𝐻 = (𝐺 ↾v 𝐴) & ⊢ 1 = (1r‘𝐺) ⇒ ⊢ (𝐴 ∈ 𝑉 → 1 = (1r‘𝐻)) | ||
| Theorem | resvcmn 33894 | Scalar restriction preserves commutative monoids. (Contributed by Thierry Arnoux, 6-Sep-2018.) |
| ⊢ 𝐻 = (𝐺 ↾v 𝐴) ⇒ ⊢ (𝐴 ∈ 𝑉 → (𝐺 ∈ CMnd ↔ 𝐻 ∈ CMnd)) | ||
| Theorem | gzcrng 33895 | The gaussian integers form a commutative ring. (Contributed by Thierry Arnoux, 18-Mar-2018.) |
| ⊢ (ℂfld ↾s ℤ[i]) ∈ CRing | ||
| Theorem | cnfldfld 33896 | The complex numbers form a field. (Contributed by Thierry Arnoux, 6-Jul-2025.) |
| ⊢ ℂfld ∈ Field | ||
| Theorem | reofld 33897 | The real numbers form an ordered field. (Contributed by Thierry Arnoux, 21-Jan-2018.) |
| ⊢ ℝfld ∈ oField | ||
| Theorem | nn0omnd 33898 | The nonnegative integers form an ordered monoid. (Contributed by Thierry Arnoux, 23-Mar-2018.) |
| ⊢ (ℂfld ↾s ℕ0) ∈ oMnd | ||
| Theorem | gsumind 33899 | The group sum of an indicator function of the set 𝐴 gives the size of 𝐴. (Contributed by Thierry Arnoux, 18-Jan-2026.) |
| ⊢ (𝜑 → 𝑂 ∈ 𝑉) & ⊢ (𝜑 → 𝐴 ⊆ 𝑂) & ⊢ (𝜑 → 𝐴 ∈ Fin) ⇒ ⊢ (𝜑 → (ℂfld Σg ((𝟭‘𝑂)‘𝐴)) = (♯‘𝐴)) | ||
| Theorem | rearchi 33900 | The field of the real numbers is Archimedean. See also arch 12596. (Contributed by Thierry Arnoux, 9-Apr-2018.) |
| ⊢ ℝfld ∈ Archi | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |