Metamath Proof Explorer
Description: A member of a closed subspace of a Hilbert space is a vector.
(Contributed by NM, 6Oct1999) (New usage is discouraged.)


Ref 
Expression 

Hypothesis 
chssi.1 
$${\u22a2}{H}\in {\mathbf{C}}_{\mathscr{H}}$$ 

Assertion 
cheli 
$${\u22a2}{A}\in {H}\to {A}\in \mathscr{H}$$ 
Proof
Step 
Hyp 
Ref 
Expression 
1 

chssi.1 
$${\u22a2}{H}\in {\mathbf{C}}_{\mathscr{H}}$$ 
2 
1

chssii 
$${\u22a2}{H}\subseteq \mathscr{H}$$ 
3 
2

sseli 
$${\u22a2}{A}\in {H}\to {A}\in \mathscr{H}$$ 