HomeTheorem List (p. 347 of 513)
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. 347 of 513) | < 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-31550) |
Hilbert Space Explorer
(31551-33073) |
Users' Mathboxes
(33074-51270) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | elunitge0 34601 | 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 34602 | 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 34603 | 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 34604 | 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 34605 | The union of the closed set is the underlying set of the topology. (Contributed by Thierry Arnoux, 21-Sep-2017.) |
| ⊢ 𝐽 ∈ Top & ⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ∪ (Clsd‘𝐽) = 𝑋 | ||
| Theorem | tpr2tp 34606 | 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 34607 | 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 34608 | 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 34609 | 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 34610 | 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 34611 | 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 34612* | Lemma for cnre2csqima 34613. (Contributed by Thierry Arnoux, 27-Sep-2017.) |
| ⊢ (𝐺 ↾ (ℝ × ℝ)) = (𝐻 ∘ 𝐹) & ⊢ 𝐹 Fn (ℝ × ℝ) & ⊢ 𝐺 Fn V & ⊢ (𝑥 ∈ (ℝ × ℝ) → (𝐺‘𝑥) ∈ ℝ) & ⊢ ((𝑥 ∈ ran 𝐹 ∧ 𝑦 ∈ ran 𝐹) → (𝐻‘(𝑥 − 𝑦)) = ((𝐻‘𝑥) − (𝐻‘𝑦))) ⇒ ⊢ ((𝑋 ∈ (ℝ × ℝ) ∧ 𝑌 ∈ (ℝ × ℝ) ∧ 𝐷 ∈ ℝ+) → (𝑌 ∈ (◡(𝐺 ↾ (ℝ × ℝ)) “ (((𝐺‘𝑋) − 𝐷)(,)((𝐺‘𝑋) + 𝐷))) → (abs‘(𝐻‘((𝐹‘𝑌) − (𝐹‘𝑋)))) < 𝐷)) | ||
| Theorem | cnre2csqima 34613* | 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 34614* | 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 34615* | 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 34616 | Domain of the relation of a proset. (Contributed by Thierry Arnoux, 11-Sep-2015.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = ((le‘𝐾) ∩ (𝐵 × 𝐵)) ⇒ ⊢ (𝐾 ∈ Proset → dom ≤ = 𝐵) | ||
| Theorem | prsrn 34617 | Range of the relation of a proset. (Contributed by Thierry Arnoux, 11-Sep-2018.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = ((le‘𝐾) ∩ (𝐵 × 𝐵)) ⇒ ⊢ (𝐾 ∈ Proset → ran ≤ = 𝐵) | ||
| Theorem | prsss 34618 | Relation of a subproset. (Contributed by Thierry Arnoux, 13-Sep-2018.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = ((le‘𝐾) ∩ (𝐵 × 𝐵)) ⇒ ⊢ ((𝐾 ∈ Proset ∧ 𝐴 ⊆ 𝐵) → ( ≤ ∩ (𝐴 × 𝐴)) = ((le‘𝐾) ∩ (𝐴 × 𝐴))) | ||
| Theorem | prsssdm 34619 | Domain of a subproset relation. (Contributed by Thierry Arnoux, 12-Sep-2018.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = ((le‘𝐾) ∩ (𝐵 × 𝐵)) ⇒ ⊢ ((𝐾 ∈ Proset ∧ 𝐴 ⊆ 𝐵) → dom ( ≤ ∩ (𝐴 × 𝐴)) = 𝐴) | ||
| Theorem | ordtprsval 34620* | 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 34621* | Value of the order topology. (Contributed by Thierry Arnoux, 13-Sep-2018.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = ((le‘𝐾) ∩ (𝐵 × 𝐵)) & ⊢ 𝐸 = ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥}) & ⊢ 𝐹 = ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦}) ⇒ ⊢ (𝐾 ∈ Proset → 𝐵 = ∪ ({𝐵} ∪ (𝐸 ∪ 𝐹))) | ||
| Theorem | ordtcnvNEW 34622 | 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 34623 | 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 34624* | Lemma for ordtrest2NEW 34625. (Contributed by Mario Carneiro, 9-Sep-2015.) (Revised by Thierry Arnoux, 11-Sep-2018.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = ((le‘𝐾) ∩ (𝐵 × 𝐵)) & ⊢ (𝜑 → 𝐾 ∈ Toset) & ⊢ (𝜑 → 𝐴 ⊆ 𝐵) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → {𝑧 ∈ 𝐵 ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦)} ⊆ 𝐴) ⇒ ⊢ (𝜑 → ∀𝑣 ∈ ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑤 ≤ 𝑧})(𝑣 ∩ 𝐴) ∈ (ordTop‘( ≤ ∩ (𝐴 × 𝐴)))) | ||
| Theorem | ordtrest2NEW 34625* | 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 34626* | Connectedness in the order topology of a toset. This is the "easy" direction of ordtconn 34627. See also reconnlem1 25176. (Contributed by Thierry Arnoux, 14-Sep-2018.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = ((le‘𝐾) ∩ (𝐵 × 𝐵)) & ⊢ 𝐽 = (ordTop‘ ≤ ) ⇒ ⊢ ((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) → ((𝐽 ↾t 𝐴) ∈ Conn → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑟 ∈ 𝐵 ((𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦) → 𝑟 ∈ 𝐴))) | ||
| Theorem | ordtconn 34627 | Connectedness in the order topology of a complete uniform totally ordered space. (Contributed by Thierry Arnoux, 15-Sep-2018.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = ((le‘𝐾) ∩ (𝐵 × 𝐵)) & ⊢ 𝐽 = (ordTop‘ ≤ ) ⇒ ⊢ ⊤ | ||
| Theorem | mndpluscn 34628* | 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 34629 | 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 34630* | Multiplication by a real constant is a continuous function. (Contributed by Thierry Arnoux, 23-May-2017.) Avoid ax-mulf 11307. (Revised by GG, 16-Mar-2025.) |
| ⊢ 𝐽 = (topGen‘ran (,)) & ⊢ (𝜑 → 𝐶 ∈ ℝ) ⇒ ⊢ (𝜑 → (𝑥 ∈ ℝ ↦ (𝑥 · 𝐶)) ∈ (𝐽 Cn 𝐽)) | ||
| Theorem | raddcn 34631* | Addition in the real numbers is a continuous function. (Contributed by Thierry Arnoux, 23-May-2017.) |
| ⊢ 𝐽 = (topGen‘ran (,)) ⇒ ⊢ (𝑥 ∈ ℝ, 𝑦 ∈ ℝ ↦ (𝑥 + 𝑦)) ∈ ((𝐽 ×t 𝐽) Cn 𝐽) | ||
| Theorem | xrmulc1cn 34632* | 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 34633 | 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 34634 | The extended nonnegative reals are homeomorphic to the closed unit interval. (Contributed by Thierry Arnoux, 24-Mar-2017.) |
| ⊢ II ≃ ((ordTop‘ ≤ ) ↾t (0[,]+∞)) | ||
| Theorem | xrge0iifcnv 34635* | Define a bijection from [0, 1] onto [0, +∞]. (Contributed by Thierry Arnoux, 29-Mar-2017.) |
| ⊢ 𝐹 = (𝑥 ∈ (0[,]1) ↦ if(𝑥 = 0, +∞, -(log‘𝑥))) ⇒ ⊢ (𝐹:(0[,]1)⟶1-1onto(0[,]+∞) ∧ ◡𝐹 = (𝑦 ∈ (0[,]+∞) ↦ if(𝑦 = +∞, 0, (exp‘ -𝑦)))) | ||
| Theorem | xrge0iifcv 34636* | 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 34637* | 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 34638* | 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 34639* | 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)) → (𝐹‘(𝑋 · 𝑌)) = ((𝐹‘𝑋) +e (𝐹‘𝑌))) | ||
| Theorem | xrge0iif1 34640* | 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 34641* | 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 34642* | 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[,]+∞)) & ⊢ + = ( +e ↾ ((0[,]+∞) × (0[,]+∞))) ⇒ ⊢ + ∈ ((𝐽 ×t 𝐽) Cn 𝐽) | ||
| Theorem | xrge0mulc1cn 34643* | 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 34644 | The extended nonnegative real numbers monoid forms a topological space. (Contributed by Thierry Arnoux, 19-Jun-2017.) |
| ⊢ (ℝ*𝑠 ↾s (0[,]+∞)) ∈ TopSp | ||
| Theorem | xrge0topn 34645 | The topology of the extended nonnegative real numbers. (Contributed by Thierry Arnoux, 20-Jun-2017.) |
| ⊢ (TopOpen‘(ℝ*𝑠 ↾s (0[,]+∞))) = ((ordTop‘ ≤ ) ↾t (0[,]+∞)) | ||
| Theorem | xrge0haus 34646 | The topology of the extended nonnegative real numbers is Hausdorff. (Contributed by Thierry Arnoux, 26-Jul-2017.) |
| ⊢ (TopOpen‘(ℝ*𝑠 ↾s (0[,]+∞))) ∈ Haus | ||
| Theorem | xrge0tmd 34647 | 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 34648 | Alternate proof of xrge0tmd 34647. (Contributed by Thierry Arnoux, 26-Mar-2017.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ (ℝ*𝑠 ↾s (0[,]+∞)) ∈ TopMnd | ||
| Theorem | lmlim 34649 | 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 34650 | 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 34651 | Implication of convergence for a nonnegative series. This could be used to shorten prmreclem6 17128. (Contributed by Thierry Arnoux, 28-Jul-2017.) |
| ⊢ ((𝐹:ℕ⟶(0[,)+∞) ∧ seq1( + , 𝐹) ∈ dom ⇝ ) → sup(ran seq1( + , 𝐹), ℝ, < ) ∈ ℝ) | ||
| Theorem | fsumcvg4 34652 | 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 34653* | A neighborhood of +∞ contains an unbounded interval based at a real number. See pnfnei 23568. (Contributed by Thierry Arnoux, 31-Jul-2017.) |
| ⊢ 𝐽 = (TopOpen‘(ℝ*𝑠 ↾s (0[,]+∞))) ⇒ ⊢ ((𝐴 ∈ 𝐽 ∧ +∞ ∈ 𝐴) → ∃𝑥 ∈ ℝ (𝑥(,]+∞) ⊆ 𝐴) | ||
| Theorem | lmxrge0 34654* | 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 34655* | If a monotonic sequence of real numbers diverges, it is unbounded. (Contributed by Thierry Arnoux, 4-Aug-2017.) |
| ⊢ (𝜑 → 𝐹:ℕ⟶(0[,)+∞)) & ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐹‘𝑘) ≤ (𝐹‘(𝑘 + 1))) & ⊢ (𝜑 → ¬ 𝐹 ∈ dom ⇝ ) ⇒ ⊢ (𝜑 → ∀𝑥 ∈ ℝ ∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑗)𝑥 < (𝐹‘𝑘)) | ||
| Theorem | lmdvglim 34656* | 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 34657 | A univariate polynomial is continuous. (Contributed by Thierry Arnoux, 17-Sep-2018.) |
| ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐸 = (eval1‘𝑅) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 𝐾 = (Base‘𝑅) & ⊢ 𝐽 = (TopOpen‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝑅 ∈ TopRing) & ⊢ (𝜑 → 𝐹 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝐸‘𝐹) ∈ (𝐽 Cn 𝐽)) | ||
| Syntax | chcmp 34658 | Extend class notation with the Hausdorff uniform completion relation. |
| class HCmp | ||
| Definition | df-hcmp 34659* | 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 34660 | 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 34661 | 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 34662 | Zero of a ℤ-module. (Contributed by Thierry Arnoux, 8-Nov-2017.) |
| ⊢ 𝑊 = (ℤMod‘𝐺) & ⊢ 0 = (0g‘𝐺) ⇒ ⊢ 0 = (0g‘𝑊) | ||
| Theorem | zlm1 34663 | Unity element of a ℤ-module (if present). (Contributed by Thierry Arnoux, 8-Nov-2017.) |
| ⊢ 𝑊 = (ℤMod‘𝐺) & ⊢ 1 = (1r‘𝐺) ⇒ ⊢ 1 = (1r‘𝑊) | ||
| Theorem | zlmds 34664 | 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 34665 | 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 34666 | Norm of a ℤ-module (if present). (Contributed by Thierry Arnoux, 8-Nov-2017.) |
| ⊢ 𝑊 = (ℤMod‘𝐺) & ⊢ 𝑁 = (norm‘𝐺) ⇒ ⊢ (𝐺 ∈ 𝑉 → 𝑁 = (norm‘𝑊)) | ||
| Theorem | zhmnrg 34667 | The ℤ-module built from a normed ring is also a normed ring. (Contributed by Thierry Arnoux, 8-Nov-2017.) |
| ⊢ 𝑊 = (ℤMod‘𝐺) ⇒ ⊢ (𝐺 ∈ NrmRing → 𝑊 ∈ NrmRing) | ||
| Theorem | nmmulg 34668 | 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 34669 | 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 34670 | The ℤ-module of ℂ is a normed module. (Contributed by Thierry Arnoux, 25-Feb-2018.) |
| ⊢ (ℤMod‘ℂfld) ∈ NrmMod | ||
| Theorem | rezh 34671 | The ℤ-module of ℝ is a normed module. (Contributed by Thierry Arnoux, 14-Feb-2018.) |
| ⊢ (ℤMod‘ℝfld) ∈ NrmMod | ||
| Syntax | cqqh 34672 | Map the rationals into a field. |
| class ℚHom | ||
| Definition | df-qqh 34673* | 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 34674* | 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 34675 | 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 34676 | 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 34677 | 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 34678 | 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 34679 | 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 34680 | 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 34681 | 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 34682 | Lemma for qqhval2 34684. (Contributed by Thierry Arnoux, 29-Oct-2017.) |
| ⊢ (𝑀 ∈ (ℤ ∖ {0}) → (𝑀 ∈ ℕ ∨ -𝑀 ∈ ℕ)) | ||
| Theorem | qqhval2lem 34683 | Lemma for qqhval2 34684. (Contributed by Thierry Arnoux, 29-Oct-2017.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ / = (/r‘𝑅) & ⊢ 𝐿 = (ℤRHom‘𝑅) ⇒ ⊢ (((𝑅 ∈ DivRing ∧ (chr‘𝑅) = 0) ∧ (𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ∧ 𝑌 ≠ 0)) → ((𝐿‘(numer‘(𝑋 / 𝑌))) / (𝐿‘(denom‘(𝑋 / 𝑌)))) = ((𝐿‘𝑋) / (𝐿‘𝑌))) | ||
| Theorem | qqhval2 34684* | 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 34685 | 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 34686 | 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 34687 | 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 34688 | ℚHom as a function. (Contributed by Thierry Arnoux, 28-Oct-2017.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ / = (/r‘𝑅) & ⊢ 𝐿 = (ℤRHom‘𝑅) ⇒ ⊢ ((𝑅 ∈ DivRing ∧ (chr‘𝑅) = 0) → (ℚHom‘𝑅):ℚ⟶𝐵) | ||
| Theorem | qqhvq 34689 | 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 34690 | 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 34691 | 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 34692 | 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 34693 | 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 34694 | 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 34695 | Map the real numbers into a complete field. |
| class ℝHom | ||
| Syntax | crrext 34696 | Extend class notation with the class of extension fields of ℝ. |
| class ℝExt | ||
| Definition | df-rrh 34697 | 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 34698 | 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 34699 | 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 34700 | 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‘𝑅):ℝ⟶𝐵) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |