Theorem sumpr

Description: A sum over a pair is the sum of the elements. (Contributed by Thierry Arnoux, 12-Dec-2016)

	Ref	Expression
Hypotheses	sumpr.1	⊢ ( 𝑘 = 𝐴 → 𝐶 = 𝐷 )
	sumpr.2	⊢ ( 𝑘 = 𝐵 → 𝐶 = 𝐸 )
	sumpr.3	⊢ ( 𝜑 → ( 𝐷 ∈ ℂ ∧ 𝐸 ∈ ℂ ) )
	sumpr.4	⊢ ( 𝜑 → ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) )
	sumpr.5	⊢ ( 𝜑 → 𝐴 ≠ 𝐵 )
Assertion	sumpr	⊢ ( 𝜑 → Σ 𝑘 ∈ { 𝐴 , 𝐵 } 𝐶 = ( 𝐷 + 𝐸 ) )

Proof

Step	Hyp	Ref	Expression
1		sumpr.1	⊢ ( 𝑘 = 𝐴 → 𝐶 = 𝐷 )
2		sumpr.2	⊢ ( 𝑘 = 𝐵 → 𝐶 = 𝐸 )
3		sumpr.3	⊢ ( 𝜑 → ( 𝐷 ∈ ℂ ∧ 𝐸 ∈ ℂ ) )
4		sumpr.4	⊢ ( 𝜑 → ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) )
5		sumpr.5	⊢ ( 𝜑 → 𝐴 ≠ 𝐵 )
6		disjsn2	⊢ ( 𝐴 ≠ 𝐵 → ( { 𝐴 } ∩ { 𝐵 } ) = ∅ )
7	5 6	syl	⊢ ( 𝜑 → ( { 𝐴 } ∩ { 𝐵 } ) = ∅ )
8		df-pr	⊢ { 𝐴 , 𝐵 } = ( { 𝐴 } ∪ { 𝐵 } )
9	8	a1i	⊢ ( 𝜑 → { 𝐴 , 𝐵 } = ( { 𝐴 } ∪ { 𝐵 } ) )
10		prfi	⊢ { 𝐴 , 𝐵 } ∈ Fin
11	10	a1i	⊢ ( 𝜑 → { 𝐴 , 𝐵 } ∈ Fin )
12	1	eleq1d	⊢ ( 𝑘 = 𝐴 → ( 𝐶 ∈ ℂ ↔ 𝐷 ∈ ℂ ) )
13	2	eleq1d	⊢ ( 𝑘 = 𝐵 → ( 𝐶 ∈ ℂ ↔ 𝐸 ∈ ℂ ) )
14	12 13	ralprg	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ∀ 𝑘 ∈ { 𝐴 , 𝐵 } 𝐶 ∈ ℂ ↔ ( 𝐷 ∈ ℂ ∧ 𝐸 ∈ ℂ ) ) )
15	4 14	syl	⊢ ( 𝜑 → ( ∀ 𝑘 ∈ { 𝐴 , 𝐵 } 𝐶 ∈ ℂ ↔ ( 𝐷 ∈ ℂ ∧ 𝐸 ∈ ℂ ) ) )
16	3 15	mpbird	⊢ ( 𝜑 → ∀ 𝑘 ∈ { 𝐴 , 𝐵 } 𝐶 ∈ ℂ )
17	16	r19.21bi	⊢ ( ( 𝜑 ∧ 𝑘 ∈ { 𝐴 , 𝐵 } ) → 𝐶 ∈ ℂ )
18	7 9 11 17	fsumsplit	⊢ ( 𝜑 → Σ 𝑘 ∈ { 𝐴 , 𝐵 } 𝐶 = ( Σ 𝑘 ∈ { 𝐴 } 𝐶 + Σ 𝑘 ∈ { 𝐵 } 𝐶 ) )
19	4	simpld	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
20	3	simpld	⊢ ( 𝜑 → 𝐷 ∈ ℂ )
21	1	sumsn	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐷 ∈ ℂ ) → Σ 𝑘 ∈ { 𝐴 } 𝐶 = 𝐷 )
22	19 20 21	syl2anc	⊢ ( 𝜑 → Σ 𝑘 ∈ { 𝐴 } 𝐶 = 𝐷 )
23	4	simprd	⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
24	3	simprd	⊢ ( 𝜑 → 𝐸 ∈ ℂ )
25	2	sumsn	⊢ ( ( 𝐵 ∈ 𝑊 ∧ 𝐸 ∈ ℂ ) → Σ 𝑘 ∈ { 𝐵 } 𝐶 = 𝐸 )
26	23 24 25	syl2anc	⊢ ( 𝜑 → Σ 𝑘 ∈ { 𝐵 } 𝐶 = 𝐸 )
27	22 26	oveq12d	⊢ ( 𝜑 → ( Σ 𝑘 ∈ { 𝐴 } 𝐶 + Σ 𝑘 ∈ { 𝐵 } 𝐶 ) = ( 𝐷 + 𝐸 ) )
28	18 27	eqtrd	⊢ ( 𝜑 → Σ 𝑘 ∈ { 𝐴 , 𝐵 } 𝐶 = ( 𝐷 + 𝐸 ) )