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

Metamath Proof Explorer

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 ⊢ Ⅎ k φ
fsumsplitf.ab ⊢ φ → A ∩ B = ∅
fsumsplitf.u ⊢ φ → U = A ∪ B
fsumsplitf.fi ⊢ φ → U ∈ Fin
fsumsplitf.c ⊢ φ ∧ k ∈ U → C ∈ ℂ
Assertion fsumsplitf ⊢ φ → ∑ k ∈ U C = ∑ k ∈ A C + ∑ k ∈ B C

Proof

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