Metamath Proof Explorer

Theorem esumaddf

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

Ref Expression
Hypotheses esumaddf.0 ⊢ Ⅎ 𝑘 𝜑
esumaddf.a ⊢ Ⅎ 𝑘 𝐴
esumaddf.1 ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
esumaddf.2 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ( 0 [,] +∞ ) )
esumaddf.3 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐶 ∈ ( 0 [,] +∞ ) )
Assertion esumaddf ( 𝜑 → Σ* 𝑘 ∈ 𝐴 ( 𝐵 +e 𝐶 ) = ( Σ* 𝑘 ∈ 𝐴 𝐵 +e Σ* 𝑘 ∈ 𝐴 𝐶 ) )

Proof

Step Hyp Ref Expression
1 esumaddf.0 ⊢ Ⅎ 𝑘 𝜑
2 esumaddf.a ⊢ Ⅎ 𝑘 𝐴
3 esumaddf.1 ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
4 esumaddf.2 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ( 0 [,] +∞ ) )
5 esumaddf.3 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐶 ∈ ( 0 [,] +∞ ) )
6 ge0xaddcl ⊢ ( ( 𝐵 ∈ ( 0 [,] +∞ ) ∧ 𝐶 ∈ ( 0 [,] +∞ ) ) → ( 𝐵 +e 𝐶 ) ∈ ( 0 [,] +∞ ) )
7 4 5 6 syl2anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( 𝐵 +e 𝐶 ) ∈ ( 0 [,] +∞ ) )
8 xrge0base ⊢ ( 0 [,] +∞ ) = ( Base ‘ ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) )
9 xrge0plusg ⊢ +e = ( +g ‘ ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) )
10 xrge0cmn ⊢ ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) ∈ CMnd
11 10 a1i ⊢ ( 𝜑 → ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) ∈ CMnd )
12 xrge0tmd ⊢ ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) ∈ TopMnd
13 12 a1i ⊢ ( 𝜑 → ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) ∈ TopMnd )
14 nfcv ⊢ Ⅎ 𝑘 ( 0 [,] +∞ )
15 eqid ⊢ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) = ( 𝑘 ∈ 𝐴 ↦ 𝐵 )
16 1 2 14 4 15 fmptdf2 ⊢ ( 𝜑 → ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) : 𝐴 ⟶ ( 0 [,] +∞ ) )
17 eqid ⊢ ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) = ( 𝑘 ∈ 𝐴 ↦ 𝐶 )
18 1 2 14 5 17 fmptdf2 ⊢ ( 𝜑 → ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) : 𝐴 ⟶ ( 0 [,] +∞ ) )
19 1 2 3 4 esumel ⊢ ( 𝜑 → Σ* 𝑘 ∈ 𝐴 𝐵 ∈ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) tsums ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) )
20 1 2 3 5 esumel ⊢ ( 𝜑 → Σ* 𝑘 ∈ 𝐴 𝐶 ∈ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) tsums ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ) )
21 8 9 11 13 3 16 18 19 20 tsmsadd ⊢ ( 𝜑 → ( Σ* 𝑘 ∈ 𝐴 𝐵 +e Σ* 𝑘 ∈ 𝐴 𝐶 ) ∈ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) tsums ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ∘f +e ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ) ) )
22 eqidd ⊢ ( 𝜑 → ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) = ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) )
23 eqidd ⊢ ( 𝜑 → ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) = ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) )
24 1 2 3 4 5 22 23 offval2f ⊢ ( 𝜑 → ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ∘f +e ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ) = ( 𝑘 ∈ 𝐴 ↦ ( 𝐵 +e 𝐶 ) ) )
25 24 oveq2d ⊢ ( 𝜑 → ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) tsums ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ∘f +e ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ) ) = ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) tsums ( 𝑘 ∈ 𝐴 ↦ ( 𝐵 +e 𝐶 ) ) ) )
26 21 25 eleqtrd ⊢ ( 𝜑 → ( Σ* 𝑘 ∈ 𝐴 𝐵 +e Σ* 𝑘 ∈ 𝐴 𝐶 ) ∈ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) tsums ( 𝑘 ∈ 𝐴 ↦ ( 𝐵 +e 𝐶 ) ) ) )
27 1 2 3 7 26 esumid ⊢ ( 𝜑 → Σ* 𝑘 ∈ 𝐴 ( 𝐵 +e 𝐶 ) = ( Σ* 𝑘 ∈ 𝐴 𝐵 +e Σ* 𝑘 ∈ 𝐴 𝐶 ) )