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 φ A Fin
esumpfinval.b φ k A B 0 +∞
Assertion esumpfinval φ * k A B = k A B

Proof

Step Hyp Ref Expression
1 esumpfinval.a φ A Fin
2 esumpfinval.b φ k A B 0 +∞
3 df-esum * k A B = 𝑠 * 𝑠 0 +∞ tsums k A B
4 xrge0base 0 +∞ = Base 𝑠 * 𝑠 0 +∞
5 xrge00 0 = 0 𝑠 * 𝑠 0 +∞
6 xrge0cmn 𝑠 * 𝑠 0 +∞ CMnd
7 6 a1i φ 𝑠 * 𝑠 0 +∞ CMnd
8 xrge0tps 𝑠 * 𝑠 0 +∞ TopSp
9 8 a1i φ 𝑠 * 𝑠 0 +∞ TopSp
10 icossicc 0 +∞ 0 +∞
11 10 2 sseldi φ k A B 0 +∞
12 11 fmpttd φ k A B : A 0 +∞
13 eqid k A B = k A B
14 c0ex 0 V
15 14 a1i φ 0 V
16 13 1 2 15 fsuppmptdm φ finSupp 0 k A B
17 xrge0topn TopOpen 𝑠 * 𝑠 0 +∞ = ordTop 𝑡 0 +∞
18 17 eqcomi ordTop 𝑡 0 +∞ = TopOpen 𝑠 * 𝑠 0 +∞
19 xrhaus ordTop Haus
20 ovex 0 +∞ V
21 resthaus ordTop Haus 0 +∞ V ordTop 𝑡 0 +∞ Haus
22 19 20 21 mp2an ordTop 𝑡 0 +∞ Haus
23 22 a1i φ ordTop 𝑡 0 +∞ Haus
24 4 5 7 9 1 12 16 18 23 haustsmsid φ 𝑠 * 𝑠 0 +∞ tsums k A B = 𝑠 * 𝑠 0 +∞ k A B
25 24 unieqd φ 𝑠 * 𝑠 0 +∞ tsums k A B = 𝑠 * 𝑠 0 +∞ k A B
26 3 25 syl5eq φ * k A B = 𝑠 * 𝑠 0 +∞ k A B
27 ovex 𝑠 * 𝑠 0 +∞ k A B V
28 27 unisn 𝑠 * 𝑠 0 +∞ k A B = 𝑠 * 𝑠 0 +∞ k A B
29 26 28 syl6eq φ * k A B = 𝑠 * 𝑠 0 +∞ k A B
30 2 fmpttd φ k A B : A 0 +∞
31 esumpfinvallem A Fin k A B : A 0 +∞ fld k A B = 𝑠 * 𝑠 0 +∞ k A B
32 1 30 31 syl2anc φ fld k A B = 𝑠 * 𝑠 0 +∞ k A B
33 rge0ssre 0 +∞
34 ax-resscn
35 33 34 sstri 0 +∞
36 35 2 sseldi φ k A B
37 1 36 gsumfsum φ fld k A B = k A B
38 29 32 37 3eqtr2d φ * k A B = k A B