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 ⊢ k = A → C = D
sumpr.2 ⊢ k = B → C = E
sumpr.3 ⊢ φ → D ∈ ℂ ∧ E ∈ ℂ
sumpr.4 ⊢ φ → A ∈ V ∧ B ∈ W
sumpr.5 ⊢ φ → A ≠ B
Assertion sumpr ⊢ φ → ∑ k ∈ A B C = D + E

Proof

Step Hyp Ref Expression
1 sumpr.1 ⊢ k = A → C = D
2 sumpr.2 ⊢ k = B → C = E
3 sumpr.3 ⊢ φ → D ∈ ℂ ∧ E ∈ ℂ
4 sumpr.4 ⊢ φ → A ∈ V ∧ B ∈ W
5 sumpr.5 ⊢ φ → A ≠ B
6 disjsn2 ⊢ A ≠ B → A ∩ B = ∅
7 5 6 syl ⊢ φ → A ∩ B = ∅
8 df-pr ⊢ A B = A ∪ B
9 8 a1i ⊢ φ → A B = A ∪ B
10 prfi ⊢ A B ∈ Fin
11 10 a1i ⊢ φ → A B ∈ Fin
12 1 eleq1d ⊢ k = A → C ∈ ℂ ↔ D ∈ ℂ
13 2 eleq1d ⊢ k = B → C ∈ ℂ ↔ E ∈ ℂ
14 12 13 ralprg ⊢ A ∈ V ∧ B ∈ W → ∀ k ∈ A B C ∈ ℂ ↔ D ∈ ℂ ∧ E ∈ ℂ
15 4 14 syl ⊢ φ → ∀ k ∈ A B C ∈ ℂ ↔ D ∈ ℂ ∧ E ∈ ℂ
16 3 15 mpbird ⊢ φ → ∀ k ∈ A B C ∈ ℂ
17 16 r19.21bi ⊢ φ ∧ k ∈ A B → C ∈ ℂ
18 7 9 11 17 fsumsplit ⊢ φ → ∑ k ∈ A B C = ∑ k ∈ A C + ∑ k ∈ B C
19 4 simpld ⊢ φ → A ∈ V
20 3 simpld ⊢ φ → D ∈ ℂ
21 1 sumsn ⊢ A ∈ V ∧ D ∈ ℂ → ∑ k ∈ A C = D
22 19 20 21 syl2anc ⊢ φ → ∑ k ∈ A C = D
23 4 simprd ⊢ φ → B ∈ W
24 3 simprd ⊢ φ → E ∈ ℂ
25 2 sumsn ⊢ B ∈ W ∧ E ∈ ℂ → ∑ k ∈ B C = E
26 23 24 25 syl2anc ⊢ φ → ∑ k ∈ B C = E
27 22 26 oveq12d ⊢ φ → ∑ k ∈ A C + ∑ k ∈ B C = D + E
28 18 27 eqtrd ⊢ φ → ∑ k ∈ A B C = D + E