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 H S
sheli.1 A H
Assertion shelii A

Proof

Step Hyp Ref Expression
1 shssi.1 H S
2 sheli.1 A H
3 1 shssii H
4 3 2 sselii A