Metamath Proof Explorer

Theorem esumel

Description: The extended sum is a limit point of the corresponding infinite group sum. (Contributed by Thierry Arnoux, 24-Mar-2017)

Ref Expression
Hypotheses esumel.1 
|- F/ k ph
esumel.2 
|- F/_ k A
esumel.3 
|- ( ph -> A e. V )
esumel.4 
|- ( ( ph /\ k e. A ) -> B e. ( 0 [,] +oo ) )
Assertion esumel 
|- ( ph -> sum* k e. A B e. ( ( RR*s |`s ( 0 [,] +oo ) ) tsums ( k e. A |-> B ) ) )

Proof

Step Hyp Ref Expression
1 esumel.1 
 |-  F/ k ph
2 esumel.2 
 |-  F/_ k A
3 esumel.3 
 |-  ( ph -> A e. V )
4 esumel.4 
 |-  ( ( ph /\ k e. A ) -> B e. ( 0 [,] +oo ) )
5 4 ex 
 |-  ( ph -> ( k e. A -> B e. ( 0 [,] +oo ) ) )
6 1 5 ralrimi 
 |-  ( ph -> A. k e. A B e. ( 0 [,] +oo ) )
7 2 esumcl 
 |-  ( ( A e. V /\ A. k e. A B e. ( 0 [,] +oo ) ) -> sum* k e. A B e. ( 0 [,] +oo ) )
8 3 6 7 syl2anc 
 |-  ( ph -> sum* k e. A B e. ( 0 [,] +oo ) )
9 snidg 
 |-  ( sum* k e. A B e. ( 0 [,] +oo ) -> sum* k e. A B e. { sum* k e. A B } )
10 8 9 syl 
 |-  ( ph -> sum* k e. A B e. { sum* k e. A B } )
11 eqid 
 |-  ( RR*s |`s ( 0 [,] +oo ) ) = ( RR*s |`s ( 0 [,] +oo ) )
12 nfcv 
 |-  F/_ k ( 0 [,] +oo )
13 eqid 
 |-  ( k e. A |-> B ) = ( k e. A |-> B )
14 1 2 12 4 13 fmptdF 
 |-  ( ph -> ( k e. A |-> B ) : A --> ( 0 [,] +oo ) )
15 inss1 
 |-  ( ~P A i^i Fin ) C_ ~P A
16 simpr 
 |-  ( ( ph /\ x e. ( ~P A i^i Fin ) ) -> x e. ( ~P A i^i Fin ) )
17 15 16 sseldi 
 |-  ( ( ph /\ x e. ( ~P A i^i Fin ) ) -> x e. ~P A )
18 17 elpwid 
 |-  ( ( ph /\ x e. ( ~P A i^i Fin ) ) -> x C_ A )
19 nfcv 
 |-  F/_ k x
20 2 19 resmptf 
 |-  ( x C_ A -> ( ( k e. A |-> B ) |` x ) = ( k e. x |-> B ) )
21 18 20 syl 
 |-  ( ( ph /\ x e. ( ~P A i^i Fin ) ) -> ( ( k e. A |-> B ) |` x ) = ( k e. x |-> B ) )
22 21 eqcomd 
 |-  ( ( ph /\ x e. ( ~P A i^i Fin ) ) -> ( k e. x |-> B ) = ( ( k e. A |-> B ) |` x ) )
23 22 oveq2d 
 |-  ( ( ph /\ x e. ( ~P A i^i Fin ) ) -> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( k e. x |-> B ) ) = ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( ( k e. A |-> B ) |` x ) ) )
24 1 2 3 4 23 esumval 
 |-  ( ph -> sum* k e. A B = sup ( ran ( x e. ( ~P A i^i Fin ) |-> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( ( k e. A |-> B ) |` x ) ) ) , RR* , < ) )
25 11 3 14 24 xrge0tsmsd 
 |-  ( ph -> ( ( RR*s |`s ( 0 [,] +oo ) ) tsums ( k e. A |-> B ) ) = { sum* k e. A B } )
26 10 25 eleqtrrd 
 |-  ( ph -> sum* k e. A B e. ( ( RR*s |`s ( 0 [,] +oo ) ) tsums ( k e. A |-> B ) ) )