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 ⊢ Ⅎ 𝑘 𝜑
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 ⊢ ( 𝜑 → Σ 𝑘 ∈ 𝑈 𝐶 = ( Σ 𝑘 ∈ 𝐴 𝐶 + Σ 𝑘 ∈ 𝐵 𝐶 ) )