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 ⊢Ⅎ_kA
Assertion esumcl ⊢A∈V∧∀k∈AB∈0+∞→∑*k∈AB∈0+∞

Proof

Step Hyp Ref Expression
1 esumcl.1 ⊢Ⅎ_kA
2 xrge0base ⊢0+∞=Baseℝ𝑠*↾𝑠0+∞
3 xrge0cmn ⊢ℝ𝑠*↾𝑠0+∞∈CMnd
4 3 a1i ⊢A∈V∧∀k∈AB∈0+∞→ℝ𝑠*↾𝑠0+∞∈CMnd
5 xrge0tps ⊢ℝ𝑠*↾𝑠0+∞∈TopSp
6 5 a1i ⊢A∈V∧∀k∈AB∈0+∞→ℝ𝑠*↾𝑠0+∞∈TopSp
7 simpl ⊢A∈V∧∀k∈AB∈0+∞→A∈V
8 1 nfel1 ⊢ℲkA∈V
9 nfra1 ⊢Ⅎk∀k∈AB∈0+∞
10 8 9 nfan ⊢ℲkA∈V∧∀k∈AB∈0+∞
11 nfcv ⊢Ⅎ_k0+∞
12 simpr ⊢A∈V∧∀k∈AB∈0+∞→∀k∈AB∈0+∞
13 12 r19.21bi ⊢A∈V∧∀k∈AB∈0+∞∧k∈A→B∈0+∞
14 eqid ⊢k∈A⟼B=k∈A⟼B
15 10 1 11 13 14 fmptdF ⊢A∈V∧∀k∈AB∈0+∞→k∈A⟼B:A⟶0+∞
16 2 4 6 7 15 tsmscl ⊢A∈V∧∀k∈AB∈0+∞→ℝ𝑠*↾𝑠0+∞tsumsk∈A⟼B⊆0+∞
17 df-esum ⊢∑*k∈AB=⋃ℝ𝑠*↾𝑠0+∞tsumsk∈A⟼B
18 eqid ⊢ℝ𝑠*↾𝑠0+∞=ℝ𝑠*↾𝑠0+∞
19 18 7 15 xrge0tsmsbi ⊢A∈V∧∀k∈AB∈0+∞→∑*k∈AB∈ℝ𝑠*↾𝑠0+∞tsumsk∈A⟼B↔∑*k∈AB=⋃ℝ𝑠*↾𝑠0+∞tsumsk∈A⟼B
20 17 19 mpbiri ⊢A∈V∧∀k∈AB∈0+∞→∑*k∈AB∈ℝ𝑠*↾𝑠0+∞tsumsk∈A⟼B
21 16 20 sseldd ⊢A∈V∧∀k∈AB∈0+∞→∑*k∈AB∈0+∞