Metamath Proof Explorer

Theorem esumcl

Description: Closure for extended sum in the extended positive reals. (Contributed by Thierry Arnoux, 2-Jan-2017)

Ref Expression
Hypothesis esumcl.1 
|- F/_ k A
Assertion esumcl 
|- ( ( A e. V /\ A. k e. A B e. ( 0 [,] +oo ) ) -> sum* k e. A B e. ( 0 [,] +oo ) )

Proof

Step Hyp Ref Expression
1 esumcl.1 
 |-  F/_ k A
2 xrge0base 
 |-  ( 0 [,] +oo ) = ( Base ` ( RR*s |`s ( 0 [,] +oo ) ) )
3 xrge0cmn 
 |-  ( RR*s |`s ( 0 [,] +oo ) ) e. CMnd
4 3 a1i 
 |-  ( ( A e. V /\ A. k e. A B e. ( 0 [,] +oo ) ) -> ( RR*s |`s ( 0 [,] +oo ) ) e. CMnd )
5 xrge0tps 
 |-  ( RR*s |`s ( 0 [,] +oo ) ) e. TopSp
6 5 a1i 
 |-  ( ( A e. V /\ A. k e. A B e. ( 0 [,] +oo ) ) -> ( RR*s |`s ( 0 [,] +oo ) ) e. TopSp )
7 simpl 
 |-  ( ( A e. V /\ A. k e. A B e. ( 0 [,] +oo ) ) -> A e. V )
8 1 nfel1 
 |-  F/ k A e. V
9 nfra1 
 |-  F/ k A. k e. A B e. ( 0 [,] +oo )
10 8 9 nfan 
 |-  F/ k ( A e. V /\ A. k e. A B e. ( 0 [,] +oo ) )
11 nfcv 
 |-  F/_ k ( 0 [,] +oo )
12 simpr 
 |-  ( ( A e. V /\ A. k e. A B e. ( 0 [,] +oo ) ) -> A. k e. A B e. ( 0 [,] +oo ) )
13 12 r19.21bi 
 |-  ( ( ( A e. V /\ A. k e. A B e. ( 0 [,] +oo ) ) /\ k e. A ) -> B e. ( 0 [,] +oo ) )
14 eqid 
 |-  ( k e. A |-> B ) = ( k e. A |-> B )
15 10 1 11 13 14 fmptdF 
 |-  ( ( A e. V /\ A. k e. A B e. ( 0 [,] +oo ) ) -> ( k e. A |-> B ) : A --> ( 0 [,] +oo ) )
16 2 4 6 7 15 tsmscl 
 |-  ( ( A e. V /\ A. k e. A B e. ( 0 [,] +oo ) ) -> ( ( RR*s |`s ( 0 [,] +oo ) ) tsums ( k e. A |-> B ) ) C_ ( 0 [,] +oo ) )
17 df-esum 
 |-  sum* k e. A B = U. ( ( RR*s |`s ( 0 [,] +oo ) ) tsums ( k e. A |-> B ) )
18 eqid 
 |-  ( RR*s |`s ( 0 [,] +oo ) ) = ( RR*s |`s ( 0 [,] +oo ) )
19 18 7 15 xrge0tsmsbi 
 |-  ( ( A e. V /\ A. k e. A B e. ( 0 [,] +oo ) ) -> ( sum* k e. A B e. ( ( RR*s |`s ( 0 [,] +oo ) ) tsums ( k e. A |-> B ) ) <-> sum* k e. A B = U. ( ( RR*s |`s ( 0 [,] +oo ) ) tsums ( k e. A |-> B ) ) ) )
20 17 19 mpbiri 
 |-  ( ( A e. V /\ A. k e. A B e. ( 0 [,] +oo ) ) -> sum* k e. A B e. ( ( RR*s |`s ( 0 [,] +oo ) ) tsums ( k e. A |-> B ) ) )
21 16 20 sseldd 
 |-  ( ( A e. V /\ A. k e. A B e. ( 0 [,] +oo ) ) -> sum* k e. A B e. ( 0 [,] +oo ) )