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

Proof

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