HomeTheorem List (p. 340 of 499)
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. 340 of 499) | < 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-30888) |
Hilbert Space Explorer
(30889-32411) |
Users' Mathboxes
(32412-49816) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | hauseqcn 33901 | In a Hausdorff topology, two continuous functions which agree on a dense set agree everywhere. (Contributed by Thierry Arnoux, 28-Dec-2017.) |
| ⊢ 𝑋 = ∪ 𝐽 & ⊢ (𝜑 → 𝐾 ∈ Haus) & ⊢ (𝜑 → 𝐹 ∈ (𝐽 Cn 𝐾)) & ⊢ (𝜑 → 𝐺 ∈ (𝐽 Cn 𝐾)) & ⊢ (𝜑 → (𝐹 ↾ 𝐴) = (𝐺 ↾ 𝐴)) & ⊢ (𝜑 → 𝐴 ⊆ 𝑋) & ⊢ (𝜑 → ((cls‘𝐽)‘𝐴) = 𝑋) ⇒ ⊢ (𝜑 → 𝐹 = 𝐺) | ||
| Theorem | elunitge0 33902 | An element of the closed unit interval is positive. Useful lemma for manipulating probabilities within the closed unit interval. (Contributed by Thierry Arnoux, 20-Dec-2016.) |
| ⊢ (𝐴 ∈ (0[,]1) → 0 ≤ 𝐴) | ||
| Theorem | unitssxrge0 33903 | The closed unit interval is a subset of the set of the extended nonnegative reals. Useful lemma for manipulating probabilities within the closed unit interval. (Contributed by Thierry Arnoux, 12-Dec-2016.) |
| ⊢ (0[,]1) ⊆ (0[,]+∞) | ||
| Theorem | unitdivcld 33904 | Necessary conditions for a quotient to be in the closed unit interval. (somewhat too strong, it would be sufficient that A and B are in RR+) (Contributed by Thierry Arnoux, 20-Dec-2016.) |
| ⊢ ((𝐴 ∈ (0[,]1) ∧ 𝐵 ∈ (0[,]1) ∧ 𝐵 ≠ 0) → (𝐴 ≤ 𝐵 ↔ (𝐴 / 𝐵) ∈ (0[,]1))) | ||
| Theorem | iistmd 33905 | The closed unit interval forms a topological monoid under multiplication. (Contributed by Thierry Arnoux, 25-Mar-2017.) |
| ⊢ 𝐼 = ((mulGrp‘ℂfld) ↾s (0[,]1)) ⇒ ⊢ 𝐼 ∈ TopMnd | ||
| Theorem | unicls 33906 | The union of the closed set is the underlying set of the topology. (Contributed by Thierry Arnoux, 21-Sep-2017.) |
| ⊢ 𝐽 ∈ Top & ⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ∪ (Clsd‘𝐽) = 𝑋 | ||
| Theorem | tpr2tp 33907 | The usual topology on (ℝ × ℝ) is the product topology of the usual topology on ℝ. (Contributed by Thierry Arnoux, 21-Sep-2017.) |
| ⊢ 𝐽 = (topGen‘ran (,)) ⇒ ⊢ (𝐽 ×t 𝐽) ∈ (TopOn‘(ℝ × ℝ)) | ||
| Theorem | tpr2uni 33908 | The usual topology on (ℝ × ℝ) is the product topology of the usual topology on ℝ. (Contributed by Thierry Arnoux, 21-Sep-2017.) |
| ⊢ 𝐽 = (topGen‘ran (,)) ⇒ ⊢ ∪ (𝐽 ×t 𝐽) = (ℝ × ℝ) | ||
| Theorem | xpinpreima 33909 | Rewrite the cartesian product of two sets as the intersection of their preimage by 1st and 2nd, the projections on the first and second elements. (Contributed by Thierry Arnoux, 22-Sep-2017.) |
| ⊢ (𝐴 × 𝐵) = ((◡(1st ↾ (V × V)) “ 𝐴) ∩ (◡(2nd ↾ (V × V)) “ 𝐵)) | ||
| Theorem | xpinpreima2 33910 | Rewrite the cartesian product of two sets as the intersection of their preimage by 1st and 2nd, the projections on the first and second elements. (Contributed by Thierry Arnoux, 22-Sep-2017.) |
| ⊢ ((𝐴 ⊆ 𝐸 ∧ 𝐵 ⊆ 𝐹) → (𝐴 × 𝐵) = ((◡(1st ↾ (𝐸 × 𝐹)) “ 𝐴) ∩ (◡(2nd ↾ (𝐸 × 𝐹)) “ 𝐵))) | ||
| Theorem | sqsscirc1 33911 | The complex square of side 𝐷 is a subset of the complex circle of radius 𝐷. (Contributed by Thierry Arnoux, 25-Sep-2017.) |
| ⊢ ((((𝑋 ∈ ℝ ∧ 0 ≤ 𝑋) ∧ (𝑌 ∈ ℝ ∧ 0 ≤ 𝑌)) ∧ 𝐷 ∈ ℝ+) → ((𝑋 < (𝐷 / 2) ∧ 𝑌 < (𝐷 / 2)) → (√‘((𝑋↑2) + (𝑌↑2))) < 𝐷)) | ||
| Theorem | sqsscirc2 33912 | The complex square of side 𝐷 is a subset of the complex disc of radius 𝐷. (Contributed by Thierry Arnoux, 25-Sep-2017.) |
| ⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝐷 ∈ ℝ+) → (((abs‘(ℜ‘(𝐵 − 𝐴))) < (𝐷 / 2) ∧ (abs‘(ℑ‘(𝐵 − 𝐴))) < (𝐷 / 2)) → (abs‘(𝐵 − 𝐴)) < 𝐷)) | ||
| Theorem | cnre2csqlem 33913* | Lemma for cnre2csqima 33914. (Contributed by Thierry Arnoux, 27-Sep-2017.) |
| ⊢ (𝐺 ↾ (ℝ × ℝ)) = (𝐻 ∘ 𝐹) & ⊢ 𝐹 Fn (ℝ × ℝ) & ⊢ 𝐺 Fn V & ⊢ (𝑥 ∈ (ℝ × ℝ) → (𝐺‘𝑥) ∈ ℝ) & ⊢ ((𝑥 ∈ ran 𝐹 ∧ 𝑦 ∈ ran 𝐹) → (𝐻‘(𝑥 − 𝑦)) = ((𝐻‘𝑥) − (𝐻‘𝑦))) ⇒ ⊢ ((𝑋 ∈ (ℝ × ℝ) ∧ 𝑌 ∈ (ℝ × ℝ) ∧ 𝐷 ∈ ℝ+) → (𝑌 ∈ (◡(𝐺 ↾ (ℝ × ℝ)) “ (((𝐺‘𝑋) − 𝐷)(,)((𝐺‘𝑋) + 𝐷))) → (abs‘(𝐻‘((𝐹‘𝑌) − (𝐹‘𝑋)))) < 𝐷)) | ||
| Theorem | cnre2csqima 33914* | Image of a centered square by the canonical bijection from (ℝ × ℝ) to ℂ. (Contributed by Thierry Arnoux, 27-Sep-2017.) |
| ⊢ 𝐹 = (𝑥 ∈ ℝ, 𝑦 ∈ ℝ ↦ (𝑥 + (i · 𝑦))) ⇒ ⊢ ((𝑋 ∈ (ℝ × ℝ) ∧ 𝑌 ∈ (ℝ × ℝ) ∧ 𝐷 ∈ ℝ+) → (𝑌 ∈ ((((1st ‘𝑋) − 𝐷)(,)((1st ‘𝑋) + 𝐷)) × (((2nd ‘𝑋) − 𝐷)(,)((2nd ‘𝑋) + 𝐷))) → ((abs‘(ℜ‘((𝐹‘𝑌) − (𝐹‘𝑋)))) < 𝐷 ∧ (abs‘(ℑ‘((𝐹‘𝑌) − (𝐹‘𝑋)))) < 𝐷))) | ||
| Theorem | tpr2rico 33915* | For any point of an open set of the usual topology on (ℝ × ℝ) there is an open square which contains that point and is entirely in the open set. This is square is actually a ball by the (𝑙↑+∞) norm 𝑋. (Contributed by Thierry Arnoux, 21-Sep-2017.) |
| ⊢ 𝐽 = (topGen‘ran (,)) & ⊢ 𝐺 = (𝑢 ∈ ℝ, 𝑣 ∈ ℝ ↦ (𝑢 + (i · 𝑣))) & ⊢ 𝐵 = ran (𝑥 ∈ ran (,), 𝑦 ∈ ran (,) ↦ (𝑥 × 𝑦)) ⇒ ⊢ ((𝐴 ∈ (𝐽 ×t 𝐽) ∧ 𝑋 ∈ 𝐴) → ∃𝑟 ∈ 𝐵 (𝑋 ∈ 𝑟 ∧ 𝑟 ⊆ 𝐴)) | ||
| Theorem | cnvordtrestixx 33916* | The restriction of the 'greater than' order to an interval gives the same topology as the subspace topology. (Contributed by Thierry Arnoux, 1-Apr-2017.) |
| ⊢ 𝐴 ⊆ ℝ* & ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑥[,]𝑦) ⊆ 𝐴) ⇒ ⊢ ((ordTop‘ ≤ ) ↾t 𝐴) = (ordTop‘(◡ ≤ ∩ (𝐴 × 𝐴))) | ||
| Theorem | prsdm 33917 | Domain of the relation of a proset. (Contributed by Thierry Arnoux, 11-Sep-2015.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = ((le‘𝐾) ∩ (𝐵 × 𝐵)) ⇒ ⊢ (𝐾 ∈ Proset → dom ≤ = 𝐵) | ||
| Theorem | prsrn 33918 | Range of the relation of a proset. (Contributed by Thierry Arnoux, 11-Sep-2018.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = ((le‘𝐾) ∩ (𝐵 × 𝐵)) ⇒ ⊢ (𝐾 ∈ Proset → ran ≤ = 𝐵) | ||
| Theorem | prsss 33919 | Relation of a subproset. (Contributed by Thierry Arnoux, 13-Sep-2018.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = ((le‘𝐾) ∩ (𝐵 × 𝐵)) ⇒ ⊢ ((𝐾 ∈ Proset ∧ 𝐴 ⊆ 𝐵) → ( ≤ ∩ (𝐴 × 𝐴)) = ((le‘𝐾) ∩ (𝐴 × 𝐴))) | ||
| Theorem | prsssdm 33920 | Domain of a subproset relation. (Contributed by Thierry Arnoux, 12-Sep-2018.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = ((le‘𝐾) ∩ (𝐵 × 𝐵)) ⇒ ⊢ ((𝐾 ∈ Proset ∧ 𝐴 ⊆ 𝐵) → dom ( ≤ ∩ (𝐴 × 𝐴)) = 𝐴) | ||
| Theorem | ordtprsval 33921* | Value of the order topology for a proset. (Contributed by Thierry Arnoux, 11-Sep-2015.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = ((le‘𝐾) ∩ (𝐵 × 𝐵)) & ⊢ 𝐸 = ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥}) & ⊢ 𝐹 = ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦}) ⇒ ⊢ (𝐾 ∈ Proset → (ordTop‘ ≤ ) = (topGen‘(fi‘({𝐵} ∪ (𝐸 ∪ 𝐹))))) | ||
| Theorem | ordtprsuni 33922* | Value of the order topology. (Contributed by Thierry Arnoux, 13-Sep-2018.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = ((le‘𝐾) ∩ (𝐵 × 𝐵)) & ⊢ 𝐸 = ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥}) & ⊢ 𝐹 = ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦}) ⇒ ⊢ (𝐾 ∈ Proset → 𝐵 = ∪ ({𝐵} ∪ (𝐸 ∪ 𝐹))) | ||
| Theorem | ordtcnvNEW 33923 | The order dual generates the same topology as the original order. (Contributed by Mario Carneiro, 3-Sep-2015.) (Revised by Thierry Arnoux, 13-Sep-2018.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = ((le‘𝐾) ∩ (𝐵 × 𝐵)) ⇒ ⊢ (𝐾 ∈ Proset → (ordTop‘◡ ≤ ) = (ordTop‘ ≤ )) | ||
| Theorem | ordtrestNEW 33924 | The subspace topology of an order topology is in general finer than the topology generated by the restricted order, but we do have inclusion in one direction. (Contributed by Mario Carneiro, 9-Sep-2015.) (Revised by Thierry Arnoux, 11-Sep-2018.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = ((le‘𝐾) ∩ (𝐵 × 𝐵)) ⇒ ⊢ ((𝐾 ∈ Proset ∧ 𝐴 ⊆ 𝐵) → (ordTop‘( ≤ ∩ (𝐴 × 𝐴))) ⊆ ((ordTop‘ ≤ ) ↾t 𝐴)) | ||
| Theorem | ordtrest2NEWlem 33925* | Lemma for ordtrest2NEW 33926. (Contributed by Mario Carneiro, 9-Sep-2015.) (Revised by Thierry Arnoux, 11-Sep-2018.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = ((le‘𝐾) ∩ (𝐵 × 𝐵)) & ⊢ (𝜑 → 𝐾 ∈ Toset) & ⊢ (𝜑 → 𝐴 ⊆ 𝐵) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → {𝑧 ∈ 𝐵 ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦)} ⊆ 𝐴) ⇒ ⊢ (𝜑 → ∀𝑣 ∈ ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑤 ≤ 𝑧})(𝑣 ∩ 𝐴) ∈ (ordTop‘( ≤ ∩ (𝐴 × 𝐴)))) | ||
| Theorem | ordtrest2NEW 33926* | An interval-closed set 𝐴 in a total order has the same subspace topology as the restricted order topology. (An interval-closed set is the same thing as an open or half-open or closed interval in ℝ, but in other sets like ℚ there are interval-closed sets like (π, +∞) ∩ ℚ that are not intervals.) (Contributed by Mario Carneiro, 9-Sep-2015.) (Revised by Thierry Arnoux, 11-Sep-2018.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = ((le‘𝐾) ∩ (𝐵 × 𝐵)) & ⊢ (𝜑 → 𝐾 ∈ Toset) & ⊢ (𝜑 → 𝐴 ⊆ 𝐵) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → {𝑧 ∈ 𝐵 ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦)} ⊆ 𝐴) ⇒ ⊢ (𝜑 → (ordTop‘( ≤ ∩ (𝐴 × 𝐴))) = ((ordTop‘ ≤ ) ↾t 𝐴)) | ||
| Theorem | ordtconnlem1 33927* | Connectedness in the order topology of a toset. This is the "easy" direction of ordtconn 33928. See also reconnlem1 24735. (Contributed by Thierry Arnoux, 14-Sep-2018.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = ((le‘𝐾) ∩ (𝐵 × 𝐵)) & ⊢ 𝐽 = (ordTop‘ ≤ ) ⇒ ⊢ ((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) → ((𝐽 ↾t 𝐴) ∈ Conn → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑟 ∈ 𝐵 ((𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦) → 𝑟 ∈ 𝐴))) | ||
| Theorem | ordtconn 33928 | Connectedness in the order topology of a complete uniform totally ordered space. (Contributed by Thierry Arnoux, 15-Sep-2018.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = ((le‘𝐾) ∩ (𝐵 × 𝐵)) & ⊢ 𝐽 = (ordTop‘ ≤ ) ⇒ ⊢ ⊤ | ||
| Theorem | mndpluscn 33929* | A mapping that is both a homeomorphism and a monoid homomorphism preserves the "continuousness" of the operation. (Contributed by Thierry Arnoux, 25-Mar-2017.) |
| ⊢ 𝐹 ∈ (𝐽Homeo𝐾) & ⊢ + :(𝐵 × 𝐵)⟶𝐵 & ⊢ ∗ :(𝐶 × 𝐶)⟶𝐶 & ⊢ 𝐽 ∈ (TopOn‘𝐵) & ⊢ 𝐾 ∈ (TopOn‘𝐶) & ⊢ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝐹‘(𝑥 + 𝑦)) = ((𝐹‘𝑥) ∗ (𝐹‘𝑦))) & ⊢ + ∈ ((𝐽 ×t 𝐽) Cn 𝐽) ⇒ ⊢ ∗ ∈ ((𝐾 ×t 𝐾) Cn 𝐾) | ||
| Theorem | mhmhmeotmd 33930 | 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 33931* | Multiplication by a real constant is a continuous function. (Contributed by Thierry Arnoux, 23-May-2017.) Avoid ax-mulf 11078. (Revised by GG, 16-Mar-2025.) |
| ⊢ 𝐽 = (topGen‘ran (,)) & ⊢ (𝜑 → 𝐶 ∈ ℝ) ⇒ ⊢ (𝜑 → (𝑥 ∈ ℝ ↦ (𝑥 · 𝐶)) ∈ (𝐽 Cn 𝐽)) | ||
| Theorem | raddcn 33932* | Addition in the real numbers is a continuous function. (Contributed by Thierry Arnoux, 23-May-2017.) |
| ⊢ 𝐽 = (topGen‘ran (,)) ⇒ ⊢ (𝑥 ∈ ℝ, 𝑦 ∈ ℝ ↦ (𝑥 + 𝑦)) ∈ ((𝐽 ×t 𝐽) Cn 𝐽) | ||
| Theorem | xrmulc1cn 33933* | 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 33934 | 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 33935 | The extended nonnegative reals are homeomorphic to the closed unit interval. (Contributed by Thierry Arnoux, 24-Mar-2017.) |
| ⊢ II ≃ ((ordTop‘ ≤ ) ↾t (0[,]+∞)) | ||
| Theorem | xrge0iifcnv 33936* | Define a bijection from [0, 1] onto [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 33937* | 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 33938* | The defined bijection from the closed unit interval onto 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 33939* | Expose a homeomorphism from the closed unit interval to the extended nonnegative reals. (Contributed by Thierry Arnoux, 1-Apr-2017.) |
| ⊢ 𝐹 = (𝑥 ∈ (0[,]1) ↦ if(𝑥 = 0, +∞, -(log‘𝑥))) & ⊢ 𝐽 = ((ordTop‘ ≤ ) ↾t (0[,]+∞)) ⇒ ⊢ 𝐹 ∈ (IIHomeo𝐽) | ||
| Theorem | xrge0iifhom 33940* | The defined function from the closed unit interval to the extended nonnegative reals is a monoid homomorphism. (Contributed by Thierry Arnoux, 5-Apr-2017.) |
| ⊢ 𝐹 = (𝑥 ∈ (0[,]1) ↦ if(𝑥 = 0, +∞, -(log‘𝑥))) & ⊢ 𝐽 = ((ordTop‘ ≤ ) ↾t (0[,]+∞)) ⇒ ⊢ ((𝑋 ∈ (0[,]1) ∧ 𝑌 ∈ (0[,]1)) → (𝐹‘(𝑋 · 𝑌)) = ((𝐹‘𝑋) +𝑒 (𝐹‘𝑌))) | ||
| Theorem | xrge0iif1 33941* | 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 33942* | The defined function from the closed unit interval to 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 33943* | 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 33944* | 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 33945 | The extended nonnegative real numbers monoid forms a topological space. (Contributed by Thierry Arnoux, 19-Jun-2017.) |
| ⊢ (ℝ*𝑠 ↾s (0[,]+∞)) ∈ TopSp | ||
| Theorem | xrge0topn 33946 | The topology of the extended nonnegative real numbers. (Contributed by Thierry Arnoux, 20-Jun-2017.) |
| ⊢ (TopOpen‘(ℝ*𝑠 ↾s (0[,]+∞))) = ((ordTop‘ ≤ ) ↾t (0[,]+∞)) | ||
| Theorem | xrge0haus 33947 | The topology of the extended nonnegative real numbers is Hausdorff. (Contributed by Thierry Arnoux, 26-Jul-2017.) |
| ⊢ (TopOpen‘(ℝ*𝑠 ↾s (0[,]+∞))) ∈ Haus | ||
| Theorem | xrge0tmd 33948 | 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 | xrge0tmdALT 33949 | Alternate proof of xrge0tmd 33948. (Contributed by Thierry Arnoux, 26-Mar-2017.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ (ℝ*𝑠 ↾s (0[,]+∞)) ∈ TopMnd | ||
| Theorem | lmlim 33950 | 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 33951 | 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 33952 | Implication of convergence for a nonnegative series. This could be used to shorten prmreclem6 16825. (Contributed by Thierry Arnoux, 28-Jul-2017.) |
| ⊢ ((𝐹:ℕ⟶(0[,)+∞) ∧ seq1( + , 𝐹) ∈ dom ⇝ ) → sup(ran seq1( + , 𝐹), ℝ, < ) ∈ ℝ) | ||
| Theorem | fsumcvg4 33953 | 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 33954* | A neighborhood of +∞ contains an unbounded interval based at a real number. See pnfnei 23128. (Contributed by Thierry Arnoux, 31-Jul-2017.) |
| ⊢ 𝐽 = (TopOpen‘(ℝ*𝑠 ↾s (0[,]+∞))) ⇒ ⊢ ((𝐴 ∈ 𝐽 ∧ +∞ ∈ 𝐴) → ∃𝑥 ∈ ℝ (𝑥(,]+∞) ⊆ 𝐴) | ||
| Theorem | lmxrge0 33955* | 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 33956* | If a monotonic sequence of real numbers diverges, it is unbounded. (Contributed by Thierry Arnoux, 4-Aug-2017.) |
| ⊢ (𝜑 → 𝐹:ℕ⟶(0[,)+∞)) & ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐹‘𝑘) ≤ (𝐹‘(𝑘 + 1))) & ⊢ (𝜑 → ¬ 𝐹 ∈ dom ⇝ ) ⇒ ⊢ (𝜑 → ∀𝑥 ∈ ℝ ∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑗)𝑥 < (𝐹‘𝑘)) | ||
| Theorem | lmdvglim 33957* | 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 33958 | A univariate polynomial is continuous. (Contributed by Thierry Arnoux, 17-Sep-2018.) |
| ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐸 = (eval1‘𝑅) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 𝐾 = (Base‘𝑅) & ⊢ 𝐽 = (TopOpen‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝑅 ∈ TopRing) & ⊢ (𝜑 → 𝐹 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝐸‘𝐹) ∈ (𝐽 Cn 𝐽)) | ||
| Syntax | chcmp 33959 | Extend class notation with the Hausdorff uniform completion relation. |
| class HCmp | ||
| Definition | df-hcmp 33960* | 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 uniqueness of such a completion. (Contributed by Thierry Arnoux, 5-Mar-2018.) |
| ⊢ HCmp = {⟨𝑢, 𝑤⟩ ∣ ((𝑢 ∈ ∪ ran UnifOn ∧ 𝑤 ∈ CUnifSp) ∧ ((UnifSt‘𝑤) ↾t dom ∪ 𝑢) = 𝑢 ∧ ((cls‘(TopOpen‘𝑤))‘dom ∪ 𝑢) = (Base‘𝑤))} | ||
| Theorem | zringnm 33961 | 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 33962 | 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 33963 | Zero of a ℤ-module. (Contributed by Thierry Arnoux, 8-Nov-2017.) |
| ⊢ 𝑊 = (ℤMod‘𝐺) & ⊢ 0 = (0g‘𝐺) ⇒ ⊢ 0 = (0g‘𝑊) | ||
| Theorem | zlm1 33964 | Unity element of a ℤ-module (if present). (Contributed by Thierry Arnoux, 8-Nov-2017.) |
| ⊢ 𝑊 = (ℤMod‘𝐺) & ⊢ 1 = (1r‘𝐺) ⇒ ⊢ 1 = (1r‘𝑊) | ||
| Theorem | zlmds 33965 | Distance in a ℤ-module (if present). (Contributed by Thierry Arnoux, 8-Nov-2017.) (Proof shortened by AV, 11-Nov-2024.) |
| ⊢ 𝑊 = (ℤMod‘𝐺) & ⊢ 𝐷 = (dist‘𝐺) ⇒ ⊢ (𝐺 ∈ 𝑉 → 𝐷 = (dist‘𝑊)) | ||
| Theorem | zlmtset 33966 | Topology in a ℤ-module (if present). (Contributed by Thierry Arnoux, 8-Nov-2017.) (Proof shortened by AV, 12-Nov-2024.) |
| ⊢ 𝑊 = (ℤMod‘𝐺) & ⊢ 𝐽 = (TopSet‘𝐺) ⇒ ⊢ (𝐺 ∈ 𝑉 → 𝐽 = (TopSet‘𝑊)) | ||
| Theorem | zlmnm 33967 | Norm of a ℤ-module (if present). (Contributed by Thierry Arnoux, 8-Nov-2017.) |
| ⊢ 𝑊 = (ℤMod‘𝐺) & ⊢ 𝑁 = (norm‘𝐺) ⇒ ⊢ (𝐺 ∈ 𝑉 → 𝑁 = (norm‘𝑊)) | ||
| Theorem | zhmnrg 33968 | The ℤ-module built from a normed ring is also a normed ring. (Contributed by Thierry Arnoux, 8-Nov-2017.) |
| ⊢ 𝑊 = (ℤMod‘𝐺) ⇒ ⊢ (𝐺 ∈ NrmRing → 𝑊 ∈ NrmRing) | ||
| Theorem | nmmulg 33969 | 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 33970 | 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 33971 | The ℤ-module of ℂ is a normed module. (Contributed by Thierry Arnoux, 25-Feb-2018.) |
| ⊢ (ℤMod‘ℂfld) ∈ NrmMod | ||
| Theorem | rezh 33972 | The ℤ-module of ℝ is a normed module. (Contributed by Thierry Arnoux, 14-Feb-2018.) |
| ⊢ (ℤMod‘ℝfld) ∈ NrmMod | ||
| Syntax | cqqh 33973 | Map the rationals into a field. |
| class ℚHom | ||
| Definition | df-qqh 33974* | 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 33975* | 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 33976 | 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 33977 | 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 33978 | 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 33979 | The preimage by ℤRHom of the units of a division ring is (ℤ ∖ {0}). (Contributed by Thierry Arnoux, 22-Oct-2017.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝐿 = (ℤRHom‘𝑅) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ ((𝑅 ∈ DivRing ∧ (chr‘𝑅) = 0) → (◡𝐿 “ (Unit‘𝑅)) = (ℤ ∖ {0})) | ||
| Theorem | elzrhunit 33980 | 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 | zrhneg 33981 | The canonical homomorphism from the integers to a ring 𝑅 maps additive inverses to additive inverses. (Contributed by Thierry Arnoux, 5-Oct-2025.) |
| ⊢ 𝐿 = (ℤRHom‘𝑅) & ⊢ 𝐼 = (invg‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝑁 ∈ ℤ) ⇒ ⊢ (𝜑 → (𝐿‘-𝑁) = (𝐼‘(𝐿‘𝑁))) | ||
| Theorem | zrhcntr 33982 | The canonical representation of an integer 𝑁 in a ring 𝑅 is in the centralizer of the ring's multiplicative monoid. (Contributed by Thierry Arnoux, 5-Oct-2025.) |
| ⊢ 𝑀 = (mulGrp‘𝑅) & ⊢ 𝐶 = (Cntr‘𝑀) & ⊢ 𝐿 = (ℤRHom‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝑁 ∈ ℤ) ⇒ ⊢ (𝜑 → (𝐿‘𝑁) ∈ 𝐶) | ||
| Theorem | elzdif0 33983 | Lemma for qqhval2 33985. (Contributed by Thierry Arnoux, 29-Oct-2017.) |
| ⊢ (𝑀 ∈ (ℤ ∖ {0}) → (𝑀 ∈ ℕ ∨ -𝑀 ∈ ℕ)) | ||
| Theorem | qqhval2lem 33984 | Lemma for qqhval2 33985. (Contributed by Thierry Arnoux, 29-Oct-2017.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ / = (/r‘𝑅) & ⊢ 𝐿 = (ℤRHom‘𝑅) ⇒ ⊢ (((𝑅 ∈ DivRing ∧ (chr‘𝑅) = 0) ∧ (𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ∧ 𝑌 ≠ 0)) → ((𝐿‘(numer‘(𝑋 / 𝑌))) / (𝐿‘(denom‘(𝑋 / 𝑌)))) = ((𝐿‘𝑋) / (𝐿‘𝑌))) | ||
| Theorem | qqhval2 33985* | 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 33986 | 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 33987 | 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 33988 | The image of 1 by the ℚHom homomorphism is the ring unity. (Contributed by Thierry Arnoux, 22-Oct-2017.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ / = (/r‘𝑅) & ⊢ 𝐿 = (ℤRHom‘𝑅) ⇒ ⊢ ((𝑅 ∈ DivRing ∧ (chr‘𝑅) = 0) → ((ℚHom‘𝑅)‘1) = (1r‘𝑅)) | ||
| Theorem | qqhf 33989 | ℚHom as a function. (Contributed by Thierry Arnoux, 28-Oct-2017.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ / = (/r‘𝑅) & ⊢ 𝐿 = (ℤRHom‘𝑅) ⇒ ⊢ ((𝑅 ∈ DivRing ∧ (chr‘𝑅) = 0) → (ℚHom‘𝑅):ℚ⟶𝐵) | ||
| Theorem | qqhvq 33990 | 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 33991 | 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 33992 | 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 33993 | 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 33994 | 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 33995 | 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 33996 | Map the real numbers into a complete field. |
| class ℝHom | ||
| Syntax | crrext 33997 | Extend class notation with the class of extension fields of ℝ. |
| class ℝExt | ||
| Definition | df-rrh 33998 | 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 33999 | 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 34000 | 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 𝐾)) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |