elspani

Description: Membership in the span of a subset of Hilbert space. (Contributed by NM, 2-Jun-2004) (New usage is discouraged.)

		Ref	Expression
	Hypothesis	elspan.1	$⊢ B \in V$
	Assertion	elspani	$⊢ A \subseteq ℋ \to (B \in span (A) \leftrightarrow \forall x \in S_{ℋ} (A \subseteq x \to B \in x))$

Step	Hyp	Ref	Expression
1		elspan.1	$⊢ B \in V$
2		spanval	$⊢ A \subseteq ℋ \to span (A) = ⋂ \{x \in S_{ℋ} \| A \subseteq x\}$
3	2	eleq2d	$⊢ A \subseteq ℋ \to (B \in span (A) \leftrightarrow B \in ⋂ \{x \in S_{ℋ} \| A \subseteq x\})$
4	1	elintrab	$⊢ B \in ⋂ \{x \in S_{ℋ} \| A \subseteq x\} \leftrightarrow \forall x \in S_{ℋ} (A \subseteq x \to B \in x)$
5	3 4	bitrdi	$⊢ A \subseteq ℋ \to (B \in span (A) \leftrightarrow \forall x \in S_{ℋ} (A \subseteq x \to B \in x))$

Metamath Proof Explorer