Metamath Proof Explorer

Theorem esumsplit

Description: Split an extended sum into two parts. (Contributed by Thierry Arnoux, 9-May-2017)

Ref Expression
Hypotheses esumsplit.1 ⊢ Ⅎ k φ
esumsplit.2 ⊢ Ⅎ _ k A
esumsplit.3 ⊢ Ⅎ _ k B
esumsplit.4 ⊢ φ → A ∈ V
esumsplit.5 ⊢ φ → B ∈ V
esumsplit.6 ⊢ φ → A ∩ B = ∅
esumsplit.7 ⊢ φ ∧ k ∈ A → C ∈ 0 +∞
esumsplit.8 ⊢ φ ∧ k ∈ B → C ∈ 0 +∞
Assertion esumsplit ⊢ φ → ∑ * k ∈ A ∪ B C = ∑ * k ∈ A C + 𝑒 ∑ * k ∈ B C

Proof

Step Hyp Ref Expression
1 esumsplit.1 ⊢ Ⅎ k φ
2 esumsplit.2 ⊢ Ⅎ _ k A
3 esumsplit.3 ⊢ Ⅎ _ k B
4 esumsplit.4 ⊢ φ → A ∈ V
5 esumsplit.5 ⊢ φ → B ∈ V
6 esumsplit.6 ⊢ φ → A ∩ B = ∅
7 esumsplit.7 ⊢ φ ∧ k ∈ A → C ∈ 0 +∞
8 esumsplit.8 ⊢ φ ∧ k ∈ B → C ∈ 0 +∞
9 2 3 nfun ⊢ Ⅎ _ k A ∪ B
10 unexg ⊢ A ∈ V ∧ B ∈ V → A ∪ B ∈ V
11 4 5 10 syl2anc ⊢ φ → A ∪ B ∈ V
12 elun ⊢ k ∈ A ∪ B ↔ k ∈ A ∨ k ∈ B
13 7 8 jaodan ⊢ φ ∧ k ∈ A ∨ k ∈ B → C ∈ 0 +∞
14 12 13 sylan2b ⊢ φ ∧ k ∈ A ∪ B → C ∈ 0 +∞
15 xrge0base ⊢ 0 +∞ = Base ℝ 𝑠 * ↾ 𝑠 0 +∞
16 xrge0plusg ⊢ + 𝑒 = + ℝ 𝑠 * ↾ 𝑠 0 +∞
17 xrge0cmn ⊢ ℝ 𝑠 * ↾ 𝑠 0 +∞ ∈ CMnd
18 17 a1i ⊢ φ → ℝ 𝑠 * ↾ 𝑠 0 +∞ ∈ CMnd
19 xrge0tmd ⊢ ℝ 𝑠 * ↾ 𝑠 0 +∞ ∈ TopMnd
20 19 a1i ⊢ φ → ℝ 𝑠 * ↾ 𝑠 0 +∞ ∈ TopMnd
21 nfcv ⊢ Ⅎ _ k 0 +∞
22 eqid ⊢ k ∈ A ∪ B ⟼ C = k ∈ A ∪ B ⟼ C
23 1 9 21 14 22 fmptdF ⊢ φ → k ∈ A ∪ B ⟼ C : A ∪ B ⟶ 0 +∞
24 1 2 4 7 esumel ⊢ φ → ∑ * k ∈ A C ∈ ℝ 𝑠 * ↾ 𝑠 0 +∞ tsums k ∈ A ⟼ C
25 ssun1 ⊢ A ⊆ A ∪ B
26 9 2 resmptf ⊢ A ⊆ A ∪ B → k ∈ A ∪ B ⟼ C ↾ A = k ∈ A ⟼ C
27 25 26 mp1i ⊢ φ → k ∈ A ∪ B ⟼ C ↾ A = k ∈ A ⟼ C
28 27 oveq2d ⊢ φ → ℝ 𝑠 * ↾ 𝑠 0 +∞ tsums k ∈ A ∪ B ⟼ C ↾ A = ℝ 𝑠 * ↾ 𝑠 0 +∞ tsums k ∈ A ⟼ C
29 24 28 eleqtrrd ⊢ φ → ∑ * k ∈ A C ∈ ℝ 𝑠 * ↾ 𝑠 0 +∞ tsums k ∈ A ∪ B ⟼ C ↾ A
30 1 3 5 8 esumel ⊢ φ → ∑ * k ∈ B C ∈ ℝ 𝑠 * ↾ 𝑠 0 +∞ tsums k ∈ B ⟼ C
31 ssun2 ⊢ B ⊆ A ∪ B
32 9 3 resmptf ⊢ B ⊆ A ∪ B → k ∈ A ∪ B ⟼ C ↾ B = k ∈ B ⟼ C
33 31 32 mp1i ⊢ φ → k ∈ A ∪ B ⟼ C ↾ B = k ∈ B ⟼ C
34 33 oveq2d ⊢ φ → ℝ 𝑠 * ↾ 𝑠 0 +∞ tsums k ∈ A ∪ B ⟼ C ↾ B = ℝ 𝑠 * ↾ 𝑠 0 +∞ tsums k ∈ B ⟼ C
35 30 34 eleqtrrd ⊢ φ → ∑ * k ∈ B C ∈ ℝ 𝑠 * ↾ 𝑠 0 +∞ tsums k ∈ A ∪ B ⟼ C ↾ B
36 eqidd ⊢ φ → A ∪ B = A ∪ B
37 15 16 18 20 11 23 29 35 6 36 tsmssplit ⊢ φ → ∑ * k ∈ A C + 𝑒 ∑ * k ∈ B C ∈ ℝ 𝑠 * ↾ 𝑠 0 +∞ tsums k ∈ A ∪ B ⟼ C
38 1 9 11 14 37 esumid ⊢ φ → ∑ * k ∈ A ∪ B C = ∑ * k ∈ A C + 𝑒 ∑ * k ∈ B C