HomeTheorem List (p. 333 of 498)
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 498) | < 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-30880) |
Hilbert Space Explorer
(30881-32403) |
Users' Mathboxes
(32404-49791) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | 0ringsubrg 33201 | A subring of a zero ring is a zero ring. (Contributed by Thierry Arnoux, 5-Feb-2025.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → (♯‘𝐵) = 1) & ⊢ (𝜑 → 𝑆 ∈ (SubRing‘𝑅)) ⇒ ⊢ (𝜑 → (♯‘𝑆) = 1) | ||
| Theorem | 0ringcring 33202 | The zero ring is commutative. (Contributed by Thierry Arnoux, 18-May-2025.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → (♯‘𝐵) = 1) ⇒ ⊢ (𝜑 → 𝑅 ∈ CRing) | ||
| Syntax | cerl 33203 | Syntax for ring localization equivalence class operation. |
| class ~RL | ||
| Syntax | crloc 33204 | Syntax for ring localization operation. |
| class RLocal | ||
| Definition | df-erl 33205* | 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 33206* | 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 33207 | Ring localization is a proper operator, so it can be used with ovprc1 7392. (Contributed by Thierry Arnoux, 10-May-2025.) |
| ⊢ Rel dom RLocal | ||
| Theorem | erlval 33208* | 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 33209* | 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 33210 | Closure for the ring localization equivalence relation. (Contributed by Thierry Arnoux, 4-May-2025.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ ∼ = (𝑅 ~RL 𝑆) & ⊢ (𝜑 → 𝑆 ⊆ 𝐵) & ⊢ (𝜑 → 𝑈 ∼ 𝑉) ⇒ ⊢ (𝜑 → 𝑈 ∈ (𝐵 × 𝑆)) | ||
| Theorem | erlcl2 33211 | Closure for the ring localization equivalence relation. (Contributed by Thierry Arnoux, 4-May-2025.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ ∼ = (𝑅 ~RL 𝑆) & ⊢ (𝜑 → 𝑆 ⊆ 𝐵) & ⊢ (𝜑 → 𝑈 ∼ 𝑉) ⇒ ⊢ (𝜑 → 𝑉 ∈ (𝐵 × 𝑆)) | ||
| Theorem | erldi 33212* | 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 33213 | 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 33214 | 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 33215 | 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 33216* | Membership in the basis of a ring localization. (Contributed by Thierry Arnoux, 4-May-2025.) |
| ⊢ (𝜑 → 𝑋 ∈ ((𝐵 × 𝑆) / ∼ )) ⇒ ⊢ (𝜑 → ∃𝑎 ∈ 𝐵 ∃𝑏 ∈ 𝑆 𝑋 = [⟨𝑎, 𝑏⟩] ∼ ) | ||
| Theorem | rlocbas 33217 | The base set of a ring localization. (Contributed by Thierry Arnoux, 4-May-2025.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ − = (-g‘𝑅) & ⊢ 𝑊 = (𝐵 × 𝑆) & ⊢ 𝐿 = (𝑅 RLocal 𝑆) & ⊢ ∼ = (𝑅 ~RL 𝑆) & ⊢ (𝜑 → 𝑅 ∈ 𝑉) & ⊢ (𝜑 → 𝑆 ⊆ 𝐵) ⇒ ⊢ (𝜑 → (𝑊 / ∼ ) = (Base‘𝐿)) | ||
| Theorem | rlocaddval 33218 | 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 33219 | 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 33220 | 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 33221 | 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 33222 | 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 33223* | 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 33224 | 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 33225 | 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 | domnpropd 33226* | 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 33227* | If two structures have the same components (properties), one is a integral domain iff the other one is. See also domnpropd 33226. (Contributed by Thierry Arnoux, 13-Oct-2025.) |
| ⊢ (𝜑 → 𝐵 = (Base‘𝐾)) & ⊢ (𝜑 → 𝐵 = (Base‘𝐿)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(+g‘𝐾)𝑦) = (𝑥(+g‘𝐿)𝑦)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(.r‘𝐾)𝑦) = (𝑥(.r‘𝐿)𝑦)) ⇒ ⊢ (𝜑 → (𝐾 ∈ IDomn ↔ 𝐿 ∈ IDomn)) | ||
| Theorem | idomrcan 33228 | 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 33229 | Obsolete version of domnlcan 20624 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 33230 | Obsolete version of domnlcanb 20623 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 33231 | Obsolete version of idomrcan 33228 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 33232 | The multiplicative identity is a left-regular element. (Contributed by Thierry Arnoux, 6-May-2025.) |
| ⊢ 1 = (1r‘𝑅) & ⊢ 𝐸 = (RLReg‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ Ring) ⇒ ⊢ (𝜑 → 1 ∈ 𝐸) | ||
| Theorem | rrgsubm 33233 | 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 33234 | A subring of a domain is a domain. (Contributed by Thierry Arnoux, 18-May-2025.) |
| ⊢ (𝜑 → 𝑅 ∈ Domn) & ⊢ (𝜑 → 𝑆 ∈ (SubRing‘𝑅)) ⇒ ⊢ (𝜑 → (𝑅 ↾s 𝑆) ∈ Domn) | ||
| Theorem | subridom 33235 | A subring of an integral domain is an integral domain. (Contributed by Thierry Arnoux, 18-May-2025.) |
| ⊢ (𝜑 → 𝑅 ∈ IDomn) & ⊢ (𝜑 → 𝑆 ∈ (SubRing‘𝑅)) ⇒ ⊢ (𝜑 → (𝑅 ↾s 𝑆) ∈ IDomn) | ||
| Theorem | subrfld 33236 | A subring of a field is an integral domain. (Contributed by Thierry Arnoux, 18-May-2025.) |
| ⊢ (𝜑 → 𝑅 ∈ Field) & ⊢ (𝜑 → 𝑆 ∈ (SubRing‘𝑅)) ⇒ ⊢ (𝜑 → (𝑅 ↾s 𝑆) ∈ IDomn) | ||
| Syntax | ceuf 33237 | Declare the syntax for the Euclidean function index extractor. |
| class EuclF | ||
| Definition | df-euf 33238 | Define the Euclidean function. (Contributed by Thierry Arnoux, 22-Mar-2025.) Use its index-independent form eufid 33240 instead. (New usage is discouraged.) |
| ⊢ EuclF = Slot ;21 | ||
| Theorem | eufndx 33239 | Index value of the Euclidean function slot. Use ndxarg 17125. (Contributed by Thierry Arnoux, 22-Mar-2025.) (New usage is discouraged.) |
| ⊢ (EuclF‘ndx) = ;21 | ||
| Theorem | eufid 33240 | Utility theorem: index-independent form of df-euf 33238. (Contributed by Thierry Arnoux, 22-Mar-2025.) |
| ⊢ EuclF = Slot (EuclF‘ndx) | ||
| Syntax | cedom 33241 | Declare the syntax for the Euclidean Domain. |
| class EDomn | ||
| Definition | df-edom 33242* | Define Euclidean Domains. (Contributed by Thierry Arnoux, 22-Mar-2025.) |
| ⊢ EDomn = {𝑑 ∈ IDomn ∣ [(EuclF‘𝑑) / 𝑒][(Base‘𝑑) / 𝑣](Fun 𝑒 ∧ (𝑒 “ (𝑣 ∖ {(0g‘𝑑)})) ⊆ (0[,)+∞) ∧ ∀𝑎 ∈ 𝑣 ∀𝑏 ∈ (𝑣 ∖ {(0g‘𝑑)})∃𝑞 ∈ 𝑣 ∃𝑟 ∈ 𝑣 (𝑎 = ((𝑏(.r‘𝑑)𝑞)(+g‘𝑑)𝑟) ∧ (𝑟 = (0g‘𝑑) ∨ (𝑒‘𝑟) < (𝑒‘𝑏))))} | ||
| Theorem | ringinveu 33243 | 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 33244* | 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 33245 | 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 33246 | The field of rational numbers is a field. (Contributed by Thierry Arnoux, 19-Oct-2025.) |
| ⊢ 𝑄 = (ℂfld ↾s ℚ) ⇒ ⊢ 𝑄 ∈ Field | ||
| Theorem | subsdrg 33247 | A subring of a sub-division-ring is a sub-division-ring. See also subsubrg 20501. (Contributed by Thierry Arnoux, 26-Oct-2025.) |
| ⊢ 𝑆 = (𝑅 ↾s 𝐴) & ⊢ (𝜑 → 𝐴 ∈ (SubDRing‘𝑅)) ⇒ ⊢ (𝜑 → (𝐵 ∈ (SubDRing‘𝑆) ↔ (𝐵 ∈ (SubDRing‘𝑅) ∧ 𝐵 ⊆ 𝐴))) | ||
| Theorem | sdrgdvcl 33248 | 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 33249 | 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 33250 | 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 33251 | Syntax for the field of fractions of a given integral domain. |
| class Frac | ||
| Definition | df-frac 33252 | Define the field of fractions of a given integral domain. (Contributed by Thierry Arnoux, 26-Apr-2025.) |
| ⊢ Frac = (𝑟 ∈ V ↦ (𝑟 RLocal (RLReg‘𝑟))) | ||
| Theorem | fracval 33253 | Value of the field of fractions. (Contributed by Thierry Arnoux, 5-May-2025.) |
| ⊢ ( Frac ‘𝑅) = (𝑅 RLocal (RLReg‘𝑅)) | ||
| Theorem | fracbas 33254 | The base of the field of fractions. (Contributed by Thierry Arnoux, 10-May-2025.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝐸 = (RLReg‘𝑅) & ⊢ 𝐹 = ( Frac ‘𝑅) & ⊢ ∼ = (𝑅 ~RL 𝐸) ⇒ ⊢ ((𝐵 × 𝐸) / ∼ ) = (Base‘𝐹) | ||
| Theorem | fracerl 33255 | 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 33256* | 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 33257 | The field of fractions of an integral domain is a field. (Contributed by Thierry Arnoux, 4-May-2025.) |
| ⊢ (𝜑 → 𝑅 ∈ IDomn) ⇒ ⊢ (𝜑 → ( Frac ‘𝑅) ∈ Field) | ||
| Theorem | idomsubr 33258* | 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 33259 | Syntax for a function generating sub-fields. |
| class fldGen | ||
| Definition | df-fldgen 33260* | 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 33263). If the base structure is a field, this is a subfield (see fldgenfld 33269 and fldsdrgfld 20701). 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 33261* | 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 33262 | The field generated by a set of elements contains those elements. See lspssid 20906. (Contributed by Thierry Arnoux, 15-Jan-2025.) |
| ⊢ 𝐵 = (Base‘𝐹) & ⊢ (𝜑 → 𝐹 ∈ DivRing) & ⊢ (𝜑 → 𝑆 ⊆ 𝐵) ⇒ ⊢ (𝜑 → 𝑆 ⊆ (𝐹 fldGen 𝑆)) | ||
| Theorem | fldgensdrg 33263 | A generated subfield is a sub-division-ring. (Contributed by Thierry Arnoux, 11-Jan-2025.) |
| ⊢ 𝐵 = (Base‘𝐹) & ⊢ (𝜑 → 𝐹 ∈ DivRing) & ⊢ (𝜑 → 𝑆 ⊆ 𝐵) ⇒ ⊢ (𝜑 → (𝐹 fldGen 𝑆) ∈ (SubDRing‘𝐹)) | ||
| Theorem | fldgenssv 33264 | A generated subfield is a subset of the field's base. (Contributed by Thierry Arnoux, 25-Feb-2025.) |
| ⊢ 𝐵 = (Base‘𝐹) & ⊢ (𝜑 → 𝐹 ∈ DivRing) & ⊢ (𝜑 → 𝑆 ⊆ 𝐵) ⇒ ⊢ (𝜑 → (𝐹 fldGen 𝑆) ⊆ 𝐵) | ||
| Theorem | fldgenss 33265 | Generated subfields preserve subset ordering. ( see lspss 20905 and spanss 31310) (Contributed by Thierry Arnoux, 15-Jan-2025.) |
| ⊢ 𝐵 = (Base‘𝐹) & ⊢ (𝜑 → 𝐹 ∈ DivRing) & ⊢ (𝜑 → 𝑆 ⊆ 𝐵) & ⊢ (𝜑 → 𝑇 ⊆ 𝑆) ⇒ ⊢ (𝜑 → (𝐹 fldGen 𝑇) ⊆ (𝐹 fldGen 𝑆)) | ||
| Theorem | fldgenidfld 33266 | The subfield generated by a subfield is the subfield itself. (Contributed by Thierry Arnoux, 15-Jan-2025.) |
| ⊢ 𝐵 = (Base‘𝐹) & ⊢ (𝜑 → 𝐹 ∈ DivRing) & ⊢ (𝜑 → 𝑆 ∈ (SubDRing‘𝐹)) ⇒ ⊢ (𝜑 → (𝐹 fldGen 𝑆) = 𝑆) | ||
| Theorem | fldgenssp 33267 | 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 33268 | 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 33269 | A generated subfield is a field. (Contributed by Thierry Arnoux, 11-Jan-2025.) |
| ⊢ 𝐵 = (Base‘𝐹) & ⊢ (𝜑 → 𝐹 ∈ Field) & ⊢ (𝜑 → 𝑆 ⊆ 𝐵) ⇒ ⊢ (𝜑 → (𝐹 ↾s (𝐹 fldGen 𝑆)) ∈ Field) | ||
| Theorem | primefldgen1 33270 | 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 33271 | 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 33272 | A ring homomorphism preserves ratios. (Contributed by Thierry Arnoux, 22-Oct-2017.) |
| ⊢ 𝑈 = (Unit‘𝑆) & ⊢ 𝑋 = (Base‘𝑅) & ⊢ / = (/r‘𝑆) & ⊢ · = (.r‘𝑅) ⇒ ⊢ ((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋) ∧ ((𝐹‘𝐵) ∈ 𝑈 ∧ (𝐹‘𝐶) ∈ 𝑈)) → ((𝐹‘𝐴) / (𝐹‘𝐵)) = ((𝐹‘(𝐴 · 𝐶)) / (𝐹‘(𝐵 · 𝐶)))) | ||
| Theorem | kerunit 33273 | 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 33274 | Extend class notation with the scalar restriction operation. |
| class ↾v | ||
| Definition | df-resv 33275* | 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 33276 | The scalar restriction is a proper operator, so it can be used with ovprc1 7392. (Contributed by Thierry Arnoux, 6-Sep-2018.) |
| ⊢ Rel dom ↾v | ||
| Theorem | resvval 33277 | Value of structure restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.) |
| ⊢ 𝑅 = (𝑊 ↾v 𝐴) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐵 = (Base‘𝐹) ⇒ ⊢ ((𝑊 ∈ 𝑋 ∧ 𝐴 ∈ 𝑌) → 𝑅 = if(𝐵 ⊆ 𝐴, 𝑊, (𝑊 sSet ⟨(Scalar‘ndx), (𝐹 ↾s 𝐴)⟩))) | ||
| Theorem | resvid2 33278 | General behavior of trivial restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.) |
| ⊢ 𝑅 = (𝑊 ↾v 𝐴) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐵 = (Base‘𝐹) ⇒ ⊢ ((𝐵 ⊆ 𝐴 ∧ 𝑊 ∈ 𝑋 ∧ 𝐴 ∈ 𝑌) → 𝑅 = 𝑊) | ||
| Theorem | resvval2 33279 | Value of nontrivial structure restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.) |
| ⊢ 𝑅 = (𝑊 ↾v 𝐴) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐵 = (Base‘𝐹) ⇒ ⊢ ((¬ 𝐵 ⊆ 𝐴 ∧ 𝑊 ∈ 𝑋 ∧ 𝐴 ∈ 𝑌) → 𝑅 = (𝑊 sSet ⟨(Scalar‘ndx), (𝐹 ↾s 𝐴)⟩)) | ||
| Theorem | resvsca 33280 | Base set of a structure restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.) |
| ⊢ 𝑅 = (𝑊 ↾v 𝐴) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐵 = (Base‘𝐹) ⇒ ⊢ (𝐴 ∈ 𝑉 → (𝐹 ↾s 𝐴) = (Scalar‘𝑅)) | ||
| Theorem | resvlem 33281 | 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 33282 | Base is unaffected by scalar restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.) (Revised by AV, 31-Oct-2024.) |
| ⊢ 𝐻 = (𝐺 ↾v 𝐴) & ⊢ 𝐵 = (Base‘𝐺) ⇒ ⊢ (𝐴 ∈ 𝑉 → 𝐵 = (Base‘𝐻)) | ||
| Theorem | resvplusg 33283 | +g is unaffected by scalar restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.) (Revised by AV, 31-Oct-2024.) |
| ⊢ 𝐻 = (𝐺 ↾v 𝐴) & ⊢ + = (+g‘𝐺) ⇒ ⊢ (𝐴 ∈ 𝑉 → + = (+g‘𝐻)) | ||
| Theorem | resvvsca 33284 | ·𝑠 is unaffected by scalar restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.) (Proof shortened by AV, 31-Oct-2024.) |
| ⊢ 𝐻 = (𝐺 ↾v 𝐴) & ⊢ · = ( ·𝑠 ‘𝐺) ⇒ ⊢ (𝐴 ∈ 𝑉 → · = ( ·𝑠 ‘𝐻)) | ||
| Theorem | resvmulr 33285 | .r is unaffected by scalar restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.) (Revised by AV, 31-Oct-2024.) |
| ⊢ 𝐻 = (𝐺 ↾v 𝐴) & ⊢ · = (.r‘𝐺) ⇒ ⊢ (𝐴 ∈ 𝑉 → · = (.r‘𝐻)) | ||
| Theorem | resv0g 33286 | 0g is unaffected by scalar restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.) |
| ⊢ 𝐻 = (𝐺 ↾v 𝐴) & ⊢ 0 = (0g‘𝐺) ⇒ ⊢ (𝐴 ∈ 𝑉 → 0 = (0g‘𝐻)) | ||
| Theorem | resv1r 33287 | 1r is unaffected by scalar restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.) |
| ⊢ 𝐻 = (𝐺 ↾v 𝐴) & ⊢ 1 = (1r‘𝐺) ⇒ ⊢ (𝐴 ∈ 𝑉 → 1 = (1r‘𝐻)) | ||
| Theorem | resvcmn 33288 | Scalar restriction preserves commutative monoids. (Contributed by Thierry Arnoux, 6-Sep-2018.) |
| ⊢ 𝐻 = (𝐺 ↾v 𝐴) ⇒ ⊢ (𝐴 ∈ 𝑉 → (𝐺 ∈ CMnd ↔ 𝐻 ∈ CMnd)) | ||
| Theorem | gzcrng 33289 | The gaussian integers form a commutative ring. (Contributed by Thierry Arnoux, 18-Mar-2018.) |
| ⊢ (ℂfld ↾s ℤ[i]) ∈ CRing | ||
| Theorem | cnfldfld 33290 | The complex numbers form a field. (Contributed by Thierry Arnoux, 6-Jul-2025.) |
| ⊢ ℂfld ∈ Field | ||
| Theorem | reofld 33291 | The real numbers form an ordered field. (Contributed by Thierry Arnoux, 21-Jan-2018.) |
| ⊢ ℝfld ∈ oField | ||
| Theorem | nn0omnd 33292 | The nonnegative integers form an ordered monoid. (Contributed by Thierry Arnoux, 23-Mar-2018.) |
| ⊢ (ℂfld ↾s ℕ0) ∈ oMnd | ||
| Theorem | rearchi 33293 | The field of the real numbers is Archimedean. See also arch 12399. (Contributed by Thierry Arnoux, 9-Apr-2018.) |
| ⊢ ℝfld ∈ Archi | ||
| Theorem | nn0archi 33294 | The monoid of the nonnegative integers is Archimedean. (Contributed by Thierry Arnoux, 16-Sep-2018.) |
| ⊢ (ℂfld ↾s ℕ0) ∈ Archi | ||
| Theorem | xrge0slmod 33295 | The extended nonnegative real numbers form a semiring left module. One could also have used subringAlg to get the same structure. (Contributed by Thierry Arnoux, 6-Sep-2018.) |
| ⊢ 𝐺 = (ℝ*𝑠 ↾s (0[,]+∞)) & ⊢ 𝑊 = (𝐺 ↾v (0[,)+∞)) ⇒ ⊢ 𝑊 ∈ SLMod | ||
| Theorem | qusker 33296* | The kernel of a quotient map. (Contributed by Thierry Arnoux, 20-May-2023.) |
| ⊢ 𝑉 = (Base‘𝑀) & ⊢ 𝐹 = (𝑥 ∈ 𝑉 ↦ [𝑥](𝑀 ~QG 𝐺)) & ⊢ 𝑁 = (𝑀 /s (𝑀 ~QG 𝐺)) & ⊢ 0 = (0g‘𝑁) ⇒ ⊢ (𝐺 ∈ (NrmSGrp‘𝑀) → (◡𝐹 “ { 0 }) = 𝐺) | ||
| Theorem | eqgvscpbl 33297 | The left coset equivalence relation is compatible with the scalar multiplication operation. (Contributed by Thierry Arnoux, 18-May-2023.) |
| ⊢ 𝐵 = (Base‘𝑀) & ⊢ ∼ = (𝑀 ~QG 𝐺) & ⊢ 𝑆 = (Base‘(Scalar‘𝑀)) & ⊢ · = ( ·𝑠 ‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ LMod) & ⊢ (𝜑 → 𝐺 ∈ (LSubSp‘𝑀)) & ⊢ (𝜑 → 𝐾 ∈ 𝑆) ⇒ ⊢ (𝜑 → (𝑋 ∼ 𝑌 → (𝐾 · 𝑋) ∼ (𝐾 · 𝑌))) | ||
| Theorem | qusvscpbl 33298* | The quotient map distributes over the scalar multiplication. (Contributed by Thierry Arnoux, 18-May-2023.) |
| ⊢ 𝐵 = (Base‘𝑀) & ⊢ ∼ = (𝑀 ~QG 𝐺) & ⊢ 𝑆 = (Base‘(Scalar‘𝑀)) & ⊢ · = ( ·𝑠 ‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ LMod) & ⊢ (𝜑 → 𝐺 ∈ (LSubSp‘𝑀)) & ⊢ (𝜑 → 𝐾 ∈ 𝑆) & ⊢ 𝑁 = (𝑀 /s (𝑀 ~QG 𝐺)) & ⊢ ∙ = ( ·𝑠 ‘𝑁) & ⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ [𝑥](𝑀 ~QG 𝐺)) & ⊢ (𝜑 → 𝑈 ∈ 𝐵) & ⊢ (𝜑 → 𝑉 ∈ 𝐵) ⇒ ⊢ (𝜑 → ((𝐹‘𝑈) = (𝐹‘𝑉) → (𝐹‘(𝐾 · 𝑈)) = (𝐹‘(𝐾 · 𝑉)))) | ||
| Theorem | qusvsval 33299 | Value of the scalar multiplication operation on the quotient structure. (Contributed by Thierry Arnoux, 18-May-2023.) |
| ⊢ 𝐵 = (Base‘𝑀) & ⊢ ∼ = (𝑀 ~QG 𝐺) & ⊢ 𝑆 = (Base‘(Scalar‘𝑀)) & ⊢ · = ( ·𝑠 ‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ LMod) & ⊢ (𝜑 → 𝐺 ∈ (LSubSp‘𝑀)) & ⊢ (𝜑 → 𝐾 ∈ 𝑆) & ⊢ 𝑁 = (𝑀 /s (𝑀 ~QG 𝐺)) & ⊢ ∙ = ( ·𝑠 ‘𝑁) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝐾 ∙ [𝑋](𝑀 ~QG 𝐺)) = [(𝐾 · 𝑋)](𝑀 ~QG 𝐺)) | ||
| Theorem | imaslmod 33300* | The image structure of a left module is a left module. (Contributed by Thierry Arnoux, 15-May-2023.) |
| ⊢ (𝜑 → 𝑁 = (𝐹 “s 𝑀)) & ⊢ 𝑉 = (Base‘𝑀) & ⊢ 𝑆 = (Base‘(Scalar‘𝑀)) & ⊢ + = (+g‘𝑀) & ⊢ · = ( ·𝑠 ‘𝑀) & ⊢ 0 = (0g‘𝑀) & ⊢ (𝜑 → 𝐹:𝑉–onto→𝐵) & ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → (((𝐹‘𝑎) = (𝐹‘𝑝) ∧ (𝐹‘𝑏) = (𝐹‘𝑞)) → (𝐹‘(𝑎 + 𝑏)) = (𝐹‘(𝑝 + 𝑞)))) & ⊢ ((𝜑 ∧ (𝑘 ∈ 𝑆 ∧ 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) → ((𝐹‘𝑎) = (𝐹‘𝑏) → (𝐹‘(𝑘 · 𝑎)) = (𝐹‘(𝑘 · 𝑏)))) & ⊢ (𝜑 → 𝑀 ∈ LMod) ⇒ ⊢ (𝜑 → 𝑁 ∈ LMod) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |