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