Metamath Proof Explorer

Theorem esumaddf

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

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

Proof

Step Hyp Ref Expression
1 esumaddf.0 ⊢ Ⅎ k φ
2 esumaddf.a ⊢ Ⅎ _ k A
3 esumaddf.1 ⊢ φ → A ∈ V
4 esumaddf.2 ⊢ φ ∧ k ∈ A → B ∈ 0 +∞
5 esumaddf.3 ⊢ φ ∧ k ∈ A → C ∈ 0 +∞
6 ge0xaddcl ⊢ B ∈ 0 +∞ ∧ C ∈ 0 +∞ → B + 𝑒 C ∈ 0 +∞
7 4 5 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 nfcv ⊢ Ⅎ _ k 0 +∞
15 eqid ⊢ k ∈ A ⟼ B = k ∈ A ⟼ B
16 1 2 14 4 15 fmptdf2 ⊢ φ → k ∈ A ⟼ B : A ⟶ 0 +∞
17 eqid ⊢ k ∈ A ⟼ C = k ∈ A ⟼ C
18 1 2 14 5 17 fmptdf2 ⊢ φ → k ∈ A ⟼ C : A ⟶ 0 +∞
19 1 2 3 4 esumel ⊢ φ → ∑ * k ∈ A B ∈ ℝ 𝑠 * ↾ 𝑠 0 +∞ tsums k ∈ A ⟼ B
20 1 2 3 5 esumel ⊢ φ → ∑ * k ∈ A C ∈ ℝ 𝑠 * ↾ 𝑠 0 +∞ tsums k ∈ A ⟼ C
21 8 9 11 13 3 16 18 19 20 tsmsadd ⊢ φ → ∑ * k ∈ A B + 𝑒 ∑ * k ∈ A C ∈ ℝ 𝑠 * ↾ 𝑠 0 +∞ tsums k ∈ A ⟼ B + 𝑒 f k ∈ A ⟼ C
22 eqidd ⊢ φ → k ∈ A ⟼ B = k ∈ A ⟼ B
23 eqidd ⊢ φ → k ∈ A ⟼ C = k ∈ A ⟼ C
24 1 2 3 4 5 22 23 offval2f ⊢ φ → k ∈ A ⟼ B + 𝑒 f k ∈ A ⟼ C = k ∈ A ⟼ B + 𝑒 C
25 24 oveq2d ⊢ φ → ℝ 𝑠 * ↾ 𝑠 0 +∞ tsums k ∈ A ⟼ B + 𝑒 f k ∈ A ⟼ C = ℝ 𝑠 * ↾ 𝑠 0 +∞ tsums k ∈ A ⟼ B + 𝑒 C
26 21 25 eleqtrd ⊢ φ → ∑ * k ∈ A B + 𝑒 ∑ * k ∈ A C ∈ ℝ 𝑠 * ↾ 𝑠 0 +∞ tsums k ∈ A ⟼ B + 𝑒 C
27 1 2 3 7 26 esumid ⊢ φ → ∑ * k ∈ A B + 𝑒 C = ∑ * k ∈ A B + 𝑒 ∑ * k ∈ A C