Theorem sge0snmpt

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

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

Proof

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