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

Metamath Proof Explorer

Theorem spanss2

Description: A subset of Hilbert space is included in its span. (Contributed by NM, 2-Jun-2004) (New usage is discouraged.)

		Ref	Expression
	Assertion	spanss2	$⊢ A \subseteq ℋ \to A \subseteq span (A)$

Step	Hyp	Ref	Expression
1		ssintub	$⊢ A \subseteq ⋂ \{x \in S_{ℋ} \| A \subseteq x\}$
2		spanval	$⊢ A \subseteq ℋ \to span (A) = ⋂ \{x \in S_{ℋ} \| A \subseteq x\}$
3	1 2	sseqtrrid	$⊢ A \subseteq ℋ \to A \subseteq span (A)$