Theorem esumrnmpt

Description: Rewrite an extended sum into a sum on the range of a mapping function. (Contributed by Thierry Arnoux, 27-May-2020)

	Ref	Expression
Hypotheses	esumrnmpt.0	$$⊢\underset{\_}{Ⅎ}kA$$
	esumrnmpt.1	$$⊢y=B\to C=D$$
	esumrnmpt.2	$$⊢\phi \to A\in V$$
	esumrnmpt.3	$$⊢\left(\phi \wedge k\in A\right)\to D\in \left[0,\mathrm{+\infty }\right]$$
	esumrnmpt.4	$$⊢\left(\phi \wedge k\in A\right)\to B\in \left(W\setminus \left\{\varnothing \right\}\right)$$
	esumrnmpt.5	$$⊢\phi \to \underset{k\in A}{Disj}B$$
Assertion	esumrnmpt	$$⊢\phi \to \underset{y\in \mathrm{ran}\left(k\in A⟼B\right)}{{\sum }^{*}}C=\underset{k\in A}{{\sum }^{*}}D$$

Proof

Step	Hyp	Ref	Expression
1		esumrnmpt.0	$$⊢\underset{\_}{Ⅎ}kA$$
2		esumrnmpt.1	$$⊢y=B\to C=D$$
3		esumrnmpt.2	$$⊢\phi \to A\in V$$
4		esumrnmpt.3	$$⊢\left(\phi \wedge k\in A\right)\to D\in \left[0,\mathrm{+\infty }\right]$$
5		esumrnmpt.4	$$⊢\left(\phi \wedge k\in A\right)\to B\in \left(W\setminus \left\{\varnothing \right\}\right)$$
6		esumrnmpt.5	$$⊢\phi \to \underset{k\in A}{Disj}B$$
7		eqid	$$⊢\left(k\in A⟼B\right)=\left(k\in A⟼B\right)$$
8	7	rnmpt	$$⊢\mathrm{ran}\left(k\in A⟼B\right)=\left\{z|\exists k\in Az=B\right\}$$
9		esumeq1	$$⊢\mathrm{ran}\left(k\in A⟼B\right)=\left\{z|\exists k\in Az=B\right\}\to \underset{y\in \mathrm{ran}\left(k\in A⟼B\right)}{{\sum }^{*}}C=\underset{y\in \left\{z|\exists k\in Az=B\right\}}{{\sum }^{*}}C$$
10	8 9	ax-mp	$$⊢\underset{y\in \mathrm{ran}\left(k\in A⟼B\right)}{{\sum }^{*}}C=\underset{y\in \left\{z|\exists k\in Az=B\right\}}{{\sum }^{*}}C$$
11		nfcv	$$⊢\underset{\_}{Ⅎ}kC$$
12		nfv	$$⊢Ⅎk\phi$$
13	12 1 5 6	disjdsct	$$⊢\phi \to \mathrm{Fun}{\left(k\in A⟼B\right)}^{-1}$$
14	11 12 1 2 3 13 4 5	esumc	$$⊢\phi \to \underset{k\in A}{{\sum }^{*}}D=\underset{y\in \left\{z|\exists k\in Az=B\right\}}{{\sum }^{*}}C$$
15	10 14	eqtr4id	$$⊢\phi \to \underset{y\in \mathrm{ran}\left(k\in A⟼B\right)}{{\sum }^{*}}C=\underset{k\in A}{{\sum }^{*}}D$$