Metamath Proof Explorer

Theorem chel

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

Ref Expression
Assertion chel 
|- ( ( H e. CH /\ A e. H ) -> A e. ~H )

Proof

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