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 e. SH /\ A e. H ) -> A e. ~H )

Proof

Step Hyp Ref Expression
1 shss
 |-  ( H e. SH -> H C_ ~H )
2 1 sselda
 |-  ( ( H e. SH /\ A e. H ) -> A e. ~H )