Theorem esumf1o

Description: Re-index an extended sum using a bijection. (Contributed by Thierry Arnoux, 6-Apr-2017)

	Ref	Expression
Hypotheses	esumf1o.0	$$⊢Ⅎn\phi$$
	esumf1o.b	$$⊢\underset{\_}{Ⅎ}nB$$
	esumf1o.d	$$⊢\underset{\_}{Ⅎ}kD$$
	esumf1o.a	$$⊢\underset{\_}{Ⅎ}nA$$
	esumf1o.c	$$⊢\underset{\_}{Ⅎ}nC$$
	esumf1o.f	$$⊢\underset{\_}{Ⅎ}nF$$
	esumf1o.1	$$⊢k=G\to B=D$$
	esumf1o.2	$$⊢\phi \to A\in V$$
	esumf1o.3	$$⊢\phi \to F:C\underset{1-1\; onto}{⟶}A$$
	esumf1o.4	$$⊢\left(\phi \wedge n\in C\right)\to F\left(n\right)=G$$
	esumf1o.5	$$⊢\left(\phi \wedge k\in A\right)\to B\in \left[0,\mathrm{+\infty }\right]$$
Assertion	esumf1o	$$⊢\phi \to \underset{k\in A}{{\sum }^{*}}B=\underset{n\in C}{{\sum }^{*}}D$$

Proof

Step	Hyp	Ref	Expression
1		esumf1o.0	$$⊢Ⅎn\phi$$
2		esumf1o.b	$$⊢\underset{\_}{Ⅎ}nB$$
3		esumf1o.d	$$⊢\underset{\_}{Ⅎ}kD$$
4		esumf1o.a	$$⊢\underset{\_}{Ⅎ}nA$$
5		esumf1o.c	$$⊢\underset{\_}{Ⅎ}nC$$
6		esumf1o.f	$$⊢\underset{\_}{Ⅎ}nF$$
7		esumf1o.1	$$⊢k=G\to B=D$$
8		esumf1o.2	$$⊢\phi \to A\in V$$
9		esumf1o.3	$$⊢\phi \to F:C\underset{1-1\; onto}{⟶}A$$
10		esumf1o.4	$$⊢\left(\phi \wedge n\in C\right)\to F\left(n\right)=G$$
11		esumf1o.5	$$⊢\left(\phi \wedge k\in A\right)\to B\in \left[0,\mathrm{+\infty }\right]$$
12		xrge0base	$$⊢\left[0,\mathrm{+\infty }\right]={\mathrm{Base}}_{\left({ℝ}_{𝑠}^{*}{\upharpoonright }_{𝑠}\left[0,\mathrm{+\infty }\right]\right)}$$
13		xrge0cmn	$$⊢{ℝ}_{𝑠}^{*}{\upharpoonright }_{𝑠}\left[0,\mathrm{+\infty }\right]\in \mathrm{CMnd}$$
14	13	a1i	$$⊢\phi \to {ℝ}_{𝑠}^{*}{\upharpoonright }_{𝑠}\left[0,\mathrm{+\infty }\right]\in \mathrm{CMnd}$$
15		xrge0tps	$$⊢{ℝ}_{𝑠}^{*}{\upharpoonright }_{𝑠}\left[0,\mathrm{+\infty }\right]\in \mathrm{TopSp}$$
16	15	a1i	$$⊢\phi \to {ℝ}_{𝑠}^{*}{\upharpoonright }_{𝑠}\left[0,\mathrm{+\infty }\right]\in \mathrm{TopSp}$$
17	11	fmpttd	$$⊢\phi \to \left(k\in A⟼B\right):A⟶\left[0,\mathrm{+\infty }\right]$$
18	12 14 16 8 17 9	tsmsf1o	$$⊢\phi \to \left({ℝ}_{𝑠}^{*}{\upharpoonright }_{𝑠}\left[0,\mathrm{+\infty }\right]\right)\mathrm{tsums}\left(k\in A⟼B\right)=\left({ℝ}_{𝑠}^{*}{\upharpoonright }_{𝑠}\left[0,\mathrm{+\infty }\right]\right)\mathrm{tsums}\left(\left(k\in A⟼B\right)\circ F\right)$$
19		f1of	$$⊢F:C\underset{1-1\; onto}{⟶}A\to F:C⟶A$$
20	9 19	syl	$$⊢\phi \to F:C⟶A$$
21	20	ffvelcdmda	$$⊢\left(\phi \wedge n\in C\right)\to F\left(n\right)\in A$$
22	10 21	eqeltrrd	$$⊢\left(\phi \wedge n\in C\right)\to G\in A$$
23	22	ex	$$⊢\phi \to \left(n\in C\to G\in A\right)$$
24	1 23	ralrimi	$$⊢\phi \to \forall n\in CG\in A$$
25	5 6 20	feqmptdf	$$⊢\phi \to F=\left(n\in C⟼F\left(n\right)\right)$$
26	1 10	mpteq2da	$$⊢\phi \to \left(n\in C⟼F\left(n\right)\right)=\left(n\in C⟼G\right)$$
27	25 26	eqtrd	$$⊢\phi \to F=\left(n\in C⟼G\right)$$
28		eqidd	$$⊢\phi \to \left(k\in A⟼B\right)=\left(k\in A⟼B\right)$$
29	2 3 5 4 1 24 27 28 7	fmptcof2	$$⊢\phi \to \left(k\in A⟼B\right)\circ F=\left(n\in C⟼D\right)$$
30	29	oveq2d	$$⊢\phi \to \left({ℝ}_{𝑠}^{*}{\upharpoonright }_{𝑠}\left[0,\mathrm{+\infty }\right]\right)\mathrm{tsums}\left(\left(k\in A⟼B\right)\circ F\right)=\left({ℝ}_{𝑠}^{*}{\upharpoonright }_{𝑠}\left[0,\mathrm{+\infty }\right]\right)\mathrm{tsums}\left(n\in C⟼D\right)$$
31	18 30	eqtrd	$$⊢\phi \to \left({ℝ}_{𝑠}^{*}{\upharpoonright }_{𝑠}\left[0,\mathrm{+\infty }\right]\right)\mathrm{tsums}\left(k\in A⟼B\right)=\left({ℝ}_{𝑠}^{*}{\upharpoonright }_{𝑠}\left[0,\mathrm{+\infty }\right]\right)\mathrm{tsums}\left(n\in C⟼D\right)$$
32	31	unieqd	$$⊢\phi \to \bigcup \left(\left({ℝ}_{𝑠}^{*}{\upharpoonright }_{𝑠}\left[0,\mathrm{+\infty }\right]\right)\mathrm{tsums}\left(k\in A⟼B\right)\right)=\bigcup \left(\left({ℝ}_{𝑠}^{*}{\upharpoonright }_{𝑠}\left[0,\mathrm{+\infty }\right]\right)\mathrm{tsums}\left(n\in C⟼D\right)\right)$$
33		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)$$
34		df-esum	$$⊢\underset{n\in C}{{\sum }^{*}}D=\bigcup \left(\left({ℝ}_{𝑠}^{*}{\upharpoonright }_{𝑠}\left[0,\mathrm{+\infty }\right]\right)\mathrm{tsums}\left(n\in C⟼D\right)\right)$$
35	32 33 34	3eqtr4g	$$⊢\phi \to \underset{k\in A}{{\sum }^{*}}B=\underset{n\in C}{{\sum }^{*}}D$$