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

Metamath Proof Explorer

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

Proof

Step Hyp Ref Expression
1 sumpair.1 ⊢ φ → Ⅎ _ k D
2 sumpair.3 ⊢ φ → Ⅎ _ k E
3 sumupair.1 ⊢ φ → A ∈ V
4 sumupair.2 ⊢ φ → B ∈ W
5 sumupair.3 ⊢ φ → D ∈ ℂ
6 sumupair.4 ⊢ φ → E ∈ ℂ
7 sumupair.5 ⊢ φ → A ≠ B
8 sumupair.8 ⊢ φ ∧ k = A → C = D
9 sumupair.9 ⊢ φ ∧ k = B → C = E
10 disjsn2 ⊢ A ≠ B → A ∩ B = ∅
11 7 10 syl ⊢ φ → A ∩ B = ∅
12 df-pr ⊢ A B = A ∪ B
13 12 a1i ⊢ φ → A B = A ∪ B
14 prfi ⊢ A B ∈ Fin
15 14 a1i ⊢ φ → A B ∈ Fin
16 elpri ⊢ k ∈ A B → k = A ∨ k = B
17 5 adantr ⊢ φ ∧ k = A → D ∈ ℂ
18 8 17 eqeltrd ⊢ φ ∧ k = A → C ∈ ℂ
19 6 adantr ⊢ φ ∧ k = B → E ∈ ℂ
20 9 19 eqeltrd ⊢ φ ∧ k = B → C ∈ ℂ
21 18 20 jaodan ⊢ φ ∧ k = A ∨ k = B → C ∈ ℂ
22 16 21 sylan2 ⊢ φ ∧ k ∈ A B → C ∈ ℂ
23 11 13 15 22 fsumsplit ⊢ φ → ∑ k ∈ A B C = ∑ k ∈ A C + ∑ k ∈ B C
24 nfv ⊢ Ⅎ k φ
25 1 24 8 3 5 sumsnd ⊢ φ → ∑ k ∈ A C = D
26 2 24 9 4 6 sumsnd ⊢ φ → ∑ k ∈ B C = E
27 25 26 oveq12d ⊢ φ → ∑ k ∈ A C + ∑ k ∈ B C = D + E
28 23 27 eqtrd ⊢ φ → ∑ k ∈ A B C = D + E