Metamath Proof Explorer

Theorem esumpfinval

Description: The value of the extended sum of a finite set of nonnegative finite terms. (Contributed by Thierry Arnoux, 28-Jun-2017) (Proof shortened by AV, 25-Jul-2019)

Ref Expression
Hypotheses esumpfinval.a 
|- ( ph -> A e. Fin )
esumpfinval.b 
|- ( ( ph /\ k e. A ) -> B e. ( 0 [,) +oo ) )
Assertion esumpfinval 
|- ( ph -> sum* k e. A B = sum_ k e. A B )

Proof

Step Hyp Ref Expression
1 esumpfinval.a 
 |-  ( ph -> A e. Fin )
2 esumpfinval.b 
 |-  ( ( ph /\ k e. A ) -> B e. ( 0 [,) +oo ) )
3 df-esum 
 |-  sum* k e. A B = U. ( ( RR*s |`s ( 0 [,] +oo ) ) tsums ( k e. A |-> B ) )
4 xrge0base 
 |-  ( 0 [,] +oo ) = ( Base ` ( RR*s |`s ( 0 [,] +oo ) ) )
5 xrge00 
 |-  0 = ( 0g ` ( RR*s |`s ( 0 [,] +oo ) ) )
6 xrge0cmn 
 |-  ( RR*s |`s ( 0 [,] +oo ) ) e. CMnd
7 6 a1i 
 |-  ( ph -> ( RR*s |`s ( 0 [,] +oo ) ) e. CMnd )
8 xrge0tps 
 |-  ( RR*s |`s ( 0 [,] +oo ) ) e. TopSp
9 8 a1i 
 |-  ( ph -> ( RR*s |`s ( 0 [,] +oo ) ) e. TopSp )
10 icossicc 
 |-  ( 0 [,) +oo ) C_ ( 0 [,] +oo )
11 10 2 sselid 
 |-  ( ( ph /\ k e. A ) -> B e. ( 0 [,] +oo ) )
12 11 fmpttd 
 |-  ( ph -> ( k e. A |-> B ) : A --> ( 0 [,] +oo ) )
13 eqid 
 |-  ( k e. A |-> B ) = ( k e. A |-> B )
14 c0ex 
 |-  0 e. _V
15 14 a1i 
 |-  ( ph -> 0 e. _V )
16 13 1 2 15 fsuppmptdm 
 |-  ( ph -> ( k e. A |-> B ) finSupp 0 )
17 xrge0topn 
 |-  ( TopOpen ` ( RR*s |`s ( 0 [,] +oo ) ) ) = ( ( ordTop ` <_ ) |`t ( 0 [,] +oo ) )
18 17 eqcomi 
 |-  ( ( ordTop ` <_ ) |`t ( 0 [,] +oo ) ) = ( TopOpen ` ( RR*s |`s ( 0 [,] +oo ) ) )
19 xrhaus 
 |-  ( ordTop ` <_ ) e. Haus
20 ovex 
 |-  ( 0 [,] +oo ) e. _V
21 resthaus 
 |-  ( ( ( ordTop ` <_ ) e. Haus /\ ( 0 [,] +oo ) e. _V ) -> ( ( ordTop ` <_ ) |`t ( 0 [,] +oo ) ) e. Haus )
22 19 20 21 mp2an 
 |-  ( ( ordTop ` <_ ) |`t ( 0 [,] +oo ) ) e. Haus
23 22 a1i 
 |-  ( ph -> ( ( ordTop ` <_ ) |`t ( 0 [,] +oo ) ) e. Haus )
24 4 5 7 9 1 12 16 18 23 haustsmsid 
 |-  ( ph -> ( ( RR*s |`s ( 0 [,] +oo ) ) tsums ( k e. A |-> B ) ) = { ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( k e. A |-> B ) ) } )
25 24 unieqd 
 |-  ( ph -> U. ( ( RR*s |`s ( 0 [,] +oo ) ) tsums ( k e. A |-> B ) ) = U. { ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( k e. A |-> B ) ) } )
26 3 25 eqtrid 
 |-  ( ph -> sum* k e. A B = U. { ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( k e. A |-> B ) ) } )
27 ovex 
 |-  ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( k e. A |-> B ) ) e. _V
28 27 unisn 
 |-  U. { ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( k e. A |-> B ) ) } = ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( k e. A |-> B ) )
29 26 28 eqtrdi 
 |-  ( ph -> sum* k e. A B = ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( k e. A |-> B ) ) )
30 2 fmpttd 
 |-  ( ph -> ( k e. A |-> B ) : A --> ( 0 [,) +oo ) )
31 esumpfinvallem 
 |-  ( ( A e. Fin /\ ( k e. A |-> B ) : A --> ( 0 [,) +oo ) ) -> ( CCfld gsum ( k e. A |-> B ) ) = ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( k e. A |-> B ) ) )
32 1 30 31 syl2anc 
 |-  ( ph -> ( CCfld gsum ( k e. A |-> B ) ) = ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( k e. A |-> B ) ) )
33 rge0ssre 
 |-  ( 0 [,) +oo ) C_ RR
34 ax-resscn 
 |-  RR C_ CC
35 33 34 sstri 
 |-  ( 0 [,) +oo ) C_ CC
36 35 2 sselid 
 |-  ( ( ph /\ k e. A ) -> B e. CC )
37 1 36 gsumfsum 
 |-  ( ph -> ( CCfld gsum ( k e. A |-> B ) ) = sum_ k e. A B )
38 29 32 37 3eqtr2d 
 |-  ( ph -> sum* k e. A B = sum_ k e. A B )