This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cheli

Description: A member of a closed subspace of a Hilbert space is a vector. (Contributed by NM, 6-Oct-1999) (New usage is discouraged.)

Ref Expression
Hypothesis chssi.1 ⊢ 𝐻 ∈ Cℋ
Assertion cheli ( 𝐴 ∈ 𝐻 → 𝐴 ∈ ℋ )

Proof

Step Hyp Ref Expression
1 chssi.1 ⊢ 𝐻 ∈ Cℋ
2 1 chssii ⊢ 𝐻 ⊆ ℋ
3 2 sseli ⊢ ( 𝐴 ∈ 𝐻 → 𝐴 ∈ ℋ )