Home | Metamath
Proof Explorer Theorem List (p. 294 of 424) | < 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-27159) |
Hilbert Space Explorer
(27160-28684) |
Users' Mathboxes
(28685-42360) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | mhmhmeotmd 29301 | Deduce a Topological Monoid using mapping that is both a homeomorphism and a monoid homomorphism. (Contributed by Thierry Arnoux, 21-Jun-2017.) |
⊢ 𝐹 ∈ (𝑆 MndHom 𝑇) & ⊢ 𝐹 ∈ ((TopOpen‘𝑆)Homeo(TopOpen‘𝑇)) & ⊢ 𝑆 ∈ TopMnd & ⊢ 𝑇 ∈ TopSp ⇒ ⊢ 𝑇 ∈ TopMnd | ||
Theorem | rmulccn 29302* | Multiplication by a real constant is a continuous function. (Contributed by Thierry Arnoux, 23-May-2017.) |
⊢ 𝐽 = (topGen‘ran (,)) & ⊢ (𝜑 → 𝐶 ∈ ℝ) ⇒ ⊢ (𝜑 → (𝑥 ∈ ℝ ↦ (𝑥 · 𝐶)) ∈ (𝐽 Cn 𝐽)) | ||
Theorem | raddcn 29303* | Addition in the real numbers is a continuous function. (Contributed by Thierry Arnoux, 23-May-2017.) |
⊢ 𝐽 = (topGen‘ran (,)) ⇒ ⊢ (𝑥 ∈ ℝ, 𝑦 ∈ ℝ ↦ (𝑥 + 𝑦)) ∈ ((𝐽 ×t 𝐽) Cn 𝐽) | ||
Theorem | xrmulc1cn 29304* | The operation multiplying an extended real number by a nonnegative constant is continuous. (Contributed by Thierry Arnoux, 5-Jul-2017.) |
⊢ 𝐽 = (ordTop‘ ≤ ) & ⊢ 𝐹 = (𝑥 ∈ ℝ* ↦ (𝑥 ·e 𝐶)) & ⊢ (𝜑 → 𝐶 ∈ ℝ+) ⇒ ⊢ (𝜑 → 𝐹 ∈ (𝐽 Cn 𝐽)) | ||
Theorem | fmcncfil 29305 | The image of a Cauchy filter by a continuous filter map is a Cauchy filter. (Contributed by Thierry Arnoux, 12-Nov-2017.) |
⊢ 𝐽 = (MetOpen‘𝐷) & ⊢ 𝐾 = (MetOpen‘𝐸) ⇒ ⊢ (((𝐷 ∈ (CMet‘𝑋) ∧ 𝐸 ∈ (∞Met‘𝑌) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ 𝐵 ∈ (CauFil‘𝐷)) → ((𝑌 FilMap 𝐹)‘𝐵) ∈ (CauFil‘𝐸)) | ||
Theorem | xrge0hmph 29306 | The extended nonnegative reals are homeomorphic to the closed unit interval. (Contributed by Thierry Arnoux, 24-Mar-2017.) |
⊢ II ≃ ((ordTop‘ ≤ ) ↾t (0[,]+∞)) | ||
Theorem | xrge0iifcnv 29307* | Define a bijection from [0, 1] to [0, +∞]. (Contributed by Thierry Arnoux, 29-Mar-2017.) |
⊢ 𝐹 = (𝑥 ∈ (0[,]1) ↦ if(𝑥 = 0, +∞, -(log‘𝑥))) ⇒ ⊢ (𝐹:(0[,]1)–1-1-onto→(0[,]+∞) ∧ ◡𝐹 = (𝑦 ∈ (0[,]+∞) ↦ if(𝑦 = +∞, 0, (exp‘-𝑦)))) | ||
Theorem | xrge0iifcv 29308* | The defined function's value in the real. (Contributed by Thierry Arnoux, 1-Apr-2017.) |
⊢ 𝐹 = (𝑥 ∈ (0[,]1) ↦ if(𝑥 = 0, +∞, -(log‘𝑥))) ⇒ ⊢ (𝑋 ∈ (0(,]1) → (𝐹‘𝑋) = -(log‘𝑋)) | ||
Theorem | xrge0iifiso 29309* | The defined bijection from the closed unit interval and the extended nonnegative reals is an order isomorphism. (Contributed by Thierry Arnoux, 31-Mar-2017.) |
⊢ 𝐹 = (𝑥 ∈ (0[,]1) ↦ if(𝑥 = 0, +∞, -(log‘𝑥))) ⇒ ⊢ 𝐹 Isom < , ◡ < ((0[,]1), (0[,]+∞)) | ||
Theorem | xrge0iifhmeo 29310* | Expose a homeomorphism from the closed unit interval and the extended nonnegative reals. (Contributed by Thierry Arnoux, 1-Apr-2017.) |
⊢ 𝐹 = (𝑥 ∈ (0[,]1) ↦ if(𝑥 = 0, +∞, -(log‘𝑥))) & ⊢ 𝐽 = ((ordTop‘ ≤ ) ↾t (0[,]+∞)) ⇒ ⊢ 𝐹 ∈ (IIHomeo𝐽) | ||
Theorem | xrge0iifhom 29311* | The defined function from the closed unit interval and the extended nonnegative reals is also a monoid homomorphism. (Contributed by Thierry Arnoux, 5-Apr-2017.) |
⊢ 𝐹 = (𝑥 ∈ (0[,]1) ↦ if(𝑥 = 0, +∞, -(log‘𝑥))) & ⊢ 𝐽 = ((ordTop‘ ≤ ) ↾t (0[,]+∞)) ⇒ ⊢ ((𝑋 ∈ (0[,]1) ∧ 𝑌 ∈ (0[,]1)) → (𝐹‘(𝑋 · 𝑌)) = ((𝐹‘𝑋) +𝑒 (𝐹‘𝑌))) | ||
Theorem | xrge0iif1 29312* | Condition for the defined function, -(log‘𝑥) to be a monoid homomorphism. (Contributed by Thierry Arnoux, 20-Jun-2017.) |
⊢ 𝐹 = (𝑥 ∈ (0[,]1) ↦ if(𝑥 = 0, +∞, -(log‘𝑥))) & ⊢ 𝐽 = ((ordTop‘ ≤ ) ↾t (0[,]+∞)) ⇒ ⊢ (𝐹‘1) = 0 | ||
Theorem | xrge0iifmhm 29313* | The defined function from the closed unit interval and the extended nonnegative reals is a monoid homomorphism. (Contributed by Thierry Arnoux, 21-Jun-2017.) |
⊢ 𝐹 = (𝑥 ∈ (0[,]1) ↦ if(𝑥 = 0, +∞, -(log‘𝑥))) & ⊢ 𝐽 = ((ordTop‘ ≤ ) ↾t (0[,]+∞)) ⇒ ⊢ 𝐹 ∈ (((mulGrp‘ℂfld) ↾s (0[,]1)) MndHom (ℝ*𝑠 ↾s (0[,]+∞))) | ||
Theorem | xrge0pluscn 29314* | The addition operation of the extended nonnegative real numbers monoid is continuous. (Contributed by Thierry Arnoux, 24-Mar-2017.) |
⊢ 𝐹 = (𝑥 ∈ (0[,]1) ↦ if(𝑥 = 0, +∞, -(log‘𝑥))) & ⊢ 𝐽 = ((ordTop‘ ≤ ) ↾t (0[,]+∞)) & ⊢ + = ( +𝑒 ↾ ((0[,]+∞) × (0[,]+∞))) ⇒ ⊢ + ∈ ((𝐽 ×t 𝐽) Cn 𝐽) | ||
Theorem | xrge0mulc1cn 29315* | The operation multiplying a nonnegative real numbers by a nonnegative constant is continuous. (Contributed by Thierry Arnoux, 6-Jul-2017.) |
⊢ 𝐽 = ((ordTop‘ ≤ ) ↾t (0[,]+∞)) & ⊢ 𝐹 = (𝑥 ∈ (0[,]+∞) ↦ (𝑥 ·e 𝐶)) & ⊢ (𝜑 → 𝐶 ∈ (0[,)+∞)) ⇒ ⊢ (𝜑 → 𝐹 ∈ (𝐽 Cn 𝐽)) | ||
Theorem | xrge0tps 29316 | The extended nonnegative real numbers monoid forms a topological space. (Contributed by Thierry Arnoux, 19-Jun-2017.) |
⊢ (ℝ*𝑠 ↾s (0[,]+∞)) ∈ TopSp | ||
Theorem | xrge0topn 29317 | The topology of the extended nonnegative real numbers. (Contributed by Thierry Arnoux, 20-Jun-2017.) |
⊢ (TopOpen‘(ℝ*𝑠 ↾s (0[,]+∞))) = ((ordTop‘ ≤ ) ↾t (0[,]+∞)) | ||
Theorem | xrge0haus 29318 | The topology of the extended nonnegative real numbers is Hausdorff. (Contributed by Thierry Arnoux, 26-Jul-2017.) |
⊢ (TopOpen‘(ℝ*𝑠 ↾s (0[,]+∞))) ∈ Haus | ||
Theorem | xrge0tmdOLD 29319 | The extended nonnegative real numbers monoid is a topological monoid. (Contributed by Thierry Arnoux, 26-Mar-2017.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (ℝ*𝑠 ↾s (0[,]+∞)) ∈ TopMnd | ||
Theorem | xrge0tmd 29320 | The extended nonnegative real numbers monoid is a topological monoid. (Contributed by Thierry Arnoux, 26-Mar-2017.) (Proof Shortened by Thierry Arnoux, 21-Jun-2017.) |
⊢ (ℝ*𝑠 ↾s (0[,]+∞)) ∈ TopMnd | ||
Theorem | lmlim 29321 | Relate a limit in a given topology to a complex number limit, provided that topology agrees with the common topology on ℂ on the required subset. (Contributed by Thierry Arnoux, 11-Jul-2017.) |
⊢ 𝐽 ∈ (TopOn‘𝑌) & ⊢ (𝜑 → 𝐹:ℕ⟶𝑋) & ⊢ (𝜑 → 𝑃 ∈ 𝑋) & ⊢ (𝐽 ↾t 𝑋) = ((TopOpen‘ℂfld) ↾t 𝑋) & ⊢ 𝑋 ⊆ ℂ ⇒ ⊢ (𝜑 → (𝐹(⇝𝑡‘𝐽)𝑃 ↔ 𝐹 ⇝ 𝑃)) | ||
Theorem | lmlimxrge0 29322 | Relate a limit in the nonnegative extended reals to a complex limit, provided the considered function is a real function. (Contributed by Thierry Arnoux, 11-Jul-2017.) |
⊢ 𝐽 = (TopOpen‘(ℝ*𝑠 ↾s (0[,]+∞))) & ⊢ (𝜑 → 𝐹:ℕ⟶𝑋) & ⊢ (𝜑 → 𝑃 ∈ 𝑋) & ⊢ 𝑋 ⊆ (0[,)+∞) ⇒ ⊢ (𝜑 → (𝐹(⇝𝑡‘𝐽)𝑃 ↔ 𝐹 ⇝ 𝑃)) | ||
Theorem | rge0scvg 29323 | Implication of convergence for a nonnegative series. This could be used to shorten prmreclem6 15463. (Contributed by Thierry Arnoux, 28-Jul-2017.) |
⊢ ((𝐹:ℕ⟶(0[,)+∞) ∧ seq1( + , 𝐹) ∈ dom ⇝ ) → sup(ran seq1( + , 𝐹), ℝ, < ) ∈ ℝ) | ||
Theorem | fsumcvg4 29324 | A serie with finite support is a finite sum, and therefore converges. (Contributed by Thierry Arnoux, 6-Sep-2017.) (Revised by Thierry Arnoux, 1-Sep-2019.) |
⊢ 𝑆 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐹:𝑆⟶ℂ) & ⊢ (𝜑 → (◡𝐹 “ (ℂ ∖ {0})) ∈ Fin) ⇒ ⊢ (𝜑 → seq𝑀( + , 𝐹) ∈ dom ⇝ ) | ||
Theorem | pnfneige0 29325* | A neighborhood of +∞ contains an unbounded interval based at a real number. See pnfnei 20834. (Contributed by Thierry Arnoux, 31-Jul-2017.) |
⊢ 𝐽 = (TopOpen‘(ℝ*𝑠 ↾s (0[,]+∞))) ⇒ ⊢ ((𝐴 ∈ 𝐽 ∧ +∞ ∈ 𝐴) → ∃𝑥 ∈ ℝ (𝑥(,]+∞) ⊆ 𝐴) | ||
Theorem | lmxrge0 29326* | Express "sequence 𝐹 converges to plus infinity" (i.e. diverges), for a sequence of nonnegative extended real numbers. (Contributed by Thierry Arnoux, 2-Aug-2017.) |
⊢ 𝐽 = (TopOpen‘(ℝ*𝑠 ↾s (0[,]+∞))) & ⊢ (𝜑 → 𝐹:ℕ⟶(0[,]+∞)) & ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐹‘𝑘) = 𝐴) ⇒ ⊢ (𝜑 → (𝐹(⇝𝑡‘𝐽)+∞ ↔ ∀𝑥 ∈ ℝ ∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑗)𝑥 < 𝐴)) | ||
Theorem | lmdvg 29327* | If a monotonic sequence of real numbers diverges, it is unbounded. (Contributed by Thierry Arnoux, 4-Aug-2017.) |
⊢ (𝜑 → 𝐹:ℕ⟶(0[,)+∞)) & ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐹‘𝑘) ≤ (𝐹‘(𝑘 + 1))) & ⊢ (𝜑 → ¬ 𝐹 ∈ dom ⇝ ) ⇒ ⊢ (𝜑 → ∀𝑥 ∈ ℝ ∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑗)𝑥 < (𝐹‘𝑘)) | ||
Theorem | lmdvglim 29328* | If a monotonic real number sequence 𝐹 diverges, it converges in the extended real numbers and its limit is plus infinity. (Contributed by Thierry Arnoux, 3-Aug-2017.) |
⊢ 𝐽 = (TopOpen‘(ℝ*𝑠 ↾s (0[,]+∞))) & ⊢ (𝜑 → 𝐹:ℕ⟶(0[,)+∞)) & ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐹‘𝑘) ≤ (𝐹‘(𝑘 + 1))) & ⊢ (𝜑 → ¬ 𝐹 ∈ dom ⇝ ) ⇒ ⊢ (𝜑 → 𝐹(⇝𝑡‘𝐽)+∞) | ||
Theorem | pl1cn 29329 | A univariate polynomial is continuous. (Contributed by Thierry Arnoux, 17-Sep-2018.) |
⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐸 = (eval1‘𝑅) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 𝐾 = (Base‘𝑅) & ⊢ 𝐽 = (TopOpen‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝑅 ∈ TopRing) & ⊢ (𝜑 → 𝐹 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝐸‘𝐹) ∈ (𝐽 Cn 𝐽)) | ||
Syntax | chcmp 29330 | Extend class notation with the Hausdorff uniform completion relation. |
class HCmp | ||
Definition | df-hcmp 29331* | Definition of the Hausdorff completion. In this definition, a structure 𝑤 is a Hausdorff completion of a uniform structure 𝑢 if 𝑤 is a complete uniform space, in which 𝑢 is dense, and which admits the same uniform structure. Theorem 3 of [BourbakiTop1] p. II.21. states the existence and unicity of such a completion. (Contributed by Thierry Arnoux, 5-Mar-2018.) |
⊢ HCmp = {〈𝑢, 𝑤〉 ∣ ((𝑢 ∈ ∪ ran UnifOn ∧ 𝑤 ∈ CUnifSp) ∧ ((UnifSt‘𝑤) ↾t dom ∪ 𝑢) = 𝑢 ∧ ((cls‘(TopOpen‘𝑤))‘dom ∪ 𝑢) = (Base‘𝑤))} | ||
Theorem | zringnm 29332 | 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 29333 | 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 29334 | Zero of a ℤ-module. (Contributed by Thierry Arnoux, 8-Nov-2017.) |
⊢ 𝑊 = (ℤMod‘𝐺) & ⊢ 0 = (0g‘𝐺) ⇒ ⊢ 0 = (0g‘𝑊) | ||
Theorem | zlm1 29335 | Unit of a ℤ-module (if present). (Contributed by Thierry Arnoux, 8-Nov-2017.) |
⊢ 𝑊 = (ℤMod‘𝐺) & ⊢ 1 = (1r‘𝐺) ⇒ ⊢ 1 = (1r‘𝑊) | ||
Theorem | zlmds 29336 | Distance in a ℤ-module (if present). (Contributed by Thierry Arnoux, 8-Nov-2017.) |
⊢ 𝑊 = (ℤMod‘𝐺) & ⊢ 𝐷 = (dist‘𝐺) ⇒ ⊢ (𝐺 ∈ 𝑉 → 𝐷 = (dist‘𝑊)) | ||
Theorem | zlmtset 29337 | Topology in a ℤ-module (if present). (Contributed by Thierry Arnoux, 8-Nov-2017.) |
⊢ 𝑊 = (ℤMod‘𝐺) & ⊢ 𝐽 = (TopSet‘𝐺) ⇒ ⊢ (𝐺 ∈ 𝑉 → 𝐽 = (TopSet‘𝑊)) | ||
Theorem | zlmnm 29338 | Norm of a ℤ-module (if present). (Contributed by Thierry Arnoux, 8-Nov-2017.) |
⊢ 𝑊 = (ℤMod‘𝐺) & ⊢ 𝑁 = (norm‘𝐺) ⇒ ⊢ (𝐺 ∈ 𝑉 → 𝑁 = (norm‘𝑊)) | ||
Theorem | zhmnrg 29339 | The ℤ-module built from a normed ring is also a normed ring. (Contributed by Thierry Arnoux, 8-Nov-2017.) |
⊢ 𝑊 = (ℤMod‘𝐺) ⇒ ⊢ (𝐺 ∈ NrmRing → 𝑊 ∈ NrmRing) | ||
Theorem | nmmulg 29340 | 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 29341 | 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 29342 | The ℤ-module of ℂ is a normed module. (Contributed by Thierry Arnoux, 25-Feb-2018.) |
⊢ (ℤMod‘ℂfld) ∈ NrmMod | ||
Theorem | rezh 29343 | The ℤ-module of ℝ is a normed module. (Contributed by Thierry Arnoux, 14-Feb-2018.) |
⊢ (ℤMod‘ℝfld) ∈ NrmMod | ||
Syntax | cqqh 29344 | Map the rationals into a field. |
class ℚHom | ||
Definition | df-qqh 29345* | 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 29346* | 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 29347 | The kernel of the homomorphism from the integers to a ring, if it is injective. (Contributed by Thierry Arnoux, 26-Oct-2017.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝐿 = (ℤRHom‘𝑅) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ (𝑅 ∈ Ring → (𝐿:ℤ–1-1→𝐵 ↔ (◡𝐿 “ { 0 }) = {0})) | ||
Theorem | zrhchr 29348 | 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 29349 | 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 29350 | 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 29351 | 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 29352 | Lemma for qqhval2 29354. (Contributed by Thierry Arnoux, 29-Oct-2017.) |
⊢ (𝑀 ∈ (ℤ ∖ {0}) → (𝑀 ∈ ℕ ∨ -𝑀 ∈ ℕ)) | ||
Theorem | qqhval2lem 29353 | Lemma for qqhval2 29354. (Contributed by Thierry Arnoux, 29-Oct-2017.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ / = (/r‘𝑅) & ⊢ 𝐿 = (ℤRHom‘𝑅) ⇒ ⊢ (((𝑅 ∈ DivRing ∧ (chr‘𝑅) = 0) ∧ (𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ∧ 𝑌 ≠ 0)) → ((𝐿‘(numer‘(𝑋 / 𝑌))) / (𝐿‘(denom‘(𝑋 / 𝑌)))) = ((𝐿‘𝑋) / (𝐿‘𝑌))) | ||
Theorem | qqhval2 29354* | 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 29355 | 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 29356 | 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 29357 | 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 29358 | ℚHom as a function. (Contributed by Thierry Arnoux, 28-Oct-2017.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ / = (/r‘𝑅) & ⊢ 𝐿 = (ℤRHom‘𝑅) ⇒ ⊢ ((𝑅 ∈ DivRing ∧ (chr‘𝑅) = 0) → (ℚHom‘𝑅):ℚ⟶𝐵) | ||
Theorem | qqhvq 29359 | 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 29360 | 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 29361 | 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 29362 | 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 29363 | 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 29364 | 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 29365 | Map the real numbers into a complete field. |
class ℝHom | ||
Syntax | crrext 29366 | Extend class notation with the class of extension fields of ℝ. |
class ℝExt | ||
Definition | df-rrh 29367 | 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 29368 | 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 29369 | 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 29370 | 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 29371 | 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 29372 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 29372 | 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 29373 | An extension of ℝ is a normed ring. (Contributed by Thierry Arnoux, 2-May-2018.) |
⊢ (𝑅 ∈ ℝExt → 𝑅 ∈ NrmRing) | ||
Theorem | rrextdrg 29374 | An extension of ℝ is a division ring. (Contributed by Thierry Arnoux, 2-May-2018.) |
⊢ (𝑅 ∈ ℝExt → 𝑅 ∈ DivRing) | ||
Theorem | rrextnlm 29375 | The norm of an extension of ℝ is absolutely homogeneous. (Contributed by Thierry Arnoux, 2-May-2018.) |
⊢ 𝑍 = (ℤMod‘𝑅) ⇒ ⊢ (𝑅 ∈ ℝExt → 𝑍 ∈ NrmMod) | ||
Theorem | rrextchr 29376 | The ring characteristic of an extension of ℝ is zero. (Contributed by Thierry Arnoux, 2-May-2018.) |
⊢ (𝑅 ∈ ℝExt → (chr‘𝑅) = 0) | ||
Theorem | rrextcusp 29377 | An extension of ℝ is a complete uniform space. (Contributed by Thierry Arnoux, 2-May-2018.) |
⊢ (𝑅 ∈ ℝExt → 𝑅 ∈ CUnifSp) | ||
Theorem | rrexttps 29378 | An extension of ℝ is a topological space. (Contributed by Thierry Arnoux, 7-Sep-2018.) |
⊢ (𝑅 ∈ ℝExt → 𝑅 ∈ TopSp) | ||
Theorem | rrexthaus 29379 | The topology of an extension of ℝ is Hausdorff. (Contributed by Thierry Arnoux, 7-Sep-2018.) |
⊢ 𝐾 = (TopOpen‘𝑅) ⇒ ⊢ (𝑅 ∈ ℝExt → 𝐾 ∈ Haus) | ||
Theorem | rrextust 29380 | 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 29381 | The field of the real numbers is an extension of the real numbers. (Contributed by Thierry Arnoux, 2-May-2018.) |
⊢ ℝfld ∈ ℝExt | ||
Theorem | cnrrext 29382 | The field of the complex numbers is an extension of the real numbers. (Contributed by Thierry Arnoux, 2-May-2018.) |
⊢ ℂfld ∈ ℝExt | ||
Theorem | qqtopn 29383 | The topology of the field of the rational numbers. (Contributed by Thierry Arnoux, 29-Aug-2020.) |
⊢ ((TopOpen‘ℝfld) ↾t ℚ) = (TopOpen‘(ℂfld ↾s ℚ)) | ||
Theorem | rrhfe 29384 | 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 29385 | 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 29386 | The ℝHom homomorphism leaves rational numbers unchanged. (Contributed by Thierry Arnoux, 27-Mar-2018.) |
⊢ ((𝑅 ∈ ℝExt ∧ 𝑄 ∈ ℚ) → ((ℝHom‘𝑅)‘𝑄) = ((ℚHom‘𝑅)‘𝑄)) | ||
Theorem | rrh0 29387 | 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 29388 | Map the extended real numbers into a complete lattice. |
class ℝ*Hom | ||
Definition | df-xrh 29389* | 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 29390* | 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 29391 | The ℤRHom homomorphism for the real number structure is the identity. (Contributed by Thierry Arnoux, 31-Oct-2017.) |
⊢ (ℤRHom‘ℝfld) = ( I ↾ ℤ) | ||
Theorem | qqhre 29392 | The ℚHom homomorphism for the real number structure is the identity. (Contributed by Thierry Arnoux, 31-Oct-2017.) |
⊢ (ℚHom‘ℝfld) = ( I ↾ ℚ) | ||
Theorem | rrhre 29393 | 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 characterise topological manifold, and then to extends 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 29394 | The class of n-manifold topologies. |
class ManTop | ||
Definition | df-mntop 29395* | 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 29396 | Manifold is a relation. (Contributed by Thierry Arnoux, 28-Dec-2019.) |
⊢ Rel ManTop | ||
Theorem | ismntoplly 29397 | Property of being a manifold. (Contributed by Thierry Arnoux, 28-Dec-2019.) |
⊢ ((𝑁 ∈ ℕ0 ∧ 𝐽 ∈ 𝑉) → (𝑁ManTop𝐽 ↔ (𝐽 ∈ 2nd𝜔 ∧ 𝐽 ∈ Haus ∧ 𝐽 ∈ Locally [(TopOpen‘(𝔼hil‘𝑁))] ≃ ))) | ||
Theorem | ismntop 29398* | Property of being a manifold. (Contributed by Thierry Arnoux, 5-Jan-2020.) |
⊢ ((𝑁 ∈ ℕ0 ∧ 𝐽 ∈ 𝑉) → (𝑁ManTop𝐽 ↔ (𝐽 ∈ 2nd𝜔 ∧ 𝐽 ∈ Haus ∧ ∀𝑥 ∈ 𝐽 ∀𝑦 ∈ 𝑥 ∃𝑢 ∈ (𝐽 ∩ 𝒫 𝑥)(𝑦 ∈ 𝑢 ∧ (𝐽 ↾t 𝑢) ≃ (TopOpen‘(𝔼hil‘𝑁)))))) | ||
Theorem | nexple 29399 | A lower bound for an exponentiation. (Contributed by Thierry Arnoux, 19-Aug-2017.) |
⊢ ((𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℝ ∧ 2 ≤ 𝐵) → 𝐴 ≤ (𝐵↑𝐴)) | ||
Syntax | cind 29400 | Extend class notation with the indicator function generator. |
class 𝟭 |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |