# Metamath Proof Explorer

## Theorem spansni

Description: The span of a singleton in Hilbert space equals its closure. (Contributed by NM, 3-Jun-2004) (New usage is discouraged.)

Ref Expression
Hypothesis spansn.1 ${⊢}{A}\in ℋ$
Assertion spansni ${⊢}\mathrm{span}\left(\left\{{A}\right\}\right)=\perp \left(\perp \left(\left\{{A}\right\}\right)\right)$

### Proof

Step Hyp Ref Expression
1 spansn.1 ${⊢}{A}\in ℋ$
2 snssi ${⊢}{A}\in ℋ\to \left\{{A}\right\}\subseteq ℋ$
3 spanssoc ${⊢}\left\{{A}\right\}\subseteq ℋ\to \mathrm{span}\left(\left\{{A}\right\}\right)\subseteq \perp \left(\perp \left(\left\{{A}\right\}\right)\right)$
4 1 2 3 mp2b ${⊢}\mathrm{span}\left(\left\{{A}\right\}\right)\subseteq \perp \left(\perp \left(\left\{{A}\right\}\right)\right)$
5 1 elexi ${⊢}{A}\in \mathrm{V}$
6 5 snss ${⊢}{A}\in {y}↔\left\{{A}\right\}\subseteq {y}$
7 shmulcl ${⊢}\left({y}\in {\mathbf{S}}_{ℋ}\wedge {z}\in ℂ\wedge {A}\in {y}\right)\to {z}{\cdot }_{ℎ}{A}\in {y}$
8 7 3expia ${⊢}\left({y}\in {\mathbf{S}}_{ℋ}\wedge {z}\in ℂ\right)\to \left({A}\in {y}\to {z}{\cdot }_{ℎ}{A}\in {y}\right)$
9 8 ancoms ${⊢}\left({z}\in ℂ\wedge {y}\in {\mathbf{S}}_{ℋ}\right)\to \left({A}\in {y}\to {z}{\cdot }_{ℎ}{A}\in {y}\right)$
10 6 9 syl5bir ${⊢}\left({z}\in ℂ\wedge {y}\in {\mathbf{S}}_{ℋ}\right)\to \left(\left\{{A}\right\}\subseteq {y}\to {z}{\cdot }_{ℎ}{A}\in {y}\right)$
11 eleq1 ${⊢}{x}={z}{\cdot }_{ℎ}{A}\to \left({x}\in {y}↔{z}{\cdot }_{ℎ}{A}\in {y}\right)$
12 11 imbi2d ${⊢}{x}={z}{\cdot }_{ℎ}{A}\to \left(\left(\left\{{A}\right\}\subseteq {y}\to {x}\in {y}\right)↔\left(\left\{{A}\right\}\subseteq {y}\to {z}{\cdot }_{ℎ}{A}\in {y}\right)\right)$
13 10 12 syl5ibrcom ${⊢}\left({z}\in ℂ\wedge {y}\in {\mathbf{S}}_{ℋ}\right)\to \left({x}={z}{\cdot }_{ℎ}{A}\to \left(\left\{{A}\right\}\subseteq {y}\to {x}\in {y}\right)\right)$
14 13 ralrimdva ${⊢}{z}\in ℂ\to \left({x}={z}{\cdot }_{ℎ}{A}\to \forall {y}\in {\mathbf{S}}_{ℋ}\phantom{\rule{.4em}{0ex}}\left(\left\{{A}\right\}\subseteq {y}\to {x}\in {y}\right)\right)$
15 14 rexlimiv ${⊢}\exists {z}\in ℂ\phantom{\rule{.4em}{0ex}}{x}={z}{\cdot }_{ℎ}{A}\to \forall {y}\in {\mathbf{S}}_{ℋ}\phantom{\rule{.4em}{0ex}}\left(\left\{{A}\right\}\subseteq {y}\to {x}\in {y}\right)$
16 1 h1de2ci ${⊢}{x}\in \perp \left(\perp \left(\left\{{A}\right\}\right)\right)↔\exists {z}\in ℂ\phantom{\rule{.4em}{0ex}}{x}={z}{\cdot }_{ℎ}{A}$
17 vex ${⊢}{x}\in \mathrm{V}$
18 17 elspani ${⊢}\left\{{A}\right\}\subseteq ℋ\to \left({x}\in \mathrm{span}\left(\left\{{A}\right\}\right)↔\forall {y}\in {\mathbf{S}}_{ℋ}\phantom{\rule{.4em}{0ex}}\left(\left\{{A}\right\}\subseteq {y}\to {x}\in {y}\right)\right)$
19 1 2 18 mp2b ${⊢}{x}\in \mathrm{span}\left(\left\{{A}\right\}\right)↔\forall {y}\in {\mathbf{S}}_{ℋ}\phantom{\rule{.4em}{0ex}}\left(\left\{{A}\right\}\subseteq {y}\to {x}\in {y}\right)$
20 15 16 19 3imtr4i ${⊢}{x}\in \perp \left(\perp \left(\left\{{A}\right\}\right)\right)\to {x}\in \mathrm{span}\left(\left\{{A}\right\}\right)$
21 20 ssriv ${⊢}\perp \left(\perp \left(\left\{{A}\right\}\right)\right)\subseteq \mathrm{span}\left(\left\{{A}\right\}\right)$
22 4 21 eqssi ${⊢}\mathrm{span}\left(\left\{{A}\right\}\right)=\perp \left(\perp \left(\left\{{A}\right\}\right)\right)$