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

Proof

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