Metamath Proof Explorer

Theorem esumpfinvalf

Description: Same as esumpfinval , minus distinct variable restrictions. (Contributed by Thierry Arnoux, 28-Aug-2017) (Proof shortened by AV, 25-Jul-2019)

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

Proof

Step Hyp Ref Expression
1 esumpfinvalf.1 
 |-  F/_ k A
2 esumpfinvalf.2 
 |-  F/ k ph
3 esumpfinvalf.a 
 |-  ( ph -> A e. Fin )
4 esumpfinvalf.b 
 |-  ( ( ph /\ k e. A ) -> B e. ( 0 [,) +oo ) )
5 df-esum 
 |-  sum* k e. A B = U. ( ( RR*s |`s ( 0 [,] +oo ) ) tsums ( k e. A |-> B ) )
6 xrge0base 
 |-  ( 0 [,] +oo ) = ( Base ` ( RR*s |`s ( 0 [,] +oo ) ) )
7 xrge00 
 |-  0 = ( 0g ` ( RR*s |`s ( 0 [,] +oo ) ) )
8 xrge0cmn 
 |-  ( RR*s |`s ( 0 [,] +oo ) ) e. CMnd
9 8 a1i 
 |-  ( ph -> ( RR*s |`s ( 0 [,] +oo ) ) e. CMnd )
10 xrge0tps 
 |-  ( RR*s |`s ( 0 [,] +oo ) ) e. TopSp
11 10 a1i 
 |-  ( ph -> ( RR*s |`s ( 0 [,] +oo ) ) e. TopSp )
12 nfcv 
 |-  F/_ k ( 0 [,] +oo )
13 icossicc 
 |-  ( 0 [,) +oo ) C_ ( 0 [,] +oo )
14 13 4 sselid 
 |-  ( ( ph /\ k e. A ) -> B e. ( 0 [,] +oo ) )
15 eqid 
 |-  ( k e. A |-> B ) = ( k e. A |-> B )
16 2 1 12 14 15 fmptdF 
 |-  ( ph -> ( k e. A |-> B ) : A --> ( 0 [,] +oo ) )
17 c0ex 
 |-  0 e. _V
18 17 a1i 
 |-  ( ph -> 0 e. _V )
19 16 3 18 fdmfifsupp 
 |-  ( ph -> ( k e. A |-> B ) finSupp 0 )
20 xrge0topn 
 |-  ( TopOpen ` ( RR*s |`s ( 0 [,] +oo ) ) ) = ( ( ordTop ` <_ ) |`t ( 0 [,] +oo ) )
21 20 eqcomi 
 |-  ( ( ordTop ` <_ ) |`t ( 0 [,] +oo ) ) = ( TopOpen ` ( RR*s |`s ( 0 [,] +oo ) ) )
22 xrhaus 
 |-  ( ordTop ` <_ ) e. Haus
23 ovex 
 |-  ( 0 [,] +oo ) e. _V
24 resthaus 
 |-  ( ( ( ordTop ` <_ ) e. Haus /\ ( 0 [,] +oo ) e. _V ) -> ( ( ordTop ` <_ ) |`t ( 0 [,] +oo ) ) e. Haus )
25 22 23 24 mp2an 
 |-  ( ( ordTop ` <_ ) |`t ( 0 [,] +oo ) ) e. Haus
26 25 a1i 
 |-  ( ph -> ( ( ordTop ` <_ ) |`t ( 0 [,] +oo ) ) e. Haus )
27 6 7 9 11 3 16 19 21 26 haustsmsid 
 |-  ( ph -> ( ( RR*s |`s ( 0 [,] +oo ) ) tsums ( k e. A |-> B ) ) = { ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( k e. A |-> B ) ) } )
28 27 unieqd 
 |-  ( ph -> U. ( ( RR*s |`s ( 0 [,] +oo ) ) tsums ( k e. A |-> B ) ) = U. { ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( k e. A |-> B ) ) } )
29 5 28 eqtrid 
 |-  ( ph -> sum* k e. A B = U. { ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( k e. A |-> B ) ) } )
30 ovex 
 |-  ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( k e. A |-> B ) ) e. _V
31 30 unisn 
 |-  U. { ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( k e. A |-> B ) ) } = ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( k e. A |-> B ) )
32 29 31 eqtrdi 
 |-  ( ph -> sum* k e. A B = ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( k e. A |-> B ) ) )
33 nfcv 
 |-  F/_ k ( 0 [,) +oo )
34 2 1 33 4 15 fmptdF 
 |-  ( ph -> ( k e. A |-> B ) : A --> ( 0 [,) +oo ) )
35 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 ) ) )
36 3 34 35 syl2anc 
 |-  ( ph -> ( CCfld gsum ( k e. A |-> B ) ) = ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( k e. A |-> B ) ) )
37 rge0ssre 
 |-  ( 0 [,) +oo ) C_ RR
38 ax-resscn 
 |-  RR C_ CC
39 37 38 sstri 
 |-  ( 0 [,) +oo ) C_ CC
40 39 4 sselid 
 |-  ( ( ph /\ k e. A ) -> B e. CC )
41 40 sbt 
 |-  [ l / k ] ( ( ph /\ k e. A ) -> B e. CC )
42 sbim 
 |-  ( [ l / k ] ( ( ph /\ k e. A ) -> B e. CC ) <-> ( [ l / k ] ( ph /\ k e. A ) -> [ l / k ] B e. CC ) )
43 sban 
 |-  ( [ l / k ] ( ph /\ k e. A ) <-> ( [ l / k ] ph /\ [ l / k ] k e. A ) )
44 2 sbf 
 |-  ( [ l / k ] ph <-> ph )
45 1 clelsb1fw 
 |-  ( [ l / k ] k e. A <-> l e. A )
46 44 45 anbi12i 
 |-  ( ( [ l / k ] ph /\ [ l / k ] k e. A ) <-> ( ph /\ l e. A ) )
47 43 46 bitri 
 |-  ( [ l / k ] ( ph /\ k e. A ) <-> ( ph /\ l e. A ) )
48 sbsbc 
 |-  ( [ l / k ] B e. CC <-> [. l / k ]. B e. CC )
49 sbcel1g 
 |-  ( l e. _V -> ( [. l / k ]. B e. CC <-> [_ l / k ]_ B e. CC ) )
50 49 elv 
 |-  ( [. l / k ]. B e. CC <-> [_ l / k ]_ B e. CC )
51 48 50 bitri 
 |-  ( [ l / k ] B e. CC <-> [_ l / k ]_ B e. CC )
52 47 51 imbi12i 
 |-  ( ( [ l / k ] ( ph /\ k e. A ) -> [ l / k ] B e. CC ) <-> ( ( ph /\ l e. A ) -> [_ l / k ]_ B e. CC ) )
53 42 52 bitri 
 |-  ( [ l / k ] ( ( ph /\ k e. A ) -> B e. CC ) <-> ( ( ph /\ l e. A ) -> [_ l / k ]_ B e. CC ) )
54 41 53 mpbi 
 |-  ( ( ph /\ l e. A ) -> [_ l / k ]_ B e. CC )
55 3 54 gsumfsum 
 |-  ( ph -> ( CCfld gsum ( l e. A |-> [_ l / k ]_ B ) ) = sum_ l e. A [_ l / k ]_ B )
56 nfcv 
 |-  F/_ l A
57 nfcv 
 |-  F/_ l B
58 nfcsb1v 
 |-  F/_ k [_ l / k ]_ B
59 csbeq1a 
 |-  ( k = l -> B = [_ l / k ]_ B )
60 1 56 57 58 59 cbvmptf 
 |-  ( k e. A |-> B ) = ( l e. A |-> [_ l / k ]_ B )
61 60 oveq2i 
 |-  ( CCfld gsum ( k e. A |-> B ) ) = ( CCfld gsum ( l e. A |-> [_ l / k ]_ B ) )
62 59 56 1 57 58 cbvsum 
 |-  sum_ k e. A B = sum_ l e. A [_ l / k ]_ B
63 55 61 62 3eqtr4g 
 |-  ( ph -> ( CCfld gsum ( k e. A |-> B ) ) = sum_ k e. A B )
64 32 36 63 3eqtr2d 
 |-  ( ph -> sum* k e. A B = sum_ k e. A B )