Metamath Proof Explorer

Theorem fsumsplitsn

Description: Separate out a term in a finite sum. (Contributed by Glauco Siliprandi, 5-Apr-2020)

Ref Expression
Hypotheses fsumsplitsn.ph ⊢ Ⅎ k φ
fsumsplitsn.kd ⊢ Ⅎ _ k D
fsumsplitsn.a ⊢ φ → A ∈ Fin
fsumsplitsn.b ⊢ φ → B ∈ V
fsumsplitsn.ba ⊢ φ → ¬ B ∈ A
fsumsplitsn.c ⊢ φ ∧ k ∈ A → C ∈ ℂ
fsumsplitsn.d ⊢ k = B → C = D
fsumsplitsn.dcn ⊢ φ → D ∈ ℂ
Assertion fsumsplitsn ⊢ φ → ∑ k ∈ A ∪ B C = ∑ k ∈ A C + D

Proof

Step Hyp Ref Expression
1 fsumsplitsn.ph ⊢ Ⅎ k φ
2 fsumsplitsn.kd ⊢ Ⅎ _ k D
3 fsumsplitsn.a ⊢ φ → A ∈ Fin
4 fsumsplitsn.b ⊢ φ → B ∈ V
5 fsumsplitsn.ba ⊢ φ → ¬ B ∈ A
6 fsumsplitsn.c ⊢ φ ∧ k ∈ A → C ∈ ℂ
7 fsumsplitsn.d ⊢ k = B → C = D
8 fsumsplitsn.dcn ⊢ φ → D ∈ ℂ
9 disjsn ⊢ A ∩ B = ∅ ↔ ¬ B ∈ A
10 5 9 sylibr ⊢ φ → A ∩ B = ∅
11 eqidd ⊢ φ → A ∪ B = A ∪ B
12 snfi ⊢ B ∈ Fin
13 unfi ⊢ A ∈ Fin ∧ B ∈ Fin → A ∪ B ∈ Fin
14 3 12 13 sylancl ⊢ φ → A ∪ B ∈ Fin
15 6 adantlr ⊢ φ ∧ k ∈ A ∪ B ∧ k ∈ A → C ∈ ℂ
16 simpll ⊢ φ ∧ k ∈ A ∪ B ∧ ¬ k ∈ A → φ
17 elunnel1 ⊢ k ∈ A ∪ B ∧ ¬ k ∈ A → k ∈ B
18 elsni ⊢ k ∈ B → k = B
19 17 18 syl ⊢ k ∈ A ∪ B ∧ ¬ k ∈ A → k = B
20 19 adantll ⊢ φ ∧ k ∈ A ∪ B ∧ ¬ k ∈ A → k = B
21 7 adantl ⊢ φ ∧ k = B → C = D
22 8 adantr ⊢ φ ∧ k = B → D ∈ ℂ
23 21 22 eqeltrd ⊢ φ ∧ k = B → C ∈ ℂ
24 16 20 23 syl2anc ⊢ φ ∧ k ∈ A ∪ B ∧ ¬ k ∈ A → C ∈ ℂ
25 15 24 pm2.61dan ⊢ φ ∧ k ∈ A ∪ B → C ∈ ℂ
26 1 10 11 14 25 fsumsplitf ⊢ φ → ∑ k ∈ A ∪ B C = ∑ k ∈ A C + ∑ k ∈ B C
27 2 7 sumsnf ⊢ B ∈ V ∧ D ∈ ℂ → ∑ k ∈ B C = D
28 4 8 27 syl2anc ⊢ φ → ∑ k ∈ B C = D
29 28 oveq2d ⊢ φ → ∑ k ∈ A C + ∑ k ∈ B C = ∑ k ∈ A C + D
30 26 29 eqtrd ⊢ φ → ∑ k ∈ A ∪ B C = ∑ k ∈ A C + D