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