Metamath Proof Explorer
Description: Closure of the limit of a sequence on Hilbert space. (Contributed by NM, 16-Aug-1999) (New usage is discouraged.)
|
|
Ref |
Expression |
|
Hypothesis |
hlim.1 |
⊢ 𝐴 ∈ V |
|
Assertion |
hlimveci |
⊢ ( 𝐹 ⇝𝑣 𝐴 → 𝐴 ∈ ℋ ) |
Proof
Step |
Hyp |
Ref |
Expression |
1 |
|
hlim.1 |
⊢ 𝐴 ∈ V |
2 |
1
|
hlimi |
⊢ ( 𝐹 ⇝𝑣 𝐴 ↔ ( ( 𝐹 : ℕ ⟶ ℋ ∧ 𝐴 ∈ ℋ ) ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ ℕ ∀ 𝑧 ∈ ( ℤ≥ ‘ 𝑦 ) ( normℎ ‘ ( ( 𝐹 ‘ 𝑧 ) −ℎ 𝐴 ) ) < 𝑥 ) ) |
3 |
2
|
simplbi |
⊢ ( 𝐹 ⇝𝑣 𝐴 → ( 𝐹 : ℕ ⟶ ℋ ∧ 𝐴 ∈ ℋ ) ) |
4 |
3
|
simprd |
⊢ ( 𝐹 ⇝𝑣 𝐴 → 𝐴 ∈ ℋ ) |