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 nfcv ⊢ Ⅎ _ k A
9 nfcv ⊢ Ⅎ _ j A
10 nfmpt1 ⊢ Ⅎ _ k k ∈ A ⟼ B
11 nfcv ⊢ Ⅎ _ k j
12 10 11 nffv ⊢ Ⅎ _ k k ∈ A ⟼ B ⁡ j
13 nfcv ⊢ Ⅎ _ j k ∈ A ⟼ B ⁡ k
14 7 8 9 12 13 cbvsum ⊢ ∑ j ∈ A k ∈ A ⟼ B ⁡ j = ∑ k ∈ A k ∈ A ⟼ B ⁡ k
15 14 a1i ⊢ φ → ∑ j ∈ A k ∈ A ⟼ B ⁡ j = ∑ k ∈ A k ∈ A ⟼ B ⁡ k
16 simpr ⊢ φ ∧ k ∈ A → k ∈ A
17 4 fvmpt2 ⊢ k ∈ A ∧ B ∈ 0 +∞ → k ∈ A ⟼ B ⁡ k = B
18 16 3 17 syl2anc ⊢ φ ∧ k ∈ A → k ∈ A ⟼ B ⁡ k = B
19 18 ex ⊢ φ → k ∈ A → k ∈ A ⟼ B ⁡ k = B
20 1 19 ralrimi ⊢ φ → ∀ k ∈ A k ∈ A ⟼ B ⁡ k = B
21 20 sumeq2d ⊢ φ → ∑ k ∈ A k ∈ A ⟼ B ⁡ k = ∑ k ∈ A B
22 6 15 21 3eqtrd ⊢ φ → sum^ ⁡ k ∈ A ⟼ B = ∑ k ∈ A B