Theorem sge0snmptf

Description: A sum of a nonnegative extended real is the term. (Contributed by Glauco Siliprandi, 21-Nov-2020)

	Ref	Expression
Hypotheses	sge0snmptf.k	|- F/ k ph
	sge0snmptf.a	|- ( ph -> A e. V )
	sge0snmptf.c	|- ( ph -> C e. ( 0 [,] +oo ) )
	sge0snmptf.b	|- ( k = A -> B = C )
Assertion	sge0snmptf	|- ( ph -> ( sum^ ` ( k e. { A } |-> B ) ) = C )

Proof

Step	Hyp	Ref	Expression
1		sge0snmptf.k	|- F/ k ph
2		sge0snmptf.a	|- ( ph -> A e. V )
3		sge0snmptf.c	|- ( ph -> C e. ( 0 [,] +oo ) )
4		sge0snmptf.b	|- ( k = A -> B = C )
5		elsni	|- ( k e. { A } -> k = A )
6	5 4	syl	|- ( k e. { A } -> B = C )
7	6	adantl	|- ( ( ph /\ k e. { A } ) -> B = C )
8	3	adantr	|- ( ( ph /\ k e. { A } ) -> C e. ( 0 [,] +oo ) )
9	7 8	eqeltrd	|- ( ( ph /\ k e. { A } ) -> B e. ( 0 [,] +oo ) )
10		eqid	|- ( k e. { A } |-> B ) = ( k e. { A } |-> B )
11	1 9 10	fmptdf	|- ( ph -> ( k e. { A } |-> B ) : { A } --> ( 0 [,] +oo ) )
12	2 11	sge0sn	|- ( ph -> ( sum^ ` ( k e. { A } |-> B ) ) = ( ( k e. { A } |-> B ) ` A ) )
13		snidg	|- ( A e. V -> A e. { A } )
14	2 13	syl	|- ( ph -> A e. { A } )
15	10 4 14 3	fvmptd3	|- ( ph -> ( ( k e. { A } |-> B ) ` A ) = C )
16	12 15	eqtrd	|- ( ph -> ( sum^ ` ( k e. { A } |-> B ) ) = C )