Metamath Proof Explorer


Theorem shel

Description: A member of a subspace of a Hilbert space is a vector. (Contributed by NM, 14-Dec-2004) (New usage is discouraged.)

Ref Expression
Assertion shel H S A H A

Proof

Step Hyp Ref Expression
1 shss H S H
2 1 sselda H S A H A