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		nfmpt1	$⊢ \underline{Ⅎ} k (k \in A ⟼ B)$
8		nfcv	$⊢ \underline{Ⅎ} k j$
9	7 8	nffv	$⊢ \underline{Ⅎ} k (k \in A ⟼ B) (j)$
10		nfcv	$⊢ \underline{Ⅎ} j (k \in A ⟼ B) (k)$
11	6 9 10	cbvsum	$⊢ \sum_{j \in A} (k \in A ⟼ B) (j) = \sum_{k \in A} (k \in A ⟼ B) (k)$
12	11	a1i	$⊢ φ \to \sum_{j \in A} (k \in A ⟼ B) (j) = \sum_{k \in A} (k \in A ⟼ B) (k)$
13		simpr	$⊢ (φ \land k \in A) \to k \in A$
14	3	fvmpt2	$⊢ (k \in A \land B \in [0, +∞)) \to (k \in A ⟼ B) (k) = B$
15	13 2 14	syl2anc	$⊢ (φ \land k \in A) \to (k \in A ⟼ B) (k) = B$
16	15	sumeq2dv	$⊢ φ \to \sum_{k \in A} (k \in A ⟼ B) (k) = \sum_{k \in A} B$
17	5 12 16	3eqtrd	$⊢ φ \to sum^((k \in A ⟼ B)) = \sum_{k \in A} B$