Metamath Proof Explorer

Theorem sge0fsummpt

Description: The arbitrary sum of a finite set of nonnegative extended real numbers is equal to the sum of those numbers, when none of them is +oo (Contributed by Glauco Siliprandi, 17-Aug-2020)

		Ref	Expression
	Hypotheses	sge0fsummpt.a	$⊢ φ \to A \in Fin$
		sge0fsummpt.b	$⊢ (φ \land k \in A) \to B \in [0, +∞)$
	Assertion	sge0fsummpt	$⊢ φ \to sum^((k \in A ⟼ B)) = \sum_{k \in A} B$

Proof

Step	Hyp	Ref	Expression
1		sge0fsummpt.a	$⊢ φ \to A \in Fin$
2		sge0fsummpt.b	$⊢ (φ \land k \in A) \to B \in [0, +∞)$
3		eqid	$⊢ (k \in A ⟼ B) = (k \in A ⟼ B)$
4	2 3	fmptd	$⊢ φ \to (k \in A ⟼ B) : A ⟶ [0, +∞)$
5	1 4	sge0fsum	$⊢ φ \to sum^((k \in A ⟼ B)) = \sum_{j \in A} (k \in A ⟼ B) (j)$
6		fveq2	$⊢ j = k \to (k \in A ⟼ B) (j) = (k \in A ⟼ B) (k)$
7		nfcv	$⊢ \underline{Ⅎ} k A$
8		nfcv	$⊢ \underline{Ⅎ} j A$
9		nfmpt1	$⊢ \underline{Ⅎ} k (k \in A ⟼ B)$
10		nfcv	$⊢ \underline{Ⅎ} k j$
11	9 10	nffv	$⊢ \underline{Ⅎ} k (k \in A ⟼ B) (j)$
12		nfcv	$⊢ \underline{Ⅎ} j (k \in A ⟼ B) (k)$
13	6 7 8 11 12	cbvsum	$⊢ \sum_{j \in A} (k \in A ⟼ B) (j) = \sum_{k \in A} (k \in A ⟼ B) (k)$
14	13	a1i	$⊢ φ \to \sum_{j \in A} (k \in A ⟼ B) (j) = \sum_{k \in A} (k \in A ⟼ B) (k)$
15		simpr	$⊢ (φ \land k \in A) \to k \in A$
16	3	fvmpt2	$⊢ (k \in A \land B \in [0, +∞)) \to (k \in A ⟼ B) (k) = B$
17	15 2 16	syl2anc	$⊢ (φ \land k \in A) \to (k \in A ⟼ B) (k) = B$
18	17	sumeq2dv	$⊢ φ \to \sum_{k \in A} (k \in A ⟼ B) (k) = \sum_{k \in A} B$
19	5 14 18	3eqtrd	$⊢ φ \to sum^((k \in A ⟼ B)) = \sum_{k \in A} B$