esumgsum

Description: A finite extended sum is the group sum over the extended nonnegative real numbers. (Contributed by Thierry Arnoux, 24-Apr-2020)

	Ref	Expression
Hypotheses	esumgsum.1	$⊢ Ⅎ k φ$
	esumgsum.2	$⊢ \underline{Ⅎ} k A$
	esumgsum.3	$⊢ φ \to A \in Fin$
	esumgsum.4	$⊢ (φ \land k \in A) \to B \in [0, +∞]$
Assertion	esumgsum	$⊢ φ \to \underset{k \in A}{\sum^{}} B = \underset{k \in A}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} B$

Step	Hyp	Ref	Expression
1		esumgsum.1	$⊢ Ⅎ k φ$
2		esumgsum.2	$⊢ \underline{Ⅎ} k A$
3		esumgsum.3	$⊢ φ \to A \in Fin$
4		esumgsum.4	$⊢ (φ \land k \in A) \to B \in [0, +∞]$
5		xrge0base	$⊢ [0, +∞] = {Base}_{(ℝ_{𝑠}^{*} ↾_{𝑠} [0, +∞])}$
6		xrge00	$⊢ 0 = 0_{(ℝ_{𝑠}^{*} ↾_{𝑠} [0, +∞])}$
7		xrge0cmn	$⊢ ℝ_{𝑠}^{*} ↾_{𝑠} [0, +∞] \in CMnd$
8	7	a1i	$⊢ φ \to ℝ_{𝑠}^{*} ↾_{𝑠} [0, +∞] \in CMnd$
9		xrge0tps	$⊢ ℝ_{𝑠}^{*} ↾_{𝑠} [0, +∞] \in TopSp$
10	9	a1i	$⊢ φ \to ℝ_{𝑠}^{*} ↾_{𝑠} [0, +∞] \in TopSp$
11		nfcv	$⊢ \underline{Ⅎ} k [0, +∞]$
12		eqid	$⊢ (k \in A ⟼ B) = (k \in A ⟼ B)$
13	1 2 11 4 12	fmptdF	$⊢ φ \to (k \in A ⟼ B) : A ⟶ [0, +∞]$
14	4	ex	$⊢ φ \to (k \in A \to B \in [0, +∞])$
15	1 14	ralrimi	$⊢ φ \to \forall k \in A B \in [0, +∞]$
16	2	fnmptf	$⊢ \forall k \in A B \in [0, +∞] \to (k \in A ⟼ B) Fn A$
17	15 16	syl	$⊢ φ \to (k \in A ⟼ B) Fn A$
18		0xr	$⊢ 0 \in ℝ^{*}$
19	18	a1i	$⊢ φ \to 0 \in ℝ^{*}$
20	17 3 19	fndmfifsupp	$⊢ φ \to {finSupp}_{0} ((k \in A ⟼ B))$
21	5 6 8 10 3 13 20	tsmsid	$⊢ φ \to \underset{k \in A}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} B \in ((ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]) tsums (k \in A ⟼ B))$
22	1 2 3 4 21	esumid	$⊢ φ \to \underset{k \in A}{\sum^{}} B = \underset{k \in A}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} B$

Metamath Proof Explorer