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 = ( RR*s |`s ( 0 [,] +oo ) )
	xrge0tsmseq.a	|- ( ph -> A e. V )
	xrge0tsmseq.f	|- ( ph -> F : A --> ( 0 [,] +oo ) )
	xrge0tsmseq.h	|- ( ph -> C e. ( G tsums F ) )
Assertion	xrge0tsmseq	|- ( ph -> C = U. ( G tsums F ) )

Proof

Step	Hyp	Ref	Expression
1		xrge0tsmseq.g	|- G = ( RR*s |`s ( 0 [,] +oo ) )
2		xrge0tsmseq.a	|- ( ph -> A e. V )
3		xrge0tsmseq.f	|- ( ph -> F : A --> ( 0 [,] +oo ) )
4		xrge0tsmseq.h	|- ( ph -> C e. ( G tsums F ) )
5	1	xrge0tsms2	|- ( ( A e. V /\ F : A --> ( 0 [,] +oo ) ) -> ( G tsums F ) ~~ 1o )
6	2 3 5	syl2anc	|- ( ph -> ( G tsums F ) ~~ 1o )
7		en1eqsn	|- ( ( C e. ( G tsums F ) /\ ( G tsums F ) ~~ 1o ) -> ( G tsums F ) = { C } )
8	4 6 7	syl2anc	|- ( ph -> ( G tsums F ) = { C } )
9	8	unieqd	|- ( ph -> U. ( G tsums F ) = U. { C } )
10		unisng	|- ( C e. ( G tsums F ) -> U. { C } = C )
11	4 10	syl	|- ( ph -> U. { C } = C )
12	9 11	eqtr2d	|- ( ph -> C = U. ( G tsums F ) )