Metamath Proof Explorer

Theorem 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 ⊢ φ → A ∈ Fin
sge0fsummptf.b ⊢ φ ∧ k ∈ A → B ∈ 0 +∞
Assertion sge0fsummptf ⊢ φ → sum^ ⁡ k ∈ A ⟼ B = ∑ k ∈ A B

Proof

Step Hyp Ref Expression
1 sge0fsummptf.k ⊢ Ⅎ k φ
2 sge0fsummptf.a ⊢ φ → A ∈ Fin
3 sge0fsummptf.b ⊢ φ ∧ k ∈ A → B ∈ 0 +∞
4 eqid ⊢ k ∈ A ⟼ B = k ∈ A ⟼ B
5 1 3 4 fmptdf ⊢ φ → k ∈ A ⟼ B : A ⟶ 0 +∞
6 2 5 sge0fsum ⊢ φ → sum^ ⁡ k ∈ A ⟼ B = ∑ j ∈ A k ∈ A ⟼ B ⁡ j
7 fveq2 ⊢ j = k → k ∈ A ⟼ B ⁡ j = k ∈ A ⟼ B ⁡ k
8 nfmpt1 ⊢ Ⅎ _ k k ∈ A ⟼ B
9 nfcv ⊢ Ⅎ _ k j
10 8 9 nffv ⊢ Ⅎ _ k k ∈ A ⟼ B ⁡ j
11 nfcv ⊢ Ⅎ _ j k ∈ A ⟼ B ⁡ k
12 7 10 11 cbvsum ⊢ ∑ j ∈ A k ∈ A ⟼ B ⁡ j = ∑ k ∈ A k ∈ A ⟼ B ⁡ k
13 12 a1i ⊢ φ → ∑ j ∈ A k ∈ A ⟼ B ⁡ j = ∑ k ∈ A k ∈ A ⟼ B ⁡ k
14 simpr ⊢ φ ∧ k ∈ A → k ∈ A
15 4 fvmpt2 ⊢ k ∈ A ∧ B ∈ 0 +∞ → k ∈ A ⟼ B ⁡ k = B
16 14 3 15 syl2anc ⊢ φ ∧ k ∈ A → k ∈ A ⟼ B ⁡ k = B
17 16 ex ⊢ φ → k ∈ A → k ∈ A ⟼ B ⁡ k = B
18 1 17 ralrimi ⊢ φ → ∀ k ∈ A k ∈ A ⟼ B ⁡ k = B
19 18 sumeq2d ⊢ φ → ∑ k ∈ A k ∈ A ⟼ B ⁡ k = ∑ k ∈ A B
20 6 13 19 3eqtrd ⊢ φ → sum^ ⁡ k ∈ A ⟼ B = ∑ k ∈ A B