P. 342 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 34101-34200   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	zlmtset 34101	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 34102	Norm of a ℤ-module (if present). (Contributed by Thierry Arnoux, 8-Nov-2017.)
⊢ 𝑊 = (ℤMod‘𝐺)    &   ⊢ 𝑁 = (norm‘𝐺)    ⇒   ⊢ (𝐺 ∈ 𝑉 → 𝑁 = (norm‘𝑊))
Theorem	zhmnrg 34103	The ℤ-module built from a normed ring is also a normed ring. (Contributed by Thierry Arnoux, 8-Nov-2017.)
⊢ 𝑊 = (ℤMod‘𝐺)    ⇒   ⊢ (𝐺 ∈ NrmRing → 𝑊 ∈ NrmRing)
Theorem	nmmulg 34104	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 34105	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 34106	The ℤ-module of ℂ is a normed module. (Contributed by Thierry Arnoux, 25-Feb-2018.)
⊢ (ℤMod‘ℂfld) ∈ NrmMod
Theorem	rezh 34107	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 34108	Map the rationals into a field.
class ℚHom
Definition	df-qqh 34109*	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 34110*	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 34111	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 34112	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 34113	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 34114	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 34115	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 34116	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 34117	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 34118	Lemma for qqhval2 34120. (Contributed by Thierry Arnoux, 29-Oct-2017.)
⊢ (𝑀 ∈ (ℤ ∖ {0}) → (𝑀 ∈ ℕ ∨ -𝑀 ∈ ℕ))
Theorem	qqhval2lem 34119	Lemma for qqhval2 34120. (Contributed by Thierry Arnoux, 29-Oct-2017.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ / = (/r‘𝑅)    &   ⊢ 𝐿 = (ℤRHom‘𝑅)    ⇒   ⊢ (((𝑅 ∈ DivRing ∧ (chr‘𝑅) = 0) ∧ (𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ∧ 𝑌 ≠ 0)) → ((𝐿‘(numer‘(𝑋 / 𝑌))) / (𝐿‘(denom‘(𝑋 / 𝑌)))) = ((𝐿‘𝑋) / (𝐿‘𝑌)))
Theorem	qqhval2 34120*	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 34121	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 34122	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 34123	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 34124	ℚHom as a function. (Contributed by Thierry Arnoux, 28-Oct-2017.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ / = (/r‘𝑅)    &   ⊢ 𝐿 = (ℤRHom‘𝑅)    ⇒   ⊢ ((𝑅 ∈ DivRing ∧ (chr‘𝑅) = 0) → (ℚHom‘𝑅):ℚ⟶𝐵)
Theorem	qqhvq 34125	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 34126	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 34127	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 34128	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 34129	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 34130	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 34131	Map the real numbers into a complete field.
class ℝHom
Syntax	crrext 34132	Extend class notation with the class of extension fields of ℝ.
class ℝExt
Definition	df-rrh 34133	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 34134	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 34135	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 34136	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 34137	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 34138 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 34138	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 34139	An extension of ℝ is a normed ring. (Contributed by Thierry Arnoux, 2-May-2018.)
⊢ (𝑅 ∈ ℝExt → 𝑅 ∈ NrmRing)
Theorem	rrextdrg 34140	An extension of ℝ is a division ring. (Contributed by Thierry Arnoux, 2-May-2018.)
⊢ (𝑅 ∈ ℝExt → 𝑅 ∈ DivRing)
Theorem	rrextnlm 34141	The norm of an extension of ℝ is absolutely homogeneous. (Contributed by Thierry Arnoux, 2-May-2018.)
⊢ 𝑍 = (ℤMod‘𝑅)    ⇒   ⊢ (𝑅 ∈ ℝExt → 𝑍 ∈ NrmMod)
Theorem	rrextchr 34142	The ring characteristic of an extension of ℝ is zero. (Contributed by Thierry Arnoux, 2-May-2018.)
⊢ (𝑅 ∈ ℝExt → (chr‘𝑅) = 0)
Theorem	rrextcusp 34143	An extension of ℝ is a complete uniform space. (Contributed by Thierry Arnoux, 2-May-2018.)
⊢ (𝑅 ∈ ℝExt → 𝑅 ∈ CUnifSp)
Theorem	rrexttps 34144	An extension of ℝ is a topological space. (Contributed by Thierry Arnoux, 7-Sep-2018.)
⊢ (𝑅 ∈ ℝExt → 𝑅 ∈ TopSp)
Theorem	rrexthaus 34145	The topology of an extension of ℝ is Hausdorff. (Contributed by Thierry Arnoux, 7-Sep-2018.)
⊢ 𝐾 = (TopOpen‘𝑅)    ⇒   ⊢ (𝑅 ∈ ℝExt → 𝐾 ∈ Haus)
Theorem	rrextust 34146	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 34147	The field of the real numbers is an extension of the real numbers. (Contributed by Thierry Arnoux, 2-May-2018.)
⊢ ℝfld ∈ ℝExt
Theorem	cnrrext 34148	The field of the complex numbers is an extension of the real numbers. (Contributed by Thierry Arnoux, 2-May-2018.)
⊢ ℂfld ∈ ℝExt
Theorem	qqtopn 34149	The topology of the field of the rational numbers. (Contributed by Thierry Arnoux, 29-Aug-2020.)
⊢ ((TopOpen‘ℝfld) ↾t ℚ) = (TopOpen‘(ℂfld ↾s ℚ))
Theorem	rrhfe 34150	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 34151	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 34152	The ℝHom homomorphism leaves rational numbers unchanged. (Contributed by Thierry Arnoux, 27-Mar-2018.)
⊢ ((𝑅 ∈ ℝExt ∧ 𝑄 ∈ ℚ) → ((ℝHom‘𝑅)‘𝑄) = ((ℚHom‘𝑅)‘𝑄))
Theorem	rrh0 34153	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 34154	Map the extended real numbers into a complete lattice.
class ℝ*Hom
Definition	df-xrh 34155*	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 34156*	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 34157	The ℤRHom homomorphism for the real number structure is the identity. (Contributed by Thierry Arnoux, 31-Oct-2017.)
⊢ (ℤRHom‘ℝfld) = ( I ↾ ℤ)
Theorem	qqhre 34158	The ℚHom homomorphism for the real number structure is the identity. (Contributed by Thierry Arnoux, 31-Oct-2017.)
⊢ (ℚHom‘ℝfld) = ( I ↾ ℚ)
Theorem	rrhre 34159	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 34160	The class of n-manifold topologies.
class ManTop
Definition	df-mntop 34161*	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 34162	Manifold is a relation. (Contributed by Thierry Arnoux, 28-Dec-2019.)
⊢ Rel ManTop
Theorem	ismntoplly 34163	Property of being a manifold. (Contributed by Thierry Arnoux, 28-Dec-2019.)
⊢ ((𝑁 ∈ ℕ0 ∧ 𝐽 ∈ 𝑉) → (𝑁ManTop𝐽 ↔ (𝐽 ∈ 2ndω ∧ 𝐽 ∈ Haus ∧ 𝐽 ∈ Locally [(TopOpen‘(𝔼hil‘𝑁))] ≃ )))
Theorem	ismntop 34164*	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 34165	Extend class notation to include infinite summations.
class Σ*𝑘 ∈ 𝐴𝐵
Definition	df-esum 34166	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 34167	An extended sum is a set by definition. (Contributed by Thierry Arnoux, 5-Sep-2017.)
⊢ Σ*𝑘 ∈ 𝐴𝐵 ∈ V
Theorem	esumcl 34168*	Closure for extended sum in the extended positive reals. (Contributed by Thierry Arnoux, 2-Jan-2017.)
⊢ Ⅎ𝑘𝐴    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑘 ∈ 𝐴 𝐵 ∈ (0[,]+∞)) → Σ*𝑘 ∈ 𝐴𝐵 ∈ (0[,]+∞))
Theorem	esumeq12dvaf 34169	Equality deduction for extended sum. (Contributed by Thierry Arnoux, 26-Mar-2017.)
⊢ Ⅎ𝑘𝜑    &   ⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → Σ*𝑘 ∈ 𝐴𝐶 = Σ*𝑘 ∈ 𝐵𝐷)
Theorem	esumeq12dva 34170*	Equality deduction for extended sum. (Contributed by Thierry Arnoux, 18-Feb-2017.) (Revised by Thierry Arnoux, 29-Jun-2017.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → Σ*𝑘 ∈ 𝐴𝐶 = Σ*𝑘 ∈ 𝐵𝐷)
Theorem	esumeq12d 34171*	Equality deduction for extended sum. (Contributed by Thierry Arnoux, 18-Feb-2017.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → Σ*𝑘 ∈ 𝐴𝐶 = Σ*𝑘 ∈ 𝐵𝐷)
Theorem	esumeq1 34172*	Equality theorem for an extended sum. (Contributed by Thierry Arnoux, 18-Feb-2017.)
⊢ (𝐴 = 𝐵 → Σ*𝑘 ∈ 𝐴𝐶 = Σ*𝑘 ∈ 𝐵𝐶)
Theorem	esumeq1d 34173	Equality theorem for an extended sum. (Contributed by Thierry Arnoux, 19-Oct-2017.)
⊢ Ⅎ𝑘𝜑    &   ⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → Σ*𝑘 ∈ 𝐴𝐶 = Σ*𝑘 ∈ 𝐵𝐶)
Theorem	esumeq2 34174*	Equality theorem for extended sum. (Contributed by Thierry Arnoux, 24-Dec-2016.)
⊢ (∀𝑘 ∈ 𝐴 𝐵 = 𝐶 → Σ*𝑘 ∈ 𝐴𝐵 = Σ*𝑘 ∈ 𝐴𝐶)
Theorem	esumeq2d 34175	Equality deduction for extended sum. (Contributed by Thierry Arnoux, 21-Sep-2016.)
⊢ Ⅎ𝑘𝜑    &   ⊢ (𝜑 → ∀𝑘 ∈ 𝐴 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → Σ*𝑘 ∈ 𝐴𝐵 = Σ*𝑘 ∈ 𝐴𝐶)
Theorem	esumeq2dv 34176*	Equality deduction for extended sum. (Contributed by Thierry Arnoux, 2-Jan-2017.)
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → Σ*𝑘 ∈ 𝐴𝐵 = Σ*𝑘 ∈ 𝐴𝐶)
Theorem	esumeq2sdv 34177*	Equality deduction for extended sum. (Contributed by Thierry Arnoux, 25-Dec-2016.)
⊢ (𝜑 → 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → Σ*𝑘 ∈ 𝐴𝐵 = Σ*𝑘 ∈ 𝐴𝐶)
Theorem	nfesum1 34178	Bound-variable hypothesis builder for extended sum. (Contributed by Thierry Arnoux, 19-Oct-2017.)
⊢ Ⅎ𝑘𝐴    ⇒   ⊢ Ⅎ𝑘Σ*𝑘 ∈ 𝐴𝐵
Theorem	nfesum2 34179*	Bound-variable hypothesis builder for extended sum. (Contributed by Thierry Arnoux, 2-May-2020.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ Ⅎ𝑥Σ*𝑘 ∈ 𝐴𝐵
Theorem	cbvesum 34180*	Change bound variable in an extended sum. (Contributed by Thierry Arnoux, 19-Jun-2017.)
⊢ (𝑗 = 𝑘 → 𝐵 = 𝐶)    &   ⊢ Ⅎ𝑘𝐴    &   ⊢ Ⅎ𝑗𝐴    &   ⊢ Ⅎ𝑘𝐵    &   ⊢ Ⅎ𝑗𝐶    ⇒   ⊢ Σ*𝑗 ∈ 𝐴𝐵 = Σ*𝑘 ∈ 𝐴𝐶
Theorem	cbvesumv 34181*	Change bound variable in an extended sum. (Contributed by Thierry Arnoux, 19-Jun-2017.)
⊢ (𝑗 = 𝑘 → 𝐵 = 𝐶)    ⇒   ⊢ Σ*𝑗 ∈ 𝐴𝐵 = Σ*𝑘 ∈ 𝐴𝐶
Theorem	esumid 34182	Identify the extended sum as any limit points of the infinite sum. (Contributed by Thierry Arnoux, 9-May-2017.)
⊢ Ⅎ𝑘𝜑    &   ⊢ Ⅎ𝑘𝐴    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ (0[,]+∞))    &   ⊢ (𝜑 → 𝐶 ∈ ((ℝ*𝑠 ↾s (0[,]+∞)) tsums (𝑘 ∈ 𝐴 ↦ 𝐵)))    ⇒   ⊢ (𝜑 → Σ*𝑘 ∈ 𝐴𝐵 = 𝐶)
Theorem	esumgsum 34183	A finite extended sum is the group sum over the extended nonnegative real numbers. (Contributed by Thierry Arnoux, 24-Apr-2020.)
⊢ Ⅎ𝑘𝜑    &   ⊢ Ⅎ𝑘𝐴    &   ⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ (0[,]+∞))    ⇒   ⊢ (𝜑 → Σ*𝑘 ∈ 𝐴𝐵 = ((ℝ*𝑠 ↾s (0[,]+∞)) Σg (𝑘 ∈ 𝐴 ↦ 𝐵)))
Theorem	esumval 34184*	Develop the value of the extended sum. (Contributed by Thierry Arnoux, 4-Jan-2017.)
⊢ Ⅎ𝑘𝜑    &   ⊢ Ⅎ𝑘𝐴    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ (0[,]+∞))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝐴 ∩ Fin)) → ((ℝ*𝑠 ↾s (0[,]+∞)) Σg (𝑘 ∈ 𝑥 ↦ 𝐵)) = 𝐶)    ⇒   ⊢ (𝜑 → Σ*𝑘 ∈ 𝐴𝐵 = sup(ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ 𝐶), ℝ*, < ))
Theorem	esumel 34185*	The extended sum is a limit point of the corresponding infinite group sum. (Contributed by Thierry Arnoux, 24-Mar-2017.)
⊢ Ⅎ𝑘𝜑    &   ⊢ Ⅎ𝑘𝐴    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ (0[,]+∞))    ⇒   ⊢ (𝜑 → Σ*𝑘 ∈ 𝐴𝐵 ∈ ((ℝ*𝑠 ↾s (0[,]+∞)) tsums (𝑘 ∈ 𝐴 ↦ 𝐵)))
Theorem	esumnul 34186	Extended sum over the empty set. (Contributed by Thierry Arnoux, 19-Feb-2017.)
⊢ Σ*𝑥 ∈ ∅𝐴 = 0
Theorem	esum0 34187*	Extended sum of zero. (Contributed by Thierry Arnoux, 3-Mar-2017.)
⊢ Ⅎ𝑘𝐴    ⇒   ⊢ (𝐴 ∈ 𝑉 → Σ*𝑘 ∈ 𝐴0 = 0)
Theorem	esumf1o 34188*	Re-index an extended sum using a bijection. (Contributed by Thierry Arnoux, 6-Apr-2017.)
⊢ Ⅎ𝑛𝜑    &   ⊢ Ⅎ𝑛𝐵    &   ⊢ Ⅎ𝑘𝐷    &   ⊢ Ⅎ𝑛𝐴    &   ⊢ Ⅎ𝑛𝐶    &   ⊢ Ⅎ𝑛𝐹    &   ⊢ (𝑘 = 𝐺 → 𝐵 = 𝐷)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹:𝐶–1-1-onto→𝐴)    &   ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶) → (𝐹‘𝑛) = 𝐺)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ (0[,]+∞))    ⇒   ⊢ (𝜑 → Σ*𝑘 ∈ 𝐴𝐵 = Σ*𝑛 ∈ 𝐶𝐷)
Theorem	esumc 34189*	Convert from the collection form to the class-variable form of a sum. (Contributed by Thierry Arnoux, 10-May-2017.)
⊢ Ⅎ𝑘𝐷    &   ⊢ Ⅎ𝑘𝜑    &   ⊢ Ⅎ𝑘𝐴    &   ⊢ (𝑦 = 𝐶 → 𝐷 = 𝐵)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → Fun ◡(𝑘 ∈ 𝐴 ↦ 𝐶))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ (0[,]+∞))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐶 ∈ 𝑊)    ⇒   ⊢ (𝜑 → Σ*𝑘 ∈ 𝐴𝐵 = Σ*𝑦 ∈ {𝑧 ∣ ∃𝑘 ∈ 𝐴 𝑧 = 𝐶}𝐷)
Theorem	esumrnmpt 34190*	Rewrite an extended sum into a sum on the range of a mapping function. (Contributed by Thierry Arnoux, 27-May-2020.)
⊢ Ⅎ𝑘𝐴    &   ⊢ (𝑦 = 𝐵 → 𝐶 = 𝐷)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐷 ∈ (0[,]+∞))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ (𝑊 ∖ {∅}))    &   ⊢ (𝜑 → Disj 𝑘 ∈ 𝐴 𝐵)    ⇒   ⊢ (𝜑 → Σ*𝑦 ∈ ran (𝑘 ∈ 𝐴 ↦ 𝐵)𝐶 = Σ*𝑘 ∈ 𝐴𝐷)
Theorem	esumsplit 34191	Split an extended sum into two parts. (Contributed by Thierry Arnoux, 9-May-2017.)
⊢ Ⅎ𝑘𝜑    &   ⊢ Ⅎ𝑘𝐴    &   ⊢ Ⅎ𝑘𝐵    &   ⊢ (𝜑 → 𝐴 ∈ V)    &   ⊢ (𝜑 → 𝐵 ∈ V)    &   ⊢ (𝜑 → (𝐴 ∩ 𝐵) = ∅)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐶 ∈ (0[,]+∞))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵) → 𝐶 ∈ (0[,]+∞))    ⇒   ⊢ (𝜑 → Σ*𝑘 ∈ (𝐴 ∪ 𝐵)𝐶 = (Σ*𝑘 ∈ 𝐴𝐶 +𝑒 Σ*𝑘 ∈ 𝐵𝐶))
Theorem	esummono 34192*	Extended sum is monotonic. (Contributed by Thierry Arnoux, 19-Oct-2017.)
⊢ Ⅎ𝑘𝜑    &   ⊢ (𝜑 → 𝐶 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐶) → 𝐵 ∈ (0[,]+∞))    &   ⊢ (𝜑 → 𝐴 ⊆ 𝐶)    ⇒   ⊢ (𝜑 → Σ*𝑘 ∈ 𝐴𝐵 ≤ Σ*𝑘 ∈ 𝐶𝐵)
Theorem	esumpad 34193*	Extend an extended sum by padding outside with zeroes. (Contributed by Thierry Arnoux, 31-May-2020.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐶 ∈ (0[,]+∞))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵) → 𝐶 = 0)    ⇒   ⊢ (𝜑 → Σ*𝑘 ∈ (𝐴 ∪ 𝐵)𝐶 = Σ*𝑘 ∈ 𝐴𝐶)
Theorem	esumpad2 34194*	Remove zeroes from an extended sum. (Contributed by Thierry Arnoux, 5-Jun-2020.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐶 ∈ (0[,]+∞))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵) → 𝐶 = 0)    ⇒   ⊢ (𝜑 → Σ*𝑘 ∈ (𝐴 ∖ 𝐵)𝐶 = Σ*𝑘 ∈ 𝐴𝐶)
Theorem	esumadd 34195*	Addition of infinite sums. (Contributed by Thierry Arnoux, 24-Mar-2017.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ (0[,]+∞))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐶 ∈ (0[,]+∞))    ⇒   ⊢ (𝜑 → Σ*𝑘 ∈ 𝐴(𝐵 +𝑒 𝐶) = (Σ*𝑘 ∈ 𝐴𝐵 +𝑒 Σ*𝑘 ∈ 𝐴𝐶))
Theorem	esumle 34196*	If all of the terms of an extended sums compare, so do the sums. (Contributed by Thierry Arnoux, 8-Jun-2017.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ (0[,]+∞))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐶 ∈ (0[,]+∞))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ≤ 𝐶)    ⇒   ⊢ (𝜑 → Σ*𝑘 ∈ 𝐴𝐵 ≤ Σ*𝑘 ∈ 𝐴𝐶)
Theorem	gsumesum 34197*	Relate a group sum on (ℝ*𝑠 ↾s (0[,]+∞)) to a finite extended sum. (Contributed by Thierry Arnoux, 19-Oct-2017.) (Proof shortened by AV, 12-Dec-2019.)
⊢ Ⅎ𝑘𝜑    &   ⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ (0[,]+∞))    ⇒   ⊢ (𝜑 → ((ℝ*𝑠 ↾s (0[,]+∞)) Σg (𝑘 ∈ 𝐴 ↦ 𝐵)) = Σ*𝑘 ∈ 𝐴𝐵)
Theorem	esumlub 34198*	The extended sum is the lowest upper bound for the partial sums. (Contributed by Thierry Arnoux, 19-Oct-2017.) (Proof shortened by AV, 12-Dec-2019.)
⊢ Ⅎ𝑘𝜑    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ (0[,]+∞))    &   ⊢ (𝜑 → 𝑋 ∈ ℝ*)    &   ⊢ (𝜑 → 𝑋 < Σ*𝑘 ∈ 𝐴𝐵)    ⇒   ⊢ (𝜑 → ∃𝑎 ∈ (𝒫 𝐴 ∩ Fin)𝑋 < Σ*𝑘 ∈ 𝑎𝐵)
Theorem	esumaddf 34199*	Addition of infinite sums. (Contributed by Thierry Arnoux, 22-Jun-2017.)
⊢ Ⅎ𝑘𝜑    &   ⊢ Ⅎ𝑘𝐴    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ (0[,]+∞))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐶 ∈ (0[,]+∞))    ⇒   ⊢ (𝜑 → Σ*𝑘 ∈ 𝐴(𝐵 +𝑒 𝐶) = (Σ*𝑘 ∈ 𝐴𝐵 +𝑒 Σ*𝑘 ∈ 𝐴𝐶))
Theorem	esumlef 34200*	If all of the terms of an extended sums compare, so do the sums. (Contributed by Thierry Arnoux, 8-Jun-2017.)
⊢ Ⅎ𝑘𝜑    &   ⊢ Ⅎ𝑘𝐴    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ (0[,]+∞))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐶 ∈ (0[,]+∞))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ≤ 𝐶)    ⇒   ⊢ (𝜑 → Σ*𝑘 ∈ 𝐴𝐵 ≤ Σ*𝑘 ∈ 𝐴𝐶)