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({ℝ}_{𝑠}^{*}{\upharpoonright }_{𝑠}\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({ℝ}_{𝑠}^{*}{\upharpoonright }_{𝑠}\left[0,\mathrm{+\infty }\right]\right)}$$
5		xrge00	$$⊢0=0_{\left({ℝ}_{𝑠}^{*}{\upharpoonright }_{𝑠}\left[0,\mathrm{+\infty }\right]\right)}$$
6		xrge0cmn	$$⊢{ℝ}_{𝑠}^{*}{\upharpoonright }_{𝑠}\left[0,\mathrm{+\infty }\right]\in \mathrm{CMnd}$$
7	6	a1i	$$⊢\phi \to {ℝ}_{𝑠}^{*}{\upharpoonright }_{𝑠}\left[0,\mathrm{+\infty }\right]\in \mathrm{CMnd}$$
8		xrge0tps	$$⊢{ℝ}_{𝑠}^{*}{\upharpoonright }_{𝑠}\left[0,\mathrm{+\infty }\right]\in \mathrm{TopSp}$$
9	8	a1i	$$⊢\phi \to {ℝ}_{𝑠}^{*}{\upharpoonright }_{𝑠}\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({ℝ}_{𝑠}^{*}{\upharpoonright }_{𝑠}\left[0,\mathrm{+\infty }\right]\right)=\mathrm{ordTop}\left(\le \right){\upharpoonright }_{𝑡}\left[0,\mathrm{+\infty }\right]$$
18	17	eqcomi	$$⊢\mathrm{ordTop}\left(\le \right){\upharpoonright }_{𝑡}\left[0,\mathrm{+\infty }\right]=\mathrm{TopOpen}\left({ℝ}_{𝑠}^{*}{\upharpoonright }_{𝑠}\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){\upharpoonright }_{𝑡}\left[0,\mathrm{+\infty }\right]\in \mathrm{Haus}$$
22	19 20 21	mp2an	$$⊢\mathrm{ordTop}\left(\le \right){\upharpoonright }_{𝑡}\left[0,\mathrm{+\infty }\right]\in \mathrm{Haus}$$
23	22	a1i	$$⊢\phi \to \mathrm{ordTop}\left(\le \right){\upharpoonright }_{𝑡}\left[0,\mathrm{+\infty }\right]\in \mathrm{Haus}$$
24	4 5 7 9 1 12 16 18 23	haustsmsid	$$⊢\phi \to \left({ℝ}_{𝑠}^{*}{\upharpoonright }_{𝑠}\left[0,\mathrm{+\infty }\right]\right)\mathrm{tsums}\left(k\in A⟼B\right)=\left\{\underset{k\in A}{{\sum }_{{ℝ}_{𝑠}^{*}{\upharpoonright }_{𝑠}\left[0,\mathrm{+\infty }\right]}}B\right\}$$
25	24	unieqd	$$⊢\phi \to \bigcup \left(\left({ℝ}_{𝑠}^{*}{\upharpoonright }_{𝑠}\left[0,\mathrm{+\infty }\right]\right)\mathrm{tsums}\left(k\in A⟼B\right)\right)=\bigcup \left\{\underset{k\in A}{{\sum }_{{ℝ}_{𝑠}^{*}{\upharpoonright }_{𝑠}\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 }_{{ℝ}_{𝑠}^{*}{\upharpoonright }_{𝑠}\left[0,\mathrm{+\infty }\right]}}B\right\}$$
27		ovex	$$⊢\underset{k\in A}{{\sum }_{{ℝ}_{𝑠}^{*}{\upharpoonright }_{𝑠}\left[0,\mathrm{+\infty }\right]}}B\in \mathrm{V}$$
28	27	unisn	$$⊢\bigcup \left\{\underset{k\in A}{{\sum }_{{ℝ}_{𝑠}^{*}{\upharpoonright }_{𝑠}\left[0,\mathrm{+\infty }\right]}}B\right\}=\underset{k\in A}{{\sum }_{{ℝ}_{𝑠}^{*}{\upharpoonright }_{𝑠}\left[0,\mathrm{+\infty }\right]}}B$$
29	26 28	eqtrdi	$$⊢\phi \to \underset{k\in A}{{\sum }^{*}}B=\underset{k\in A}{{\sum }_{{ℝ}_{𝑠}^{*}{\upharpoonright }_{𝑠}\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 }_{{ℝ}_{𝑠}^{*}{\upharpoonright }_{𝑠}\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 }_{{ℝ}_{𝑠}^{*}{\upharpoonright }_{𝑠}\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$$