P. 340 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 33901-34000   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	ordtcnvNEW 33901	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 33902	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 33903*	Lemma for ordtrest2NEW 33904. (Contributed by Mario Carneiro, 9-Sep-2015.) (Revised by Thierry Arnoux, 11-Sep-2018.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = ((le‘𝐾) ∩ (𝐵 × 𝐵))    &   ⊢ (𝜑 → 𝐾 ∈ Toset)    &   ⊢ (𝜑 → 𝐴 ⊆ 𝐵)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → {𝑧 ∈ 𝐵 ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦)} ⊆ 𝐴)    ⇒   ⊢ (𝜑 → ∀𝑣 ∈ ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑤 ≤ 𝑧})(𝑣 ∩ 𝐴) ∈ (ordTop‘( ≤ ∩ (𝐴 × 𝐴))))
Theorem	ordtrest2NEW 33904*	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 33905*	Connectedness in the order topology of a toset. This is the "easy" direction of ordtconn 33906. See also reconnlem1 24696. (Contributed by Thierry Arnoux, 14-Sep-2018.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = ((le‘𝐾) ∩ (𝐵 × 𝐵))    &   ⊢ 𝐽 = (ordTop‘ ≤ )    ⇒   ⊢ ((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) → ((𝐽 ↾t 𝐴) ∈ Conn → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑟 ∈ 𝐵 ((𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦) → 𝑟 ∈ 𝐴)))
Theorem	ordtconn 33906	Connectedness in the order topology of a complete uniform totally ordered space. (Contributed by Thierry Arnoux, 15-Sep-2018.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = ((le‘𝐾) ∩ (𝐵 × 𝐵))    &   ⊢ 𝐽 = (ordTop‘ ≤ )    ⇒   ⊢ ⊤
21.3.14.13  Continuity in topological spaces - misc. additions
Theorem	mndpluscn 33907*	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 33908	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 33909*	Multiplication by a real constant is a continuous function. (Contributed by Thierry Arnoux, 23-May-2017.) Avoid ax-mulf 11077. (Revised by GG, 16-Mar-2025.)
⊢ 𝐽 = (topGen‘ran (,))    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    ⇒   ⊢ (𝜑 → (𝑥 ∈ ℝ ↦ (𝑥 · 𝐶)) ∈ (𝐽 Cn 𝐽))
Theorem	raddcn 33910*	Addition in the real numbers is a continuous function. (Contributed by Thierry Arnoux, 23-May-2017.)
⊢ 𝐽 = (topGen‘ran (,))    ⇒   ⊢ (𝑥 ∈ ℝ, 𝑦 ∈ ℝ ↦ (𝑥 + 𝑦)) ∈ ((𝐽 ×t 𝐽) Cn 𝐽)
Theorem	xrmulc1cn 33911*	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 33912	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.14.14  Topology of the extended nonnegative real numbers ordered monoid
Theorem	xrge0hmph 33913	The extended nonnegative reals are homeomorphic to the closed unit interval. (Contributed by Thierry Arnoux, 24-Mar-2017.)
⊢ II ≃ ((ordTop‘ ≤ ) ↾t (0[,]+∞))
Theorem	xrge0iifcnv 33914*	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 33915*	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 33916*	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 33917*	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 33918*	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 33919*	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 33920*	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 33921*	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 33922*	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 33923	The extended nonnegative real numbers monoid forms a topological space. (Contributed by Thierry Arnoux, 19-Jun-2017.)
⊢ (ℝ*𝑠 ↾s (0[,]+∞)) ∈ TopSp
Theorem	xrge0topn 33924	The topology of the extended nonnegative real numbers. (Contributed by Thierry Arnoux, 20-Jun-2017.)
⊢ (TopOpen‘(ℝ*𝑠 ↾s (0[,]+∞))) = ((ordTop‘ ≤ ) ↾t (0[,]+∞))
Theorem	xrge0haus 33925	The topology of the extended nonnegative real numbers is Hausdorff. (Contributed by Thierry Arnoux, 26-Jul-2017.)
⊢ (TopOpen‘(ℝ*𝑠 ↾s (0[,]+∞))) ∈ Haus
Theorem	xrge0tmd 33926	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 33927	Alternate proof of xrge0tmd 33926. (Contributed by Thierry Arnoux, 26-Mar-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (ℝ*𝑠 ↾s (0[,]+∞)) ∈ TopMnd
21.3.14.15  Limits - misc additions
Theorem	lmlim 33928	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 33929	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 33930	Implication of convergence for a nonnegative series. This could be used to shorten prmreclem6 16820. (Contributed by Thierry Arnoux, 28-Jul-2017.)
⊢ ((𝐹:ℕ⟶(0[,)+∞) ∧ seq1( + , 𝐹) ∈ dom ⇝ ) → sup(ran seq1( + , 𝐹), ℝ, < ) ∈ ℝ)
Theorem	fsumcvg4 33931	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 33932*	A neighborhood of +∞ contains an unbounded interval based at a real number. See pnfnei 23089. (Contributed by Thierry Arnoux, 31-Jul-2017.)
⊢ 𝐽 = (TopOpen‘(ℝ*𝑠 ↾s (0[,]+∞)))    ⇒   ⊢ ((𝐴 ∈ 𝐽 ∧ +∞ ∈ 𝐴) → ∃𝑥 ∈ ℝ (𝑥(,]+∞) ⊆ 𝐴)
Theorem	lmxrge0 33933*	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 33934*	If a monotonic sequence of real numbers diverges, it is unbounded. (Contributed by Thierry Arnoux, 4-Aug-2017.)
⊢ (𝜑 → 𝐹:ℕ⟶(0[,)+∞))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐹‘𝑘) ≤ (𝐹‘(𝑘 + 1)))    &   ⊢ (𝜑 → ¬ 𝐹 ∈ dom ⇝ )    ⇒   ⊢ (𝜑 → ∀𝑥 ∈ ℝ ∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑗)𝑥 < (𝐹‘𝑘))
Theorem	lmdvglim 33935*	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.14.16  Univariate polynomials
Theorem	pl1cn 33936	A univariate polynomial is continuous. (Contributed by Thierry Arnoux, 17-Sep-2018.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐸 = (eval1‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 𝐾 = (Base‘𝑅)    &   ⊢ 𝐽 = (TopOpen‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝑅 ∈ TopRing)    &   ⊢ (𝜑 → 𝐹 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝐸‘𝐹) ∈ (𝐽 Cn 𝐽))
21.3.15  Uniform Stuctures and Spaces
21.3.15.1  Hausdorff uniform completion
Syntax	chcmp 33937	Extend class notation with the Hausdorff uniform completion relation.
class HCmp
Definition	df-hcmp 33938*	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.16  Topology and algebraic structures
21.3.16.1  The norm on the ring of the integer numbers
Theorem	zringnm 33939	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 33940	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.16.2  Topological ` ZZ ` -modules
Theorem	zlm0 33941	Zero of a ℤ-module. (Contributed by Thierry Arnoux, 8-Nov-2017.)
⊢ 𝑊 = (ℤMod‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    ⇒   ⊢ 0 = (0g‘𝑊)
Theorem	zlm1 33942	Unity element of a ℤ-module (if present). (Contributed by Thierry Arnoux, 8-Nov-2017.)
⊢ 𝑊 = (ℤMod‘𝐺)    &   ⊢ 1 = (1r‘𝐺)    ⇒   ⊢ 1 = (1r‘𝑊)
Theorem	zlmds 33943	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 33944	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 33945	Norm of a ℤ-module (if present). (Contributed by Thierry Arnoux, 8-Nov-2017.)
⊢ 𝑊 = (ℤMod‘𝐺)    &   ⊢ 𝑁 = (norm‘𝐺)    ⇒   ⊢ (𝐺 ∈ 𝑉 → 𝑁 = (norm‘𝑊))
Theorem	zhmnrg 33946	The ℤ-module built from a normed ring is also a normed ring. (Contributed by Thierry Arnoux, 8-Nov-2017.)
⊢ 𝑊 = (ℤMod‘𝐺)    ⇒   ⊢ (𝐺 ∈ NrmRing → 𝑊 ∈ NrmRing)
Theorem	nmmulg 33947	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 33948	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 33949	The ℤ-module of ℂ is a normed module. (Contributed by Thierry Arnoux, 25-Feb-2018.)
⊢ (ℤMod‘ℂfld) ∈ NrmMod
Theorem	rezh 33950	The ℤ-module of ℝ is a normed module. (Contributed by Thierry Arnoux, 14-Feb-2018.)
⊢ (ℤMod‘ℝfld) ∈ NrmMod
21.3.16.3  Canonical embedding of the field of the rational numbers into a division ring
Syntax	cqqh 33951	Map the rationals into a field.
class ℚHom
Definition	df-qqh 33952*	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 33953*	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 33954	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 33955	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 33956	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 33957	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 33958	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 33959	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 33960	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 33961	Lemma for qqhval2 33963. (Contributed by Thierry Arnoux, 29-Oct-2017.)
⊢ (𝑀 ∈ (ℤ ∖ {0}) → (𝑀 ∈ ℕ ∨ -𝑀 ∈ ℕ))
Theorem	qqhval2lem 33962	Lemma for qqhval2 33963. (Contributed by Thierry Arnoux, 29-Oct-2017.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ / = (/r‘𝑅)    &   ⊢ 𝐿 = (ℤRHom‘𝑅)    ⇒   ⊢ (((𝑅 ∈ DivRing ∧ (chr‘𝑅) = 0) ∧ (𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ∧ 𝑌 ≠ 0)) → ((𝐿‘(numer‘(𝑋 / 𝑌))) / (𝐿‘(denom‘(𝑋 / 𝑌)))) = ((𝐿‘𝑋) / (𝐿‘𝑌)))
Theorem	qqhval2 33963*	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 33964	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 33965	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 33966	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 33967	ℚHom as a function. (Contributed by Thierry Arnoux, 28-Oct-2017.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ / = (/r‘𝑅)    &   ⊢ 𝐿 = (ℤRHom‘𝑅)    ⇒   ⊢ ((𝑅 ∈ DivRing ∧ (chr‘𝑅) = 0) → (ℚHom‘𝑅):ℚ⟶𝐵)
Theorem	qqhvq 33968	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 33969	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 33970	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 33971	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 33972	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 33973	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.16.4  Canonical embedding of the real numbers into a complete ordered field
Syntax	crrh 33974	Map the real numbers into a complete field.
class ℝHom
Syntax	crrext 33975	Extend class notation with the class of extension fields of ℝ.
class ℝExt
Definition	df-rrh 33976	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 33977	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 33978	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 33979	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 33980	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 33981 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 33981	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 33982	An extension of ℝ is a normed ring. (Contributed by Thierry Arnoux, 2-May-2018.)
⊢ (𝑅 ∈ ℝExt → 𝑅 ∈ NrmRing)
Theorem	rrextdrg 33983	An extension of ℝ is a division ring. (Contributed by Thierry Arnoux, 2-May-2018.)
⊢ (𝑅 ∈ ℝExt → 𝑅 ∈ DivRing)
Theorem	rrextnlm 33984	The norm of an extension of ℝ is absolutely homogeneous. (Contributed by Thierry Arnoux, 2-May-2018.)
⊢ 𝑍 = (ℤMod‘𝑅)    ⇒   ⊢ (𝑅 ∈ ℝExt → 𝑍 ∈ NrmMod)
Theorem	rrextchr 33985	The ring characteristic of an extension of ℝ is zero. (Contributed by Thierry Arnoux, 2-May-2018.)
⊢ (𝑅 ∈ ℝExt → (chr‘𝑅) = 0)
Theorem	rrextcusp 33986	An extension of ℝ is a complete uniform space. (Contributed by Thierry Arnoux, 2-May-2018.)
⊢ (𝑅 ∈ ℝExt → 𝑅 ∈ CUnifSp)
Theorem	rrexttps 33987	An extension of ℝ is a topological space. (Contributed by Thierry Arnoux, 7-Sep-2018.)
⊢ (𝑅 ∈ ℝExt → 𝑅 ∈ TopSp)
Theorem	rrexthaus 33988	The topology of an extension of ℝ is Hausdorff. (Contributed by Thierry Arnoux, 7-Sep-2018.)
⊢ 𝐾 = (TopOpen‘𝑅)    ⇒   ⊢ (𝑅 ∈ ℝExt → 𝐾 ∈ Haus)
Theorem	rrextust 33989	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 33990	The field of the real numbers is an extension of the real numbers. (Contributed by Thierry Arnoux, 2-May-2018.)
⊢ ℝfld ∈ ℝExt
Theorem	cnrrext 33991	The field of the complex numbers is an extension of the real numbers. (Contributed by Thierry Arnoux, 2-May-2018.)
⊢ ℂfld ∈ ℝExt
Theorem	qqtopn 33992	The topology of the field of the rational numbers. (Contributed by Thierry Arnoux, 29-Aug-2020.)
⊢ ((TopOpen‘ℝfld) ↾t ℚ) = (TopOpen‘(ℂfld ↾s ℚ))
Theorem	rrhfe 33993	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 33994	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 33995	The ℝHom homomorphism leaves rational numbers unchanged. (Contributed by Thierry Arnoux, 27-Mar-2018.)
⊢ ((𝑅 ∈ ℝExt ∧ 𝑄 ∈ ℚ) → ((ℝHom‘𝑅)‘𝑄) = ((ℚHom‘𝑅)‘𝑄))
Theorem	rrh0 33996	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.16.5  Embedding from the extended real numbers into a complete lattice
Syntax	cxrh 33997	Map the extended real numbers into a complete lattice.
class ℝ*Hom
Definition	df-xrh 33998*	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 33999*	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.16.6  Canonical embeddings into the ordered field of the real numbers
Theorem	zrhre 34000	The ℤRHom homomorphism for the real number structure is the identity. (Contributed by Thierry Arnoux, 31-Oct-2017.)
⊢ (ℤRHom‘ℝfld) = ( I ↾ ℤ)