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

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 ⊢ ( 𝜑 → Σ 𝑘 ∈ 𝐴 𝐵 = ( 𝐷 + Σ 𝑘 ∈ ( 𝐴 ∖ { 𝐶 } ) 𝐵 ) )