Theorem esumpr

Description: Extended sum over a pair. (Contributed by Thierry Arnoux, 2-Jan-2017)

	Ref	Expression
Hypotheses	esumpr.1	$$⊢\left(\phi \wedge k=A\right)\to C=D$$
	esumpr.2	$$⊢\left(\phi \wedge k=B\right)\to C=E$$
	esumpr.3	$$⊢\phi \to A\in V$$
	esumpr.4	$$⊢\phi \to B\in W$$
	esumpr.5	$$⊢\phi \to D\in \left[0,\mathrm{+\infty }\right]$$
	esumpr.6	$$⊢\phi \to E\in \left[0,\mathrm{+\infty }\right]$$
	esumpr.7	$$⊢\phi \to A\ne B$$
Assertion	esumpr	$$⊢\phi \to \underset{k\in \left\{A,B\right\}}{{\sum }^{*}}C=D{+}_{𝑒}E$$

Proof

Step	Hyp	Ref	Expression
1		esumpr.1	$$⊢\left(\phi \wedge k=A\right)\to C=D$$
2		esumpr.2	$$⊢\left(\phi \wedge k=B\right)\to C=E$$
3		esumpr.3	$$⊢\phi \to A\in V$$
4		esumpr.4	$$⊢\phi \to B\in W$$
5		esumpr.5	$$⊢\phi \to D\in \left[0,\mathrm{+\infty }\right]$$
6		esumpr.6	$$⊢\phi \to E\in \left[0,\mathrm{+\infty }\right]$$
7		esumpr.7	$$⊢\phi \to A\ne B$$
8		df-pr	$$⊢\left\{A,B\right\}=\left\{A\right\}\cup \left\{B\right\}$$
9		esumeq1	$$⊢\left\{A,B\right\}=\left\{A\right\}\cup \left\{B\right\}\to \underset{k\in \left\{A,B\right\}}{{\sum }^{*}}C=\underset{k\in \left\{A\right\}\cup \left\{B\right\}}{{\sum }^{*}}C$$
10	8 9	mp1i	$$⊢\phi \to \underset{k\in \left\{A,B\right\}}{{\sum }^{*}}C=\underset{k\in \left\{A\right\}\cup \left\{B\right\}}{{\sum }^{*}}C$$
11		nfv	$$⊢Ⅎk\phi$$
12		nfcv	$$⊢\underset{\_}{Ⅎ}k\left\{A\right\}$$
13		nfcv	$$⊢\underset{\_}{Ⅎ}k\left\{B\right\}$$
14		snex	$$⊢\left\{A\right\}\in \mathrm{V}$$
15	14	a1i	$$⊢\phi \to \left\{A\right\}\in \mathrm{V}$$
16		snex	$$⊢\left\{B\right\}\in \mathrm{V}$$
17	16	a1i	$$⊢\phi \to \left\{B\right\}\in \mathrm{V}$$
18		disjsn2	$$⊢A\ne B\to \left\{A\right\}\cap \left\{B\right\}=\varnothing$$
19	7 18	syl	$$⊢\phi \to \left\{A\right\}\cap \left\{B\right\}=\varnothing$$
20		elsni	$$⊢k\in \left\{A\right\}\to k=A$$
21	20 1	sylan2	$$⊢\left(\phi \wedge k\in \left\{A\right\}\right)\to C=D$$
22	5	adantr	$$⊢\left(\phi \wedge k\in \left\{A\right\}\right)\to D\in \left[0,\mathrm{+\infty }\right]$$
23	21 22	eqeltrd	$$⊢\left(\phi \wedge k\in \left\{A\right\}\right)\to C\in \left[0,\mathrm{+\infty }\right]$$
24		elsni	$$⊢k\in \left\{B\right\}\to k=B$$
25	24 2	sylan2	$$⊢\left(\phi \wedge k\in \left\{B\right\}\right)\to C=E$$
26	6	adantr	$$⊢\left(\phi \wedge k\in \left\{B\right\}\right)\to E\in \left[0,\mathrm{+\infty }\right]$$
27	25 26	eqeltrd	$$⊢\left(\phi \wedge k\in \left\{B\right\}\right)\to C\in \left[0,\mathrm{+\infty }\right]$$
28	11 12 13 15 17 19 23 27	esumsplit	$$⊢\phi \to \underset{k\in \left\{A\right\}\cup \left\{B\right\}}{{\sum }^{*}}C=\underset{k\in \left\{A\right\}}{{\sum }^{*}}C{+}_{𝑒}\underset{k\in \left\{B\right\}}{{\sum }^{*}}C$$
29	1 3 5	esumsn	$$⊢\phi \to \underset{k\in \left\{A\right\}}{{\sum }^{*}}C=D$$
30	2 4 6	esumsn	$$⊢\phi \to \underset{k\in \left\{B\right\}}{{\sum }^{*}}C=E$$
31	29 30	oveq12d	$$⊢\phi \to \underset{k\in \left\{A\right\}}{{\sum }^{*}}C{+}_{𝑒}\underset{k\in \left\{B\right\}}{{\sum }^{*}}C=D{+}_{𝑒}E$$
32	10 28 31	3eqtrd	$$⊢\phi \to \underset{k\in \left\{A,B\right\}}{{\sum }^{*}}C=D{+}_{𝑒}E$$