P. 341 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 34001-34100   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	zrhnm 34001	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 34002	The ℤ-module of ℂ is a normed module. (Contributed by Thierry Arnoux, 25-Feb-2018.)
⊢ (ℤMod‘ℂfld) ∈ NrmMod
Theorem	rezh 34003	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 34004	Map the rationals into a field.
class ℚHom
Definition	df-qqh 34005*	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 34006*	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 34007	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 34008	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 34009	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 34010	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 34011	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 34012	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 34013	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 34014	Lemma for qqhval2 34016. (Contributed by Thierry Arnoux, 29-Oct-2017.)
⊢ (𝑀 ∈ (ℤ ∖ {0}) → (𝑀 ∈ ℕ ∨ -𝑀 ∈ ℕ))
Theorem	qqhval2lem 34015	Lemma for qqhval2 34016. (Contributed by Thierry Arnoux, 29-Oct-2017.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ / = (/r‘𝑅)    &   ⊢ 𝐿 = (ℤRHom‘𝑅)    ⇒   ⊢ (((𝑅 ∈ DivRing ∧ (chr‘𝑅) = 0) ∧ (𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ∧ 𝑌 ≠ 0)) → ((𝐿‘(numer‘(𝑋 / 𝑌))) / (𝐿‘(denom‘(𝑋 / 𝑌)))) = ((𝐿‘𝑋) / (𝐿‘𝑌)))
Theorem	qqhval2 34016*	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 34017	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 34018	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 34019	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 34020	ℚHom as a function. (Contributed by Thierry Arnoux, 28-Oct-2017.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ / = (/r‘𝑅)    &   ⊢ 𝐿 = (ℤRHom‘𝑅)    ⇒   ⊢ ((𝑅 ∈ DivRing ∧ (chr‘𝑅) = 0) → (ℚHom‘𝑅):ℚ⟶𝐵)
Theorem	qqhvq 34021	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 34022	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 34023	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 34024	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 34025	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 34026	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 34027	Map the real numbers into a complete field.
class ℝHom
Syntax	crrext 34028	Extend class notation with the class of extension fields of ℝ.
class ℝExt
Definition	df-rrh 34029	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 34030	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 34031	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 34032	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 34033	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 34034 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 34034	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 34035	An extension of ℝ is a normed ring. (Contributed by Thierry Arnoux, 2-May-2018.)
⊢ (𝑅 ∈ ℝExt → 𝑅 ∈ NrmRing)
Theorem	rrextdrg 34036	An extension of ℝ is a division ring. (Contributed by Thierry Arnoux, 2-May-2018.)
⊢ (𝑅 ∈ ℝExt → 𝑅 ∈ DivRing)
Theorem	rrextnlm 34037	The norm of an extension of ℝ is absolutely homogeneous. (Contributed by Thierry Arnoux, 2-May-2018.)
⊢ 𝑍 = (ℤMod‘𝑅)    ⇒   ⊢ (𝑅 ∈ ℝExt → 𝑍 ∈ NrmMod)
Theorem	rrextchr 34038	The ring characteristic of an extension of ℝ is zero. (Contributed by Thierry Arnoux, 2-May-2018.)
⊢ (𝑅 ∈ ℝExt → (chr‘𝑅) = 0)
Theorem	rrextcusp 34039	An extension of ℝ is a complete uniform space. (Contributed by Thierry Arnoux, 2-May-2018.)
⊢ (𝑅 ∈ ℝExt → 𝑅 ∈ CUnifSp)
Theorem	rrexttps 34040	An extension of ℝ is a topological space. (Contributed by Thierry Arnoux, 7-Sep-2018.)
⊢ (𝑅 ∈ ℝExt → 𝑅 ∈ TopSp)
Theorem	rrexthaus 34041	The topology of an extension of ℝ is Hausdorff. (Contributed by Thierry Arnoux, 7-Sep-2018.)
⊢ 𝐾 = (TopOpen‘𝑅)    ⇒   ⊢ (𝑅 ∈ ℝExt → 𝐾 ∈ Haus)
Theorem	rrextust 34042	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 34043	The field of the real numbers is an extension of the real numbers. (Contributed by Thierry Arnoux, 2-May-2018.)
⊢ ℝfld ∈ ℝExt
Theorem	cnrrext 34044	The field of the complex numbers is an extension of the real numbers. (Contributed by Thierry Arnoux, 2-May-2018.)
⊢ ℂfld ∈ ℝExt
Theorem	qqtopn 34045	The topology of the field of the rational numbers. (Contributed by Thierry Arnoux, 29-Aug-2020.)
⊢ ((TopOpen‘ℝfld) ↾t ℚ) = (TopOpen‘(ℂfld ↾s ℚ))
Theorem	rrhfe 34046	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 34047	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 34048	The ℝHom homomorphism leaves rational numbers unchanged. (Contributed by Thierry Arnoux, 27-Mar-2018.)
⊢ ((𝑅 ∈ ℝExt ∧ 𝑄 ∈ ℚ) → ((ℝHom‘𝑅)‘𝑄) = ((ℚHom‘𝑅)‘𝑄))
Theorem	rrh0 34049	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 34050	Map the extended real numbers into a complete lattice.
class ℝ*Hom
Definition	df-xrh 34051*	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 34052*	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 34053	The ℤRHom homomorphism for the real number structure is the identity. (Contributed by Thierry Arnoux, 31-Oct-2017.)
⊢ (ℤRHom‘ℝfld) = ( I ↾ ℤ)
Theorem	qqhre 34054	The ℚHom homomorphism for the real number structure is the identity. (Contributed by Thierry Arnoux, 31-Oct-2017.)
⊢ (ℚHom‘ℝfld) = ( I ↾ ℚ)
Theorem	rrhre 34055	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 34056	The class of n-manifold topologies.
class ManTop
Definition	df-mntop 34057*	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 34058	Manifold is a relation. (Contributed by Thierry Arnoux, 28-Dec-2019.)
⊢ Rel ManTop
Theorem	ismntoplly 34059	Property of being a manifold. (Contributed by Thierry Arnoux, 28-Dec-2019.)
⊢ ((𝑁 ∈ ℕ0 ∧ 𝐽 ∈ 𝑉) → (𝑁ManTop𝐽 ↔ (𝐽 ∈ 2ndω ∧ 𝐽 ∈ Haus ∧ 𝐽 ∈ Locally [(TopOpen‘(𝔼hil‘𝑁))] ≃ )))
Theorem	ismntop 34060*	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 34061	Extend class notation to include infinite summations.
class Σ*𝑘 ∈ 𝐴𝐵
Definition	df-esum 34062	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 34063	An extended sum is a set by definition. (Contributed by Thierry Arnoux, 5-Sep-2017.)
⊢ Σ*𝑘 ∈ 𝐴𝐵 ∈ V
Theorem	esumcl 34064*	Closure for extended sum in the extended positive reals. (Contributed by Thierry Arnoux, 2-Jan-2017.)
⊢ Ⅎ𝑘𝐴    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑘 ∈ 𝐴 𝐵 ∈ (0[,]+∞)) → Σ*𝑘 ∈ 𝐴𝐵 ∈ (0[,]+∞))
Theorem	esumeq12dvaf 34065	Equality deduction for extended sum. (Contributed by Thierry Arnoux, 26-Mar-2017.)
⊢ Ⅎ𝑘𝜑    &   ⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → Σ*𝑘 ∈ 𝐴𝐶 = Σ*𝑘 ∈ 𝐵𝐷)
Theorem	esumeq12dva 34066*	Equality deduction for extended sum. (Contributed by Thierry Arnoux, 18-Feb-2017.) (Revised by Thierry Arnoux, 29-Jun-2017.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → Σ*𝑘 ∈ 𝐴𝐶 = Σ*𝑘 ∈ 𝐵𝐷)
Theorem	esumeq12d 34067*	Equality deduction for extended sum. (Contributed by Thierry Arnoux, 18-Feb-2017.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → Σ*𝑘 ∈ 𝐴𝐶 = Σ*𝑘 ∈ 𝐵𝐷)
Theorem	esumeq1 34068*	Equality theorem for an extended sum. (Contributed by Thierry Arnoux, 18-Feb-2017.)
⊢ (𝐴 = 𝐵 → Σ*𝑘 ∈ 𝐴𝐶 = Σ*𝑘 ∈ 𝐵𝐶)
Theorem	esumeq1d 34069	Equality theorem for an extended sum. (Contributed by Thierry Arnoux, 19-Oct-2017.)
⊢ Ⅎ𝑘𝜑    &   ⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → Σ*𝑘 ∈ 𝐴𝐶 = Σ*𝑘 ∈ 𝐵𝐶)
Theorem	esumeq2 34070*	Equality theorem for extended sum. (Contributed by Thierry Arnoux, 24-Dec-2016.)
⊢ (∀𝑘 ∈ 𝐴 𝐵 = 𝐶 → Σ*𝑘 ∈ 𝐴𝐵 = Σ*𝑘 ∈ 𝐴𝐶)
Theorem	esumeq2d 34071	Equality deduction for extended sum. (Contributed by Thierry Arnoux, 21-Sep-2016.)
⊢ Ⅎ𝑘𝜑    &   ⊢ (𝜑 → ∀𝑘 ∈ 𝐴 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → Σ*𝑘 ∈ 𝐴𝐵 = Σ*𝑘 ∈ 𝐴𝐶)
Theorem	esumeq2dv 34072*	Equality deduction for extended sum. (Contributed by Thierry Arnoux, 2-Jan-2017.)
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → Σ*𝑘 ∈ 𝐴𝐵 = Σ*𝑘 ∈ 𝐴𝐶)
Theorem	esumeq2sdv 34073*	Equality deduction for extended sum. (Contributed by Thierry Arnoux, 25-Dec-2016.)
⊢ (𝜑 → 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → Σ*𝑘 ∈ 𝐴𝐵 = Σ*𝑘 ∈ 𝐴𝐶)
Theorem	nfesum1 34074	Bound-variable hypothesis builder for extended sum. (Contributed by Thierry Arnoux, 19-Oct-2017.)
⊢ Ⅎ𝑘𝐴    ⇒   ⊢ Ⅎ𝑘Σ*𝑘 ∈ 𝐴𝐵
Theorem	nfesum2 34075*	Bound-variable hypothesis builder for extended sum. (Contributed by Thierry Arnoux, 2-May-2020.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ Ⅎ𝑥Σ*𝑘 ∈ 𝐴𝐵
Theorem	cbvesum 34076*	Change bound variable in an extended sum. (Contributed by Thierry Arnoux, 19-Jun-2017.)
⊢ (𝑗 = 𝑘 → 𝐵 = 𝐶)    &   ⊢ Ⅎ𝑘𝐴    &   ⊢ Ⅎ𝑗𝐴    &   ⊢ Ⅎ𝑘𝐵    &   ⊢ Ⅎ𝑗𝐶    ⇒   ⊢ Σ*𝑗 ∈ 𝐴𝐵 = Σ*𝑘 ∈ 𝐴𝐶
Theorem	cbvesumv 34077*	Change bound variable in an extended sum. (Contributed by Thierry Arnoux, 19-Jun-2017.)
⊢ (𝑗 = 𝑘 → 𝐵 = 𝐶)    ⇒   ⊢ Σ*𝑗 ∈ 𝐴𝐵 = Σ*𝑘 ∈ 𝐴𝐶
Theorem	esumid 34078	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 34079	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 34080*	Develop the value of the extended sum. (Contributed by Thierry Arnoux, 4-Jan-2017.)
⊢ Ⅎ𝑘𝜑    &   ⊢ Ⅎ𝑘𝐴    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ (0[,]+∞))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝐴 ∩ Fin)) → ((ℝ*𝑠 ↾s (0[,]+∞)) Σg (𝑘 ∈ 𝑥 ↦ 𝐵)) = 𝐶)    ⇒   ⊢ (𝜑 → Σ*𝑘 ∈ 𝐴𝐵 = sup(ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ 𝐶), ℝ*, < ))
Theorem	esumel 34081*	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 34082	Extended sum over the empty set. (Contributed by Thierry Arnoux, 19-Feb-2017.)
⊢ Σ*𝑥 ∈ ∅𝐴 = 0
Theorem	esum0 34083*	Extended sum of zero. (Contributed by Thierry Arnoux, 3-Mar-2017.)
⊢ Ⅎ𝑘𝐴    ⇒   ⊢ (𝐴 ∈ 𝑉 → Σ*𝑘 ∈ 𝐴0 = 0)
Theorem	esumf1o 34084*	Re-index an extended sum using a bijection. (Contributed by Thierry Arnoux, 6-Apr-2017.)
⊢ Ⅎ𝑛𝜑    &   ⊢ Ⅎ𝑛𝐵    &   ⊢ Ⅎ𝑘𝐷    &   ⊢ Ⅎ𝑛𝐴    &   ⊢ Ⅎ𝑛𝐶    &   ⊢ Ⅎ𝑛𝐹    &   ⊢ (𝑘 = 𝐺 → 𝐵 = 𝐷)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹:𝐶–1-1-onto→𝐴)    &   ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶) → (𝐹‘𝑛) = 𝐺)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ (0[,]+∞))    ⇒   ⊢ (𝜑 → Σ*𝑘 ∈ 𝐴𝐵 = Σ*𝑛 ∈ 𝐶𝐷)
Theorem	esumc 34085*	Convert from the collection form to the class-variable form of a sum. (Contributed by Thierry Arnoux, 10-May-2017.)
⊢ Ⅎ𝑘𝐷    &   ⊢ Ⅎ𝑘𝜑    &   ⊢ Ⅎ𝑘𝐴    &   ⊢ (𝑦 = 𝐶 → 𝐷 = 𝐵)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → Fun ◡(𝑘 ∈ 𝐴 ↦ 𝐶))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ (0[,]+∞))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐶 ∈ 𝑊)    ⇒   ⊢ (𝜑 → Σ*𝑘 ∈ 𝐴𝐵 = Σ*𝑦 ∈ {𝑧 ∣ ∃𝑘 ∈ 𝐴 𝑧 = 𝐶}𝐷)
Theorem	esumrnmpt 34086*	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 34087	Split an extended sum into two parts. (Contributed by Thierry Arnoux, 9-May-2017.)
⊢ Ⅎ𝑘𝜑    &   ⊢ Ⅎ𝑘𝐴    &   ⊢ Ⅎ𝑘𝐵    &   ⊢ (𝜑 → 𝐴 ∈ V)    &   ⊢ (𝜑 → 𝐵 ∈ V)    &   ⊢ (𝜑 → (𝐴 ∩ 𝐵) = ∅)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐶 ∈ (0[,]+∞))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵) → 𝐶 ∈ (0[,]+∞))    ⇒   ⊢ (𝜑 → Σ*𝑘 ∈ (𝐴 ∪ 𝐵)𝐶 = (Σ*𝑘 ∈ 𝐴𝐶 +𝑒 Σ*𝑘 ∈ 𝐵𝐶))
Theorem	esummono 34088*	Extended sum is monotonic. (Contributed by Thierry Arnoux, 19-Oct-2017.)
⊢ Ⅎ𝑘𝜑    &   ⊢ (𝜑 → 𝐶 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐶) → 𝐵 ∈ (0[,]+∞))    &   ⊢ (𝜑 → 𝐴 ⊆ 𝐶)    ⇒   ⊢ (𝜑 → Σ*𝑘 ∈ 𝐴𝐵 ≤ Σ*𝑘 ∈ 𝐶𝐵)
Theorem	esumpad 34089*	Extend an extended sum by padding outside with zeroes. (Contributed by Thierry Arnoux, 31-May-2020.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐶 ∈ (0[,]+∞))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵) → 𝐶 = 0)    ⇒   ⊢ (𝜑 → Σ*𝑘 ∈ (𝐴 ∪ 𝐵)𝐶 = Σ*𝑘 ∈ 𝐴𝐶)
Theorem	esumpad2 34090*	Remove zeroes from an extended sum. (Contributed by Thierry Arnoux, 5-Jun-2020.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐶 ∈ (0[,]+∞))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵) → 𝐶 = 0)    ⇒   ⊢ (𝜑 → Σ*𝑘 ∈ (𝐴 ∖ 𝐵)𝐶 = Σ*𝑘 ∈ 𝐴𝐶)
Theorem	esumadd 34091*	Addition of infinite sums. (Contributed by Thierry Arnoux, 24-Mar-2017.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ (0[,]+∞))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐶 ∈ (0[,]+∞))    ⇒   ⊢ (𝜑 → Σ*𝑘 ∈ 𝐴(𝐵 +𝑒 𝐶) = (Σ*𝑘 ∈ 𝐴𝐵 +𝑒 Σ*𝑘 ∈ 𝐴𝐶))
Theorem	esumle 34092*	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 34093*	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 34094*	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 34095*	Addition of infinite sums. (Contributed by Thierry Arnoux, 22-Jun-2017.)
⊢ Ⅎ𝑘𝜑    &   ⊢ Ⅎ𝑘𝐴    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ (0[,]+∞))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐶 ∈ (0[,]+∞))    ⇒   ⊢ (𝜑 → Σ*𝑘 ∈ 𝐴(𝐵 +𝑒 𝐶) = (Σ*𝑘 ∈ 𝐴𝐵 +𝑒 Σ*𝑘 ∈ 𝐴𝐶))
Theorem	esumlef 34096*	If all of the terms of an extended sums compare, so do the sums. (Contributed by Thierry Arnoux, 8-Jun-2017.)
⊢ Ⅎ𝑘𝜑    &   ⊢ Ⅎ𝑘𝐴    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ (0[,]+∞))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐶 ∈ (0[,]+∞))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ≤ 𝐶)    ⇒   ⊢ (𝜑 → Σ*𝑘 ∈ 𝐴𝐵 ≤ Σ*𝑘 ∈ 𝐴𝐶)
Theorem	esumcst 34097*	The extended sum of a constant. (Contributed by Thierry Arnoux, 3-Mar-2017.) (Revised by Thierry Arnoux, 5-Jul-2017.)
⊢ Ⅎ𝑘𝐴    &   ⊢ Ⅎ𝑘𝐵    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (0[,]+∞)) → Σ*𝑘 ∈ 𝐴𝐵 = ((♯‘𝐴) ·e 𝐵))
Theorem	esumsnf 34098*	The extended sum of a singleton is the term. (Contributed by Thierry Arnoux, 2-Jan-2017.) (Revised by Thierry Arnoux, 2-May-2020.)
⊢ Ⅎ𝑘𝐵    &   ⊢ ((𝜑 ∧ 𝑘 = 𝑀) → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝑀 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ (0[,]+∞))    ⇒   ⊢ (𝜑 → Σ*𝑘 ∈ {𝑀}𝐴 = 𝐵)
Theorem	esumsn 34099*	The extended sum of a singleton is the term. (Contributed by Thierry Arnoux, 2-Jan-2017.) (Shortened by Thierry Arnoux, 2-May-2020.)
⊢ ((𝜑 ∧ 𝑘 = 𝑀) → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝑀 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ (0[,]+∞))    ⇒   ⊢ (𝜑 → Σ*𝑘 ∈ {𝑀}𝐴 = 𝐵)
Theorem	esumpr 34100*	Extended sum over a pair. (Contributed by Thierry Arnoux, 2-Jan-2017.)
⊢ ((𝜑 ∧ 𝑘 = 𝐴) → 𝐶 = 𝐷)    &   ⊢ ((𝜑 ∧ 𝑘 = 𝐵) → 𝐶 = 𝐸)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐷 ∈ (0[,]+∞))    &   ⊢ (𝜑 → 𝐸 ∈ (0[,]+∞))    &   ⊢ (𝜑 → 𝐴 ≠ 𝐵)    ⇒   ⊢ (𝜑 → Σ*𝑘 ∈ {𝐴, 𝐵}𝐶 = (𝐷 +𝑒 𝐸))