Metamath Proof Explorer


Theorem shelii

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

Ref Expression
Hypotheses shssi.1 𝐻S
sheli.1 𝐴𝐻
Assertion shelii 𝐴 ∈ ℋ

Proof

Step Hyp Ref Expression
1 shssi.1 𝐻S
2 sheli.1 𝐴𝐻
3 1 shssii 𝐻 ⊆ ℋ
4 3 2 sselii 𝐴 ∈ ℋ