![]() |
Metamath
Proof Explorer Theorem List (p. 338 of 486) | < 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: | ![]() (1-30851) |
![]() (30852-32374) |
![]() (32375-48553) |
Type | Label | Description |
---|---|---|
Statement | ||
Syntax | cmetid 33701 | Extend class notation with the class of metric identifications. |
class ~Met | ||
Syntax | cpstm 33702 | Extend class notation with the metric induced by a pseudometric. |
class pstoMet | ||
Definition | df-metid 33703* | Define the metric identification relation for a pseudometric. (Contributed by Thierry Arnoux, 7-Feb-2018.) |
⊢ ~Met = (𝑑 ∈ ∪ ran PsMet ↦ {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ dom dom 𝑑 ∧ 𝑦 ∈ dom dom 𝑑) ∧ (𝑥𝑑𝑦) = 0)}) | ||
Definition | df-pstm 33704* | Define the metric induced by a pseudometric. (Contributed by Thierry Arnoux, 7-Feb-2018.) |
⊢ pstoMet = (𝑑 ∈ ∪ ran PsMet ↦ (𝑎 ∈ (dom dom 𝑑 / (~Met‘𝑑)), 𝑏 ∈ (dom dom 𝑑 / (~Met‘𝑑)) ↦ ∪ {𝑧 ∣ ∃𝑥 ∈ 𝑎 ∃𝑦 ∈ 𝑏 𝑧 = (𝑥𝑑𝑦)})) | ||
Theorem | metidval 33705* | Value of the metric identification relation. (Contributed by Thierry Arnoux, 7-Feb-2018.) |
⊢ (𝐷 ∈ (PsMet‘𝑋) → (~Met‘𝐷) = {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) ∧ (𝑥𝐷𝑦) = 0)}) | ||
Theorem | metidss 33706 | As a relation, the metric identification is a subset of a Cartesian product. (Contributed by Thierry Arnoux, 7-Feb-2018.) |
⊢ (𝐷 ∈ (PsMet‘𝑋) → (~Met‘𝐷) ⊆ (𝑋 × 𝑋)) | ||
Theorem | metidv 33707 | 𝐴 and 𝐵 identify by the metric 𝐷 if their distance is zero. (Contributed by Thierry Arnoux, 7-Feb-2018.) |
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → (𝐴(~Met‘𝐷)𝐵 ↔ (𝐴𝐷𝐵) = 0)) | ||
Theorem | metideq 33708 | Basic property of the metric identification relation. (Contributed by Thierry Arnoux, 7-Feb-2018.) |
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝐴(~Met‘𝐷)𝐵 ∧ 𝐸(~Met‘𝐷)𝐹)) → (𝐴𝐷𝐸) = (𝐵𝐷𝐹)) | ||
Theorem | metider 33709 | The metric identification is an equivalence relation. (Contributed by Thierry Arnoux, 11-Feb-2018.) |
⊢ (𝐷 ∈ (PsMet‘𝑋) → (~Met‘𝐷) Er 𝑋) | ||
Theorem | pstmval 33710* | Value of the metric induced by a pseudometric 𝐷. (Contributed by Thierry Arnoux, 7-Feb-2018.) |
⊢ ∼ = (~Met‘𝐷) ⇒ ⊢ (𝐷 ∈ (PsMet‘𝑋) → (pstoMet‘𝐷) = (𝑎 ∈ (𝑋 / ∼ ), 𝑏 ∈ (𝑋 / ∼ ) ↦ ∪ {𝑧 ∣ ∃𝑥 ∈ 𝑎 ∃𝑦 ∈ 𝑏 𝑧 = (𝑥𝐷𝑦)})) | ||
Theorem | pstmfval 33711 | Function value of the metric induced by a pseudometric 𝐷 (Contributed by Thierry Arnoux, 11-Feb-2018.) |
⊢ ∼ = (~Met‘𝐷) ⇒ ⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ([𝐴] ∼ (pstoMet‘𝐷)[𝐵] ∼ ) = (𝐴𝐷𝐵)) | ||
Theorem | pstmxmet 33712 | The metric induced by a pseudometric is a full-fledged metric on the equivalence classes of the metric identification. (Contributed by Thierry Arnoux, 11-Feb-2018.) |
⊢ ∼ = (~Met‘𝐷) ⇒ ⊢ (𝐷 ∈ (PsMet‘𝑋) → (pstoMet‘𝐷) ∈ (∞Met‘(𝑋 / ∼ ))) | ||
Theorem | hauseqcn 33713 | 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 33714 | 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 33715 | 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 33716 | 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 33717 | 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 33718 | The union of the closed set is the underlying set of the topology. (Contributed by Thierry Arnoux, 21-Sep-2017.) |
⊢ 𝐽 ∈ Top & ⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ∪ (Clsd‘𝐽) = 𝑋 | ||
Theorem | tpr2tp 33719 | 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 33720 | 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 33721 | 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 33722 | 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 33723 | 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 33724 | 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 33725* | Lemma for cnre2csqima 33726. (Contributed by Thierry Arnoux, 27-Sep-2017.) |
⊢ (𝐺 ↾ (ℝ × ℝ)) = (𝐻 ∘ 𝐹) & ⊢ 𝐹 Fn (ℝ × ℝ) & ⊢ 𝐺 Fn V & ⊢ (𝑥 ∈ (ℝ × ℝ) → (𝐺‘𝑥) ∈ ℝ) & ⊢ ((𝑥 ∈ ran 𝐹 ∧ 𝑦 ∈ ran 𝐹) → (𝐻‘(𝑥 − 𝑦)) = ((𝐻‘𝑥) − (𝐻‘𝑦))) ⇒ ⊢ ((𝑋 ∈ (ℝ × ℝ) ∧ 𝑌 ∈ (ℝ × ℝ) ∧ 𝐷 ∈ ℝ+) → (𝑌 ∈ (◡(𝐺 ↾ (ℝ × ℝ)) “ (((𝐺‘𝑋) − 𝐷)(,)((𝐺‘𝑋) + 𝐷))) → (abs‘(𝐻‘((𝐹‘𝑌) − (𝐹‘𝑋)))) < 𝐷)) | ||
Theorem | cnre2csqima 33726* | 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 33727* | 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 33728* | 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 33729 | Domain of the relation of a proset. (Contributed by Thierry Arnoux, 11-Sep-2015.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = ((le‘𝐾) ∩ (𝐵 × 𝐵)) ⇒ ⊢ (𝐾 ∈ Proset → dom ≤ = 𝐵) | ||
Theorem | prsrn 33730 | Range of the relation of a proset. (Contributed by Thierry Arnoux, 11-Sep-2018.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = ((le‘𝐾) ∩ (𝐵 × 𝐵)) ⇒ ⊢ (𝐾 ∈ Proset → ran ≤ = 𝐵) | ||
Theorem | prsss 33731 | Relation of a subproset. (Contributed by Thierry Arnoux, 13-Sep-2018.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = ((le‘𝐾) ∩ (𝐵 × 𝐵)) ⇒ ⊢ ((𝐾 ∈ Proset ∧ 𝐴 ⊆ 𝐵) → ( ≤ ∩ (𝐴 × 𝐴)) = ((le‘𝐾) ∩ (𝐴 × 𝐴))) | ||
Theorem | prsssdm 33732 | Domain of a subproset relation. (Contributed by Thierry Arnoux, 12-Sep-2018.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = ((le‘𝐾) ∩ (𝐵 × 𝐵)) ⇒ ⊢ ((𝐾 ∈ Proset ∧ 𝐴 ⊆ 𝐵) → dom ( ≤ ∩ (𝐴 × 𝐴)) = 𝐴) | ||
Theorem | ordtprsval 33733* | 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 33734* | Value of the order topology. (Contributed by Thierry Arnoux, 13-Sep-2018.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = ((le‘𝐾) ∩ (𝐵 × 𝐵)) & ⊢ 𝐸 = ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥}) & ⊢ 𝐹 = ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦}) ⇒ ⊢ (𝐾 ∈ Proset → 𝐵 = ∪ ({𝐵} ∪ (𝐸 ∪ 𝐹))) | ||
Theorem | ordtcnvNEW 33735 | 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 33736 | 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 33737* | Lemma for ordtrest2NEW 33738. (Contributed by Mario Carneiro, 9-Sep-2015.) (Revised by Thierry Arnoux, 11-Sep-2018.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = ((le‘𝐾) ∩ (𝐵 × 𝐵)) & ⊢ (𝜑 → 𝐾 ∈ Toset) & ⊢ (𝜑 → 𝐴 ⊆ 𝐵) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → {𝑧 ∈ 𝐵 ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦)} ⊆ 𝐴) ⇒ ⊢ (𝜑 → ∀𝑣 ∈ ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑤 ≤ 𝑧})(𝑣 ∩ 𝐴) ∈ (ordTop‘( ≤ ∩ (𝐴 × 𝐴)))) | ||
Theorem | ordtrest2NEW 33738* | 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 33739* | Connectedness in the order topology of a toset. This is the "easy" direction of ordtconn 33740. See also reconnlem1 24833. (Contributed by Thierry Arnoux, 14-Sep-2018.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = ((le‘𝐾) ∩ (𝐵 × 𝐵)) & ⊢ 𝐽 = (ordTop‘ ≤ ) ⇒ ⊢ ((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) → ((𝐽 ↾t 𝐴) ∈ Conn → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑟 ∈ 𝐵 ((𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦) → 𝑟 ∈ 𝐴))) | ||
Theorem | ordtconn 33740 | Connectedness in the order topology of a complete uniform totally ordered space. (Contributed by Thierry Arnoux, 15-Sep-2018.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = ((le‘𝐾) ∩ (𝐵 × 𝐵)) & ⊢ 𝐽 = (ordTop‘ ≤ ) ⇒ ⊢ ⊤ | ||
Theorem | mndpluscn 33741* | 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 33742 | 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 33743* | Multiplication by a real constant is a continuous function. (Contributed by Thierry Arnoux, 23-May-2017.) Avoid ax-mulf 11238. (Revised by GG, 16-Mar-2025.) |
⊢ 𝐽 = (topGen‘ran (,)) & ⊢ (𝜑 → 𝐶 ∈ ℝ) ⇒ ⊢ (𝜑 → (𝑥 ∈ ℝ ↦ (𝑥 · 𝐶)) ∈ (𝐽 Cn 𝐽)) | ||
Theorem | raddcn 33744* | Addition in the real numbers is a continuous function. (Contributed by Thierry Arnoux, 23-May-2017.) |
⊢ 𝐽 = (topGen‘ran (,)) ⇒ ⊢ (𝑥 ∈ ℝ, 𝑦 ∈ ℝ ↦ (𝑥 + 𝑦)) ∈ ((𝐽 ×t 𝐽) Cn 𝐽) | ||
Theorem | xrmulc1cn 33745* | 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 33746 | 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 33747 | The extended nonnegative reals are homeomorphic to the closed unit interval. (Contributed by Thierry Arnoux, 24-Mar-2017.) |
⊢ II ≃ ((ordTop‘ ≤ ) ↾t (0[,]+∞)) | ||
Theorem | xrge0iifcnv 33748* | 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 33749* | 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 33750* | 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 33751* | 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 33752* | 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 33753* | 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 33754* | 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 33755* | 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 33756* | 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 33757 | The extended nonnegative real numbers monoid forms a topological space. (Contributed by Thierry Arnoux, 19-Jun-2017.) |
⊢ (ℝ*𝑠 ↾s (0[,]+∞)) ∈ TopSp | ||
Theorem | xrge0topn 33758 | The topology of the extended nonnegative real numbers. (Contributed by Thierry Arnoux, 20-Jun-2017.) |
⊢ (TopOpen‘(ℝ*𝑠 ↾s (0[,]+∞))) = ((ordTop‘ ≤ ) ↾t (0[,]+∞)) | ||
Theorem | xrge0haus 33759 | The topology of the extended nonnegative real numbers is Hausdorff. (Contributed by Thierry Arnoux, 26-Jul-2017.) |
⊢ (TopOpen‘(ℝ*𝑠 ↾s (0[,]+∞))) ∈ Haus | ||
Theorem | xrge0tmd 33760 | 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 33761 | Alternate proof of xrge0tmd 33760. (Contributed by Thierry Arnoux, 26-Mar-2017.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (ℝ*𝑠 ↾s (0[,]+∞)) ∈ TopMnd | ||
Theorem | lmlim 33762 | 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 33763 | 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 33764 | Implication of convergence for a nonnegative series. This could be used to shorten prmreclem6 16923. (Contributed by Thierry Arnoux, 28-Jul-2017.) |
⊢ ((𝐹:ℕ⟶(0[,)+∞) ∧ seq1( + , 𝐹) ∈ dom ⇝ ) → sup(ran seq1( + , 𝐹), ℝ, < ) ∈ ℝ) | ||
Theorem | fsumcvg4 33765 | 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 33766* | A neighborhood of +∞ contains an unbounded interval based at a real number. See pnfnei 23215. (Contributed by Thierry Arnoux, 31-Jul-2017.) |
⊢ 𝐽 = (TopOpen‘(ℝ*𝑠 ↾s (0[,]+∞))) ⇒ ⊢ ((𝐴 ∈ 𝐽 ∧ +∞ ∈ 𝐴) → ∃𝑥 ∈ ℝ (𝑥(,]+∞) ⊆ 𝐴) | ||
Theorem | lmxrge0 33767* | 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 33768* | If a monotonic sequence of real numbers diverges, it is unbounded. (Contributed by Thierry Arnoux, 4-Aug-2017.) |
⊢ (𝜑 → 𝐹:ℕ⟶(0[,)+∞)) & ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐹‘𝑘) ≤ (𝐹‘(𝑘 + 1))) & ⊢ (𝜑 → ¬ 𝐹 ∈ dom ⇝ ) ⇒ ⊢ (𝜑 → ∀𝑥 ∈ ℝ ∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑗)𝑥 < (𝐹‘𝑘)) | ||
Theorem | lmdvglim 33769* | 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 33770 | A univariate polynomial is continuous. (Contributed by Thierry Arnoux, 17-Sep-2018.) |
⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐸 = (eval1‘𝑅) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 𝐾 = (Base‘𝑅) & ⊢ 𝐽 = (TopOpen‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝑅 ∈ TopRing) & ⊢ (𝜑 → 𝐹 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝐸‘𝐹) ∈ (𝐽 Cn 𝐽)) | ||
Syntax | chcmp 33771 | Extend class notation with the Hausdorff uniform completion relation. |
class HCmp | ||
Definition | df-hcmp 33772* | 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 33773 | 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 33774 | 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 33775 | Zero of a ℤ-module. (Contributed by Thierry Arnoux, 8-Nov-2017.) |
⊢ 𝑊 = (ℤMod‘𝐺) & ⊢ 0 = (0g‘𝐺) ⇒ ⊢ 0 = (0g‘𝑊) | ||
Theorem | zlm1 33776 | Unity element of a ℤ-module (if present). (Contributed by Thierry Arnoux, 8-Nov-2017.) |
⊢ 𝑊 = (ℤMod‘𝐺) & ⊢ 1 = (1r‘𝐺) ⇒ ⊢ 1 = (1r‘𝑊) | ||
Theorem | zlmds 33777 | Distance in a ℤ-module (if present). (Contributed by Thierry Arnoux, 8-Nov-2017.) (Proof shortened by AV, 11-Nov-2024.) |
⊢ 𝑊 = (ℤMod‘𝐺) & ⊢ 𝐷 = (dist‘𝐺) ⇒ ⊢ (𝐺 ∈ 𝑉 → 𝐷 = (dist‘𝑊)) | ||
Theorem | zlmdsOLD 33778 | Obsolete proof of zlmds 33777 as of 11-Nov-2024. Distance in a ℤ -module (if present). (Contributed by Thierry Arnoux, 8-Nov-2017.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝑊 = (ℤMod‘𝐺) & ⊢ 𝐷 = (dist‘𝐺) ⇒ ⊢ (𝐺 ∈ 𝑉 → 𝐷 = (dist‘𝑊)) | ||
Theorem | zlmtset 33779 | Topology in a ℤ-module (if present). (Contributed by Thierry Arnoux, 8-Nov-2017.) (Proof shortened by AV, 12-Nov-2024.) |
⊢ 𝑊 = (ℤMod‘𝐺) & ⊢ 𝐽 = (TopSet‘𝐺) ⇒ ⊢ (𝐺 ∈ 𝑉 → 𝐽 = (TopSet‘𝑊)) | ||
Theorem | zlmtsetOLD 33780 | Obsolete proof of zlmtset 33779 as of 11-Nov-2024. Topology in a ℤ -module (if present). (Contributed by Thierry Arnoux, 8-Nov-2017.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝑊 = (ℤMod‘𝐺) & ⊢ 𝐽 = (TopSet‘𝐺) ⇒ ⊢ (𝐺 ∈ 𝑉 → 𝐽 = (TopSet‘𝑊)) | ||
Theorem | zlmnm 33781 | Norm of a ℤ-module (if present). (Contributed by Thierry Arnoux, 8-Nov-2017.) |
⊢ 𝑊 = (ℤMod‘𝐺) & ⊢ 𝑁 = (norm‘𝐺) ⇒ ⊢ (𝐺 ∈ 𝑉 → 𝑁 = (norm‘𝑊)) | ||
Theorem | zhmnrg 33782 | The ℤ-module built from a normed ring is also a normed ring. (Contributed by Thierry Arnoux, 8-Nov-2017.) |
⊢ 𝑊 = (ℤMod‘𝐺) ⇒ ⊢ (𝐺 ∈ NrmRing → 𝑊 ∈ NrmRing) | ||
Theorem | nmmulg 33783 | 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 33784 | 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 33785 | The ℤ-module of ℂ is a normed module. (Contributed by Thierry Arnoux, 25-Feb-2018.) |
⊢ (ℤMod‘ℂfld) ∈ NrmMod | ||
Theorem | rezh 33786 | The ℤ-module of ℝ is a normed module. (Contributed by Thierry Arnoux, 14-Feb-2018.) |
⊢ (ℤMod‘ℝfld) ∈ NrmMod | ||
Syntax | cqqh 33787 | Map the rationals into a field. |
class ℚHom | ||
Definition | df-qqh 33788* | 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 33789* | 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 33790 | 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 33791 | 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 33792 | 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 33793 | 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 33794 | 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 33795 | Lemma for qqhval2 33797. (Contributed by Thierry Arnoux, 29-Oct-2017.) |
⊢ (𝑀 ∈ (ℤ ∖ {0}) → (𝑀 ∈ ℕ ∨ -𝑀 ∈ ℕ)) | ||
Theorem | qqhval2lem 33796 | Lemma for qqhval2 33797. (Contributed by Thierry Arnoux, 29-Oct-2017.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ / = (/r‘𝑅) & ⊢ 𝐿 = (ℤRHom‘𝑅) ⇒ ⊢ (((𝑅 ∈ DivRing ∧ (chr‘𝑅) = 0) ∧ (𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ∧ 𝑌 ≠ 0)) → ((𝐿‘(numer‘(𝑋 / 𝑌))) / (𝐿‘(denom‘(𝑋 / 𝑌)))) = ((𝐿‘𝑋) / (𝐿‘𝑌))) | ||
Theorem | qqhval2 33797* | 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 33798 | 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 33799 | 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 33800 | 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‘𝑅)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |