P. 326 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 32501-32600   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	ordtcnvNEW 32501	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 32502	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 32503*	Lemma for ordtrest2NEW 32504. (Contributed by Mario Carneiro, 9-Sep-2015.) (Revised by Thierry Arnoux, 11-Sep-2018.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = ((le‘𝐾) ∩ (𝐵 × 𝐵))    &   ⊢ (𝜑 → 𝐾 ∈ Toset)    &   ⊢ (𝜑 → 𝐴 ⊆ 𝐵)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → {𝑧 ∈ 𝐵 ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦)} ⊆ 𝐴)    ⇒   ⊢ (𝜑 → ∀𝑣 ∈ ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑤 ≤ 𝑧})(𝑣 ∩ 𝐴) ∈ (ordTop‘( ≤ ∩ (𝐴 × 𝐴))))
Theorem	ordtrest2NEW 32504*	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 32505*	Connectedness in the order topology of a toset. This is the "easy" direction of ordtconn 32506. See also reconnlem1 24189. (Contributed by Thierry Arnoux, 14-Sep-2018.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = ((le‘𝐾) ∩ (𝐵 × 𝐵))    &   ⊢ 𝐽 = (ordTop‘ ≤ )    ⇒   ⊢ ((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) → ((𝐽 ↾t 𝐴) ∈ Conn → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑟 ∈ 𝐵 ((𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦) → 𝑟 ∈ 𝐴)))
Theorem	ordtconn 32506	Connectedness in the order topology of a complete uniform totally ordered space. (Contributed by Thierry Arnoux, 15-Sep-2018.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = ((le‘𝐾) ∩ (𝐵 × 𝐵))    &   ⊢ 𝐽 = (ordTop‘ ≤ )    ⇒   ⊢ ⊤
21.3.12.13  Continuity in topological spaces - misc. additions
Theorem	mndpluscn 32507*	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 32508	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 32509*	Multiplication by a real constant is a continuous function. (Contributed by Thierry Arnoux, 23-May-2017.)
⊢ 𝐽 = (topGen‘ran (,))    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    ⇒   ⊢ (𝜑 → (𝑥 ∈ ℝ ↦ (𝑥 · 𝐶)) ∈ (𝐽 Cn 𝐽))
Theorem	raddcn 32510*	Addition in the real numbers is a continuous function. (Contributed by Thierry Arnoux, 23-May-2017.)
⊢ 𝐽 = (topGen‘ran (,))    ⇒   ⊢ (𝑥 ∈ ℝ, 𝑦 ∈ ℝ ↦ (𝑥 + 𝑦)) ∈ ((𝐽 ×t 𝐽) Cn 𝐽)
Theorem	xrmulc1cn 32511*	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 32512	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‘𝐸))
21.3.12.14  Topology of the extended nonnegative real numbers ordered monoid
Theorem	xrge0hmph 32513	The extended nonnegative reals are homeomorphic to the closed unit interval. (Contributed by Thierry Arnoux, 24-Mar-2017.)
⊢ II ≃ ((ordTop‘ ≤ ) ↾t (0[,]+∞))
Theorem	xrge0iifcnv 32514*	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 32515*	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 32516*	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 32517*	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 32518*	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 32519*	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 32520*	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 32521*	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 32522*	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 32523	The extended nonnegative real numbers monoid forms a topological space. (Contributed by Thierry Arnoux, 19-Jun-2017.)
⊢ (ℝ*𝑠 ↾s (0[,]+∞)) ∈ TopSp
Theorem	xrge0topn 32524	The topology of the extended nonnegative real numbers. (Contributed by Thierry Arnoux, 20-Jun-2017.)
⊢ (TopOpen‘(ℝ*𝑠 ↾s (0[,]+∞))) = ((ordTop‘ ≤ ) ↾t (0[,]+∞))
Theorem	xrge0haus 32525	The topology of the extended nonnegative real numbers is Hausdorff. (Contributed by Thierry Arnoux, 26-Jul-2017.)
⊢ (TopOpen‘(ℝ*𝑠 ↾s (0[,]+∞))) ∈ Haus
Theorem	xrge0tmd 32526	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 32527	Alternate proof of xrge0tmd 32526. (Contributed by Thierry Arnoux, 26-Mar-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (ℝ*𝑠 ↾s (0[,]+∞)) ∈ TopMnd
21.3.12.15  Limits - misc additions
Theorem	lmlim 32528	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 32529	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 32530	Implication of convergence for a nonnegative series. This could be used to shorten prmreclem6 16793. (Contributed by Thierry Arnoux, 28-Jul-2017.)
⊢ ((𝐹:ℕ⟶(0[,)+∞) ∧ seq1( + , 𝐹) ∈ dom ⇝ ) → sup(ran seq1( + , 𝐹), ℝ, < ) ∈ ℝ)
Theorem	fsumcvg4 32531	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 32532*	A neighborhood of +∞ contains an unbounded interval based at a real number. See pnfnei 22571. (Contributed by Thierry Arnoux, 31-Jul-2017.)
⊢ 𝐽 = (TopOpen‘(ℝ*𝑠 ↾s (0[,]+∞)))    ⇒   ⊢ ((𝐴 ∈ 𝐽 ∧ +∞ ∈ 𝐴) → ∃𝑥 ∈ ℝ (𝑥(,]+∞) ⊆ 𝐴)
Theorem	lmxrge0 32533*	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 32534*	If a monotonic sequence of real numbers diverges, it is unbounded. (Contributed by Thierry Arnoux, 4-Aug-2017.)
⊢ (𝜑 → 𝐹:ℕ⟶(0[,)+∞))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐹‘𝑘) ≤ (𝐹‘(𝑘 + 1)))    &   ⊢ (𝜑 → ¬ 𝐹 ∈ dom ⇝ )    ⇒   ⊢ (𝜑 → ∀𝑥 ∈ ℝ ∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑗)𝑥 < (𝐹‘𝑘))
Theorem	lmdvglim 32535*	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 ⇝ )    ⇒   ⊢ (𝜑 → 𝐹(⇝𝑡‘𝐽)+∞)
21.3.12.16  Univariate polynomials
Theorem	pl1cn 32536	A univariate polynomial is continuous. (Contributed by Thierry Arnoux, 17-Sep-2018.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐸 = (eval1‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 𝐾 = (Base‘𝑅)    &   ⊢ 𝐽 = (TopOpen‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝑅 ∈ TopRing)    &   ⊢ (𝜑 → 𝐹 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝐸‘𝐹) ∈ (𝐽 Cn 𝐽))
21.3.13  Uniform Stuctures and Spaces
21.3.13.1  Hausdorff uniform completion
Syntax	chcmp 32537	Extend class notation with the Hausdorff uniform completion relation.
class HCmp
Definition	df-hcmp 32538*	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‘𝑤))}
21.3.14  Topology and algebraic structures
21.3.14.1  The norm on the ring of the integer numbers
Theorem	zringnm 32539	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 32540	The norm of the ring of the integers. (Contributed by Thierry Arnoux, 8-Nov-2017.) (Revised by AV, 13-Jun-2019.)
⊢ (𝑀 ∈ ℤ → (abs‘𝑀) = ((norm‘ℤring)‘𝑀))
21.3.14.2  Topological ` ZZ ` -modules
Theorem	zlm0 32541	Zero of a ℤ-module. (Contributed by Thierry Arnoux, 8-Nov-2017.)
⊢ 𝑊 = (ℤMod‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    ⇒   ⊢ 0 = (0g‘𝑊)
Theorem	zlm1 32542	Unity element of a ℤ-module (if present). (Contributed by Thierry Arnoux, 8-Nov-2017.)
⊢ 𝑊 = (ℤMod‘𝐺)    &   ⊢ 1 = (1r‘𝐺)    ⇒   ⊢ 1 = (1r‘𝑊)
Theorem	zlmds 32543	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 32544	Obsolete proof of zlmds 32543 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 32545	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 32546	Obsolete proof of zlmtset 32545 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 32547	Norm of a ℤ-module (if present). (Contributed by Thierry Arnoux, 8-Nov-2017.)
⊢ 𝑊 = (ℤMod‘𝐺)    &   ⊢ 𝑁 = (norm‘𝐺)    ⇒   ⊢ (𝐺 ∈ 𝑉 → 𝑁 = (norm‘𝑊))
Theorem	zhmnrg 32548	The ℤ-module built from a normed ring is also a normed ring. (Contributed by Thierry Arnoux, 8-Nov-2017.)
⊢ 𝑊 = (ℤMod‘𝐺)    ⇒   ⊢ (𝐺 ∈ NrmRing → 𝑊 ∈ NrmRing)
Theorem	nmmulg 32549	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 32550	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 32551	The ℤ-module of ℂ is a normed module. (Contributed by Thierry Arnoux, 25-Feb-2018.)
⊢ (ℤMod‘ℂfld) ∈ NrmMod
Theorem	rezh 32552	The ℤ-module of ℝ is a normed module. (Contributed by Thierry Arnoux, 14-Feb-2018.)
⊢ (ℤMod‘ℝfld) ∈ NrmMod
21.3.14.3  Canonical embedding of the field of the rational numbers into a division ring
Syntax	cqqh 32553	Map the rationals into a field.
class ℚHom
Definition	df-qqh 32554*	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 32555*	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 32556	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 32557	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 32558	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 32559	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 32560	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 32561	Lemma for qqhval2 32563. (Contributed by Thierry Arnoux, 29-Oct-2017.)
⊢ (𝑀 ∈ (ℤ ∖ {0}) → (𝑀 ∈ ℕ ∨ -𝑀 ∈ ℕ))
Theorem	qqhval2lem 32562	Lemma for qqhval2 32563. (Contributed by Thierry Arnoux, 29-Oct-2017.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ / = (/r‘𝑅)    &   ⊢ 𝐿 = (ℤRHom‘𝑅)    ⇒   ⊢ (((𝑅 ∈ DivRing ∧ (chr‘𝑅) = 0) ∧ (𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ∧ 𝑌 ≠ 0)) → ((𝐿‘(numer‘(𝑋 / 𝑌))) / (𝐿‘(denom‘(𝑋 / 𝑌)))) = ((𝐿‘𝑋) / (𝐿‘𝑌)))
Theorem	qqhval2 32563*	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 32564	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 32565	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 32566	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 32567	ℚHom as a function. (Contributed by Thierry Arnoux, 28-Oct-2017.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ / = (/r‘𝑅)    &   ⊢ 𝐿 = (ℤRHom‘𝑅)    ⇒   ⊢ ((𝑅 ∈ DivRing ∧ (chr‘𝑅) = 0) → (ℚHom‘𝑅):ℚ⟶𝐵)
Theorem	qqhvq 32568	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 32569	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 32570	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 32571	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 32572	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 32573	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𝑉))
21.3.14.4  Canonical embedding of the real numbers into a complete ordered field
Syntax	crrh 32574	Map the real numbers into a complete field.
class ℝHom
Syntax	crrext 32575	Extend class notation with the class of extension fields of ℝ.
class ℝExt
Definition	df-rrh 32576	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 32577	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 32578	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 32579	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 32580	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 32581 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 32581	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 32582	An extension of ℝ is a normed ring. (Contributed by Thierry Arnoux, 2-May-2018.)
⊢ (𝑅 ∈ ℝExt → 𝑅 ∈ NrmRing)
Theorem	rrextdrg 32583	An extension of ℝ is a division ring. (Contributed by Thierry Arnoux, 2-May-2018.)
⊢ (𝑅 ∈ ℝExt → 𝑅 ∈ DivRing)
Theorem	rrextnlm 32584	The norm of an extension of ℝ is absolutely homogeneous. (Contributed by Thierry Arnoux, 2-May-2018.)
⊢ 𝑍 = (ℤMod‘𝑅)    ⇒   ⊢ (𝑅 ∈ ℝExt → 𝑍 ∈ NrmMod)
Theorem	rrextchr 32585	The ring characteristic of an extension of ℝ is zero. (Contributed by Thierry Arnoux, 2-May-2018.)
⊢ (𝑅 ∈ ℝExt → (chr‘𝑅) = 0)
Theorem	rrextcusp 32586	An extension of ℝ is a complete uniform space. (Contributed by Thierry Arnoux, 2-May-2018.)
⊢ (𝑅 ∈ ℝExt → 𝑅 ∈ CUnifSp)
Theorem	rrexttps 32587	An extension of ℝ is a topological space. (Contributed by Thierry Arnoux, 7-Sep-2018.)
⊢ (𝑅 ∈ ℝExt → 𝑅 ∈ TopSp)
Theorem	rrexthaus 32588	The topology of an extension of ℝ is Hausdorff. (Contributed by Thierry Arnoux, 7-Sep-2018.)
⊢ 𝐾 = (TopOpen‘𝑅)    ⇒   ⊢ (𝑅 ∈ ℝExt → 𝐾 ∈ Haus)
Theorem	rrextust 32589	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 32590	The field of the real numbers is an extension of the real numbers. (Contributed by Thierry Arnoux, 2-May-2018.)
⊢ ℝfld ∈ ℝExt
Theorem	cnrrext 32591	The field of the complex numbers is an extension of the real numbers. (Contributed by Thierry Arnoux, 2-May-2018.)
⊢ ℂfld ∈ ℝExt
Theorem	qqtopn 32592	The topology of the field of the rational numbers. (Contributed by Thierry Arnoux, 29-Aug-2020.)
⊢ ((TopOpen‘ℝfld) ↾t ℚ) = (TopOpen‘(ℂfld ↾s ℚ))
Theorem	rrhfe 32593	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 32594	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 32595	The ℝHom homomorphism leaves rational numbers unchanged. (Contributed by Thierry Arnoux, 27-Mar-2018.)
⊢ ((𝑅 ∈ ℝExt ∧ 𝑄 ∈ ℚ) → ((ℝHom‘𝑅)‘𝑄) = ((ℚHom‘𝑅)‘𝑄))
Theorem	rrh0 32596	The image of 0 by the ℝHom homomorphism is the ring's zero. (Contributed by Thierry Arnoux, 22-Oct-2017.)
⊢ (𝑅 ∈ ℝExt → ((ℝHom‘𝑅)‘0) = (0g‘𝑅))
21.3.14.5  Embedding from the extended real numbers into a complete lattice
Syntax	cxrh 32597	Map the extended real numbers into a complete lattice.
class ℝ*Hom
Definition	df-xrh 32598*	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 32599*	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(𝑥 = +∞, (𝑈‘𝐵), (𝐿‘𝐵)))))
21.3.14.6  Canonical embeddings into the ordered field of the real numbers
Theorem	zrhre 32600	The ℤRHom homomorphism for the real number structure is the identity. (Contributed by Thierry Arnoux, 31-Oct-2017.)
⊢ (ℤRHom‘ℝfld) = ( I ↾ ℤ)