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		nfmpt1	|- F/_ k ( k e. A |-> B )
8		nfcv	|- F/_ k j
9	7 8	nffv	|- F/_ k ( ( k e. A |-> B ) ` j )
10		nfcv	|- F/_ j ( ( k e. A |-> B ) ` k )
11	6 9 10	cbvsum	|- sum_ j e. A ( ( k e. A |-> B ) ` j ) = sum_ k e. A ( ( k e. A |-> B ) ` k )
12	11	a1i	|- ( ph -> sum_ j e. A ( ( k e. A |-> B ) ` j ) = sum_ k e. A ( ( k e. A |-> B ) ` k ) )
13		simpr	|- ( ( ph /\ k e. A ) -> k e. A )
14	3	fvmpt2	|- ( ( k e. A /\ B e. ( 0 [,) +oo ) ) -> ( ( k e. A |-> B ) ` k ) = B )
15	13 2 14	syl2anc	|- ( ( ph /\ k e. A ) -> ( ( k e. A |-> B ) ` k ) = B )
16	15	sumeq2dv	|- ( ph -> sum_ k e. A ( ( k e. A |-> B ) ` k ) = sum_ k e. A B )
17	5 12 16	3eqtrd	|- ( ph -> ( sum^ ` ( k e. A |-> B ) ) = sum_ k e. A B )