Metamath Proof Explorer

Theorem esumval

Description: Develop the value of the extended sum. (Contributed by Thierry Arnoux, 4-Jan-2017)

Ref Expression
Hypotheses esumval.p 
|- F/ k ph
esumval.0 
|- F/_ k A
esumval.1 
|- ( ph -> A e. V )
esumval.2 
|- ( ( ph /\ k e. A ) -> B e. ( 0 [,] +oo ) )
esumval.3 
|- ( ( ph /\ x e. ( ~P A i^i Fin ) ) -> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( k e. x |-> B ) ) = C )
Assertion esumval 
|- ( ph -> sum* k e. A B = sup ( ran ( x e. ( ~P A i^i Fin ) |-> C ) , RR* , < ) )

Proof

Step Hyp Ref Expression
1 esumval.p 
 |-  F/ k ph
2 esumval.0 
 |-  F/_ k A
3 esumval.1 
 |-  ( ph -> A e. V )
4 esumval.2 
 |-  ( ( ph /\ k e. A ) -> B e. ( 0 [,] +oo ) )
5 esumval.3 
 |-  ( ( ph /\ x e. ( ~P A i^i Fin ) ) -> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( k e. x |-> B ) ) = C )
6 df-esum 
 |-  sum* k e. A B = U. ( ( RR*s |`s ( 0 [,] +oo ) ) tsums ( k e. A |-> B ) )
7 eqid 
 |-  ( RR*s |`s ( 0 [,] +oo ) ) = ( RR*s |`s ( 0 [,] +oo ) )
8 nfcv 
 |-  F/_ k ( 0 [,] +oo )
9 eqid 
 |-  ( k e. A |-> B ) = ( k e. A |-> B )
10 1 2 8 4 9 fmptdF 
 |-  ( ph -> ( k e. A |-> B ) : A --> ( 0 [,] +oo ) )
11 inss1 
 |-  ( ~P A i^i Fin ) C_ ~P A
12 11 sseli 
 |-  ( x e. ( ~P A i^i Fin ) -> x e. ~P A )
13 12 elpwid 
 |-  ( x e. ( ~P A i^i Fin ) -> x C_ A )
14 13 adantl 
 |-  ( ( ph /\ x e. ( ~P A i^i Fin ) ) -> x C_ A )
15 nfcv 
 |-  F/_ k x
16 2 15 resmptf 
 |-  ( x C_ A -> ( ( k e. A |-> B ) |` x ) = ( k e. x |-> B ) )
17 14 16 syl 
 |-  ( ( ph /\ x e. ( ~P A i^i Fin ) ) -> ( ( k e. A |-> B ) |` x ) = ( k e. x |-> B ) )
18 17 oveq2d 
 |-  ( ( ph /\ x e. ( ~P A i^i Fin ) ) -> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( ( k e. A |-> B ) |` x ) ) = ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( k e. x |-> B ) ) )
19 18 5 eqtr2d 
 |-  ( ( ph /\ x e. ( ~P A i^i Fin ) ) -> C = ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( ( k e. A |-> B ) |` x ) ) )
20 19 mpteq2dva 
 |-  ( ph -> ( x e. ( ~P A i^i Fin ) |-> C ) = ( x e. ( ~P A i^i Fin ) |-> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( ( k e. A |-> B ) |` x ) ) ) )
21 20 rneqd 
 |-  ( ph -> ran ( x e. ( ~P A i^i Fin ) |-> C ) = ran ( x e. ( ~P A i^i Fin ) |-> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( ( k e. A |-> B ) |` x ) ) ) )
22 21 supeq1d 
 |-  ( ph -> sup ( ran ( x e. ( ~P A i^i Fin ) |-> C ) , RR* , < ) = sup ( ran ( x e. ( ~P A i^i Fin ) |-> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( ( k e. A |-> B ) |` x ) ) ) , RR* , < ) )
23 7 3 10 22 xrge0tsmsd 
 |-  ( ph -> ( ( RR*s |`s ( 0 [,] +oo ) ) tsums ( k e. A |-> B ) ) = { sup ( ran ( x e. ( ~P A i^i Fin ) |-> C ) , RR* , < ) } )
24 23 unieqd 
 |-  ( ph -> U. ( ( RR*s |`s ( 0 [,] +oo ) ) tsums ( k e. A |-> B ) ) = U. { sup ( ran ( x e. ( ~P A i^i Fin ) |-> C ) , RR* , < ) } )
25 6 24 syl5eq 
 |-  ( ph -> sum* k e. A B = U. { sup ( ran ( x e. ( ~P A i^i Fin ) |-> C ) , RR* , < ) } )
26 xrltso 
 |-  < Or RR*
27 26 supex 
 |-  sup ( ran ( x e. ( ~P A i^i Fin ) |-> C ) , RR* , < ) e. _V
28 27 unisn 
 |-  U. { sup ( ran ( x e. ( ~P A i^i Fin ) |-> C ) , RR* , < ) } = sup ( ran ( x e. ( ~P A i^i Fin ) |-> C ) , RR* , < )
29 25 28 eqtrdi 
 |-  ( ph -> sum* k e. A B = sup ( ran ( x e. ( ~P A i^i Fin ) |-> C ) , RR* , < ) )