Theorem xrge0tsmseq

Description: Any limit of a finite or infinite sum in the nonnegative extended reals is the union of the sets limits, since this set is a singleton. (Contributed by Thierry Arnoux, 24-Mar-2017)

	Ref	Expression
Hypotheses	xrge0tsmseq.g	$$⊢G={ℝ}_{𝑠}^{*}{\upharpoonright }_{𝑠}\left[0,\mathrm{+\infty }\right]$$
	xrge0tsmseq.a	$$⊢\phi \to A\in V$$
	xrge0tsmseq.f	$$⊢\phi \to F:A⟶\left[0,\mathrm{+\infty }\right]$$
	xrge0tsmseq.h	$$⊢\phi \to C\in \left(G\mathrm{tsums}F\right)$$
Assertion	xrge0tsmseq	$$⊢\phi \to C=\bigcup \left(G\mathrm{tsums}F\right)$$

Proof

Step	Hyp	Ref	Expression
1		xrge0tsmseq.g	$$⊢G={ℝ}_{𝑠}^{*}{\upharpoonright }_{𝑠}\left[0,\mathrm{+\infty }\right]$$
2		xrge0tsmseq.a	$$⊢\phi \to A\in V$$
3		xrge0tsmseq.f	$$⊢\phi \to F:A⟶\left[0,\mathrm{+\infty }\right]$$
4		xrge0tsmseq.h	$$⊢\phi \to C\in \left(G\mathrm{tsums}F\right)$$
5	1	xrge0tsms2	$$⊢\left(A\in V\wedge F:A⟶\left[0,\mathrm{+\infty }\right]\right)\to \left(G\mathrm{tsums}F\right)\approx 1_{𝑜}$$
6	2 3 5	syl2anc	$$⊢\phi \to \left(G\mathrm{tsums}F\right)\approx 1_{𝑜}$$
7		en1eqsn	$$⊢\left(C\in \left(G\mathrm{tsums}F\right)\wedge \left(G\mathrm{tsums}F\right)\approx 1_{𝑜}\right)\to G\mathrm{tsums}F=\left\{C\right\}$$
8	4 6 7	syl2anc	$$⊢\phi \to G\mathrm{tsums}F=\left\{C\right\}$$
9	8	unieqd	$$⊢\phi \to \bigcup \left(G\mathrm{tsums}F\right)=\bigcup \left\{C\right\}$$
10		unisng	$$⊢C\in \left(G\mathrm{tsums}F\right)\to \bigcup \left\{C\right\}=C$$
11	4 10	syl	$$⊢\phi \to \bigcup \left\{C\right\}=C$$
12	9 11	eqtr2d	$$⊢\phi \to C=\bigcup \left(G\mathrm{tsums}F\right)$$