Metamath Proof Explorer


Theorem hlimveci

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 ( 𝐹𝑣 𝐴𝐴 ∈ ℋ )