Theorem spanval

Description: Value of the linear span of a subset of Hilbert space. The span is the intersection of all subspaces constraining the subset. Definition of span in Schechter p. 276. (Contributed by NM, 2-Jun-2004) (Revised by Mario Carneiro, 23-Dec-2013) (New usage is discouraged.)

	Ref	Expression
Assertion	spanval	$$⊢A\subseteq \mathscr{H}\to \mathrm{span}\left(A\right)=\bigcap \left\{x\in {\mathbf{S}}_{\mathscr{H}}|A\subseteq x\right\}$$

Proof

Step	Hyp	Ref	Expression
1		df-span	$$⊢\mathrm{span}=\left(y\in 𝒫\mathscr{H}⟼\bigcap \left\{x\in {\mathbf{S}}_{\mathscr{H}}|y\subseteq x\right\}\right)$$
2		sseq1	$$⊢y=A\to \left(y\subseteq x\leftrightarrow A\subseteq x\right)$$
3	2	rabbidv	$$⊢y=A\to \left\{x\in {\mathbf{S}}_{\mathscr{H}}|y\subseteq x\right\}=\left\{x\in {\mathbf{S}}_{\mathscr{H}}|A\subseteq x\right\}$$
4	3	inteqd	$$⊢y=A\to \bigcap \left\{x\in {\mathbf{S}}_{\mathscr{H}}|y\subseteq x\right\}=\bigcap \left\{x\in {\mathbf{S}}_{\mathscr{H}}|A\subseteq x\right\}$$
5		ax-hilex	$$⊢\mathscr{H}\in \mathrm{V}$$
6	5	elpw2	$$⊢A\in 𝒫\mathscr{H}\leftrightarrow A\subseteq \mathscr{H}$$
7	6	biimpri	$$⊢A\subseteq \mathscr{H}\to A\in 𝒫\mathscr{H}$$
8		helsh	$$⊢\mathscr{H}\in {\mathbf{S}}_{\mathscr{H}}$$
9		sseq2	$$⊢x=\mathscr{H}\to \left(A\subseteq x\leftrightarrow A\subseteq \mathscr{H}\right)$$
10	9	rspcev	$$⊢\left(\mathscr{H}\in {\mathbf{S}}_{\mathscr{H}}\wedge A\subseteq \mathscr{H}\right)\to \exists x\in {\mathbf{S}}_{\mathscr{H}}A\subseteq x$$
11	8 10	mpan	$$⊢A\subseteq \mathscr{H}\to \exists x\in {\mathbf{S}}_{\mathscr{H}}A\subseteq x$$
12		intexrab	$$⊢\exists x\in {\mathbf{S}}_{\mathscr{H}}A\subseteq x\leftrightarrow \bigcap \left\{x\in {\mathbf{S}}_{\mathscr{H}}|A\subseteq x\right\}\in \mathrm{V}$$
13	11 12	sylib	$$⊢A\subseteq \mathscr{H}\to \bigcap \left\{x\in {\mathbf{S}}_{\mathscr{H}}|A\subseteq x\right\}\in \mathrm{V}$$
14	1 4 7 13	fvmptd3	$$⊢A\subseteq \mathscr{H}\to \mathrm{span}\left(A\right)=\bigcap \left\{x\in {\mathbf{S}}_{\mathscr{H}}|A\subseteq x\right\}$$