Metamath Proof Explorer

Theorem esumadd

Description: Addition of infinite sums. (Contributed by Thierry Arnoux, 24-Mar-2017)

Ref Expression
Hypotheses esumadd.0 ⊢ φ → A ∈ V
esumadd.1 ⊢ φ ∧ k ∈ A → B ∈ 0 +∞
esumadd.2 ⊢ φ ∧ k ∈ A → C ∈ 0 +∞
Assertion esumadd ⊢ φ → ∑ * k ∈ A B + 𝑒 C = ∑ * k ∈ A B + 𝑒 ∑ * k ∈ A C

Proof

Step Hyp Ref Expression
1 esumadd.0 ⊢ φ → A ∈ V
2 esumadd.1 ⊢ φ ∧ k ∈ A → B ∈ 0 +∞
3 esumadd.2 ⊢ φ ∧ k ∈ A → C ∈ 0 +∞
4 nfv ⊢ Ⅎ k φ
5 nfcv ⊢ Ⅎ _ k A
6 ge0xaddcl ⊢ B ∈ 0 +∞ ∧ C ∈ 0 +∞ → B + 𝑒 C ∈ 0 +∞
7 2 3 6 syl2anc ⊢ φ ∧ k ∈ A → B + 𝑒 C ∈ 0 +∞
8 xrge0base ⊢ 0 +∞ = Base ℝ 𝑠 * ↾ 𝑠 0 +∞
9 xrge0plusg ⊢ + 𝑒 = + ℝ 𝑠 * ↾ 𝑠 0 +∞
10 xrge0cmn ⊢ ℝ 𝑠 * ↾ 𝑠 0 +∞ ∈ CMnd
11 10 a1i ⊢ φ → ℝ 𝑠 * ↾ 𝑠 0 +∞ ∈ CMnd
12 xrge0tmd ⊢ ℝ 𝑠 * ↾ 𝑠 0 +∞ ∈ TopMnd
13 12 a1i ⊢ φ → ℝ 𝑠 * ↾ 𝑠 0 +∞ ∈ TopMnd
14 2 fmpttd ⊢ φ → k ∈ A ⟼ B : A ⟶ 0 +∞
15 3 fmpttd ⊢ φ → k ∈ A ⟼ C : A ⟶ 0 +∞
16 4 5 1 2 esumel ⊢ φ → ∑ * k ∈ A B ∈ ℝ 𝑠 * ↾ 𝑠 0 +∞ tsums k ∈ A ⟼ B
17 4 5 1 3 esumel ⊢ φ → ∑ * k ∈ A C ∈ ℝ 𝑠 * ↾ 𝑠 0 +∞ tsums k ∈ A ⟼ C
18 8 9 11 13 1 14 15 16 17 tsmsadd ⊢ φ → ∑ * k ∈ A B + 𝑒 ∑ * k ∈ A C ∈ ℝ 𝑠 * ↾ 𝑠 0 +∞ tsums k ∈ A ⟼ B + 𝑒 f k ∈ A ⟼ C
19 eqidd ⊢ φ → k ∈ A ⟼ B = k ∈ A ⟼ B
20 eqidd ⊢ φ → k ∈ A ⟼ C = k ∈ A ⟼ C
21 1 2 3 19 20 offval2 ⊢ φ → k ∈ A ⟼ B + 𝑒 f k ∈ A ⟼ C = k ∈ A ⟼ B + 𝑒 C
22 21 oveq2d ⊢ φ → ℝ 𝑠 * ↾ 𝑠 0 +∞ tsums k ∈ A ⟼ B + 𝑒 f k ∈ A ⟼ C = ℝ 𝑠 * ↾ 𝑠 0 +∞ tsums k ∈ A ⟼ B + 𝑒 C
23 18 22 eleqtrd ⊢ φ → ∑ * k ∈ A B + 𝑒 ∑ * k ∈ A C ∈ ℝ 𝑠 * ↾ 𝑠 0 +∞ tsums k ∈ A ⟼ B + 𝑒 C
24 4 5 1 7 23 esumid ⊢ φ → ∑ * k ∈ A B + 𝑒 C = ∑ * k ∈ A B + 𝑒 ∑ * k ∈ A C