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 φAFin
sge0fsummpt.b φkAB0+∞
Assertion sge0fsummpt φsum^kAB=kAB

Proof

Step Hyp Ref Expression
1 sge0fsummpt.a φAFin
2 sge0fsummpt.b φkAB0+∞
3 eqid kAB=kAB
4 2 3 fmptd φkAB:A0+∞
5 1 4 sge0fsum φsum^kAB=jAkABj
6 fveq2 j=kkABj=kABk
7 nfcv _kA
8 nfcv _jA
9 nfmpt1 _kkAB
10 nfcv _kj
11 9 10 nffv _kkABj
12 nfcv _jkABk
13 6 7 8 11 12 cbvsum jAkABj=kAkABk
14 13 a1i φjAkABj=kAkABk
15 simpr φkAkA
16 3 fvmpt2 kAB0+∞kABk=B
17 15 2 16 syl2anc φkAkABk=B
18 17 sumeq2dv φkAkABk=kAB
19 5 14 18 3eqtrd φsum^kAB=kAB