# 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 ${⊢}{\phi }\to {A}\in \mathrm{Fin}$
esumpfinval.b ${⊢}\left({\phi }\wedge {k}\in {A}\right)\to {B}\in \left[0,\mathrm{+\infty }\right)$
Assertion esumpfinval ${⊢}{\phi }\to \underset{{k}\in {A}}{{\sum }^{*}}{B}=\sum _{{k}\in {A}}{B}$

### Proof

Step Hyp Ref Expression
1 esumpfinval.a ${⊢}{\phi }\to {A}\in \mathrm{Fin}$
2 esumpfinval.b ${⊢}\left({\phi }\wedge {k}\in {A}\right)\to {B}\in \left[0,\mathrm{+\infty }\right)$
3 df-esum ${⊢}\underset{{k}\in {A}}{{\sum }^{*}}{B}=\bigcup \left(\left({ℝ}_{𝑠}^{*}{↾}_{𝑠}\left[0,\mathrm{+\infty }\right]\right)\mathrm{tsums}\left({k}\in {A}⟼{B}\right)\right)$
4 xrge0base ${⊢}\left[0,\mathrm{+\infty }\right]={\mathrm{Base}}_{\left({ℝ}_{𝑠}^{*}{↾}_{𝑠}\left[0,\mathrm{+\infty }\right]\right)}$
5 xrge00 ${⊢}0={0}_{\left({ℝ}_{𝑠}^{*}{↾}_{𝑠}\left[0,\mathrm{+\infty }\right]\right)}$
6 xrge0cmn ${⊢}{ℝ}_{𝑠}^{*}{↾}_{𝑠}\left[0,\mathrm{+\infty }\right]\in \mathrm{CMnd}$
7 6 a1i ${⊢}{\phi }\to {ℝ}_{𝑠}^{*}{↾}_{𝑠}\left[0,\mathrm{+\infty }\right]\in \mathrm{CMnd}$
8 xrge0tps ${⊢}{ℝ}_{𝑠}^{*}{↾}_{𝑠}\left[0,\mathrm{+\infty }\right]\in \mathrm{TopSp}$
9 8 a1i ${⊢}{\phi }\to {ℝ}_{𝑠}^{*}{↾}_{𝑠}\left[0,\mathrm{+\infty }\right]\in \mathrm{TopSp}$
10 icossicc ${⊢}\left[0,\mathrm{+\infty }\right)\subseteq \left[0,\mathrm{+\infty }\right]$
11 10 2 sseldi ${⊢}\left({\phi }\wedge {k}\in {A}\right)\to {B}\in \left[0,\mathrm{+\infty }\right]$
12 11 fmpttd ${⊢}{\phi }\to \left({k}\in {A}⟼{B}\right):{A}⟶\left[0,\mathrm{+\infty }\right]$
13 eqid ${⊢}\left({k}\in {A}⟼{B}\right)=\left({k}\in {A}⟼{B}\right)$
14 c0ex ${⊢}0\in \mathrm{V}$
15 14 a1i ${⊢}{\phi }\to 0\in \mathrm{V}$
16 13 1 2 15 fsuppmptdm ${⊢}{\phi }\to {finSupp}_{0}\left(\left({k}\in {A}⟼{B}\right)\right)$
17 xrge0topn ${⊢}\mathrm{TopOpen}\left({ℝ}_{𝑠}^{*}{↾}_{𝑠}\left[0,\mathrm{+\infty }\right]\right)=\mathrm{ordTop}\left(\le \right){↾}_{𝑡}\left[0,\mathrm{+\infty }\right]$
18 17 eqcomi ${⊢}\mathrm{ordTop}\left(\le \right){↾}_{𝑡}\left[0,\mathrm{+\infty }\right]=\mathrm{TopOpen}\left({ℝ}_{𝑠}^{*}{↾}_{𝑠}\left[0,\mathrm{+\infty }\right]\right)$
19 xrhaus ${⊢}\mathrm{ordTop}\left(\le \right)\in \mathrm{Haus}$
20 ovex ${⊢}\left[0,\mathrm{+\infty }\right]\in \mathrm{V}$
21 resthaus ${⊢}\left(\mathrm{ordTop}\left(\le \right)\in \mathrm{Haus}\wedge \left[0,\mathrm{+\infty }\right]\in \mathrm{V}\right)\to \mathrm{ordTop}\left(\le \right){↾}_{𝑡}\left[0,\mathrm{+\infty }\right]\in \mathrm{Haus}$
22 19 20 21 mp2an ${⊢}\mathrm{ordTop}\left(\le \right){↾}_{𝑡}\left[0,\mathrm{+\infty }\right]\in \mathrm{Haus}$
23 22 a1i ${⊢}{\phi }\to \mathrm{ordTop}\left(\le \right){↾}_{𝑡}\left[0,\mathrm{+\infty }\right]\in \mathrm{Haus}$
24 4 5 7 9 1 12 16 18 23 haustsmsid ${⊢}{\phi }\to \left({ℝ}_{𝑠}^{*}{↾}_{𝑠}\left[0,\mathrm{+\infty }\right]\right)\mathrm{tsums}\left({k}\in {A}⟼{B}\right)=\left\{\underset{{k}\in {A}}{{\sum }_{{ℝ}_{𝑠}^{*}{↾}_{𝑠}\left[0,\mathrm{+\infty }\right]}}{B}\right\}$
25 24 unieqd ${⊢}{\phi }\to \bigcup \left(\left({ℝ}_{𝑠}^{*}{↾}_{𝑠}\left[0,\mathrm{+\infty }\right]\right)\mathrm{tsums}\left({k}\in {A}⟼{B}\right)\right)=\bigcup \left\{\underset{{k}\in {A}}{{\sum }_{{ℝ}_{𝑠}^{*}{↾}_{𝑠}\left[0,\mathrm{+\infty }\right]}}{B}\right\}$
26 3 25 syl5eq ${⊢}{\phi }\to \underset{{k}\in {A}}{{\sum }^{*}}{B}=\bigcup \left\{\underset{{k}\in {A}}{{\sum }_{{ℝ}_{𝑠}^{*}{↾}_{𝑠}\left[0,\mathrm{+\infty }\right]}}{B}\right\}$
27 ovex ${⊢}\underset{{k}\in {A}}{{\sum }_{{ℝ}_{𝑠}^{*}{↾}_{𝑠}\left[0,\mathrm{+\infty }\right]}}{B}\in \mathrm{V}$
28 27 unisn ${⊢}\bigcup \left\{\underset{{k}\in {A}}{{\sum }_{{ℝ}_{𝑠}^{*}{↾}_{𝑠}\left[0,\mathrm{+\infty }\right]}}{B}\right\}=\underset{{k}\in {A}}{{\sum }_{{ℝ}_{𝑠}^{*}{↾}_{𝑠}\left[0,\mathrm{+\infty }\right]}}{B}$
29 26 28 syl6eq ${⊢}{\phi }\to \underset{{k}\in {A}}{{\sum }^{*}}{B}=\underset{{k}\in {A}}{{\sum }_{{ℝ}_{𝑠}^{*}{↾}_{𝑠}\left[0,\mathrm{+\infty }\right]}}{B}$
30 2 fmpttd ${⊢}{\phi }\to \left({k}\in {A}⟼{B}\right):{A}⟶\left[0,\mathrm{+\infty }\right)$
31 esumpfinvallem ${⊢}\left({A}\in \mathrm{Fin}\wedge \left({k}\in {A}⟼{B}\right):{A}⟶\left[0,\mathrm{+\infty }\right)\right)\to \underset{{k}\in {A}}{{\sum }_{{ℂ}_{\mathrm{fld}}}}{B}=\underset{{k}\in {A}}{{\sum }_{{ℝ}_{𝑠}^{*}{↾}_{𝑠}\left[0,\mathrm{+\infty }\right]}}{B}$
32 1 30 31 syl2anc ${⊢}{\phi }\to \underset{{k}\in {A}}{{\sum }_{{ℂ}_{\mathrm{fld}}}}{B}=\underset{{k}\in {A}}{{\sum }_{{ℝ}_{𝑠}^{*}{↾}_{𝑠}\left[0,\mathrm{+\infty }\right]}}{B}$
33 rge0ssre ${⊢}\left[0,\mathrm{+\infty }\right)\subseteq ℝ$
34 ax-resscn ${⊢}ℝ\subseteq ℂ$
35 33 34 sstri ${⊢}\left[0,\mathrm{+\infty }\right)\subseteq ℂ$
36 35 2 sseldi ${⊢}\left({\phi }\wedge {k}\in {A}\right)\to {B}\in ℂ$
37 1 36 gsumfsum ${⊢}{\phi }\to \underset{{k}\in {A}}{{\sum }_{{ℂ}_{\mathrm{fld}}}}{B}=\sum _{{k}\in {A}}{B}$
38 29 32 37 3eqtr2d ${⊢}{\phi }\to \underset{{k}\in {A}}{{\sum }^{*}}{B}=\sum _{{k}\in {A}}{B}$