Home | Metamath
Proof Explorer Theorem List (p. 312 of 449) | < 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-28623) |
Hilbert Space Explorer
(28624-30146) |
Users' Mathboxes
(30147-44804) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | zringnm 31101 | The norm (function) for a ring of integers is the absolute value function (restricted to the integers). (Contributed by AV, 13-Jun-2019.) |
⊢ (norm‘ℤring) = (abs ↾ ℤ) | ||
Theorem | zzsnm 31102 | The norm of the ring of the integers. (Contributed by Thierry Arnoux, 8-Nov-2017.) (Revised by AV, 13-Jun-2019.) |
⊢ (𝑀 ∈ ℤ → (abs‘𝑀) = ((norm‘ℤring)‘𝑀)) | ||
Theorem | zlm0 31103 | Zero of a ℤ-module. (Contributed by Thierry Arnoux, 8-Nov-2017.) |
⊢ 𝑊 = (ℤMod‘𝐺) & ⊢ 0 = (0g‘𝐺) ⇒ ⊢ 0 = (0g‘𝑊) | ||
Theorem | zlm1 31104 | Unit of a ℤ-module (if present). (Contributed by Thierry Arnoux, 8-Nov-2017.) |
⊢ 𝑊 = (ℤMod‘𝐺) & ⊢ 1 = (1r‘𝐺) ⇒ ⊢ 1 = (1r‘𝑊) | ||
Theorem | zlmds 31105 | Distance in a ℤ-module (if present). (Contributed by Thierry Arnoux, 8-Nov-2017.) |
⊢ 𝑊 = (ℤMod‘𝐺) & ⊢ 𝐷 = (dist‘𝐺) ⇒ ⊢ (𝐺 ∈ 𝑉 → 𝐷 = (dist‘𝑊)) | ||
Theorem | zlmtset 31106 | Topology in a ℤ-module (if present). (Contributed by Thierry Arnoux, 8-Nov-2017.) |
⊢ 𝑊 = (ℤMod‘𝐺) & ⊢ 𝐽 = (TopSet‘𝐺) ⇒ ⊢ (𝐺 ∈ 𝑉 → 𝐽 = (TopSet‘𝑊)) | ||
Theorem | zlmnm 31107 | Norm of a ℤ-module (if present). (Contributed by Thierry Arnoux, 8-Nov-2017.) |
⊢ 𝑊 = (ℤMod‘𝐺) & ⊢ 𝑁 = (norm‘𝐺) ⇒ ⊢ (𝐺 ∈ 𝑉 → 𝑁 = (norm‘𝑊)) | ||
Theorem | zhmnrg 31108 | The ℤ-module built from a normed ring is also a normed ring. (Contributed by Thierry Arnoux, 8-Nov-2017.) |
⊢ 𝑊 = (ℤMod‘𝐺) ⇒ ⊢ (𝐺 ∈ NrmRing → 𝑊 ∈ NrmRing) | ||
Theorem | nmmulg 31109 | The norm of a group product, provided the ℤ-module is normed. (Contributed by Thierry Arnoux, 8-Nov-2017.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝑁 = (norm‘𝑅) & ⊢ 𝑍 = (ℤMod‘𝑅) & ⊢ · = (.g‘𝑅) ⇒ ⊢ ((𝑍 ∈ NrmMod ∧ 𝑀 ∈ ℤ ∧ 𝑋 ∈ 𝐵) → (𝑁‘(𝑀 · 𝑋)) = ((abs‘𝑀) · (𝑁‘𝑋))) | ||
Theorem | zrhnm 31110 | The norm of the image by ℤRHom of an integer in a normed ring. (Contributed by Thierry Arnoux, 8-Nov-2017.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝑁 = (norm‘𝑅) & ⊢ 𝑍 = (ℤMod‘𝑅) & ⊢ 𝐿 = (ℤRHom‘𝑅) ⇒ ⊢ (((𝑍 ∈ NrmMod ∧ 𝑍 ∈ NrmRing ∧ 𝑅 ∈ NzRing) ∧ 𝑀 ∈ ℤ) → (𝑁‘(𝐿‘𝑀)) = (abs‘𝑀)) | ||
Theorem | cnzh 31111 | The ℤ-module of ℂ is a normed module. (Contributed by Thierry Arnoux, 25-Feb-2018.) |
⊢ (ℤMod‘ℂfld) ∈ NrmMod | ||
Theorem | rezh 31112 | The ℤ-module of ℝ is a normed module. (Contributed by Thierry Arnoux, 14-Feb-2018.) |
⊢ (ℤMod‘ℝfld) ∈ NrmMod | ||
Syntax | cqqh 31113 | Map the rationals into a field. |
class ℚHom | ||
Definition | df-qqh 31114* | Define the canonical homomorphism from the rationals into any field. (Contributed by Mario Carneiro, 22-Oct-2017.) (Revised by Thierry Arnoux, 23-Oct-2017.) |
⊢ ℚHom = (𝑟 ∈ V ↦ ran (𝑥 ∈ ℤ, 𝑦 ∈ (◡(ℤRHom‘𝑟) “ (Unit‘𝑟)) ↦ 〈(𝑥 / 𝑦), (((ℤRHom‘𝑟)‘𝑥)(/r‘𝑟)((ℤRHom‘𝑟)‘𝑦))〉)) | ||
Theorem | qqhval 31115* | Value of the canonical homormorphism from the rational number to a field. (Contributed by Thierry Arnoux, 22-Oct-2017.) |
⊢ / = (/r‘𝑅) & ⊢ 1 = (1r‘𝑅) & ⊢ 𝐿 = (ℤRHom‘𝑅) ⇒ ⊢ (𝑅 ∈ V → (ℚHom‘𝑅) = ran (𝑥 ∈ ℤ, 𝑦 ∈ (◡𝐿 “ (Unit‘𝑅)) ↦ 〈(𝑥 / 𝑦), ((𝐿‘𝑥) / (𝐿‘𝑦))〉)) | ||
Theorem | zrhf1ker 31116 | The kernel of the homomorphism from the integers to a ring, if it is injective. (Contributed by Thierry Arnoux, 26-Oct-2017.) (Revised by Thierry Arnoux, 23-May-2023.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝐿 = (ℤRHom‘𝑅) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ (𝑅 ∈ Ring → (𝐿:ℤ–1-1→𝐵 ↔ (◡𝐿 “ { 0 }) = {0})) | ||
Theorem | zrhchr 31117 | The kernel of the homomorphism from the integers to a ring is injective if and only if the ring has characteristic 0 . (Contributed by Thierry Arnoux, 8-Nov-2017.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝐿 = (ℤRHom‘𝑅) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ (𝑅 ∈ Ring → ((chr‘𝑅) = 0 ↔ 𝐿:ℤ–1-1→𝐵)) | ||
Theorem | zrhker 31118 | The kernel of the homomorphism from the integers to a ring with characteristic 0. (Contributed by Thierry Arnoux, 8-Nov-2017.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝐿 = (ℤRHom‘𝑅) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ (𝑅 ∈ Ring → ((chr‘𝑅) = 0 ↔ (◡𝐿 “ { 0 }) = {0})) | ||
Theorem | zrhunitpreima 31119 | The preimage by ℤRHom of the unit of a division ring is (ℤ ∖ {0}). (Contributed by Thierry Arnoux, 22-Oct-2017.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝐿 = (ℤRHom‘𝑅) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ ((𝑅 ∈ DivRing ∧ (chr‘𝑅) = 0) → (◡𝐿 “ (Unit‘𝑅)) = (ℤ ∖ {0})) | ||
Theorem | elzrhunit 31120 | Condition for the image by ℤRHom to be a unit. (Contributed by Thierry Arnoux, 30-Oct-2017.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝐿 = (ℤRHom‘𝑅) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ (((𝑅 ∈ DivRing ∧ (chr‘𝑅) = 0) ∧ (𝑀 ∈ ℤ ∧ 𝑀 ≠ 0)) → (𝐿‘𝑀) ∈ (Unit‘𝑅)) | ||
Theorem | elzdif0 31121 | Lemma for qqhval2 31123. (Contributed by Thierry Arnoux, 29-Oct-2017.) |
⊢ (𝑀 ∈ (ℤ ∖ {0}) → (𝑀 ∈ ℕ ∨ -𝑀 ∈ ℕ)) | ||
Theorem | qqhval2lem 31122 | Lemma for qqhval2 31123. (Contributed by Thierry Arnoux, 29-Oct-2017.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ / = (/r‘𝑅) & ⊢ 𝐿 = (ℤRHom‘𝑅) ⇒ ⊢ (((𝑅 ∈ DivRing ∧ (chr‘𝑅) = 0) ∧ (𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ∧ 𝑌 ≠ 0)) → ((𝐿‘(numer‘(𝑋 / 𝑌))) / (𝐿‘(denom‘(𝑋 / 𝑌)))) = ((𝐿‘𝑋) / (𝐿‘𝑌))) | ||
Theorem | qqhval2 31123* | Value of the canonical homormorphism from the rational number when the target ring is a division ring. (Contributed by Thierry Arnoux, 26-Oct-2017.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ / = (/r‘𝑅) & ⊢ 𝐿 = (ℤRHom‘𝑅) ⇒ ⊢ ((𝑅 ∈ DivRing ∧ (chr‘𝑅) = 0) → (ℚHom‘𝑅) = (𝑞 ∈ ℚ ↦ ((𝐿‘(numer‘𝑞)) / (𝐿‘(denom‘𝑞))))) | ||
Theorem | qqhvval 31124 | Value of the canonical homormorphism from the rational number when the target ring is a division ring. (Contributed by Thierry Arnoux, 30-Oct-2017.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ / = (/r‘𝑅) & ⊢ 𝐿 = (ℤRHom‘𝑅) ⇒ ⊢ (((𝑅 ∈ DivRing ∧ (chr‘𝑅) = 0) ∧ 𝑄 ∈ ℚ) → ((ℚHom‘𝑅)‘𝑄) = ((𝐿‘(numer‘𝑄)) / (𝐿‘(denom‘𝑄)))) | ||
Theorem | qqh0 31125 | The image of 0 by the ℚHom homomorphism is the ring's zero. (Contributed by Thierry Arnoux, 22-Oct-2017.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ / = (/r‘𝑅) & ⊢ 𝐿 = (ℤRHom‘𝑅) ⇒ ⊢ ((𝑅 ∈ DivRing ∧ (chr‘𝑅) = 0) → ((ℚHom‘𝑅)‘0) = (0g‘𝑅)) | ||
Theorem | qqh1 31126 | The image of 1 by the ℚHom homomorphism is the ring's unit. (Contributed by Thierry Arnoux, 22-Oct-2017.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ / = (/r‘𝑅) & ⊢ 𝐿 = (ℤRHom‘𝑅) ⇒ ⊢ ((𝑅 ∈ DivRing ∧ (chr‘𝑅) = 0) → ((ℚHom‘𝑅)‘1) = (1r‘𝑅)) | ||
Theorem | qqhf 31127 | ℚHom as a function. (Contributed by Thierry Arnoux, 28-Oct-2017.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ / = (/r‘𝑅) & ⊢ 𝐿 = (ℤRHom‘𝑅) ⇒ ⊢ ((𝑅 ∈ DivRing ∧ (chr‘𝑅) = 0) → (ℚHom‘𝑅):ℚ⟶𝐵) | ||
Theorem | qqhvq 31128 | The image of a quotient by the ℚHom homomorphism. (Contributed by Thierry Arnoux, 28-Oct-2017.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ / = (/r‘𝑅) & ⊢ 𝐿 = (ℤRHom‘𝑅) ⇒ ⊢ (((𝑅 ∈ DivRing ∧ (chr‘𝑅) = 0) ∧ (𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ∧ 𝑌 ≠ 0)) → ((ℚHom‘𝑅)‘(𝑋 / 𝑌)) = ((𝐿‘𝑋) / (𝐿‘𝑌))) | ||
Theorem | qqhghm 31129 | The ℚHom homomorphism is a group homomorphism if the target structure is a division ring. (Contributed by Thierry Arnoux, 9-Nov-2017.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ / = (/r‘𝑅) & ⊢ 𝐿 = (ℤRHom‘𝑅) & ⊢ 𝑄 = (ℂfld ↾s ℚ) ⇒ ⊢ ((𝑅 ∈ DivRing ∧ (chr‘𝑅) = 0) → (ℚHom‘𝑅) ∈ (𝑄 GrpHom 𝑅)) | ||
Theorem | qqhrhm 31130 | The ℚHom homomorphism is a ring homomorphism if the target structure is a field. If the target structure is a division ring, it is a group homomorphism, but not a ring homomorphism, because it does not preserve the ring multiplication operation. (Contributed by Thierry Arnoux, 29-Oct-2017.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ / = (/r‘𝑅) & ⊢ 𝐿 = (ℤRHom‘𝑅) & ⊢ 𝑄 = (ℂfld ↾s ℚ) ⇒ ⊢ ((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) → (ℚHom‘𝑅) ∈ (𝑄 RingHom 𝑅)) | ||
Theorem | qqhnm 31131 | The norm of the image by ℚHom of a rational number in a topological division ring. (Contributed by Thierry Arnoux, 8-Nov-2017.) |
⊢ 𝑁 = (norm‘𝑅) & ⊢ 𝑍 = (ℤMod‘𝑅) ⇒ ⊢ (((𝑅 ∈ (NrmRing ∩ DivRing) ∧ 𝑍 ∈ NrmMod ∧ (chr‘𝑅) = 0) ∧ 𝑄 ∈ ℚ) → (𝑁‘((ℚHom‘𝑅)‘𝑄)) = (abs‘𝑄)) | ||
Theorem | qqhcn 31132 | The ℚHom homomorphism is a continuous function. (Contributed by Thierry Arnoux, 9-Nov-2017.) |
⊢ 𝑄 = (ℂfld ↾s ℚ) & ⊢ 𝐽 = (TopOpen‘𝑄) & ⊢ 𝑍 = (ℤMod‘𝑅) & ⊢ 𝐾 = (TopOpen‘𝑅) ⇒ ⊢ ((𝑅 ∈ (NrmRing ∩ DivRing) ∧ 𝑍 ∈ NrmMod ∧ (chr‘𝑅) = 0) → (ℚHom‘𝑅) ∈ (𝐽 Cn 𝐾)) | ||
Theorem | qqhucn 31133 | The ℚHom homomorphism is uniformly continuous. (Contributed by Thierry Arnoux, 28-Jan-2018.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝑄 = (ℂfld ↾s ℚ) & ⊢ 𝑈 = (UnifSt‘𝑄) & ⊢ 𝑉 = (metUnif‘((dist‘𝑅) ↾ (𝐵 × 𝐵))) & ⊢ 𝑍 = (ℤMod‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ NrmRing) & ⊢ (𝜑 → 𝑅 ∈ DivRing) & ⊢ (𝜑 → 𝑍 ∈ NrmMod) & ⊢ (𝜑 → (chr‘𝑅) = 0) ⇒ ⊢ (𝜑 → (ℚHom‘𝑅) ∈ (𝑈 Cnu𝑉)) | ||
Syntax | crrh 31134 | Map the real numbers into a complete field. |
class ℝHom | ||
Syntax | crrext 31135 | Extend class notation with the class of extension fields of ℝ. |
class ℝExt | ||
Definition | df-rrh 31136 | Define the canonical homomorphism from the real numbers to any complete field, as the extension by continuity of the canonical homomorphism from the rational numbers. (Contributed by Mario Carneiro, 22-Oct-2017.) (Revised by Thierry Arnoux, 23-Oct-2017.) |
⊢ ℝHom = (𝑟 ∈ V ↦ (((topGen‘ran (,))CnExt(TopOpen‘𝑟))‘(ℚHom‘𝑟))) | ||
Theorem | rrhval 31137 | Value of the canonical homormorphism from the real numbers to a complete space. (Contributed by Thierry Arnoux, 2-Nov-2017.) |
⊢ 𝐽 = (topGen‘ran (,)) & ⊢ 𝐾 = (TopOpen‘𝑅) ⇒ ⊢ (𝑅 ∈ 𝑉 → (ℝHom‘𝑅) = ((𝐽CnExt𝐾)‘(ℚHom‘𝑅))) | ||
Theorem | rrhcn 31138 | If the topology of 𝑅 is Hausdorff, and 𝑅 is a complete uniform space, then the canonical homomorphism from the real numbers to 𝑅 is continuous. (Contributed by Thierry Arnoux, 17-Jan-2018.) |
⊢ 𝐷 = ((dist‘𝑅) ↾ (𝐵 × 𝐵)) & ⊢ 𝐽 = (topGen‘ran (,)) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝐾 = (TopOpen‘𝑅) & ⊢ 𝑍 = (ℤMod‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ DivRing) & ⊢ (𝜑 → 𝑅 ∈ NrmRing) & ⊢ (𝜑 → 𝑍 ∈ NrmMod) & ⊢ (𝜑 → (chr‘𝑅) = 0) & ⊢ (𝜑 → 𝑅 ∈ CUnifSp) & ⊢ (𝜑 → (UnifSt‘𝑅) = (metUnif‘𝐷)) ⇒ ⊢ (𝜑 → (ℝHom‘𝑅) ∈ (𝐽 Cn 𝐾)) | ||
Theorem | rrhf 31139 | If the topology of 𝑅 is Hausdorff, Cauchy sequences have at most one limit, i.e. the canonical homomorphism of ℝ into 𝑅 is a function. (Contributed by Thierry Arnoux, 2-Nov-2017.) |
⊢ 𝐷 = ((dist‘𝑅) ↾ (𝐵 × 𝐵)) & ⊢ 𝐽 = (topGen‘ran (,)) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝐾 = (TopOpen‘𝑅) & ⊢ 𝑍 = (ℤMod‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ DivRing) & ⊢ (𝜑 → 𝑅 ∈ NrmRing) & ⊢ (𝜑 → 𝑍 ∈ NrmMod) & ⊢ (𝜑 → (chr‘𝑅) = 0) & ⊢ (𝜑 → 𝑅 ∈ CUnifSp) & ⊢ (𝜑 → (UnifSt‘𝑅) = (metUnif‘𝐷)) ⇒ ⊢ (𝜑 → (ℝHom‘𝑅):ℝ⟶𝐵) | ||
Definition | df-rrext 31140 | Define the class of extensions of ℝ. This is a shorthand for listing the necessary conditions for a structure to admit a canonical embedding of ℝ into it. Interestingly, this is not coming from a mathematical reference, but was from the necessary conditions to build the embedding at each step (ℤ, ℚ and ℝ). It would be interesting see if this is formally treated in the literature. See isrrext 31141 for a better readable version. (Contributed by Thierry Arnoux, 2-May-2018.) |
⊢ ℝExt = {𝑟 ∈ (NrmRing ∩ DivRing) ∣ (((ℤMod‘𝑟) ∈ NrmMod ∧ (chr‘𝑟) = 0) ∧ (𝑟 ∈ CUnifSp ∧ (UnifSt‘𝑟) = (metUnif‘((dist‘𝑟) ↾ ((Base‘𝑟) × (Base‘𝑟))))))} | ||
Theorem | isrrext 31141 | Express the property "𝑅 is an extension of ℝ". (Contributed by Thierry Arnoux, 2-May-2018.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝐷 = ((dist‘𝑅) ↾ (𝐵 × 𝐵)) & ⊢ 𝑍 = (ℤMod‘𝑅) ⇒ ⊢ (𝑅 ∈ ℝExt ↔ ((𝑅 ∈ NrmRing ∧ 𝑅 ∈ DivRing) ∧ (𝑍 ∈ NrmMod ∧ (chr‘𝑅) = 0) ∧ (𝑅 ∈ CUnifSp ∧ (UnifSt‘𝑅) = (metUnif‘𝐷)))) | ||
Theorem | rrextnrg 31142 | An extension of ℝ is a normed ring. (Contributed by Thierry Arnoux, 2-May-2018.) |
⊢ (𝑅 ∈ ℝExt → 𝑅 ∈ NrmRing) | ||
Theorem | rrextdrg 31143 | An extension of ℝ is a division ring. (Contributed by Thierry Arnoux, 2-May-2018.) |
⊢ (𝑅 ∈ ℝExt → 𝑅 ∈ DivRing) | ||
Theorem | rrextnlm 31144 | The norm of an extension of ℝ is absolutely homogeneous. (Contributed by Thierry Arnoux, 2-May-2018.) |
⊢ 𝑍 = (ℤMod‘𝑅) ⇒ ⊢ (𝑅 ∈ ℝExt → 𝑍 ∈ NrmMod) | ||
Theorem | rrextchr 31145 | The ring characteristic of an extension of ℝ is zero. (Contributed by Thierry Arnoux, 2-May-2018.) |
⊢ (𝑅 ∈ ℝExt → (chr‘𝑅) = 0) | ||
Theorem | rrextcusp 31146 | An extension of ℝ is a complete uniform space. (Contributed by Thierry Arnoux, 2-May-2018.) |
⊢ (𝑅 ∈ ℝExt → 𝑅 ∈ CUnifSp) | ||
Theorem | rrexttps 31147 | An extension of ℝ is a topological space. (Contributed by Thierry Arnoux, 7-Sep-2018.) |
⊢ (𝑅 ∈ ℝExt → 𝑅 ∈ TopSp) | ||
Theorem | rrexthaus 31148 | The topology of an extension of ℝ is Hausdorff. (Contributed by Thierry Arnoux, 7-Sep-2018.) |
⊢ 𝐾 = (TopOpen‘𝑅) ⇒ ⊢ (𝑅 ∈ ℝExt → 𝐾 ∈ Haus) | ||
Theorem | rrextust 31149 | The uniformity of an extension of ℝ is the uniformity generated by its distance. (Contributed by Thierry Arnoux, 2-May-2018.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝐷 = ((dist‘𝑅) ↾ (𝐵 × 𝐵)) ⇒ ⊢ (𝑅 ∈ ℝExt → (UnifSt‘𝑅) = (metUnif‘𝐷)) | ||
Theorem | rerrext 31150 | The field of the real numbers is an extension of the real numbers. (Contributed by Thierry Arnoux, 2-May-2018.) |
⊢ ℝfld ∈ ℝExt | ||
Theorem | cnrrext 31151 | The field of the complex numbers is an extension of the real numbers. (Contributed by Thierry Arnoux, 2-May-2018.) |
⊢ ℂfld ∈ ℝExt | ||
Theorem | qqtopn 31152 | The topology of the field of the rational numbers. (Contributed by Thierry Arnoux, 29-Aug-2020.) |
⊢ ((TopOpen‘ℝfld) ↾t ℚ) = (TopOpen‘(ℂfld ↾s ℚ)) | ||
Theorem | rrhfe 31153 | If 𝑅 is an extension of ℝ, then the canonical homomorphism of ℝ into 𝑅 is a function. (Contributed by Thierry Arnoux, 2-May-2018.) |
⊢ 𝐵 = (Base‘𝑅) ⇒ ⊢ (𝑅 ∈ ℝExt → (ℝHom‘𝑅):ℝ⟶𝐵) | ||
Theorem | rrhcne 31154 | If 𝑅 is an extension of ℝ, then the canonical homomorphism of ℝ into 𝑅 is continuous. (Contributed by Thierry Arnoux, 2-May-2018.) |
⊢ 𝐽 = (topGen‘ran (,)) & ⊢ 𝐾 = (TopOpen‘𝑅) ⇒ ⊢ (𝑅 ∈ ℝExt → (ℝHom‘𝑅) ∈ (𝐽 Cn 𝐾)) | ||
Theorem | rrhqima 31155 | The ℝHom homomorphism leaves rational numbers unchanged. (Contributed by Thierry Arnoux, 27-Mar-2018.) |
⊢ ((𝑅 ∈ ℝExt ∧ 𝑄 ∈ ℚ) → ((ℝHom‘𝑅)‘𝑄) = ((ℚHom‘𝑅)‘𝑄)) | ||
Theorem | rrh0 31156 | The image of 0 by the ℝHom homomorphism is the ring's zero. (Contributed by Thierry Arnoux, 22-Oct-2017.) |
⊢ (𝑅 ∈ ℝExt → ((ℝHom‘𝑅)‘0) = (0g‘𝑅)) | ||
Syntax | cxrh 31157 | Map the extended real numbers into a complete lattice. |
class ℝ*Hom | ||
Definition | df-xrh 31158* | Define an embedding from the extended real number into a complete lattice. (Contributed by Thierry Arnoux, 19-Feb-2018.) |
⊢ ℝ*Hom = (𝑟 ∈ V ↦ (𝑥 ∈ ℝ* ↦ if(𝑥 ∈ ℝ, ((ℝHom‘𝑟)‘𝑥), if(𝑥 = +∞, ((lub‘𝑟)‘((ℝHom‘𝑟) “ ℝ)), ((glb‘𝑟)‘((ℝHom‘𝑟) “ ℝ)))))) | ||
Theorem | xrhval 31159* | The value of the embedding from the extended real numbers into a complete lattice. (Contributed by Thierry Arnoux, 19-Feb-2018.) |
⊢ 𝐵 = ((ℝHom‘𝑅) “ ℝ) & ⊢ 𝐿 = (glb‘𝑅) & ⊢ 𝑈 = (lub‘𝑅) ⇒ ⊢ (𝑅 ∈ 𝑉 → (ℝ*Hom‘𝑅) = (𝑥 ∈ ℝ* ↦ if(𝑥 ∈ ℝ, ((ℝHom‘𝑅)‘𝑥), if(𝑥 = +∞, (𝑈‘𝐵), (𝐿‘𝐵))))) | ||
Theorem | zrhre 31160 | The ℤRHom homomorphism for the real number structure is the identity. (Contributed by Thierry Arnoux, 31-Oct-2017.) |
⊢ (ℤRHom‘ℝfld) = ( I ↾ ℤ) | ||
Theorem | qqhre 31161 | The ℚHom homomorphism for the real number structure is the identity. (Contributed by Thierry Arnoux, 31-Oct-2017.) |
⊢ (ℚHom‘ℝfld) = ( I ↾ ℚ) | ||
Theorem | rrhre 31162 | The ℝHom homomorphism for the real numbers structure is the identity. (Contributed by Thierry Arnoux, 22-Oct-2017.) |
⊢ (ℝHom‘ℝfld) = ( I ↾ ℝ) | ||
Found this and was curious about how manifolds would be expressed in set.mm: https://mathoverflow.net/questions/336367/real-manifolds-in-a-theorem-prover This chapter proposes to define first manifold topologies, which characterize topological manifolds, and then to extend the structure with presentations, i.e., equivalence classes of atlases for a given topological space. We suggest to use the extensible structures to define the "topological space" aspect of topological manifolds, and then extend it with charts/presentations. | ||
Syntax | cmntop 31163 | The class of n-manifold topologies. |
class ManTop | ||
Definition | df-mntop 31164* | Define the class of N-manifold topologies, as 2nd countable, Hausdorff topologies, locally homeomorphic to a ball of the Euclidean space of dimension N. (Contributed by Thierry Arnoux, 22-Dec-2019.) |
⊢ ManTop = {〈𝑛, 𝑗〉 ∣ (𝑛 ∈ ℕ0 ∧ (𝑗 ∈ 2ndω ∧ 𝑗 ∈ Haus ∧ 𝑗 ∈ Locally [(TopOpen‘(𝔼hil‘𝑛))] ≃ ))} | ||
Theorem | relmntop 31165 | Manifold is a relation. (Contributed by Thierry Arnoux, 28-Dec-2019.) |
⊢ Rel ManTop | ||
Theorem | ismntoplly 31166 | Property of being a manifold. (Contributed by Thierry Arnoux, 28-Dec-2019.) |
⊢ ((𝑁 ∈ ℕ0 ∧ 𝐽 ∈ 𝑉) → (𝑁ManTop𝐽 ↔ (𝐽 ∈ 2ndω ∧ 𝐽 ∈ Haus ∧ 𝐽 ∈ Locally [(TopOpen‘(𝔼hil‘𝑁))] ≃ ))) | ||
Theorem | ismntop 31167* | Property of being a manifold. (Contributed by Thierry Arnoux, 5-Jan-2020.) |
⊢ ((𝑁 ∈ ℕ0 ∧ 𝐽 ∈ 𝑉) → (𝑁ManTop𝐽 ↔ (𝐽 ∈ 2ndω ∧ 𝐽 ∈ Haus ∧ ∀𝑥 ∈ 𝐽 ∀𝑦 ∈ 𝑥 ∃𝑢 ∈ (𝐽 ∩ 𝒫 𝑥)(𝑦 ∈ 𝑢 ∧ (𝐽 ↾t 𝑢) ≃ (TopOpen‘(𝔼hil‘𝑁)))))) | ||
Theorem | nexple 31168 | A lower bound for an exponentiation. (Contributed by Thierry Arnoux, 19-Aug-2017.) |
⊢ ((𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℝ ∧ 2 ≤ 𝐵) → 𝐴 ≤ (𝐵↑𝐴)) | ||
Syntax | cind 31169 | Extend class notation with the indicator function generator. |
class 𝟭 | ||
Definition | df-ind 31170* | Define the indicator function generator. (Contributed by Thierry Arnoux, 20-Jan-2017.) |
⊢ 𝟭 = (𝑜 ∈ V ↦ (𝑎 ∈ 𝒫 𝑜 ↦ (𝑥 ∈ 𝑜 ↦ if(𝑥 ∈ 𝑎, 1, 0)))) | ||
Theorem | indv 31171* | Value of the indicator function generator with domain 𝑂. (Contributed by Thierry Arnoux, 23-Aug-2017.) |
⊢ (𝑂 ∈ 𝑉 → (𝟭‘𝑂) = (𝑎 ∈ 𝒫 𝑂 ↦ (𝑥 ∈ 𝑂 ↦ if(𝑥 ∈ 𝑎, 1, 0)))) | ||
Theorem | indval 31172* | Value of the indicator function generator for a set 𝐴 and a domain 𝑂. (Contributed by Thierry Arnoux, 2-Feb-2017.) |
⊢ ((𝑂 ∈ 𝑉 ∧ 𝐴 ⊆ 𝑂) → ((𝟭‘𝑂)‘𝐴) = (𝑥 ∈ 𝑂 ↦ if(𝑥 ∈ 𝐴, 1, 0))) | ||
Theorem | indval2 31173 | Alternate value of the indicator function generator. (Contributed by Thierry Arnoux, 2-Feb-2017.) |
⊢ ((𝑂 ∈ 𝑉 ∧ 𝐴 ⊆ 𝑂) → ((𝟭‘𝑂)‘𝐴) = ((𝐴 × {1}) ∪ ((𝑂 ∖ 𝐴) × {0}))) | ||
Theorem | indf 31174 | An indicator function as a function with domain and codomain. (Contributed by Thierry Arnoux, 13-Aug-2017.) |
⊢ ((𝑂 ∈ 𝑉 ∧ 𝐴 ⊆ 𝑂) → ((𝟭‘𝑂)‘𝐴):𝑂⟶{0, 1}) | ||
Theorem | indfval 31175 | Value of the indicator function. (Contributed by Thierry Arnoux, 13-Aug-2017.) |
⊢ ((𝑂 ∈ 𝑉 ∧ 𝐴 ⊆ 𝑂 ∧ 𝑋 ∈ 𝑂) → (((𝟭‘𝑂)‘𝐴)‘𝑋) = if(𝑋 ∈ 𝐴, 1, 0)) | ||
Theorem | ind1 31176 | Value of the indicator function where it is 1. (Contributed by Thierry Arnoux, 14-Aug-2017.) |
⊢ ((𝑂 ∈ 𝑉 ∧ 𝐴 ⊆ 𝑂 ∧ 𝑋 ∈ 𝐴) → (((𝟭‘𝑂)‘𝐴)‘𝑋) = 1) | ||
Theorem | ind0 31177 | Value of the indicator function where it is 0. (Contributed by Thierry Arnoux, 14-Aug-2017.) |
⊢ ((𝑂 ∈ 𝑉 ∧ 𝐴 ⊆ 𝑂 ∧ 𝑋 ∈ (𝑂 ∖ 𝐴)) → (((𝟭‘𝑂)‘𝐴)‘𝑋) = 0) | ||
Theorem | ind1a 31178 | Value of the indicator function where it is 1. (Contributed by Thierry Arnoux, 22-Aug-2017.) |
⊢ ((𝑂 ∈ 𝑉 ∧ 𝐴 ⊆ 𝑂 ∧ 𝑋 ∈ 𝑂) → ((((𝟭‘𝑂)‘𝐴)‘𝑋) = 1 ↔ 𝑋 ∈ 𝐴)) | ||
Theorem | indpi1 31179 | Preimage of the singleton {1} by the indicator function. See i1f1lem 24219. (Contributed by Thierry Arnoux, 21-Aug-2017.) |
⊢ ((𝑂 ∈ 𝑉 ∧ 𝐴 ⊆ 𝑂) → (◡((𝟭‘𝑂)‘𝐴) “ {1}) = 𝐴) | ||
Theorem | indsum 31180* | Finite sum of a product with the indicator function / Cartesian product with the indicator function. (Contributed by Thierry Arnoux, 14-Aug-2017.) |
⊢ (𝜑 → 𝑂 ∈ Fin) & ⊢ (𝜑 → 𝐴 ⊆ 𝑂) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑂) → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → Σ𝑥 ∈ 𝑂 ((((𝟭‘𝑂)‘𝐴)‘𝑥) · 𝐵) = Σ𝑥 ∈ 𝐴 𝐵) | ||
Theorem | indsumin 31181* | Finite sum of a product with the indicator function / Cartesian product with the indicator function. (Contributed by Thierry Arnoux, 11-Dec-2021.) |
⊢ (𝜑 → 𝑂 ∈ 𝑉) & ⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ (𝜑 → 𝐴 ⊆ 𝑂) & ⊢ (𝜑 → 𝐵 ⊆ 𝑂) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐶 ∈ ℂ) ⇒ ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 ((((𝟭‘𝑂)‘𝐵)‘𝑘) · 𝐶) = Σ𝑘 ∈ (𝐴 ∩ 𝐵)𝐶) | ||
Theorem | prodindf 31182* | The product of indicators is one if and only if all values are in the set. (Contributed by Thierry Arnoux, 11-Dec-2021.) |
⊢ (𝜑 → 𝑂 ∈ 𝑉) & ⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ (𝜑 → 𝐵 ⊆ 𝑂) & ⊢ (𝜑 → 𝐹:𝐴⟶𝑂) ⇒ ⊢ (𝜑 → ∏𝑘 ∈ 𝐴 (((𝟭‘𝑂)‘𝐵)‘(𝐹‘𝑘)) = if(ran 𝐹 ⊆ 𝐵, 1, 0)) | ||
Theorem | indf1o 31183 | The bijection between a power set and the set of indicator functions. (Contributed by Thierry Arnoux, 14-Aug-2017.) |
⊢ (𝑂 ∈ 𝑉 → (𝟭‘𝑂):𝒫 𝑂–1-1-onto→({0, 1} ↑m 𝑂)) | ||
Theorem | indpreima 31184 | A function with range {0, 1} as an indicator of the preimage of {1}. (Contributed by Thierry Arnoux, 23-Aug-2017.) |
⊢ ((𝑂 ∈ 𝑉 ∧ 𝐹:𝑂⟶{0, 1}) → 𝐹 = ((𝟭‘𝑂)‘(◡𝐹 “ {1}))) | ||
Theorem | indf1ofs 31185* | The bijection between finite subsets and the indicator functions with finite support. (Contributed by Thierry Arnoux, 22-Aug-2017.) |
⊢ (𝑂 ∈ 𝑉 → ((𝟭‘𝑂) ↾ Fin):(𝒫 𝑂 ∩ Fin)–1-1-onto→{𝑓 ∈ ({0, 1} ↑m 𝑂) ∣ (◡𝑓 “ {1}) ∈ Fin}) | ||
Syntax | cesum 31186 | Extend class notation to include infinite summations. |
class Σ*𝑘 ∈ 𝐴𝐵 | ||
Definition | df-esum 31187 | Define a short-hand for the possibly infinite sum over the extended nonnegative reals. Σ* is relying on the properties of the tsums, developped by Mario Carneiro. (Contributed by Thierry Arnoux, 21-Sep-2016.) |
⊢ Σ*𝑘 ∈ 𝐴𝐵 = ∪ ((ℝ*𝑠 ↾s (0[,]+∞)) tsums (𝑘 ∈ 𝐴 ↦ 𝐵)) | ||
Theorem | esumex 31188 | An extended sum is a set by definition. (Contributed by Thierry Arnoux, 5-Sep-2017.) |
⊢ Σ*𝑘 ∈ 𝐴𝐵 ∈ V | ||
Theorem | esumcl 31189* | Closure for extended sum in the extended positive reals. (Contributed by Thierry Arnoux, 2-Jan-2017.) |
⊢ Ⅎ𝑘𝐴 ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑘 ∈ 𝐴 𝐵 ∈ (0[,]+∞)) → Σ*𝑘 ∈ 𝐴𝐵 ∈ (0[,]+∞)) | ||
Theorem | esumeq12dvaf 31190 | Equality deduction for extended sum. (Contributed by Thierry Arnoux, 26-Mar-2017.) |
⊢ Ⅎ𝑘𝜑 & ⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐶 = 𝐷) ⇒ ⊢ (𝜑 → Σ*𝑘 ∈ 𝐴𝐶 = Σ*𝑘 ∈ 𝐵𝐷) | ||
Theorem | esumeq12dva 31191* | Equality deduction for extended sum. (Contributed by Thierry Arnoux, 18-Feb-2017.) (Revised by Thierry Arnoux, 29-Jun-2017.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐶 = 𝐷) ⇒ ⊢ (𝜑 → Σ*𝑘 ∈ 𝐴𝐶 = Σ*𝑘 ∈ 𝐵𝐷) | ||
Theorem | esumeq12d 31192* | Equality deduction for extended sum. (Contributed by Thierry Arnoux, 18-Feb-2017.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → 𝐶 = 𝐷) ⇒ ⊢ (𝜑 → Σ*𝑘 ∈ 𝐴𝐶 = Σ*𝑘 ∈ 𝐵𝐷) | ||
Theorem | esumeq1 31193* | Equality theorem for an extended sum. (Contributed by Thierry Arnoux, 18-Feb-2017.) |
⊢ (𝐴 = 𝐵 → Σ*𝑘 ∈ 𝐴𝐶 = Σ*𝑘 ∈ 𝐵𝐶) | ||
Theorem | esumeq1d 31194 | Equality theorem for an extended sum. (Contributed by Thierry Arnoux, 19-Oct-2017.) |
⊢ Ⅎ𝑘𝜑 & ⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → Σ*𝑘 ∈ 𝐴𝐶 = Σ*𝑘 ∈ 𝐵𝐶) | ||
Theorem | esumeq2 31195* | Equality theorem for extended sum. (Contributed by Thierry Arnoux, 24-Dec-2016.) |
⊢ (∀𝑘 ∈ 𝐴 𝐵 = 𝐶 → Σ*𝑘 ∈ 𝐴𝐵 = Σ*𝑘 ∈ 𝐴𝐶) | ||
Theorem | esumeq2d 31196 | Equality deduction for extended sum. (Contributed by Thierry Arnoux, 21-Sep-2016.) |
⊢ Ⅎ𝑘𝜑 & ⊢ (𝜑 → ∀𝑘 ∈ 𝐴 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → Σ*𝑘 ∈ 𝐴𝐵 = Σ*𝑘 ∈ 𝐴𝐶) | ||
Theorem | esumeq2dv 31197* | Equality deduction for extended sum. (Contributed by Thierry Arnoux, 2-Jan-2017.) |
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → Σ*𝑘 ∈ 𝐴𝐵 = Σ*𝑘 ∈ 𝐴𝐶) | ||
Theorem | esumeq2sdv 31198* | Equality deduction for extended sum. (Contributed by Thierry Arnoux, 25-Dec-2016.) |
⊢ (𝜑 → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → Σ*𝑘 ∈ 𝐴𝐵 = Σ*𝑘 ∈ 𝐴𝐶) | ||
Theorem | nfesum1 31199 | Bound-variable hypothesis builder for extended sum. (Contributed by Thierry Arnoux, 19-Oct-2017.) |
⊢ Ⅎ𝑘𝐴 ⇒ ⊢ Ⅎ𝑘Σ*𝑘 ∈ 𝐴𝐵 | ||
Theorem | nfesum2 31200* | Bound-variable hypothesis builder for extended sum. (Contributed by Thierry Arnoux, 2-May-2020.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 ⇒ ⊢ Ⅎ𝑥Σ*𝑘 ∈ 𝐴𝐵 |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |