# Metamath Proof Explorer

## Theorem fsumsplit1

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

Ref Expression
Hypotheses fsumsplit1.kph 𝑘 𝜑
fsumsplit1.kd 𝑘 𝐷
fsumsplit1.a ( 𝜑𝐴 ∈ Fin )
fsumsplit1.b ( ( 𝜑𝑘𝐴 ) → 𝐵 ∈ ℂ )
fsumsplit1.c ( 𝜑𝐶𝐴 )
fsumsplit1.bd ( 𝑘 = 𝐶𝐵 = 𝐷 )
Assertion fsumsplit1 ( 𝜑 → Σ 𝑘𝐴 𝐵 = ( 𝐷 + Σ 𝑘 ∈ ( 𝐴 ∖ { 𝐶 } ) 𝐵 ) )

### Proof

Step Hyp Ref Expression
1 fsumsplit1.kph 𝑘 𝜑
2 fsumsplit1.kd 𝑘 𝐷
3 fsumsplit1.a ( 𝜑𝐴 ∈ Fin )
4 fsumsplit1.b ( ( 𝜑𝑘𝐴 ) → 𝐵 ∈ ℂ )
5 fsumsplit1.c ( 𝜑𝐶𝐴 )
6 fsumsplit1.bd ( 𝑘 = 𝐶𝐵 = 𝐷 )
7 uncom ( ( 𝐴 ∖ { 𝐶 } ) ∪ { 𝐶 } ) = ( { 𝐶 } ∪ ( 𝐴 ∖ { 𝐶 } ) )
8 7 a1i ( 𝜑 → ( ( 𝐴 ∖ { 𝐶 } ) ∪ { 𝐶 } ) = ( { 𝐶 } ∪ ( 𝐴 ∖ { 𝐶 } ) ) )
9 5 snssd ( 𝜑 → { 𝐶 } ⊆ 𝐴 )
10 undif ( { 𝐶 } ⊆ 𝐴 ↔ ( { 𝐶 } ∪ ( 𝐴 ∖ { 𝐶 } ) ) = 𝐴 )
11 9 10 sylib ( 𝜑 → ( { 𝐶 } ∪ ( 𝐴 ∖ { 𝐶 } ) ) = 𝐴 )
12 eqidd ( 𝜑𝐴 = 𝐴 )
13 8 11 12 3eqtrrd ( 𝜑𝐴 = ( ( 𝐴 ∖ { 𝐶 } ) ∪ { 𝐶 } ) )
14 13 sumeq1d ( 𝜑 → Σ 𝑘𝐴 𝐵 = Σ 𝑘 ∈ ( ( 𝐴 ∖ { 𝐶 } ) ∪ { 𝐶 } ) 𝐵 )
15 diffi ( 𝐴 ∈ Fin → ( 𝐴 ∖ { 𝐶 } ) ∈ Fin )
16 3 15 syl ( 𝜑 → ( 𝐴 ∖ { 𝐶 } ) ∈ Fin )
17 neldifsnd ( 𝜑 → ¬ 𝐶 ∈ ( 𝐴 ∖ { 𝐶 } ) )
18 simpl ( ( 𝜑𝑘 ∈ ( 𝐴 ∖ { 𝐶 } ) ) → 𝜑 )
19 eldifi ( 𝑘 ∈ ( 𝐴 ∖ { 𝐶 } ) → 𝑘𝐴 )
20 19 adantl ( ( 𝜑𝑘 ∈ ( 𝐴 ∖ { 𝐶 } ) ) → 𝑘𝐴 )
21 18 20 4 syl2anc ( ( 𝜑𝑘 ∈ ( 𝐴 ∖ { 𝐶 } ) ) → 𝐵 ∈ ℂ )
22 2 a1i ( 𝜑 𝑘 𝐷 )
23 simpr ( ( 𝜑𝑘 = 𝐶 ) → 𝑘 = 𝐶 )
24 23 6 syl ( ( 𝜑𝑘 = 𝐶 ) → 𝐵 = 𝐷 )
25 1 22 5 24 csbiedf ( 𝜑 𝐶 / 𝑘 𝐵 = 𝐷 )
26 25 eqcomd ( 𝜑𝐷 = 𝐶 / 𝑘 𝐵 )
27 5 ancli ( 𝜑 → ( 𝜑𝐶𝐴 ) )
28 nfcv 𝑘 𝐶
29 nfv 𝑘 𝐶𝐴
30 1 29 nfan 𝑘 ( 𝜑𝐶𝐴 )
31 28 nfcsb1 𝑘 𝐶 / 𝑘 𝐵
32 nfcv 𝑘
33 31 32 nfel 𝑘 𝐶 / 𝑘 𝐵 ∈ ℂ
34 30 33 nfim 𝑘 ( ( 𝜑𝐶𝐴 ) → 𝐶 / 𝑘 𝐵 ∈ ℂ )
35 eleq1 ( 𝑘 = 𝐶 → ( 𝑘𝐴𝐶𝐴 ) )
36 35 anbi2d ( 𝑘 = 𝐶 → ( ( 𝜑𝑘𝐴 ) ↔ ( 𝜑𝐶𝐴 ) ) )
37 csbeq1a ( 𝑘 = 𝐶𝐵 = 𝐶 / 𝑘 𝐵 )
38 37 eleq1d ( 𝑘 = 𝐶 → ( 𝐵 ∈ ℂ ↔ 𝐶 / 𝑘 𝐵 ∈ ℂ ) )
39 36 38 imbi12d ( 𝑘 = 𝐶 → ( ( ( 𝜑𝑘𝐴 ) → 𝐵 ∈ ℂ ) ↔ ( ( 𝜑𝐶𝐴 ) → 𝐶 / 𝑘 𝐵 ∈ ℂ ) ) )
40 28 34 39 4 vtoclgf ( 𝐶𝐴 → ( ( 𝜑𝐶𝐴 ) → 𝐶 / 𝑘 𝐵 ∈ ℂ ) )
41 5 27 40 sylc ( 𝜑 𝐶 / 𝑘 𝐵 ∈ ℂ )
42 26 41 eqeltrd ( 𝜑𝐷 ∈ ℂ )
43 1 2 16 5 17 21 6 42 fsumsplitsn ( 𝜑 → Σ 𝑘 ∈ ( ( 𝐴 ∖ { 𝐶 } ) ∪ { 𝐶 } ) 𝐵 = ( Σ 𝑘 ∈ ( 𝐴 ∖ { 𝐶 } ) 𝐵 + 𝐷 ) )
44 1 16 21 fsumclf ( 𝜑 → Σ 𝑘 ∈ ( 𝐴 ∖ { 𝐶 } ) 𝐵 ∈ ℂ )
45 44 42 addcomd ( 𝜑 → ( Σ 𝑘 ∈ ( 𝐴 ∖ { 𝐶 } ) 𝐵 + 𝐷 ) = ( 𝐷 + Σ 𝑘 ∈ ( 𝐴 ∖ { 𝐶 } ) 𝐵 ) )
46 14 43 45 3eqtrd ( 𝜑 → Σ 𝑘𝐴 𝐵 = ( 𝐷 + Σ 𝑘 ∈ ( 𝐴 ∖ { 𝐶 } ) 𝐵 ) )