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∈AB=∑k∈AB

Proof

Step Hyp Ref Expression
1 esumpfinval.a ⊢φ→A∈Fin
2 esumpfinval.b ⊢φ∧k∈A→B∈0+∞
3 df-esum ⊢∑*k∈AB=⋃ℝ𝑠*↾𝑠0+∞tsumsk∈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 sselid ⊢φ∧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 ⊢φ→finSupp0⁡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+∞tsumsk∈A⟼B=∑ℝ𝑠*↾𝑠0+∞k∈AB
25 24 unieqd ⊢φ→⋃ℝ𝑠*↾𝑠0+∞tsumsk∈A⟼B=⋃∑ℝ𝑠*↾𝑠0+∞k∈AB
26 3 25 eqtrid ⊢φ→∑*k∈AB=⋃∑ℝ𝑠*↾𝑠0+∞k∈AB
27 ovex ⊢∑ℝ𝑠*↾𝑠0+∞k∈AB∈V
28 27 unisn ⊢⋃∑ℝ𝑠*↾𝑠0+∞k∈AB=∑ℝ𝑠*↾𝑠0+∞k∈AB
29 26 28 eqtrdi ⊢φ→∑*k∈AB=∑ℝ𝑠*↾𝑠0+∞k∈AB
30 2 fmpttd ⊢φ→k∈A⟼B:A⟶0+∞
31 esumpfinvallem ⊢A∈Fin∧k∈A⟼B:A⟶0+∞→∑ℂfldk∈AB=∑ℝ𝑠*↾𝑠0+∞k∈AB
32 1 30 31 syl2anc ⊢φ→∑ℂfldk∈AB=∑ℝ𝑠*↾𝑠0+∞k∈AB
33 rge0ssre ⊢0+∞⊆ℝ
34 ax-resscn ⊢ℝ⊆ℂ
35 33 34 sstri ⊢0+∞⊆ℂ
36 35 2 sselid ⊢φ∧k∈A→B∈ℂ
37 1 36 gsumfsum ⊢φ→∑ℂfldk∈AB=∑k∈AB
38 29 32 37 3eqtr2d ⊢φ→∑*k∈AB=∑k∈AB