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

Proof

Step	Hyp	Ref	Expression
1		sge0snmpt.a	$$⊢\phi \to A\in V$$
2		sge0snmpt.c	$$⊢\phi \to C\in \left[0,\mathrm{+\infty }\right]$$
3		sge0snmpt.b	$$⊢k=A\to B=C$$
4		elsni	$$⊢k\in \left\{A\right\}\to k=A$$
5	4 3	syl	$$⊢k\in \left\{A\right\}\to B=C$$
6	5	adantl	$$⊢\left(\phi \wedge k\in \left\{A\right\}\right)\to B=C$$
7	2	adantr	$$⊢\left(\phi \wedge k\in \left\{A\right\}\right)\to C\in \left[0,\mathrm{+\infty }\right]$$
8	6 7	eqeltrd	$$⊢\left(\phi \wedge k\in \left\{A\right\}\right)\to B\in \left[0,\mathrm{+\infty }\right]$$
9		eqid	$$⊢\left(k\in \left\{A\right\}⟼B\right)=\left(k\in \left\{A\right\}⟼B\right)$$
10	8 9	fmptd	$$⊢\phi \to \left(k\in \left\{A\right\}⟼B\right):\left\{A\right\}⟶\left[0,\mathrm{+\infty }\right]$$
11	1 10	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)$$
12		eqidd	$$⊢\phi \to \left(k\in \left\{A\right\}⟼B\right)=\left(k\in \left\{A\right\}⟼B\right)$$
13	3	adantl	$$⊢\left(\phi \wedge k=A\right)\to B=C$$
14		snidg	$$⊢A\in V\to A\in \left\{A\right\}$$
15	1 14	syl	$$⊢\phi \to A\in \left\{A\right\}$$
16	12 13 15 2	fvmptd	$$⊢\phi \to \left(k\in \left\{A\right\}⟼B\right)\left(A\right)=C$$
17	11 16	eqtrd	$$⊢\phi \to \mathrm{sum^}\left(\left(k\in \left\{A\right\}⟼B\right)\right)=C$$