Theorem esumadd

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

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

Proof

Step	Hyp	Ref	Expression
1		esumadd.0	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
2		esumadd.1	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ( 0 [,] +∞ ) )
3		esumadd.2	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐶 ∈ ( 0 [,] +∞ ) )
4		nfv	⊢ Ⅎ 𝑘 𝜑
5		nfcv	⊢ Ⅎ 𝑘 𝐴
6		ge0xaddcl	⊢ ( ( 𝐵 ∈ ( 0 [,] +∞ ) ∧ 𝐶 ∈ ( 0 [,] +∞ ) ) → ( 𝐵 +𝑒 𝐶 ) ∈ ( 0 [,] +∞ ) )
7	2 3 6	syl2anc	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( 𝐵 +𝑒 𝐶 ) ∈ ( 0 [,] +∞ ) )
8		xrge0base	⊢ ( 0 [,] +∞ ) = ( Base ‘ ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) )
9		xrge0plusg	⊢ +𝑒 = ( +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	2	fmpttd	⊢ ( 𝜑 → ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) : 𝐴 ⟶ ( 0 [,] +∞ ) )
15	3	fmpttd	⊢ ( 𝜑 → ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) : 𝐴 ⟶ ( 0 [,] +∞ ) )
16	4 5 1 2	esumel	⊢ ( 𝜑 → Σ* 𝑘 ∈ 𝐴 𝐵 ∈ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) tsums ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) )
17	4 5 1 3	esumel	⊢ ( 𝜑 → Σ* 𝑘 ∈ 𝐴 𝐶 ∈ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) tsums ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ) )
18	8 9 11 13 1 14 15 16 17	tsmsadd	⊢ ( 𝜑 → ( Σ* 𝑘 ∈ 𝐴 𝐵 +𝑒 Σ* 𝑘 ∈ 𝐴 𝐶 ) ∈ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) tsums ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ∘f +𝑒 ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ) ) )
19		eqidd	⊢ ( 𝜑 → ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) = ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) )
20		eqidd	⊢ ( 𝜑 → ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) = ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) )
21	1 2 3 19 20	offval2	⊢ ( 𝜑 → ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ∘f +𝑒 ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ) = ( 𝑘 ∈ 𝐴 ↦ ( 𝐵 +𝑒 𝐶 ) ) )
22	21	oveq2d	⊢ ( 𝜑 → ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) tsums ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ∘f +𝑒 ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ) ) = ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) tsums ( 𝑘 ∈ 𝐴 ↦ ( 𝐵 +𝑒 𝐶 ) ) ) )
23	18 22	eleqtrd	⊢ ( 𝜑 → ( Σ* 𝑘 ∈ 𝐴 𝐵 +𝑒 Σ* 𝑘 ∈ 𝐴 𝐶 ) ∈ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) tsums ( 𝑘 ∈ 𝐴 ↦ ( 𝐵 +𝑒 𝐶 ) ) ) )
24	4 5 1 7 23	esumid	⊢ ( 𝜑 → Σ* 𝑘 ∈ 𝐴 ( 𝐵 +𝑒 𝐶 ) = ( Σ* 𝑘 ∈ 𝐴 𝐵 +𝑒 Σ* 𝑘 ∈ 𝐴 𝐶 ) )