Metamath Proof Explorer

Theorem esumcl

Description: Closure for extended sum in the extended positive reals. (Contributed by Thierry Arnoux, 2-Jan-2017)

Ref Expression
Hypothesis esumcl.1 ⊢ Ⅎ 𝑘 𝐴
Assertion esumcl ( ( 𝐴 ∈ 𝑉 ∧ ∀ 𝑘 ∈ 𝐴 𝐵 ∈ ( 0 [,] +∞ ) ) → Σ* 𝑘 ∈ 𝐴 𝐵 ∈ ( 0 [,] +∞ ) )

Proof

Step Hyp Ref Expression
1 esumcl.1 ⊢ Ⅎ 𝑘 𝐴
2 xrge0base ⊢ ( 0 [,] +∞ ) = ( Base ‘ ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) )
3 xrge0cmn ⊢ ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) ∈ CMnd
4 3 a1i ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ∀ 𝑘 ∈ 𝐴 𝐵 ∈ ( 0 [,] +∞ ) ) → ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) ∈ CMnd )
5 xrge0tps ⊢ ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) ∈ TopSp
6 5 a1i ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ∀ 𝑘 ∈ 𝐴 𝐵 ∈ ( 0 [,] +∞ ) ) → ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) ∈ TopSp )
7 simpl ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ∀ 𝑘 ∈ 𝐴 𝐵 ∈ ( 0 [,] +∞ ) ) → 𝐴 ∈ 𝑉 )
8 1 nfel1 ⊢ Ⅎ 𝑘 𝐴 ∈ 𝑉
9 nfra1 ⊢ Ⅎ 𝑘 ∀ 𝑘 ∈ 𝐴 𝐵 ∈ ( 0 [,] +∞ )
10 8 9 nfan ⊢ Ⅎ 𝑘 ( 𝐴 ∈ 𝑉 ∧ ∀ 𝑘 ∈ 𝐴 𝐵 ∈ ( 0 [,] +∞ ) )
11 nfcv ⊢ Ⅎ 𝑘 ( 0 [,] +∞ )
12 simpr ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ∀ 𝑘 ∈ 𝐴 𝐵 ∈ ( 0 [,] +∞ ) ) → ∀ 𝑘 ∈ 𝐴 𝐵 ∈ ( 0 [,] +∞ ) )
13 12 r19.21bi ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ ∀ 𝑘 ∈ 𝐴 𝐵 ∈ ( 0 [,] +∞ ) ) ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ( 0 [,] +∞ ) )
14 eqid ⊢ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) = ( 𝑘 ∈ 𝐴 ↦ 𝐵 )
15 10 1 11 13 14 fmptdf2 ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ∀ 𝑘 ∈ 𝐴 𝐵 ∈ ( 0 [,] +∞ ) ) → ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) : 𝐴 ⟶ ( 0 [,] +∞ ) )
16 2 4 6 7 15 tsmscl ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ∀ 𝑘 ∈ 𝐴 𝐵 ∈ ( 0 [,] +∞ ) ) → ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) tsums ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) ⊆ ( 0 [,] +∞ ) )
17 df-esum ⊢ Σ* 𝑘 ∈ 𝐴 𝐵 = ∪ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) tsums ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) )
18 eqid ⊢ ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) = ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) )
19 18 7 15 xrge0tsmsbi ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ∀ 𝑘 ∈ 𝐴 𝐵 ∈ ( 0 [,] +∞ ) ) → ( Σ* 𝑘 ∈ 𝐴 𝐵 ∈ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) tsums ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) ↔ Σ* 𝑘 ∈ 𝐴 𝐵 = ∪ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) tsums ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) ) )
20 17 19 mpbiri ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ∀ 𝑘 ∈ 𝐴 𝐵 ∈ ( 0 [,] +∞ ) ) → Σ* 𝑘 ∈ 𝐴 𝐵 ∈ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) tsums ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) )
21 16 20 sseldd ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ∀ 𝑘 ∈ 𝐴 𝐵 ∈ ( 0 [,] +∞ ) ) → Σ* 𝑘 ∈ 𝐴 𝐵 ∈ ( 0 [,] +∞ ) )