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

Metamath Proof Explorer

Theorem sheli

Description: A member of a subspace of a Hilbert space is a vector. (Contributed by NM, 6-Oct-1999) (New usage is discouraged.)

		Ref	Expression
	Hypothesis	shssi.1	$⊢ H \in S_{ℋ}$
	Assertion	sheli	$⊢ A \in H \to A \in ℋ$

Step	Hyp	Ref	Expression
1		shssi.1	$⊢ H \in S_{ℋ}$
2	1	shssii	$⊢ H \subseteq ℋ$
3	2	sseli	$⊢ A \in H \to A \in ℋ$