This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( 𝜑 → Σ 𝑘 ∈ { 𝐴 , 𝐵 } 𝐶 = ( 𝐷 + 𝐸 ) )