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 
|- F/ k ph
sge0fsummptf.a 
|- ( ph -> A e. Fin )
sge0fsummptf.b 
|- ( ( ph /\ k e. A ) -> B e. ( 0 [,) +oo ) )
Assertion sge0fsummptf 
|- ( ph -> ( sum^ ` ( k e. A |-> B ) ) = sum_ k e. A B )

Proof

Step Hyp Ref Expression
1 sge0fsummptf.k 
 |-  F/ k ph
2 sge0fsummptf.a 
 |-  ( ph -> A e. Fin )
3 sge0fsummptf.b 
 |-  ( ( ph /\ k e. A ) -> B e. ( 0 [,) +oo ) )
4 eqid 
 |-  ( k e. A |-> B ) = ( k e. A |-> B )
5 1 3 4 fmptdf 
 |-  ( ph -> ( k e. A |-> B ) : A --> ( 0 [,) +oo ) )
6 2 5 sge0fsum 
 |-  ( ph -> ( sum^ ` ( k e. A |-> B ) ) = sum_ j e. A ( ( k e. A |-> B ) ` j ) )
7 fveq2 
 |-  ( j = k -> ( ( k e. A |-> B ) ` j ) = ( ( k e. A |-> B ) ` k ) )
8 nfcv 
 |-  F/_ k A
9 nfcv 
 |-  F/_ j A
10 nfmpt1 
 |-  F/_ k ( k e. A |-> B )
11 nfcv 
 |-  F/_ k j
12 10 11 nffv 
 |-  F/_ k ( ( k e. A |-> B ) ` j )
13 nfcv 
 |-  F/_ j ( ( k e. A |-> B ) ` k )
14 7 8 9 12 13 cbvsum 
 |-  sum_ j e. A ( ( k e. A |-> B ) ` j ) = sum_ k e. A ( ( k e. A |-> B ) ` k )
15 14 a1i 
 |-  ( ph -> sum_ j e. A ( ( k e. A |-> B ) ` j ) = sum_ k e. A ( ( k e. A |-> B ) ` k ) )
16 simpr 
 |-  ( ( ph /\ k e. A ) -> k e. A )
17 4 fvmpt2 
 |-  ( ( k e. A /\ B e. ( 0 [,) +oo ) ) -> ( ( k e. A |-> B ) ` k ) = B )
18 16 3 17 syl2anc 
 |-  ( ( ph /\ k e. A ) -> ( ( k e. A |-> B ) ` k ) = B )
19 18 ex 
 |-  ( ph -> ( k e. A -> ( ( k e. A |-> B ) ` k ) = B ) )
20 1 19 ralrimi 
 |-  ( ph -> A. k e. A ( ( k e. A |-> B ) ` k ) = B )
21 20 sumeq2d 
 |-  ( ph -> sum_ k e. A ( ( k e. A |-> B ) ` k ) = sum_ k e. A B )
22 6 15 21 3eqtrd 
 |-  ( ph -> ( sum^ ` ( k e. A |-> B ) ) = sum_ k e. A B )