P. 343 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 34201-34300   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	xrge0haus 34201	The topology of the extended nonnegative real numbers is Hausdorff. (Contributed by Thierry Arnoux, 26-Jul-2017.)
⊢ (TopOpen‘(ℝ*𝑠 ↾s (0[,]+∞))) ∈ Haus
Theorem	xrge0tmd 34202	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 34203	Alternate proof of xrge0tmd 34202. (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 34204	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 34205	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 34206	Implication of convergence for a nonnegative series. This could be used to shorten prmreclem6 16947. (Contributed by Thierry Arnoux, 28-Jul-2017.)
⊢ ((𝐹:ℕ⟶(0[,)+∞) ∧ seq1( + , 𝐹) ∈ dom ⇝ ) → sup(ran seq1( + , 𝐹), ℝ, < ) ∈ ℝ)
Theorem	fsumcvg4 34207	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 34208*	A neighborhood of +∞ contains an unbounded interval based at a real number. See pnfnei 23267. (Contributed by Thierry Arnoux, 31-Jul-2017.)
⊢ 𝐽 = (TopOpen‘(ℝ*𝑠 ↾s (0[,]+∞)))    ⇒   ⊢ ((𝐴 ∈ 𝐽 ∧ +∞ ∈ 𝐴) → ∃𝑥 ∈ ℝ (𝑥(,]+∞) ⊆ 𝐴)
Theorem	lmxrge0 34209*	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 34210*	If a monotonic sequence of real numbers diverges, it is unbounded. (Contributed by Thierry Arnoux, 4-Aug-2017.)
⊢ (𝜑 → 𝐹:ℕ⟶(0[,)+∞))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐹‘𝑘) ≤ (𝐹‘(𝑘 + 1)))    &   ⊢ (𝜑 → ¬ 𝐹 ∈ dom ⇝ )    ⇒   ⊢ (𝜑 → ∀𝑥 ∈ ℝ ∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑗)𝑥 < (𝐹‘𝑘))
Theorem	lmdvglim 34211*	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 34212	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 34213	Extend class notation with the Hausdorff uniform completion relation.
class HCmp
Definition	df-hcmp 34214*	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 34215	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 34216	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 34217	Zero of a ℤ-module. (Contributed by Thierry Arnoux, 8-Nov-2017.)
⊢ 𝑊 = (ℤMod‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    ⇒   ⊢ 0 = (0g‘𝑊)
Theorem	zlm1 34218	Unity element of a ℤ-module (if present). (Contributed by Thierry Arnoux, 8-Nov-2017.)
⊢ 𝑊 = (ℤMod‘𝐺)    &   ⊢ 1 = (1r‘𝐺)    ⇒   ⊢ 1 = (1r‘𝑊)
Theorem	zlmds 34219	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 34220	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 34221	Norm of a ℤ-module (if present). (Contributed by Thierry Arnoux, 8-Nov-2017.)
⊢ 𝑊 = (ℤMod‘𝐺)    &   ⊢ 𝑁 = (norm‘𝐺)    ⇒   ⊢ (𝐺 ∈ 𝑉 → 𝑁 = (norm‘𝑊))
Theorem	zhmnrg 34222	The ℤ-module built from a normed ring is also a normed ring. (Contributed by Thierry Arnoux, 8-Nov-2017.)
⊢ 𝑊 = (ℤMod‘𝐺)    ⇒   ⊢ (𝐺 ∈ NrmRing → 𝑊 ∈ NrmRing)
Theorem	nmmulg 34223	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 34224	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 34225	The ℤ-module of ℂ is a normed module. (Contributed by Thierry Arnoux, 25-Feb-2018.)
⊢ (ℤMod‘ℂfld) ∈ NrmMod
Theorem	rezh 34226	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 34227	Map the rationals into a field.
class ℚHom
Definition	df-qqh 34228*	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 34229*	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 34230	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 34231	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 34232	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 34233	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 34234	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 34235	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 34236	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 34237	Lemma for qqhval2 34239. (Contributed by Thierry Arnoux, 29-Oct-2017.)
⊢ (𝑀 ∈ (ℤ ∖ {0}) → (𝑀 ∈ ℕ ∨ -𝑀 ∈ ℕ))
Theorem	qqhval2lem 34238	Lemma for qqhval2 34239. (Contributed by Thierry Arnoux, 29-Oct-2017.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ / = (/r‘𝑅)    &   ⊢ 𝐿 = (ℤRHom‘𝑅)    ⇒   ⊢ (((𝑅 ∈ DivRing ∧ (chr‘𝑅) = 0) ∧ (𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ∧ 𝑌 ≠ 0)) → ((𝐿‘(numer‘(𝑋 / 𝑌))) / (𝐿‘(denom‘(𝑋 / 𝑌)))) = ((𝐿‘𝑋) / (𝐿‘𝑌)))
Theorem	qqhval2 34239*	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 34240	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 34241	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 34242	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 34243	ℚHom as a function. (Contributed by Thierry Arnoux, 28-Oct-2017.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ / = (/r‘𝑅)    &   ⊢ 𝐿 = (ℤRHom‘𝑅)    ⇒   ⊢ ((𝑅 ∈ DivRing ∧ (chr‘𝑅) = 0) → (ℚHom‘𝑅):ℚ⟶𝐵)
Theorem	qqhvq 34244	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 34245	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 34246	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 34247	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 34248	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 34249	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 34250	Map the real numbers into a complete field.
class ℝHom
Syntax	crrext 34251	Extend class notation with the class of extension fields of ℝ.
class ℝExt
Definition	df-rrh 34252	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 34253	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 34254	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 34255	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 34256	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 34257 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 34257	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 34258	An extension of ℝ is a normed ring. (Contributed by Thierry Arnoux, 2-May-2018.)
⊢ (𝑅 ∈ ℝExt → 𝑅 ∈ NrmRing)
Theorem	rrextdrg 34259	An extension of ℝ is a division ring. (Contributed by Thierry Arnoux, 2-May-2018.)
⊢ (𝑅 ∈ ℝExt → 𝑅 ∈ DivRing)
Theorem	rrextnlm 34260	The norm of an extension of ℝ is absolutely homogeneous. (Contributed by Thierry Arnoux, 2-May-2018.)
⊢ 𝑍 = (ℤMod‘𝑅)    ⇒   ⊢ (𝑅 ∈ ℝExt → 𝑍 ∈ NrmMod)
Theorem	rrextchr 34261	The ring characteristic of an extension of ℝ is zero. (Contributed by Thierry Arnoux, 2-May-2018.)
⊢ (𝑅 ∈ ℝExt → (chr‘𝑅) = 0)
Theorem	rrextcusp 34262	An extension of ℝ is a complete uniform space. (Contributed by Thierry Arnoux, 2-May-2018.)
⊢ (𝑅 ∈ ℝExt → 𝑅 ∈ CUnifSp)
Theorem	rrexttps 34263	An extension of ℝ is a topological space. (Contributed by Thierry Arnoux, 7-Sep-2018.)
⊢ (𝑅 ∈ ℝExt → 𝑅 ∈ TopSp)
Theorem	rrexthaus 34264	The topology of an extension of ℝ is Hausdorff. (Contributed by Thierry Arnoux, 7-Sep-2018.)
⊢ 𝐾 = (TopOpen‘𝑅)    ⇒   ⊢ (𝑅 ∈ ℝExt → 𝐾 ∈ Haus)
Theorem	rrextust 34265	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 34266	The field of the real numbers is an extension of the real numbers. (Contributed by Thierry Arnoux, 2-May-2018.)
⊢ ℝfld ∈ ℝExt
Theorem	cnrrext 34267	The field of the complex numbers is an extension of the real numbers. (Contributed by Thierry Arnoux, 2-May-2018.)
⊢ ℂfld ∈ ℝExt
Theorem	qqtopn 34268	The topology of the field of the rational numbers. (Contributed by Thierry Arnoux, 29-Aug-2020.)
⊢ ((TopOpen‘ℝfld) ↾t ℚ) = (TopOpen‘(ℂfld ↾s ℚ))
Theorem	rrhfe 34269	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 34270	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 34271	The ℝHom homomorphism leaves rational numbers unchanged. (Contributed by Thierry Arnoux, 27-Mar-2018.)
⊢ ((𝑅 ∈ ℝExt ∧ 𝑄 ∈ ℚ) → ((ℝHom‘𝑅)‘𝑄) = ((ℚHom‘𝑅)‘𝑄))
Theorem	rrh0 34272	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 34273	Map the extended real numbers into a complete lattice.
class ℝ*Hom
Definition	df-xrh 34274*	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 34275*	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 34276	The ℤRHom homomorphism for the real number structure is the identity. (Contributed by Thierry Arnoux, 31-Oct-2017.)
⊢ (ℤRHom‘ℝfld) = ( I ↾ ℤ)
Theorem	qqhre 34277	The ℚHom homomorphism for the real number structure is the identity. (Contributed by Thierry Arnoux, 31-Oct-2017.)
⊢ (ℚHom‘ℝfld) = ( I ↾ ℚ)
Theorem	rrhre 34278	The ℝHom homomorphism for the real numbers structure is the identity. (Contributed by Thierry Arnoux, 22-Oct-2017.)
⊢ (ℝHom‘ℝfld) = ( I ↾ ℝ)
21.3.16.7  Topological Manifolds Found this and was curious about how manifolds would be expressed in set.mm: https://mathoverflow.net/questions/336367/real-manifolds-in-a-theorem-prover This chapter proposes to define first manifold topologies, which characterize topological manifolds, and then to extend the structure with presentations, i.e., equivalence classes of atlases for a given topological space. We suggest to use the extensible structures to define the "topological space" aspect of topological manifolds, and then extend it with charts/presentations.
Syntax	cmntop 34279	The class of n-manifold topologies.
class ManTop
Definition	df-mntop 34280*	Define the class of 𝑁-manifold topologies, as second countable Hausdorff topologies locally homeomorphic to a ball of the Euclidean space of dimension 𝑁. (Contributed by Thierry Arnoux, 22-Dec-2019.)
⊢ ManTop = {⟨𝑛, 𝑗⟩ ∣ (𝑛 ∈ ℕ0 ∧ (𝑗 ∈ 2ndω ∧ 𝑗 ∈ Haus ∧ 𝑗 ∈ Locally [(TopOpen‘(𝔼hil‘𝑛))] ≃ ))}
Theorem	relmntop 34281	Manifold is a relation. (Contributed by Thierry Arnoux, 28-Dec-2019.)
⊢ Rel ManTop
Theorem	ismntoplly 34282	Property of being a manifold. (Contributed by Thierry Arnoux, 28-Dec-2019.)
⊢ ((𝑁 ∈ ℕ0 ∧ 𝐽 ∈ 𝑉) → (𝑁ManTop𝐽 ↔ (𝐽 ∈ 2ndω ∧ 𝐽 ∈ Haus ∧ 𝐽 ∈ Locally [(TopOpen‘(𝔼hil‘𝑁))] ≃ )))
Theorem	ismntop 34283*	Property of being a manifold. (Contributed by Thierry Arnoux, 5-Jan-2020.)
⊢ ((𝑁 ∈ ℕ0 ∧ 𝐽 ∈ 𝑉) → (𝑁ManTop𝐽 ↔ (𝐽 ∈ 2ndω ∧ 𝐽 ∈ Haus ∧ ∀𝑥 ∈ 𝐽 ∀𝑦 ∈ 𝑥 ∃𝑢 ∈ (𝐽 ∩ 𝒫 𝑥)(𝑦 ∈ 𝑢 ∧ (𝐽 ↾t 𝑢) ≃ (TopOpen‘(𝔼hil‘𝑁))))))
21.3.16.8  Extended sum
Syntax	cesum 34284	Extend class notation to include infinite summations.
class Σ*𝑘 ∈ 𝐴𝐵
Definition	df-esum 34285	Define a short-hand for the possibly infinite sum over the extended nonnegative reals. Σ* is relying on the properties of the tsums, developed by Mario Carneiro. (Contributed by Thierry Arnoux, 21-Sep-2016.)
⊢ Σ*𝑘 ∈ 𝐴𝐵 = ∪ ((ℝ*𝑠 ↾s (0[,]+∞)) tsums (𝑘 ∈ 𝐴 ↦ 𝐵))
Theorem	esumex 34286	An extended sum is a set by definition. (Contributed by Thierry Arnoux, 5-Sep-2017.)
⊢ Σ*𝑘 ∈ 𝐴𝐵 ∈ V
Theorem	esumcl 34287*	Closure for extended sum in the extended positive reals. (Contributed by Thierry Arnoux, 2-Jan-2017.)
⊢ Ⅎ𝑘𝐴    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑘 ∈ 𝐴 𝐵 ∈ (0[,]+∞)) → Σ*𝑘 ∈ 𝐴𝐵 ∈ (0[,]+∞))
Theorem	esumeq12dvaf 34288	Equality deduction for extended sum. (Contributed by Thierry Arnoux, 26-Mar-2017.)
⊢ Ⅎ𝑘𝜑    &   ⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → Σ*𝑘 ∈ 𝐴𝐶 = Σ*𝑘 ∈ 𝐵𝐷)
Theorem	esumeq12dva 34289*	Equality deduction for extended sum. (Contributed by Thierry Arnoux, 18-Feb-2017.) (Revised by Thierry Arnoux, 29-Jun-2017.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → Σ*𝑘 ∈ 𝐴𝐶 = Σ*𝑘 ∈ 𝐵𝐷)
Theorem	esumeq12d 34290*	Equality deduction for extended sum. (Contributed by Thierry Arnoux, 18-Feb-2017.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → Σ*𝑘 ∈ 𝐴𝐶 = Σ*𝑘 ∈ 𝐵𝐷)
Theorem	esumeq1 34291*	Equality theorem for an extended sum. (Contributed by Thierry Arnoux, 18-Feb-2017.)
⊢ (𝐴 = 𝐵 → Σ*𝑘 ∈ 𝐴𝐶 = Σ*𝑘 ∈ 𝐵𝐶)
Theorem	esumeq1d 34292	Equality theorem for an extended sum. (Contributed by Thierry Arnoux, 19-Oct-2017.)
⊢ Ⅎ𝑘𝜑    &   ⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → Σ*𝑘 ∈ 𝐴𝐶 = Σ*𝑘 ∈ 𝐵𝐶)
Theorem	esumeq2 34293*	Equality theorem for extended sum. (Contributed by Thierry Arnoux, 24-Dec-2016.)
⊢ (∀𝑘 ∈ 𝐴 𝐵 = 𝐶 → Σ*𝑘 ∈ 𝐴𝐵 = Σ*𝑘 ∈ 𝐴𝐶)
Theorem	esumeq2d 34294	Equality deduction for extended sum. (Contributed by Thierry Arnoux, 21-Sep-2016.)
⊢ Ⅎ𝑘𝜑    &   ⊢ (𝜑 → ∀𝑘 ∈ 𝐴 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → Σ*𝑘 ∈ 𝐴𝐵 = Σ*𝑘 ∈ 𝐴𝐶)
Theorem	esumeq2dv 34295*	Equality deduction for extended sum. (Contributed by Thierry Arnoux, 2-Jan-2017.)
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → Σ*𝑘 ∈ 𝐴𝐵 = Σ*𝑘 ∈ 𝐴𝐶)
Theorem	esumeq2sdv 34296*	Equality deduction for extended sum. (Contributed by Thierry Arnoux, 25-Dec-2016.)
⊢ (𝜑 → 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → Σ*𝑘 ∈ 𝐴𝐵 = Σ*𝑘 ∈ 𝐴𝐶)
Theorem	nfesum1 34297	Bound-variable hypothesis builder for extended sum. (Contributed by Thierry Arnoux, 19-Oct-2017.)
⊢ Ⅎ𝑘𝐴    ⇒   ⊢ Ⅎ𝑘Σ*𝑘 ∈ 𝐴𝐵
Theorem	nfesum2 34298*	Bound-variable hypothesis builder for extended sum. (Contributed by Thierry Arnoux, 2-May-2020.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ Ⅎ𝑥Σ*𝑘 ∈ 𝐴𝐵
Theorem	cbvesum 34299*	Change bound variable in an extended sum. (Contributed by Thierry Arnoux, 19-Jun-2017.)
⊢ (𝑗 = 𝑘 → 𝐵 = 𝐶)    &   ⊢ Ⅎ𝑘𝐴    &   ⊢ Ⅎ𝑗𝐴    &   ⊢ Ⅎ𝑘𝐵    &   ⊢ Ⅎ𝑗𝐶    ⇒   ⊢ Σ*𝑗 ∈ 𝐴𝐵 = Σ*𝑘 ∈ 𝐴𝐶
Theorem	cbvesumv 34300*	Change bound variable in an extended sum. (Contributed by Thierry Arnoux, 19-Jun-2017.)
⊢ (𝑗 = 𝑘 → 𝐵 = 𝐶)    ⇒   ⊢ Σ*𝑗 ∈ 𝐴𝐵 = Σ*𝑘 ∈ 𝐴𝐶