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