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
|
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 ) |