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	⊢ ( 𝜑 → Ⅎ 𝑘 𝐷 )
	sumpair.3	⊢ ( 𝜑 → Ⅎ 𝑘 𝐸 )
	sumupair.1	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
	sumupair.2	⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
	sumupair.3	⊢ ( 𝜑 → 𝐷 ∈ ℂ )
	sumupair.4	⊢ ( 𝜑 → 𝐸 ∈ ℂ )
	sumupair.5	⊢ ( 𝜑 → 𝐴 ≠ 𝐵 )
	sumupair.8	⊢ ( ( 𝜑 ∧ 𝑘 = 𝐴 ) → 𝐶 = 𝐷 )
	sumupair.9	⊢ ( ( 𝜑 ∧ 𝑘 = 𝐵 ) → 𝐶 = 𝐸 )
Assertion	sumpair	⊢ ( 𝜑 → Σ 𝑘 ∈ { 𝐴 , 𝐵 } 𝐶 = ( 𝐷 + 𝐸 ) )

Proof

Step	Hyp	Ref	Expression
1		sumpair.1	⊢ ( 𝜑 → Ⅎ 𝑘 𝐷 )
2		sumpair.3	⊢ ( 𝜑 → Ⅎ 𝑘 𝐸 )
3		sumupair.1	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
4		sumupair.2	⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
5		sumupair.3	⊢ ( 𝜑 → 𝐷 ∈ ℂ )
6		sumupair.4	⊢ ( 𝜑 → 𝐸 ∈ ℂ )
7		sumupair.5	⊢ ( 𝜑 → 𝐴 ≠ 𝐵 )
8		sumupair.8	⊢ ( ( 𝜑 ∧ 𝑘 = 𝐴 ) → 𝐶 = 𝐷 )
9		sumupair.9	⊢ ( ( 𝜑 ∧ 𝑘 = 𝐵 ) → 𝐶 = 𝐸 )
10		disjsn2	⊢ ( 𝐴 ≠ 𝐵 → ( { 𝐴 } ∩ { 𝐵 } ) = ∅ )
11	7 10	syl	⊢ ( 𝜑 → ( { 𝐴 } ∩ { 𝐵 } ) = ∅ )
12		df-pr	⊢ { 𝐴 , 𝐵 } = ( { 𝐴 } ∪ { 𝐵 } )
13	12	a1i	⊢ ( 𝜑 → { 𝐴 , 𝐵 } = ( { 𝐴 } ∪ { 𝐵 } ) )
14		prfi	⊢ { 𝐴 , 𝐵 } ∈ Fin
15	14	a1i	⊢ ( 𝜑 → { 𝐴 , 𝐵 } ∈ Fin )
16		elpri	⊢ ( 𝑘 ∈ { 𝐴 , 𝐵 } → ( 𝑘 = 𝐴 ∨ 𝑘 = 𝐵 ) )
17	5	adantr	⊢ ( ( 𝜑 ∧ 𝑘 = 𝐴 ) → 𝐷 ∈ ℂ )
18	8 17	eqeltrd	⊢ ( ( 𝜑 ∧ 𝑘 = 𝐴 ) → 𝐶 ∈ ℂ )
19	6	adantr	⊢ ( ( 𝜑 ∧ 𝑘 = 𝐵 ) → 𝐸 ∈ ℂ )
20	9 19	eqeltrd	⊢ ( ( 𝜑 ∧ 𝑘 = 𝐵 ) → 𝐶 ∈ ℂ )
21	18 20	jaodan	⊢ ( ( 𝜑 ∧ ( 𝑘 = 𝐴 ∨ 𝑘 = 𝐵 ) ) → 𝐶 ∈ ℂ )
22	16 21	sylan2	⊢ ( ( 𝜑 ∧ 𝑘 ∈ { 𝐴 , 𝐵 } ) → 𝐶 ∈ ℂ )
23	11 13 15 22	fsumsplit	⊢ ( 𝜑 → Σ 𝑘 ∈ { 𝐴 , 𝐵 } 𝐶 = ( Σ 𝑘 ∈ { 𝐴 } 𝐶 + Σ 𝑘 ∈ { 𝐵 } 𝐶 ) )
24		nfv	⊢ Ⅎ 𝑘 𝜑
25	1 24 8 3 5	sumsnd	⊢ ( 𝜑 → Σ 𝑘 ∈ { 𝐴 } 𝐶 = 𝐷 )
26	2 24 9 4 6	sumsnd	⊢ ( 𝜑 → Σ 𝑘 ∈ { 𝐵 } 𝐶 = 𝐸 )
27	25 26	oveq12d	⊢ ( 𝜑 → ( Σ 𝑘 ∈ { 𝐴 } 𝐶 + Σ 𝑘 ∈ { 𝐵 } 𝐶 ) = ( 𝐷 + 𝐸 ) )
28	23 27	eqtrd	⊢ ( 𝜑 → Σ 𝑘 ∈ { 𝐴 , 𝐵 } 𝐶 = ( 𝐷 + 𝐸 ) )