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 syl5eq
 |-  ( 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 clelsb3fw
 |-  ( [ 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 )