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	$$⊢Ⅎk\phi$$
	sge0snmptf.a	$$⊢\phi \to A\in V$$
	sge0snmptf.c	$$⊢\phi \to C\in \left[0,\mathrm{+\infty }\right]$$
	sge0snmptf.b	$$⊢k=A\to B=C$$
Assertion	sge0snmptf	$$⊢\phi \to \mathrm{sum^}\left(\left(k\in \left\{A\right\}⟼B\right)\right)=C$$

Proof

Step	Hyp	Ref	Expression
1		sge0snmptf.k	$$⊢Ⅎk\phi$$
2		sge0snmptf.a	$$⊢\phi \to A\in V$$
3		sge0snmptf.c	$$⊢\phi \to C\in \left[0,\mathrm{+\infty }\right]$$
4		sge0snmptf.b	$$⊢k=A\to B=C$$
5		elsni	$$⊢k\in \left\{A\right\}\to k=A$$
6	5 4	syl	$$⊢k\in \left\{A\right\}\to B=C$$
7	6	adantl	$$⊢\left(\phi \wedge k\in \left\{A\right\}\right)\to B=C$$
8	3	adantr	$$⊢\left(\phi \wedge k\in \left\{A\right\}\right)\to C\in \left[0,\mathrm{+\infty }\right]$$
9	7 8	eqeltrd	$$⊢\left(\phi \wedge k\in \left\{A\right\}\right)\to B\in \left[0,\mathrm{+\infty }\right]$$
10		eqid	$$⊢\left(k\in \left\{A\right\}⟼B\right)=\left(k\in \left\{A\right\}⟼B\right)$$
11	1 9 10	fmptdf	$$⊢\phi \to \left(k\in \left\{A\right\}⟼B\right):\left\{A\right\}⟶\left[0,\mathrm{+\infty }\right]$$
12	2 11	sge0sn	$$⊢\phi \to \mathrm{sum^}\left(\left(k\in \left\{A\right\}⟼B\right)\right)=\left(k\in \left\{A\right\}⟼B\right)\left(A\right)$$
13		snidg	$$⊢A\in V\to A\in \left\{A\right\}$$
14	2 13	syl	$$⊢\phi \to A\in \left\{A\right\}$$
15	10 4 14 3	fvmptd3	$$⊢\phi \to \left(k\in \left\{A\right\}⟼B\right)\left(A\right)=C$$
16	12 15	eqtrd	$$⊢\phi \to \mathrm{sum^}\left(\left(k\in \left\{A\right\}⟼B\right)\right)=C$$