Theorem esumeq12dvaf

Description: Equality deduction for extended sum. (Contributed by Thierry Arnoux, 26-Mar-2017)

	Ref	Expression
Hypotheses	esumeq12dvaf.1	$$⊢Ⅎk\phi$$
	esumeq12dvaf.2	$$⊢\phi \to A=B$$
	esumeq12dvaf.3	$$⊢\left(\phi \wedge k\in A\right)\to C=D$$
Assertion	esumeq12dvaf	$$⊢\phi \to \underset{k\in A}{{\sum }^{*}}C=\underset{k\in B}{{\sum }^{*}}D$$

Proof

Step	Hyp	Ref	Expression
1		esumeq12dvaf.1	$$⊢Ⅎk\phi$$
2		esumeq12dvaf.2	$$⊢\phi \to A=B$$
3		esumeq12dvaf.3	$$⊢\left(\phi \wedge k\in A\right)\to C=D$$
4	1 2	alrimi	$$⊢\phi \to \forall kA=B$$
5	3	ex	$$⊢\phi \to \left(k\in A\to C=D\right)$$
6	1 5	ralrimi	$$⊢\phi \to \forall k\in AC=D$$
7		mpteq12f	$$⊢\left(\forall kA=B\wedge \forall k\in AC=D\right)\to \left(k\in A⟼C\right)=\left(k\in B⟼D\right)$$
8	4 6 7	syl2anc	$$⊢\phi \to \left(k\in A⟼C\right)=\left(k\in B⟼D\right)$$
9	8	oveq2d	$$⊢\phi \to \left({ℝ}_{𝑠}^{*}{\upharpoonright }_{𝑠}\left[0,\mathrm{+\infty }\right]\right)\mathrm{tsums}\left(k\in A⟼C\right)=\left({ℝ}_{𝑠}^{*}{\upharpoonright }_{𝑠}\left[0,\mathrm{+\infty }\right]\right)\mathrm{tsums}\left(k\in B⟼D\right)$$
10	9	unieqd	$$⊢\phi \to \bigcup \left(\left({ℝ}_{𝑠}^{*}{\upharpoonright }_{𝑠}\left[0,\mathrm{+\infty }\right]\right)\mathrm{tsums}\left(k\in A⟼C\right)\right)=\bigcup \left(\left({ℝ}_{𝑠}^{*}{\upharpoonright }_{𝑠}\left[0,\mathrm{+\infty }\right]\right)\mathrm{tsums}\left(k\in B⟼D\right)\right)$$
11		df-esum	$$⊢\underset{k\in A}{{\sum }^{*}}C=\bigcup \left(\left({ℝ}_{𝑠}^{*}{\upharpoonright }_{𝑠}\left[0,\mathrm{+\infty }\right]\right)\mathrm{tsums}\left(k\in A⟼C\right)\right)$$
12		df-esum	$$⊢\underset{k\in B}{{\sum }^{*}}D=\bigcup \left(\left({ℝ}_{𝑠}^{*}{\upharpoonright }_{𝑠}\left[0,\mathrm{+\infty }\right]\right)\mathrm{tsums}\left(k\in B⟼D\right)\right)$$
13	10 11 12	3eqtr4g	$$⊢\phi \to \underset{k\in A}{{\sum }^{*}}C=\underset{k\in B}{{\sum }^{*}}D$$