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∈ABC=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 ⊢AB=A∪B
9 8 a1i ⊢φ→AB=A∪B
10 prfi ⊢AB∈Fin
11 10 a1i ⊢φ→AB∈Fin
12 1 eleq1d ⊢k=A→C∈ℂ↔D∈ℂ
13 2 eleq1d ⊢k=B→C∈ℂ↔E∈ℂ
14 12 13 ralprg ⊢A∈V∧B∈W→∀k∈ABC∈ℂ↔D∈ℂ∧E∈ℂ
15 4 14 syl ⊢φ→∀k∈ABC∈ℂ↔D∈ℂ∧E∈ℂ
16 3 15 mpbird ⊢φ→∀k∈ABC∈ℂ
17 16 r19.21bi ⊢φ∧k∈AB→C∈ℂ
18 7 9 11 17 fsumsplit ⊢φ→∑k∈ABC=∑k∈AC+∑k∈BC
19 4 simpld ⊢φ→A∈V
20 3 simpld ⊢φ→D∈ℂ
21 1 sumsn ⊢A∈V∧D∈ℂ→∑k∈AC=D
22 19 20 21 syl2anc ⊢φ→∑k∈AC=D
23 4 simprd ⊢φ→B∈W
24 3 simprd ⊢φ→E∈ℂ
25 2 sumsn ⊢B∈W∧E∈ℂ→∑k∈BC=E
26 23 24 25 syl2anc ⊢φ→∑k∈BC=E
27 22 26 oveq12d ⊢φ→∑k∈AC+∑k∈BC=D+E
28 18 27 eqtrd ⊢φ→∑k∈ABC=D+E