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 )