# Metamath Proof Explorer

## 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 ℋ\to \mathrm{span}\left({A}\right)=\bigcap \left\{{x}\in {\mathbf{S}}_{ℋ}|{A}\subseteq {x}\right\}$

### Proof

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