sge0fsummptf

Description: The generalized 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, 21-Nov-2020)

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

Proof

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

Metamath Proof Explorer

Theorem sge0fsummptf

Proof