Theorem sumpair

Description: Sum of two distinct complex values. The class expression for A and B normally contain free variable k to index it. (Contributed by Glauco Siliprandi, 20-Apr-2017)

	Ref	Expression
Hypotheses	sumpair.1	$$⊢\phi \to \underset{\_}{Ⅎ}kD$$
	sumpair.3	$$⊢\phi \to \underset{\_}{Ⅎ}kE$$
	sumupair.1	$$⊢\phi \to A\in V$$
	sumupair.2	$$⊢\phi \to B\in W$$
	sumupair.3	$$⊢\phi \to D\in ℂ$$
	sumupair.4	$$⊢\phi \to E\in ℂ$$
	sumupair.5	$$⊢\phi \to A\ne B$$
	sumupair.8	$$⊢\left(\phi \wedge k=A\right)\to C=D$$
	sumupair.9	$$⊢\left(\phi \wedge k=B\right)\to C=E$$
Assertion	sumpair	$$⊢\phi \to \sum _{k\in \left\{A,B\right\}}C=D+E$$

Proof

Step	Hyp	Ref	Expression
1		sumpair.1	$$⊢\phi \to \underset{\_}{Ⅎ}kD$$
2		sumpair.3	$$⊢\phi \to \underset{\_}{Ⅎ}kE$$
3		sumupair.1	$$⊢\phi \to A\in V$$
4		sumupair.2	$$⊢\phi \to B\in W$$
5		sumupair.3	$$⊢\phi \to D\in ℂ$$
6		sumupair.4	$$⊢\phi \to E\in ℂ$$
7		sumupair.5	$$⊢\phi \to A\ne B$$
8		sumupair.8	$$⊢\left(\phi \wedge k=A\right)\to C=D$$
9		sumupair.9	$$⊢\left(\phi \wedge k=B\right)\to C=E$$
10		disjsn2	$$⊢A\ne B\to \left\{A\right\}\cap \left\{B\right\}=\varnothing$$
11	7 10	syl	$$⊢\phi \to \left\{A\right\}\cap \left\{B\right\}=\varnothing$$
12		df-pr	$$⊢\left\{A,B\right\}=\left\{A\right\}\cup \left\{B\right\}$$
13	12	a1i	$$⊢\phi \to \left\{A,B\right\}=\left\{A\right\}\cup \left\{B\right\}$$
14		prfi	$$⊢\left\{A,B\right\}\in \mathrm{Fin}$$
15	14	a1i	$$⊢\phi \to \left\{A,B\right\}\in \mathrm{Fin}$$
16		elpri	$$⊢k\in \left\{A,B\right\}\to \left(k=A\vee k=B\right)$$
17	5	adantr	$$⊢\left(\phi \wedge k=A\right)\to D\in ℂ$$
18	8 17	eqeltrd	$$⊢\left(\phi \wedge k=A\right)\to C\in ℂ$$
19	6	adantr	$$⊢\left(\phi \wedge k=B\right)\to E\in ℂ$$
20	9 19	eqeltrd	$$⊢\left(\phi \wedge k=B\right)\to C\in ℂ$$
21	18 20	jaodan	$$⊢\left(\phi \wedge \left(k=A\vee k=B\right)\right)\to C\in ℂ$$
22	16 21	sylan2	$$⊢\left(\phi \wedge k\in \left\{A,B\right\}\right)\to C\in ℂ$$
23	11 13 15 22	fsumsplit	$$⊢\phi \to \sum _{k\in \left\{A,B\right\}}C=\sum _{k\in \left\{A\right\}}C+\sum _{k\in \left\{B\right\}}C$$
24		nfv	$$⊢Ⅎk\phi$$
25	1 24 8 3 5	sumsnd	$$⊢\phi \to \sum _{k\in \left\{A\right\}}C=D$$
26	2 24 9 4 6	sumsnd	$$⊢\phi \to \sum _{k\in \left\{B\right\}}C=E$$
27	25 26	oveq12d	$$⊢\phi \to \sum _{k\in \left\{A\right\}}C+\sum _{k\in \left\{B\right\}}C=D+E$$
28	23 27	eqtrd	$$⊢\phi \to \sum _{k\in \left\{A,B\right\}}C=D+E$$