Theorem sge0ssre

Description: If a sum of nonnegative extended reals is real, than any subsum is real. (Contributed by Glauco Siliprandi, 17-Aug-2020)

	Ref	Expression
Hypotheses	sge0less.x	$$⊢\phi \to X\in V$$
	sge0less.f	$$⊢\phi \to F:X⟶\left[0,\mathrm{+\infty }\right]$$
	sge0ssre.re	$$⊢\phi \to \mathrm{sum^}\left(F\right)\in ℝ$$
Assertion	sge0ssre	$$⊢\phi \to \mathrm{sum^}\left({F\upharpoonright }_Y\right)\in ℝ$$

Proof

Step	Hyp	Ref	Expression
1		sge0less.x	$$⊢\phi \to X\in V$$
2		sge0less.f	$$⊢\phi \to F:X⟶\left[0,\mathrm{+\infty }\right]$$
3		sge0ssre.re	$$⊢\phi \to \mathrm{sum^}\left(F\right)\in ℝ$$
4		inex1g	$$⊢X\in V\to X\cap Y\in \mathrm{V}$$
5	1 4	syl	$$⊢\phi \to X\cap Y\in \mathrm{V}$$
6		fresin	$$⊢F:X⟶\left[0,\mathrm{+\infty }\right]\to \left({F\upharpoonright }_Y\right):X\cap Y⟶\left[0,\mathrm{+\infty }\right]$$
7	2 6	syl	$$⊢\phi \to \left({F\upharpoonright }_Y\right):X\cap Y⟶\left[0,\mathrm{+\infty }\right]$$
8	5 7	sge0xrcl	$$⊢\phi \to \mathrm{sum^}\left({F\upharpoonright }_Y\right)\in {ℝ}^{*}$$
9		mnfxr	$$⊢\mathrm{-\infty }\in {ℝ}^{*}$$
10	9	a1i	$$⊢\phi \to \mathrm{-\infty }\in {ℝ}^{*}$$
11		0xr	$$⊢0\in {ℝ}^{*}$$
12	11	a1i	$$⊢\phi \to 0\in {ℝ}^{*}$$
13		mnflt0	$$⊢\mathrm{-\infty }<0$$
14	13	a1i	$$⊢\phi \to \mathrm{-\infty }<0$$
15	5 7	sge0ge0	$$⊢\phi \to 0\le \mathrm{sum^}\left({F\upharpoonright }_Y\right)$$
16	10 12 8 14 15	xrltletrd	$$⊢\phi \to \mathrm{-\infty }<\mathrm{sum^}\left({F\upharpoonright }_Y\right)$$
17	1 2	sge0less	$$⊢\phi \to \mathrm{sum^}\left({F\upharpoonright }_Y\right)\le \mathrm{sum^}\left(F\right)$$
18		xrre	$$⊢\left(\left(\mathrm{sum^}\left({F\upharpoonright }_Y\right)\in {ℝ}^{*}\wedge \mathrm{sum^}\left(F\right)\in ℝ\right)\wedge \left(\mathrm{-\infty }<\mathrm{sum^}\left({F\upharpoonright }_Y\right)\wedge \mathrm{sum^}\left({F\upharpoonright }_Y\right)\le \mathrm{sum^}\left(F\right)\right)\right)\to \mathrm{sum^}\left({F\upharpoonright }_Y\right)\in ℝ$$
19	8 3 16 17 18	syl22anc	$$⊢\phi \to \mathrm{sum^}\left({F\upharpoonright }_Y\right)\in ℝ$$