# 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 𝑘 𝜑
fsumsplitsn.kd 𝑘 𝐷
fsumsplitsn.a ( 𝜑𝐴 ∈ Fin )
fsumsplitsn.b ( 𝜑𝐵𝑉 )
fsumsplitsn.ba ( 𝜑 → ¬ 𝐵𝐴 )
fsumsplitsn.c ( ( 𝜑𝑘𝐴 ) → 𝐶 ∈ ℂ )
fsumsplitsn.d ( 𝑘 = 𝐵𝐶 = 𝐷 )
fsumsplitsn.dcn ( 𝜑𝐷 ∈ ℂ )
Assertion fsumsplitsn ( 𝜑 → Σ 𝑘 ∈ ( 𝐴 ∪ { 𝐵 } ) 𝐶 = ( Σ 𝑘𝐴 𝐶 + 𝐷 ) )

### Proof

Step Hyp Ref Expression
1 fsumsplitsn.ph 𝑘 𝜑
2 fsumsplitsn.kd 𝑘 𝐷
3 fsumsplitsn.a ( 𝜑𝐴 ∈ Fin )
4 fsumsplitsn.b ( 𝜑𝐵𝑉 )
5 fsumsplitsn.ba ( 𝜑 → ¬ 𝐵𝐴 )
6 fsumsplitsn.c ( ( 𝜑𝑘𝐴 ) → 𝐶 ∈ ℂ )
7 fsumsplitsn.d ( 𝑘 = 𝐵𝐶 = 𝐷 )
8 fsumsplitsn.dcn ( 𝜑𝐷 ∈ ℂ )
9 disjsn ( ( 𝐴 ∩ { 𝐵 } ) = ∅ ↔ ¬ 𝐵𝐴 )
10 5 9 sylibr ( 𝜑 → ( 𝐴 ∩ { 𝐵 } ) = ∅ )
11 eqidd ( 𝜑 → ( 𝐴 ∪ { 𝐵 } ) = ( 𝐴 ∪ { 𝐵 } ) )
12 snfi { 𝐵 } ∈ Fin
13 unfi ( ( 𝐴 ∈ Fin ∧ { 𝐵 } ∈ Fin ) → ( 𝐴 ∪ { 𝐵 } ) ∈ Fin )
14 3 12 13 sylancl ( 𝜑 → ( 𝐴 ∪ { 𝐵 } ) ∈ Fin )
15 6 adantlr ( ( ( 𝜑𝑘 ∈ ( 𝐴 ∪ { 𝐵 } ) ) ∧ 𝑘𝐴 ) → 𝐶 ∈ ℂ )
16 simpll ( ( ( 𝜑𝑘 ∈ ( 𝐴 ∪ { 𝐵 } ) ) ∧ ¬ 𝑘𝐴 ) → 𝜑 )
17 elunnel1 ( ( 𝑘 ∈ ( 𝐴 ∪ { 𝐵 } ) ∧ ¬ 𝑘𝐴 ) → 𝑘 ∈ { 𝐵 } )
18 elsni ( 𝑘 ∈ { 𝐵 } → 𝑘 = 𝐵 )
19 17 18 syl ( ( 𝑘 ∈ ( 𝐴 ∪ { 𝐵 } ) ∧ ¬ 𝑘𝐴 ) → 𝑘 = 𝐵 )
20 19 adantll ( ( ( 𝜑𝑘 ∈ ( 𝐴 ∪ { 𝐵 } ) ) ∧ ¬ 𝑘𝐴 ) → 𝑘 = 𝐵 )
21 7 adantl ( ( 𝜑𝑘 = 𝐵 ) → 𝐶 = 𝐷 )
22 8 adantr ( ( 𝜑𝑘 = 𝐵 ) → 𝐷 ∈ ℂ )
23 21 22 eqeltrd ( ( 𝜑𝑘 = 𝐵 ) → 𝐶 ∈ ℂ )
24 16 20 23 syl2anc ( ( ( 𝜑𝑘 ∈ ( 𝐴 ∪ { 𝐵 } ) ) ∧ ¬ 𝑘𝐴 ) → 𝐶 ∈ ℂ )
25 15 24 pm2.61dan ( ( 𝜑𝑘 ∈ ( 𝐴 ∪ { 𝐵 } ) ) → 𝐶 ∈ ℂ )
26 1 10 11 14 25 fsumsplitf ( 𝜑 → Σ 𝑘 ∈ ( 𝐴 ∪ { 𝐵 } ) 𝐶 = ( Σ 𝑘𝐴 𝐶 + Σ 𝑘 ∈ { 𝐵 } 𝐶 ) )
27 2 7 sumsnf ( ( 𝐵𝑉𝐷 ∈ ℂ ) → Σ 𝑘 ∈ { 𝐵 } 𝐶 = 𝐷 )
28 4 8 27 syl2anc ( 𝜑 → Σ 𝑘 ∈ { 𝐵 } 𝐶 = 𝐷 )
29 28 oveq2d ( 𝜑 → ( Σ 𝑘𝐴 𝐶 + Σ 𝑘 ∈ { 𝐵 } 𝐶 ) = ( Σ 𝑘𝐴 𝐶 + 𝐷 ) )
30 26 29 eqtrd ( 𝜑 → Σ 𝑘 ∈ ( 𝐴 ∪ { 𝐵 } ) 𝐶 = ( Σ 𝑘𝐴 𝐶 + 𝐷 ) )