Theorem fsumsplitf

Description: Split a sum into two parts. A version of fsumsplit using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 5-Apr-2020)

	Ref	Expression
Hypotheses	fsumsplitf.ph	⊢ Ⅎ 𝑘 𝜑
	fsumsplitf.ab	⊢ ( 𝜑 → ( 𝐴 ∩ 𝐵 ) = ∅ )
	fsumsplitf.u	⊢ ( 𝜑 → 𝑈 = ( 𝐴 ∪ 𝐵 ) )
	fsumsplitf.fi	⊢ ( 𝜑 → 𝑈 ∈ Fin )
	fsumsplitf.c	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑈 ) → 𝐶 ∈ ℂ )
Assertion	fsumsplitf	⊢ ( 𝜑 → Σ 𝑘 ∈ 𝑈 𝐶 = ( Σ 𝑘 ∈ 𝐴 𝐶 + Σ 𝑘 ∈ 𝐵 𝐶 ) )

Proof

Step	Hyp	Ref	Expression
1		fsumsplitf.ph	⊢ Ⅎ 𝑘 𝜑
2		fsumsplitf.ab	⊢ ( 𝜑 → ( 𝐴 ∩ 𝐵 ) = ∅ )
3		fsumsplitf.u	⊢ ( 𝜑 → 𝑈 = ( 𝐴 ∪ 𝐵 ) )
4		fsumsplitf.fi	⊢ ( 𝜑 → 𝑈 ∈ Fin )
5		fsumsplitf.c	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑈 ) → 𝐶 ∈ ℂ )
6		csbeq1a	⊢ ( 𝑘 = 𝑗 → 𝐶 = ⦋ 𝑗 / 𝑘 ⦌ 𝐶 )
7		nfcv	⊢ Ⅎ 𝑗 𝐶
8		nfcsb1v	⊢ Ⅎ 𝑘 ⦋ 𝑗 / 𝑘 ⦌ 𝐶
9	6 7 8	cbvsum	⊢ Σ 𝑘 ∈ 𝑈 𝐶 = Σ 𝑗 ∈ 𝑈 ⦋ 𝑗 / 𝑘 ⦌ 𝐶
10	9	a1i	⊢ ( 𝜑 → Σ 𝑘 ∈ 𝑈 𝐶 = Σ 𝑗 ∈ 𝑈 ⦋ 𝑗 / 𝑘 ⦌ 𝐶 )
11		nfv	⊢ Ⅎ 𝑘 𝑗 ∈ 𝑈
12	1 11	nfan	⊢ Ⅎ 𝑘 ( 𝜑 ∧ 𝑗 ∈ 𝑈 )
13	8	nfel1	⊢ Ⅎ 𝑘 ⦋ 𝑗 / 𝑘 ⦌ 𝐶 ∈ ℂ
14	12 13	nfim	⊢ Ⅎ 𝑘 ( ( 𝜑 ∧ 𝑗 ∈ 𝑈 ) → ⦋ 𝑗 / 𝑘 ⦌ 𝐶 ∈ ℂ )
15		eleq1w	⊢ ( 𝑘 = 𝑗 → ( 𝑘 ∈ 𝑈 ↔ 𝑗 ∈ 𝑈 ) )
16	15	anbi2d	⊢ ( 𝑘 = 𝑗 → ( ( 𝜑 ∧ 𝑘 ∈ 𝑈 ) ↔ ( 𝜑 ∧ 𝑗 ∈ 𝑈 ) ) )
17	6	eleq1d	⊢ ( 𝑘 = 𝑗 → ( 𝐶 ∈ ℂ ↔ ⦋ 𝑗 / 𝑘 ⦌ 𝐶 ∈ ℂ ) )
18	16 17	imbi12d	⊢ ( 𝑘 = 𝑗 → ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑈 ) → 𝐶 ∈ ℂ ) ↔ ( ( 𝜑 ∧ 𝑗 ∈ 𝑈 ) → ⦋ 𝑗 / 𝑘 ⦌ 𝐶 ∈ ℂ ) ) )
19	14 18 5	chvarfv	⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑈 ) → ⦋ 𝑗 / 𝑘 ⦌ 𝐶 ∈ ℂ )
20	2 3 4 19	fsumsplit	⊢ ( 𝜑 → Σ 𝑗 ∈ 𝑈 ⦋ 𝑗 / 𝑘 ⦌ 𝐶 = ( Σ 𝑗 ∈ 𝐴 ⦋ 𝑗 / 𝑘 ⦌ 𝐶 + Σ 𝑗 ∈ 𝐵 ⦋ 𝑗 / 𝑘 ⦌ 𝐶 ) )
21		csbeq1a	⊢ ( 𝑗 = 𝑘 → ⦋ 𝑗 / 𝑘 ⦌ 𝐶 = ⦋ 𝑘 / 𝑗 ⦌ ⦋ 𝑗 / 𝑘 ⦌ 𝐶 )
22		csbcow	⊢ ⦋ 𝑘 / 𝑗 ⦌ ⦋ 𝑗 / 𝑘 ⦌ 𝐶 = ⦋ 𝑘 / 𝑘 ⦌ 𝐶
23		csbid	⊢ ⦋ 𝑘 / 𝑘 ⦌ 𝐶 = 𝐶
24	22 23	eqtri	⊢ ⦋ 𝑘 / 𝑗 ⦌ ⦋ 𝑗 / 𝑘 ⦌ 𝐶 = 𝐶
25	21 24	eqtrdi	⊢ ( 𝑗 = 𝑘 → ⦋ 𝑗 / 𝑘 ⦌ 𝐶 = 𝐶 )
26	25 8 7	cbvsum	⊢ Σ 𝑗 ∈ 𝐴 ⦋ 𝑗 / 𝑘 ⦌ 𝐶 = Σ 𝑘 ∈ 𝐴 𝐶
27	25 8 7	cbvsum	⊢ Σ 𝑗 ∈ 𝐵 ⦋ 𝑗 / 𝑘 ⦌ 𝐶 = Σ 𝑘 ∈ 𝐵 𝐶
28	26 27	oveq12i	⊢ ( Σ 𝑗 ∈ 𝐴 ⦋ 𝑗 / 𝑘 ⦌ 𝐶 + Σ 𝑗 ∈ 𝐵 ⦋ 𝑗 / 𝑘 ⦌ 𝐶 ) = ( Σ 𝑘 ∈ 𝐴 𝐶 + Σ 𝑘 ∈ 𝐵 𝐶 )
29	28	a1i	⊢ ( 𝜑 → ( Σ 𝑗 ∈ 𝐴 ⦋ 𝑗 / 𝑘 ⦌ 𝐶 + Σ 𝑗 ∈ 𝐵 ⦋ 𝑗 / 𝑘 ⦌ 𝐶 ) = ( Σ 𝑘 ∈ 𝐴 𝐶 + Σ 𝑘 ∈ 𝐵 𝐶 ) )
30	10 20 29	3eqtrd	⊢ ( 𝜑 → Σ 𝑘 ∈ 𝑈 𝐶 = ( Σ 𝑘 ∈ 𝐴 𝐶 + Σ 𝑘 ∈ 𝐵 𝐶 ) )