Theorem sge0resrnlem

Description: The sum of nonnegative extended reals restricted to the range of a function is less than or equal to the sum of the composition of the two functions. (Contributed by Glauco Siliprandi, 17-Aug-2020)

	Ref	Expression
Hypotheses	sge0resrnlem.a	$$⊢\phi \to A\in V$$
	sge0resrnlem.f	$$⊢\phi \to F:B⟶\left[0,\mathrm{+\infty }\right]$$
	sge0resrnlem.g	$$⊢\phi \to G:A⟶B$$
	sge0resrnlem.x	$$⊢\phi \to X\in 𝒫A$$
	sge0resrnlem.f1o	$$⊢\phi \to \left({G\upharpoonright }_X\right):X\underset{1-1\; onto}{⟶}\mathrm{ran}G$$
Assertion	sge0resrnlem	$$⊢\phi \to \mathrm{sum^}\left({F\upharpoonright }_{\mathrm{ran}G}\right)\le \mathrm{sum^}\left(F\circ G\right)$$

Proof

Step	Hyp	Ref	Expression
1		sge0resrnlem.a	$$⊢\phi \to A\in V$$
2		sge0resrnlem.f	$$⊢\phi \to F:B⟶\left[0,\mathrm{+\infty }\right]$$
3		sge0resrnlem.g	$$⊢\phi \to G:A⟶B$$
4		sge0resrnlem.x	$$⊢\phi \to X\in 𝒫A$$
5		sge0resrnlem.f1o	$$⊢\phi \to \left({G\upharpoonright }_X\right):X\underset{1-1\; onto}{⟶}\mathrm{ran}G$$
6		nfv	$$⊢Ⅎy\phi$$
7		nfv	$$⊢Ⅎx\phi$$
8		fveq2	$$⊢y=G\left(x\right)\to F\left(y\right)=F\left(G\left(x\right)\right)$$
9		fvres	$$⊢x\in X\to \left({G\upharpoonright }_X\right)\left(x\right)=G\left(x\right)$$
10	9	adantl	$$⊢\left(\phi \wedge x\in X\right)\to \left({G\upharpoonright }_X\right)\left(x\right)=G\left(x\right)$$
11	2	adantr	$$⊢\left(\phi \wedge y\in \mathrm{ran}G\right)\to F:B⟶\left[0,\mathrm{+\infty }\right]$$
12	3	frnd	$$⊢\phi \to \mathrm{ran}G\subseteq B$$
13	12	adantr	$$⊢\left(\phi \wedge y\in \mathrm{ran}G\right)\to \mathrm{ran}G\subseteq B$$
14		simpr	$$⊢\left(\phi \wedge y\in \mathrm{ran}G\right)\to y\in \mathrm{ran}G$$
15	13 14	sseldd	$$⊢\left(\phi \wedge y\in \mathrm{ran}G\right)\to y\in B$$
16	11 15	ffvelcdmd	$$⊢\left(\phi \wedge y\in \mathrm{ran}G\right)\to F\left(y\right)\in \left[0,\mathrm{+\infty }\right]$$
17	6 7 8 4 5 10 16	sge0f1o	$$⊢\phi \to \mathrm{sum^}\left(\left(y\in \mathrm{ran}G⟼F\left(y\right)\right)\right)=\mathrm{sum^}\left(\left(x\in X⟼F\left(G\left(x\right)\right)\right)\right)$$
18	2 12	feqresmpt	$$⊢\phi \to {F\upharpoonright }_{\mathrm{ran}G}=\left(y\in \mathrm{ran}G⟼F\left(y\right)\right)$$
19	18	fveq2d	$$⊢\phi \to \mathrm{sum^}\left({F\upharpoonright }_{\mathrm{ran}G}\right)=\mathrm{sum^}\left(\left(y\in \mathrm{ran}G⟼F\left(y\right)\right)\right)$$
20		fcompt	$$⊢\left(F:B⟶\left[0,\mathrm{+\infty }\right]\wedge G:A⟶B\right)\to F\circ G=\left(x\in A⟼F\left(G\left(x\right)\right)\right)$$
21	2 3 20	syl2anc	$$⊢\phi \to F\circ G=\left(x\in A⟼F\left(G\left(x\right)\right)\right)$$
22	21	reseq1d	$$⊢\phi \to {\left(F\circ G\right)\upharpoonright }_X={\left(x\in A⟼F\left(G\left(x\right)\right)\right)\upharpoonright }_X$$
23	4	elpwid	$$⊢\phi \to X\subseteq A$$
24	23	resmptd	$$⊢\phi \to {\left(x\in A⟼F\left(G\left(x\right)\right)\right)\upharpoonright }_X=\left(x\in X⟼F\left(G\left(x\right)\right)\right)$$
25	22 24	eqtrd	$$⊢\phi \to {\left(F\circ G\right)\upharpoonright }_X=\left(x\in X⟼F\left(G\left(x\right)\right)\right)$$
26	25	fveq2d	$$⊢\phi \to \mathrm{sum^}\left({\left(F\circ G\right)\upharpoonright }_X\right)=\mathrm{sum^}\left(\left(x\in X⟼F\left(G\left(x\right)\right)\right)\right)$$
27	17 19 26	3eqtr4d	$$⊢\phi \to \mathrm{sum^}\left({F\upharpoonright }_{\mathrm{ran}G}\right)=\mathrm{sum^}\left({\left(F\circ G\right)\upharpoonright }_X\right)$$
28		fco	$$⊢\left(F:B⟶\left[0,\mathrm{+\infty }\right]\wedge G:A⟶B\right)\to \left(F\circ G\right):A⟶\left[0,\mathrm{+\infty }\right]$$
29	2 3 28	syl2anc	$$⊢\phi \to \left(F\circ G\right):A⟶\left[0,\mathrm{+\infty }\right]$$
30	1 29	sge0less	$$⊢\phi \to \mathrm{sum^}\left({\left(F\circ G\right)\upharpoonright }_X\right)\le \mathrm{sum^}\left(F\circ G\right)$$
31	27 30	eqbrtrd	$$⊢\phi \to \mathrm{sum^}\left({F\upharpoonright }_{\mathrm{ran}G}\right)\le \mathrm{sum^}\left(F\circ G\right)$$