P. 331 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 33001-33100   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	ismntop 33001*	Property of being a manifold. (Contributed by Thierry Arnoux, 5-Jan-2020.)
⊢ ((𝑁 ∈ ℕ0 ∧ 𝐽 ∈ 𝑉) → (𝑁ManTop𝐽 ↔ (𝐽 ∈ 2ndω ∧ 𝐽 ∈ Haus ∧ ∀𝑥 ∈ 𝐽 ∀𝑦 ∈ 𝑥 ∃𝑢 ∈ (𝐽 ∩ 𝒫 𝑥)(𝑦 ∈ 𝑢 ∧ (𝐽 ↾t 𝑢) ≃ (TopOpen‘(𝔼hil‘𝑁))))))
21.3.15  Real and complex functions
21.3.15.1  Integer powers - misc. additions
Theorem	nexple 33002	A lower bound for an exponentiation. (Contributed by Thierry Arnoux, 19-Aug-2017.)
⊢ ((𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℝ ∧ 2 ≤ 𝐵) → 𝐴 ≤ (𝐵↑𝐴))
21.3.15.2  Indicator Functions
Syntax	cind 33003	Extend class notation with the indicator function generator.
class 𝟭
Definition	df-ind 33004*	Define the indicator function generator. (Contributed by Thierry Arnoux, 20-Jan-2017.)
⊢ 𝟭 = (𝑜 ∈ V ↦ (𝑎 ∈ 𝒫 𝑜 ↦ (𝑥 ∈ 𝑜 ↦ if(𝑥 ∈ 𝑎, 1, 0))))
Theorem	indv 33005*	Value of the indicator function generator with domain 𝑂. (Contributed by Thierry Arnoux, 23-Aug-2017.)
⊢ (𝑂 ∈ 𝑉 → (𝟭‘𝑂) = (𝑎 ∈ 𝒫 𝑂 ↦ (𝑥 ∈ 𝑂 ↦ if(𝑥 ∈ 𝑎, 1, 0))))
Theorem	indval 33006*	Value of the indicator function generator for a set 𝐴 and a domain 𝑂. (Contributed by Thierry Arnoux, 2-Feb-2017.)
⊢ ((𝑂 ∈ 𝑉 ∧ 𝐴 ⊆ 𝑂) → ((𝟭‘𝑂)‘𝐴) = (𝑥 ∈ 𝑂 ↦ if(𝑥 ∈ 𝐴, 1, 0)))
Theorem	indval2 33007	Alternate value of the indicator function generator. (Contributed by Thierry Arnoux, 2-Feb-2017.)
⊢ ((𝑂 ∈ 𝑉 ∧ 𝐴 ⊆ 𝑂) → ((𝟭‘𝑂)‘𝐴) = ((𝐴 × {1}) ∪ ((𝑂 ∖ 𝐴) × {0})))
Theorem	indf 33008	An indicator function as a function with domain and codomain. (Contributed by Thierry Arnoux, 13-Aug-2017.)
⊢ ((𝑂 ∈ 𝑉 ∧ 𝐴 ⊆ 𝑂) → ((𝟭‘𝑂)‘𝐴):𝑂⟶{0, 1})
Theorem	indfval 33009	Value of the indicator function. (Contributed by Thierry Arnoux, 13-Aug-2017.)
⊢ ((𝑂 ∈ 𝑉 ∧ 𝐴 ⊆ 𝑂 ∧ 𝑋 ∈ 𝑂) → (((𝟭‘𝑂)‘𝐴)‘𝑋) = if(𝑋 ∈ 𝐴, 1, 0))
Theorem	ind1 33010	Value of the indicator function where it is 1. (Contributed by Thierry Arnoux, 14-Aug-2017.)
⊢ ((𝑂 ∈ 𝑉 ∧ 𝐴 ⊆ 𝑂 ∧ 𝑋 ∈ 𝐴) → (((𝟭‘𝑂)‘𝐴)‘𝑋) = 1)
Theorem	ind0 33011	Value of the indicator function where it is 0. (Contributed by Thierry Arnoux, 14-Aug-2017.)
⊢ ((𝑂 ∈ 𝑉 ∧ 𝐴 ⊆ 𝑂 ∧ 𝑋 ∈ (𝑂 ∖ 𝐴)) → (((𝟭‘𝑂)‘𝐴)‘𝑋) = 0)
Theorem	ind1a 33012	Value of the indicator function where it is 1. (Contributed by Thierry Arnoux, 22-Aug-2017.)
⊢ ((𝑂 ∈ 𝑉 ∧ 𝐴 ⊆ 𝑂 ∧ 𝑋 ∈ 𝑂) → ((((𝟭‘𝑂)‘𝐴)‘𝑋) = 1 ↔ 𝑋 ∈ 𝐴))
Theorem	indpi1 33013	Preimage of the singleton {1} by the indicator function. See i1f1lem 25205. (Contributed by Thierry Arnoux, 21-Aug-2017.)
⊢ ((𝑂 ∈ 𝑉 ∧ 𝐴 ⊆ 𝑂) → (◡((𝟭‘𝑂)‘𝐴) “ {1}) = 𝐴)
Theorem	indsum 33014*	Finite sum of a product with the indicator function / Cartesian product with the indicator function. (Contributed by Thierry Arnoux, 14-Aug-2017.)
⊢ (𝜑 → 𝑂 ∈ Fin)    &   ⊢ (𝜑 → 𝐴 ⊆ 𝑂)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑂) → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → Σ𝑥 ∈ 𝑂 ((((𝟭‘𝑂)‘𝐴)‘𝑥) · 𝐵) = Σ𝑥 ∈ 𝐴 𝐵)
Theorem	indsumin 33015*	Finite sum of a product with the indicator function / Cartesian product with the indicator function. (Contributed by Thierry Arnoux, 11-Dec-2021.)
⊢ (𝜑 → 𝑂 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ (𝜑 → 𝐴 ⊆ 𝑂)    &   ⊢ (𝜑 → 𝐵 ⊆ 𝑂)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐶 ∈ ℂ)    ⇒   ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 ((((𝟭‘𝑂)‘𝐵)‘𝑘) · 𝐶) = Σ𝑘 ∈ (𝐴 ∩ 𝐵)𝐶)
Theorem	prodindf 33016*	The product of indicators is one if and only if all values are in the set. (Contributed by Thierry Arnoux, 11-Dec-2021.)
⊢ (𝜑 → 𝑂 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ (𝜑 → 𝐵 ⊆ 𝑂)    &   ⊢ (𝜑 → 𝐹:𝐴⟶𝑂)    ⇒   ⊢ (𝜑 → ∏𝑘 ∈ 𝐴 (((𝟭‘𝑂)‘𝐵)‘(𝐹‘𝑘)) = if(ran 𝐹 ⊆ 𝐵, 1, 0))
Theorem	indf1o 33017	The bijection between a power set and the set of indicator functions. (Contributed by Thierry Arnoux, 14-Aug-2017.)
⊢ (𝑂 ∈ 𝑉 → (𝟭‘𝑂):𝒫 𝑂–1-1-onto→({0, 1} ↑m 𝑂))
Theorem	indpreima 33018	A function with range {0, 1} as an indicator of the preimage of {1}. (Contributed by Thierry Arnoux, 23-Aug-2017.)
⊢ ((𝑂 ∈ 𝑉 ∧ 𝐹:𝑂⟶{0, 1}) → 𝐹 = ((𝟭‘𝑂)‘(◡𝐹 “ {1})))
Theorem	indf1ofs 33019*	The bijection between finite subsets and the indicator functions with finite support. (Contributed by Thierry Arnoux, 22-Aug-2017.)
⊢ (𝑂 ∈ 𝑉 → ((𝟭‘𝑂) ↾ Fin):(𝒫 𝑂 ∩ Fin)–1-1-onto→{𝑓 ∈ ({0, 1} ↑m 𝑂) ∣ (◡𝑓 “ {1}) ∈ Fin})
21.3.15.3  Extended sum
Syntax	cesum 33020	Extend class notation to include infinite summations.
class Σ*𝑘 ∈ 𝐴𝐵
Definition	df-esum 33021	Define a short-hand for the possibly infinite sum over the extended nonnegative reals. Σ* is relying on the properties of the tsums, developped by Mario Carneiro. (Contributed by Thierry Arnoux, 21-Sep-2016.)
⊢ Σ*𝑘 ∈ 𝐴𝐵 = ∪ ((ℝ*𝑠 ↾s (0[,]+∞)) tsums (𝑘 ∈ 𝐴 ↦ 𝐵))
Theorem	esumex 33022	An extended sum is a set by definition. (Contributed by Thierry Arnoux, 5-Sep-2017.)
⊢ Σ*𝑘 ∈ 𝐴𝐵 ∈ V
Theorem	esumcl 33023*	Closure for extended sum in the extended positive reals. (Contributed by Thierry Arnoux, 2-Jan-2017.)
⊢ Ⅎ𝑘𝐴    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑘 ∈ 𝐴 𝐵 ∈ (0[,]+∞)) → Σ*𝑘 ∈ 𝐴𝐵 ∈ (0[,]+∞))
Theorem	esumeq12dvaf 33024	Equality deduction for extended sum. (Contributed by Thierry Arnoux, 26-Mar-2017.)
⊢ Ⅎ𝑘𝜑    &   ⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → Σ*𝑘 ∈ 𝐴𝐶 = Σ*𝑘 ∈ 𝐵𝐷)
Theorem	esumeq12dva 33025*	Equality deduction for extended sum. (Contributed by Thierry Arnoux, 18-Feb-2017.) (Revised by Thierry Arnoux, 29-Jun-2017.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → Σ*𝑘 ∈ 𝐴𝐶 = Σ*𝑘 ∈ 𝐵𝐷)
Theorem	esumeq12d 33026*	Equality deduction for extended sum. (Contributed by Thierry Arnoux, 18-Feb-2017.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → Σ*𝑘 ∈ 𝐴𝐶 = Σ*𝑘 ∈ 𝐵𝐷)
Theorem	esumeq1 33027*	Equality theorem for an extended sum. (Contributed by Thierry Arnoux, 18-Feb-2017.)
⊢ (𝐴 = 𝐵 → Σ*𝑘 ∈ 𝐴𝐶 = Σ*𝑘 ∈ 𝐵𝐶)
Theorem	esumeq1d 33028	Equality theorem for an extended sum. (Contributed by Thierry Arnoux, 19-Oct-2017.)
⊢ Ⅎ𝑘𝜑    &   ⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → Σ*𝑘 ∈ 𝐴𝐶 = Σ*𝑘 ∈ 𝐵𝐶)
Theorem	esumeq2 33029*	Equality theorem for extended sum. (Contributed by Thierry Arnoux, 24-Dec-2016.)
⊢ (∀𝑘 ∈ 𝐴 𝐵 = 𝐶 → Σ*𝑘 ∈ 𝐴𝐵 = Σ*𝑘 ∈ 𝐴𝐶)
Theorem	esumeq2d 33030	Equality deduction for extended sum. (Contributed by Thierry Arnoux, 21-Sep-2016.)
⊢ Ⅎ𝑘𝜑    &   ⊢ (𝜑 → ∀𝑘 ∈ 𝐴 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → Σ*𝑘 ∈ 𝐴𝐵 = Σ*𝑘 ∈ 𝐴𝐶)
Theorem	esumeq2dv 33031*	Equality deduction for extended sum. (Contributed by Thierry Arnoux, 2-Jan-2017.)
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → Σ*𝑘 ∈ 𝐴𝐵 = Σ*𝑘 ∈ 𝐴𝐶)
Theorem	esumeq2sdv 33032*	Equality deduction for extended sum. (Contributed by Thierry Arnoux, 25-Dec-2016.)
⊢ (𝜑 → 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → Σ*𝑘 ∈ 𝐴𝐵 = Σ*𝑘 ∈ 𝐴𝐶)
Theorem	nfesum1 33033	Bound-variable hypothesis builder for extended sum. (Contributed by Thierry Arnoux, 19-Oct-2017.)
⊢ Ⅎ𝑘𝐴    ⇒   ⊢ Ⅎ𝑘Σ*𝑘 ∈ 𝐴𝐵
Theorem	nfesum2 33034*	Bound-variable hypothesis builder for extended sum. (Contributed by Thierry Arnoux, 2-May-2020.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ Ⅎ𝑥Σ*𝑘 ∈ 𝐴𝐵
Theorem	cbvesum 33035*	Change bound variable in an extended sum. (Contributed by Thierry Arnoux, 19-Jun-2017.)
⊢ (𝑗 = 𝑘 → 𝐵 = 𝐶)    &   ⊢ Ⅎ𝑘𝐴    &   ⊢ Ⅎ𝑗𝐴    &   ⊢ Ⅎ𝑘𝐵    &   ⊢ Ⅎ𝑗𝐶    ⇒   ⊢ Σ*𝑗 ∈ 𝐴𝐵 = Σ*𝑘 ∈ 𝐴𝐶
Theorem	cbvesumv 33036*	Change bound variable in an extended sum. (Contributed by Thierry Arnoux, 19-Jun-2017.)
⊢ (𝑗 = 𝑘 → 𝐵 = 𝐶)    ⇒   ⊢ Σ*𝑗 ∈ 𝐴𝐵 = Σ*𝑘 ∈ 𝐴𝐶
Theorem	esumid 33037	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 33038	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 33039*	Develop the value of the extended sum. (Contributed by Thierry Arnoux, 4-Jan-2017.)
⊢ Ⅎ𝑘𝜑    &   ⊢ Ⅎ𝑘𝐴    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ (0[,]+∞))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝐴 ∩ Fin)) → ((ℝ*𝑠 ↾s (0[,]+∞)) Σg (𝑘 ∈ 𝑥 ↦ 𝐵)) = 𝐶)    ⇒   ⊢ (𝜑 → Σ*𝑘 ∈ 𝐴𝐵 = sup(ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ 𝐶), ℝ*, < ))
Theorem	esumel 33040*	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 33041	Extended sum over the empty set. (Contributed by Thierry Arnoux, 19-Feb-2017.)
⊢ Σ*𝑥 ∈ ∅𝐴 = 0
Theorem	esum0 33042*	Extended sum of zero. (Contributed by Thierry Arnoux, 3-Mar-2017.)
⊢ Ⅎ𝑘𝐴    ⇒   ⊢ (𝐴 ∈ 𝑉 → Σ*𝑘 ∈ 𝐴0 = 0)
Theorem	esumf1o 33043*	Re-index an extended sum using a bijection. (Contributed by Thierry Arnoux, 6-Apr-2017.)
⊢ Ⅎ𝑛𝜑    &   ⊢ Ⅎ𝑛𝐵    &   ⊢ Ⅎ𝑘𝐷    &   ⊢ Ⅎ𝑛𝐴    &   ⊢ Ⅎ𝑛𝐶    &   ⊢ Ⅎ𝑛𝐹    &   ⊢ (𝑘 = 𝐺 → 𝐵 = 𝐷)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹:𝐶–1-1-onto→𝐴)    &   ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶) → (𝐹‘𝑛) = 𝐺)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ (0[,]+∞))    ⇒   ⊢ (𝜑 → Σ*𝑘 ∈ 𝐴𝐵 = Σ*𝑛 ∈ 𝐶𝐷)
Theorem	esumc 33044*	Convert from the collection form to the class-variable form of a sum. (Contributed by Thierry Arnoux, 10-May-2017.)
⊢ Ⅎ𝑘𝐷    &   ⊢ Ⅎ𝑘𝜑    &   ⊢ Ⅎ𝑘𝐴    &   ⊢ (𝑦 = 𝐶 → 𝐷 = 𝐵)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → Fun ◡(𝑘 ∈ 𝐴 ↦ 𝐶))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ (0[,]+∞))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐶 ∈ 𝑊)    ⇒   ⊢ (𝜑 → Σ*𝑘 ∈ 𝐴𝐵 = Σ*𝑦 ∈ {𝑧 ∣ ∃𝑘 ∈ 𝐴 𝑧 = 𝐶}𝐷)
Theorem	esumrnmpt 33045*	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 33046	Split an extended sum into two parts. (Contributed by Thierry Arnoux, 9-May-2017.)
⊢ Ⅎ𝑘𝜑    &   ⊢ Ⅎ𝑘𝐴    &   ⊢ Ⅎ𝑘𝐵    &   ⊢ (𝜑 → 𝐴 ∈ V)    &   ⊢ (𝜑 → 𝐵 ∈ V)    &   ⊢ (𝜑 → (𝐴 ∩ 𝐵) = ∅)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐶 ∈ (0[,]+∞))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵) → 𝐶 ∈ (0[,]+∞))    ⇒   ⊢ (𝜑 → Σ*𝑘 ∈ (𝐴 ∪ 𝐵)𝐶 = (Σ*𝑘 ∈ 𝐴𝐶 +𝑒 Σ*𝑘 ∈ 𝐵𝐶))
Theorem	esummono 33047*	Extended sum is monotonic. (Contributed by Thierry Arnoux, 19-Oct-2017.)
⊢ Ⅎ𝑘𝜑    &   ⊢ (𝜑 → 𝐶 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐶) → 𝐵 ∈ (0[,]+∞))    &   ⊢ (𝜑 → 𝐴 ⊆ 𝐶)    ⇒   ⊢ (𝜑 → Σ*𝑘 ∈ 𝐴𝐵 ≤ Σ*𝑘 ∈ 𝐶𝐵)
Theorem	esumpad 33048*	Extend an extended sum by padding outside with zeroes. (Contributed by Thierry Arnoux, 31-May-2020.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐶 ∈ (0[,]+∞))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵) → 𝐶 = 0)    ⇒   ⊢ (𝜑 → Σ*𝑘 ∈ (𝐴 ∪ 𝐵)𝐶 = Σ*𝑘 ∈ 𝐴𝐶)
Theorem	esumpad2 33049*	Remove zeroes from an extended sum. (Contributed by Thierry Arnoux, 5-Jun-2020.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐶 ∈ (0[,]+∞))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵) → 𝐶 = 0)    ⇒   ⊢ (𝜑 → Σ*𝑘 ∈ (𝐴 ∖ 𝐵)𝐶 = Σ*𝑘 ∈ 𝐴𝐶)
Theorem	esumadd 33050*	Addition of infinite sums. (Contributed by Thierry Arnoux, 24-Mar-2017.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ (0[,]+∞))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐶 ∈ (0[,]+∞))    ⇒   ⊢ (𝜑 → Σ*𝑘 ∈ 𝐴(𝐵 +𝑒 𝐶) = (Σ*𝑘 ∈ 𝐴𝐵 +𝑒 Σ*𝑘 ∈ 𝐴𝐶))
Theorem	esumle 33051*	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 33052*	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 33053*	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 33054*	Addition of infinite sums. (Contributed by Thierry Arnoux, 22-Jun-2017.)
⊢ Ⅎ𝑘𝜑    &   ⊢ Ⅎ𝑘𝐴    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ (0[,]+∞))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐶 ∈ (0[,]+∞))    ⇒   ⊢ (𝜑 → Σ*𝑘 ∈ 𝐴(𝐵 +𝑒 𝐶) = (Σ*𝑘 ∈ 𝐴𝐵 +𝑒 Σ*𝑘 ∈ 𝐴𝐶))
Theorem	esumlef 33055*	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 33056*	The extended sum of a constant. (Contributed by Thierry Arnoux, 3-Mar-2017.) (Revised by Thierry Arnoux, 5-Jul-2017.)
⊢ Ⅎ𝑘𝐴    &   ⊢ Ⅎ𝑘𝐵    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (0[,]+∞)) → Σ*𝑘 ∈ 𝐴𝐵 = ((♯‘𝐴) ·e 𝐵))
Theorem	esumsnf 33057*	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 33058*	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 33059*	Extended sum over a pair. (Contributed by Thierry Arnoux, 2-Jan-2017.)
⊢ ((𝜑 ∧ 𝑘 = 𝐴) → 𝐶 = 𝐷)    &   ⊢ ((𝜑 ∧ 𝑘 = 𝐵) → 𝐶 = 𝐸)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐷 ∈ (0[,]+∞))    &   ⊢ (𝜑 → 𝐸 ∈ (0[,]+∞))    &   ⊢ (𝜑 → 𝐴 ≠ 𝐵)    ⇒   ⊢ (𝜑 → Σ*𝑘 ∈ {𝐴, 𝐵}𝐶 = (𝐷 +𝑒 𝐸))
Theorem	esumpr2 33060*	Extended sum over a pair, with a relaxed condition compared to esumpr 33059. (Contributed by Thierry Arnoux, 2-Jan-2017.)
⊢ ((𝜑 ∧ 𝑘 = 𝐴) → 𝐶 = 𝐷)    &   ⊢ ((𝜑 ∧ 𝑘 = 𝐵) → 𝐶 = 𝐸)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐷 ∈ (0[,]+∞))    &   ⊢ (𝜑 → 𝐸 ∈ (0[,]+∞))    &   ⊢ (𝜑 → (𝐴 = 𝐵 → (𝐷 = 0 ∨ 𝐷 = +∞)))    ⇒   ⊢ (𝜑 → Σ*𝑘 ∈ {𝐴, 𝐵}𝐶 = (𝐷 +𝑒 𝐸))
Theorem	esumrnmpt2 33061*	Rewrite an extended sum into a sum on the range of a mapping function. (Contributed by Thierry Arnoux, 30-May-2020.)
⊢ (𝑦 = 𝐵 → 𝐶 = 𝐷)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐷 ∈ (0[,]+∞))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ 𝑊)    &   ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ 𝐵 = ∅) → 𝐷 = 0)    &   ⊢ (𝜑 → Disj 𝑘 ∈ 𝐴 𝐵)    ⇒   ⊢ (𝜑 → Σ*𝑦 ∈ ran (𝑘 ∈ 𝐴 ↦ 𝐵)𝐶 = Σ*𝑘 ∈ 𝐴𝐷)
Theorem	esumfzf 33062*	Formulating a partial extended sum over integers using the recursive sequence builder. (Contributed by Thierry Arnoux, 18-Oct-2017.)
⊢ Ⅎ𝑘𝐹    ⇒   ⊢ ((𝐹:ℕ⟶(0[,]+∞) ∧ 𝑁 ∈ ℕ) → Σ*𝑘 ∈ (1...𝑁)(𝐹‘𝑘) = (seq1( +𝑒 , 𝐹)‘𝑁))
Theorem	esumfsup 33063	Formulating an extended sum over integers using the recursive sequence builder. (Contributed by Thierry Arnoux, 18-Oct-2017.)
⊢ Ⅎ𝑘𝐹    ⇒   ⊢ (𝐹:ℕ⟶(0[,]+∞) → Σ*𝑘 ∈ ℕ(𝐹‘𝑘) = sup(ran seq1( +𝑒 , 𝐹), ℝ*, < ))
Theorem	esumfsupre 33064	Formulating an extended sum over integers using the recursive sequence builder. This version is limited to real-valued functions. (Contributed by Thierry Arnoux, 19-Oct-2017.)
⊢ Ⅎ𝑘𝐹    ⇒   ⊢ (𝐹:ℕ⟶(0[,)+∞) → Σ*𝑘 ∈ ℕ(𝐹‘𝑘) = sup(ran seq1( + , 𝐹), ℝ*, < ))
Theorem	esumss 33065	Change the index set to a subset by adding zeroes. (Contributed by Thierry Arnoux, 19-Jun-2017.)
⊢ Ⅎ𝑘𝜑    &   ⊢ Ⅎ𝑘𝐴    &   ⊢ Ⅎ𝑘𝐵    &   ⊢ (𝜑 → 𝐴 ⊆ 𝐵)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵) → 𝐶 ∈ (0[,]+∞))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ (𝐵 ∖ 𝐴)) → 𝐶 = 0)    ⇒   ⊢ (𝜑 → Σ*𝑘 ∈ 𝐴𝐶 = Σ*𝑘 ∈ 𝐵𝐶)
Theorem	esumpinfval 33066*	The value of the extended sum of nonnegative terms, with at least one infinite term. (Contributed by Thierry Arnoux, 19-Jun-2017.)
⊢ Ⅎ𝑘𝜑    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ (0[,]+∞))    &   ⊢ (𝜑 → ∃𝑘 ∈ 𝐴 𝐵 = +∞)    ⇒   ⊢ (𝜑 → Σ*𝑘 ∈ 𝐴𝐵 = +∞)
Theorem	esumpfinvallem 33067	Lemma for esumpfinval 33068. (Contributed by Thierry Arnoux, 28-Jun-2017.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶(0[,)+∞)) → (ℂfld Σg 𝐹) = ((ℝ*𝑠 ↾s (0[,]+∞)) Σg 𝐹))
Theorem	esumpfinval 33068*	The value of the extended sum of a finite set of nonnegative finite terms. (Contributed by Thierry Arnoux, 28-Jun-2017.) (Proof shortened by AV, 25-Jul-2019.)
⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ (0[,)+∞))    ⇒   ⊢ (𝜑 → Σ*𝑘 ∈ 𝐴𝐵 = Σ𝑘 ∈ 𝐴 𝐵)
Theorem	esumpfinvalf 33069	Same as esumpfinval 33068, minus distinct variable restrictions. (Contributed by Thierry Arnoux, 28-Aug-2017.) (Proof shortened by AV, 25-Jul-2019.)
⊢ Ⅎ𝑘𝐴    &   ⊢ Ⅎ𝑘𝜑    &   ⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ (0[,)+∞))    ⇒   ⊢ (𝜑 → Σ*𝑘 ∈ 𝐴𝐵 = Σ𝑘 ∈ 𝐴 𝐵)
Theorem	esumpinfsum 33070*	The value of the extended sum of infinitely many terms greater than one. (Contributed by Thierry Arnoux, 29-Jun-2017.)
⊢ Ⅎ𝑘𝜑    &   ⊢ Ⅎ𝑘𝐴    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → ¬ 𝐴 ∈ Fin)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ (0[,]+∞))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝑀 ≤ 𝐵)    &   ⊢ (𝜑 → 𝑀 ∈ ℝ*)    &   ⊢ (𝜑 → 0 < 𝑀)    ⇒   ⊢ (𝜑 → Σ*𝑘 ∈ 𝐴𝐵 = +∞)
Theorem	esumpcvgval 33071*	The value of the extended sum when the corresponding series sum is convergent. (Contributed by Thierry Arnoux, 31-Jul-2017.)
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝐴 ∈ (0[,)+∞))    &   ⊢ (𝑘 = 𝑙 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → (𝑛 ∈ ℕ ↦ Σ𝑘 ∈ (1...𝑛)𝐴) ∈ dom ⇝ )    ⇒   ⊢ (𝜑 → Σ*𝑘 ∈ ℕ𝐴 = Σ𝑘 ∈ ℕ 𝐴)
Theorem	esumpmono 33072*	The partial sums in an extended sum form a monotonic sequence. (Contributed by Thierry Arnoux, 31-Aug-2017.)
⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝐴 ∈ (0[,)+∞))    ⇒   ⊢ (𝜑 → Σ*𝑘 ∈ (1...𝑀)𝐴 ≤ Σ*𝑘 ∈ (1...𝑁)𝐴)
Theorem	esumcocn 33073*	Lemma for esummulc2 33075 and co. Composing with a continuous function preserves extended sums. (Contributed by Thierry Arnoux, 29-Jun-2017.)
⊢ 𝐽 = ((ordTop‘ ≤ ) ↾t (0[,]+∞))    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ (0[,]+∞))    &   ⊢ (𝜑 → 𝐶 ∈ (𝐽 Cn 𝐽))    &   ⊢ (𝜑 → (𝐶‘0) = 0)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ (0[,]+∞) ∧ 𝑦 ∈ (0[,]+∞)) → (𝐶‘(𝑥 +𝑒 𝑦)) = ((𝐶‘𝑥) +𝑒 (𝐶‘𝑦)))    ⇒   ⊢ (𝜑 → (𝐶‘Σ*𝑘 ∈ 𝐴𝐵) = Σ*𝑘 ∈ 𝐴(𝐶‘𝐵))
Theorem	esummulc1 33074*	An extended sum multiplied by a constant. (Contributed by Thierry Arnoux, 6-Jul-2017.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ (0[,]+∞))    &   ⊢ (𝜑 → 𝐶 ∈ (0[,)+∞))    ⇒   ⊢ (𝜑 → (Σ*𝑘 ∈ 𝐴𝐵 ·e 𝐶) = Σ*𝑘 ∈ 𝐴(𝐵 ·e 𝐶))
Theorem	esummulc2 33075*	An extended sum multiplied by a constant. (Contributed by Thierry Arnoux, 6-Jul-2017.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ (0[,]+∞))    &   ⊢ (𝜑 → 𝐶 ∈ (0[,)+∞))    ⇒   ⊢ (𝜑 → (𝐶 ·e Σ*𝑘 ∈ 𝐴𝐵) = Σ*𝑘 ∈ 𝐴(𝐶 ·e 𝐵))
Theorem	esumdivc 33076*	An extended sum divided by a constant. (Contributed by Thierry Arnoux, 6-Jul-2017.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ (0[,]+∞))    &   ⊢ (𝜑 → 𝐶 ∈ ℝ+)    ⇒   ⊢ (𝜑 → (Σ*𝑘 ∈ 𝐴𝐵 /𝑒 𝐶) = Σ*𝑘 ∈ 𝐴(𝐵 /𝑒 𝐶))
Theorem	hashf2 33077	Lemma for hasheuni 33078. (Contributed by Thierry Arnoux, 19-Nov-2016.)
⊢ ♯:V⟶(0[,]+∞)
Theorem	hasheuni 33078*	The cardinality of a disjoint union, not necessarily finite. cf. hashuni 15771. (Contributed by Thierry Arnoux, 19-Nov-2016.) (Revised by Thierry Arnoux, 2-Jan-2017.) (Revised by Thierry Arnoux, 20-Jun-2017.)
⊢ ((𝐴 ∈ 𝑉 ∧ Disj 𝑥 ∈ 𝐴 𝑥) → (♯‘∪ 𝐴) = Σ*𝑥 ∈ 𝐴(♯‘𝑥))
Theorem	esumcvg 33079*	The sequence of partial sums of an extended sum converges to the whole sum. cf. fsumcvg2 15672. (Contributed by Thierry Arnoux, 5-Sep-2017.)
⊢ 𝐽 = (TopOpen‘(ℝ*𝑠 ↾s (0[,]+∞)))    &   ⊢ 𝐹 = (𝑛 ∈ ℕ ↦ Σ*𝑘 ∈ (1...𝑛)𝐴)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝐴 ∈ (0[,]+∞))    &   ⊢ (𝑘 = 𝑚 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → 𝐹(⇝𝑡‘𝐽)Σ*𝑘 ∈ ℕ𝐴)
Theorem	esumcvg2 33080*	Simpler version of esumcvg 33079. (Contributed by Thierry Arnoux, 5-Sep-2017.)
⊢ 𝐽 = (TopOpen‘(ℝ*𝑠 ↾s (0[,]+∞)))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝐴 ∈ (0[,]+∞))    &   ⊢ (𝑘 = 𝑙 → 𝐴 = 𝐵)    &   ⊢ (𝑘 = 𝑚 → 𝐴 = 𝐶)    ⇒   ⊢ (𝜑 → (𝑛 ∈ ℕ ↦ Σ*𝑘 ∈ (1...𝑛)𝐴)(⇝𝑡‘𝐽)Σ*𝑘 ∈ ℕ𝐴)
Theorem	esumcvgsum 33081*	The value of the extended sum when the corresponding sum is convergent. (Contributed by Thierry Arnoux, 29-Oct-2019.)
⊢ (𝑘 = 𝑖 → 𝐴 = 𝐵)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝐴 ∈ (0[,)+∞))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐹‘𝑘) = 𝐴)    &   ⊢ (𝜑 → seq1( + , 𝐹) ⇝ 𝐿)    &   ⊢ (𝜑 → 𝐿 ∈ ℝ)    ⇒   ⊢ (𝜑 → Σ*𝑘 ∈ ℕ𝐴 = Σ𝑘 ∈ ℕ 𝐴)
Theorem	esumsup 33082*	Express an extended sum as a supremum of extended sums. (Contributed by Thierry Arnoux, 24-May-2020.)
⊢ (𝜑 → 𝐵 ∈ (0[,]+∞))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝐴 ∈ (0[,]+∞))    ⇒   ⊢ (𝜑 → Σ*𝑘 ∈ ℕ𝐴 = sup(ran (𝑛 ∈ ℕ ↦ Σ*𝑘 ∈ (1...𝑛)𝐴), ℝ*, < ))
Theorem	esumgect 33083*	"Send 𝑛 to +∞ " in an inequality with an extended sum. (Contributed by Thierry Arnoux, 24-May-2020.)
⊢ (𝜑 → 𝐵 ∈ (0[,]+∞))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝐴 ∈ (0[,]+∞))    &   ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → Σ*𝑘 ∈ (1...𝑛)𝐴 ≤ 𝐵)    ⇒   ⊢ (𝜑 → Σ*𝑘 ∈ ℕ𝐴 ≤ 𝐵)
Theorem	esumcvgre 33084*	All terms of a converging extended sum shall be finite. (Contributed by Thierry Arnoux, 23-Sep-2019.)
⊢ Ⅎ𝑘𝜑    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ (0[,]+∞))    &   ⊢ (𝜑 → Σ*𝑘 ∈ 𝐴𝐵 ∈ ℝ)    ⇒   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℝ)
Theorem	esum2dlem 33085*	Lemma for esum2d 33086 (finite case). (Contributed by Thierry Arnoux, 17-May-2020.) (Proof shortened by AV, 17-Sep-2021.)
⊢ Ⅎ𝑘𝐹    &   ⊢ (𝑧 = ⟨𝑗, 𝑘⟩ → 𝐹 = 𝐶)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → 𝐵 ∈ 𝑊)    &   ⊢ ((𝜑 ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵)) → 𝐶 ∈ (0[,]+∞))    &   ⊢ (𝜑 → 𝐴 ∈ Fin)    ⇒   ⊢ (𝜑 → Σ*𝑗 ∈ 𝐴Σ*𝑘 ∈ 𝐵𝐶 = Σ*𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵)𝐹)
Theorem	esum2d 33086*	Write a double extended sum as a sum over a two-dimensional region. Note that 𝐵(𝑗) is a function of 𝑗. This can be seen as "slicing" the relation 𝐴. (Contributed by Thierry Arnoux, 17-May-2020.)
⊢ Ⅎ𝑘𝐹    &   ⊢ (𝑧 = ⟨𝑗, 𝑘⟩ → 𝐹 = 𝐶)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → 𝐵 ∈ 𝑊)    &   ⊢ ((𝜑 ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵)) → 𝐶 ∈ (0[,]+∞))    ⇒   ⊢ (𝜑 → Σ*𝑗 ∈ 𝐴Σ*𝑘 ∈ 𝐵𝐶 = Σ*𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵)𝐹)
Theorem	esumiun 33087*	Sum over a nonnecessarily disjoint indexed union. The inequality is strict in the case where the sets B(x) overlap. (Contributed by Thierry Arnoux, 21-Sep-2019.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → 𝐵 ∈ 𝑊)    &   ⊢ (((𝜑 ∧ 𝑗 ∈ 𝐴) ∧ 𝑘 ∈ 𝐵) → 𝐶 ∈ (0[,]+∞))    ⇒   ⊢ (𝜑 → Σ*𝑘 ∈ ∪ 𝑗 ∈ 𝐴 𝐵𝐶 ≤ Σ*𝑗 ∈ 𝐴Σ*𝑘 ∈ 𝐵𝐶)
21.3.16  Mixed Function/Constant operation
Syntax	cofc 33088	Extend class notation to include mapping of an operation to an operation for a function and a constant.
class ∘f/c 𝑅
Definition	df-ofc 33089*	Define the function/constant operation map. The definition is designed so that if 𝑅 is a binary operation, then ∘f/c 𝑅 is the analogous operation on functions and constants. (Contributed by Thierry Arnoux, 21-Jan-2017.)
⊢ ∘f/c 𝑅 = (𝑓 ∈ V, 𝑐 ∈ V ↦ (𝑥 ∈ dom 𝑓 ↦ ((𝑓‘𝑥)𝑅𝑐)))
Theorem	ofceq 33090	Equality theorem for function/constant operation. (Contributed by Thierry Arnoux, 30-Jan-2017.)
⊢ (𝑅 = 𝑆 → ∘f/c 𝑅 = ∘f/c 𝑆)
Theorem	ofcfval 33091*	Value of an operation applied to a function and a constant. (Contributed by Thierry Arnoux, 30-Jan-2017.)
⊢ (𝜑 → 𝐹 Fn 𝐴)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑊)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) = 𝐵)    ⇒   ⊢ (𝜑 → (𝐹 ∘f/c 𝑅𝐶) = (𝑥 ∈ 𝐴 ↦ (𝐵𝑅𝐶)))
Theorem	ofcval 33092	Evaluate a function/constant operation at a point. (Contributed by Thierry Arnoux, 31-Jan-2017.)
⊢ (𝜑 → 𝐹 Fn 𝐴)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑊)    &   ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐴) → (𝐹‘𝑋) = 𝐵)    ⇒   ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐴) → ((𝐹 ∘f/c 𝑅𝐶)‘𝑋) = (𝐵𝑅𝐶))
Theorem	ofcfn 33093	The function operation produces a function. (Contributed by Thierry Arnoux, 31-Jan-2017.)
⊢ (𝜑 → 𝐹 Fn 𝐴)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑊)    ⇒   ⊢ (𝜑 → (𝐹 ∘f/c 𝑅𝐶) Fn 𝐴)
Theorem	ofcfeqd2 33094*	Equality theorem for function/constant operation value. (Contributed by Thierry Arnoux, 31-Jan-2017.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) ∈ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → (𝑦𝑅𝐶) = (𝑦𝑃𝐶))    &   ⊢ (𝜑 → 𝐹 Fn 𝐴)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑊)    ⇒   ⊢ (𝜑 → (𝐹 ∘f/c 𝑅𝐶) = (𝐹 ∘f/c 𝑃𝐶))
Theorem	ofcfval3 33095*	General value of (𝐹 ∘f/c 𝑅𝐶) with no assumptions on functionality of 𝐹. (Contributed by Thierry Arnoux, 31-Jan-2017.)
⊢ ((𝐹 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊) → (𝐹 ∘f/c 𝑅𝐶) = (𝑥 ∈ dom 𝐹 ↦ ((𝐹‘𝑥)𝑅𝐶)))
Theorem	ofcf 33096*	The function/constant operation produces a function. (Contributed by Thierry Arnoux, 30-Jan-2017.)
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑇)) → (𝑥𝑅𝑦) ∈ 𝑈)    &   ⊢ (𝜑 → 𝐹:𝐴⟶𝑆)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑇)    ⇒   ⊢ (𝜑 → (𝐹 ∘f/c 𝑅𝐶):𝐴⟶𝑈)
Theorem	ofcfval2 33097*	The function operation expressed as a mapping. (Contributed by Thierry Arnoux, 31-Jan-2017.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑊)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵))    ⇒   ⊢ (𝜑 → (𝐹 ∘f/c 𝑅𝐶) = (𝑥 ∈ 𝐴 ↦ (𝐵𝑅𝐶)))
Theorem	ofcfval4 33098*	The function/constant operation expressed as an operation composition. (Contributed by Thierry Arnoux, 31-Jan-2017.)
⊢ (𝜑 → 𝐹:𝐴⟶𝐵)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑊)    ⇒   ⊢ (𝜑 → (𝐹 ∘f/c 𝑅𝐶) = ((𝑥 ∈ 𝐵 ↦ (𝑥𝑅𝐶)) ∘ 𝐹))
Theorem	ofcc 33099	Left operation by a constant on a mixed operation with a constant. (Contributed by Thierry Arnoux, 31-Jan-2017.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑋)    ⇒   ⊢ (𝜑 → ((𝐴 × {𝐵}) ∘f/c 𝑅𝐶) = (𝐴 × {(𝐵𝑅𝐶)}))
Theorem	ofcof 33100	Relate function operation with operation with a constant. (Contributed by Thierry Arnoux, 3-Oct-2018.)
⊢ (𝜑 → 𝐹:𝐴⟶𝐵)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑊)    ⇒   ⊢ (𝜑 → (𝐹 ∘f/c 𝑅𝐶) = (𝐹 ∘f 𝑅(𝐴 × {𝐶})))