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∈AB+𝑒C=∑*k∈AB+𝑒∑*k∈AC

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 ⊢Ⅎ_kA
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∈AB∈ℝ𝑠*↾𝑠0+∞tsumsk∈A⟼B
17 4 5 1 3 esumel ⊢φ→∑*k∈AC∈ℝ𝑠*↾𝑠0+∞tsumsk∈A⟼C
18 8 9 11 13 1 14 15 16 17 tsmsadd ⊢φ→∑*k∈AB+𝑒∑*k∈AC∈ℝ𝑠*↾𝑠0+∞tsumsk∈A⟼B+𝑒fk∈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+𝑒fk∈A⟼C=k∈A⟼B+𝑒C
22 21 oveq2d ⊢φ→ℝ𝑠*↾𝑠0+∞tsumsk∈A⟼B+𝑒fk∈A⟼C=ℝ𝑠*↾𝑠0+∞tsumsk∈A⟼B+𝑒C
23 18 22 eleqtrd ⊢φ→∑*k∈AB+𝑒∑*k∈AC∈ℝ𝑠*↾𝑠0+∞tsumsk∈A⟼B+𝑒C
24 4 5 1 7 23 esumid ⊢φ→∑*k∈AB+𝑒C=∑*k∈AB+𝑒∑*k∈AC