This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 \in C_{ℋ} \land A \in H) \to A \in ℋ$

Step	Hyp	Ref	Expression
1		chss	$⊢ H \in C_{ℋ} \to H \subseteq ℋ$
2	1	sselda	$⊢ (H \in C_{ℋ} \land A \in H) \to A \in ℋ$