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	⊢ 𝐴 ∈ ℋ
Assertion	spansni	⊢ ( span ‘ { 𝐴 } ) = ( ⊥ ‘ ( ⊥ ‘ { 𝐴 } ) )

Proof

Step	Hyp	Ref	Expression
1		spansn.1	⊢ 𝐴 ∈ ℋ
2		snssi	⊢ ( 𝐴 ∈ ℋ → { 𝐴 } ⊆ ℋ )
3		spanssoc	⊢ ( { 𝐴 } ⊆ ℋ → ( span ‘ { 𝐴 } ) ⊆ ( ⊥ ‘ ( ⊥ ‘ { 𝐴 } ) ) )
4	1 2 3	mp2b	⊢ ( span ‘ { 𝐴 } ) ⊆ ( ⊥ ‘ ( ⊥ ‘ { 𝐴 } ) )
5	1	elexi	⊢ 𝐴 ∈ V
6	5	snss	⊢ ( 𝐴 ∈ 𝑦 ↔ { 𝐴 } ⊆ 𝑦 )
7		shmulcl	⊢ ( ( 𝑦 ∈ Sℋ ∧ 𝑧 ∈ ℂ ∧ 𝐴 ∈ 𝑦 ) → ( 𝑧 ·ℎ 𝐴 ) ∈ 𝑦 )
8	7	3expia	⊢ ( ( 𝑦 ∈ Sℋ ∧ 𝑧 ∈ ℂ ) → ( 𝐴 ∈ 𝑦 → ( 𝑧 ·ℎ 𝐴 ) ∈ 𝑦 ) )
9	8	ancoms	⊢ ( ( 𝑧 ∈ ℂ ∧ 𝑦 ∈ Sℋ ) → ( 𝐴 ∈ 𝑦 → ( 𝑧 ·ℎ 𝐴 ) ∈ 𝑦 ) )
10	6 9	syl5bir	⊢ ( ( 𝑧 ∈ ℂ ∧ 𝑦 ∈ Sℋ ) → ( { 𝐴 } ⊆ 𝑦 → ( 𝑧 ·ℎ 𝐴 ) ∈ 𝑦 ) )
11		eleq1	⊢ ( 𝑥 = ( 𝑧 ·ℎ 𝐴 ) → ( 𝑥 ∈ 𝑦 ↔ ( 𝑧 ·ℎ 𝐴 ) ∈ 𝑦 ) )
12	11	imbi2d	⊢ ( 𝑥 = ( 𝑧 ·ℎ 𝐴 ) → ( ( { 𝐴 } ⊆ 𝑦 → 𝑥 ∈ 𝑦 ) ↔ ( { 𝐴 } ⊆ 𝑦 → ( 𝑧 ·ℎ 𝐴 ) ∈ 𝑦 ) ) )
13	10 12	syl5ibrcom	⊢ ( ( 𝑧 ∈ ℂ ∧ 𝑦 ∈ Sℋ ) → ( 𝑥 = ( 𝑧 ·ℎ 𝐴 ) → ( { 𝐴 } ⊆ 𝑦 → 𝑥 ∈ 𝑦 ) ) )
14	13	ralrimdva	⊢ ( 𝑧 ∈ ℂ → ( 𝑥 = ( 𝑧 ·ℎ 𝐴 ) → ∀ 𝑦 ∈ Sℋ ( { 𝐴 } ⊆ 𝑦 → 𝑥 ∈ 𝑦 ) ) )
15	14	rexlimiv	⊢ ( ∃ 𝑧 ∈ ℂ 𝑥 = ( 𝑧 ·ℎ 𝐴 ) → ∀ 𝑦 ∈ Sℋ ( { 𝐴 } ⊆ 𝑦 → 𝑥 ∈ 𝑦 ) )
16	1	h1de2ci	⊢ ( 𝑥 ∈ ( ⊥ ‘ ( ⊥ ‘ { 𝐴 } ) ) ↔ ∃ 𝑧 ∈ ℂ 𝑥 = ( 𝑧 ·ℎ 𝐴 ) )
17		vex	⊢ 𝑥 ∈ V
18	17	elspani	⊢ ( { 𝐴 } ⊆ ℋ → ( 𝑥 ∈ ( span ‘ { 𝐴 } ) ↔ ∀ 𝑦 ∈ Sℋ ( { 𝐴 } ⊆ 𝑦 → 𝑥 ∈ 𝑦 ) ) )
19	1 2 18	mp2b	⊢ ( 𝑥 ∈ ( span ‘ { 𝐴 } ) ↔ ∀ 𝑦 ∈ Sℋ ( { 𝐴 } ⊆ 𝑦 → 𝑥 ∈ 𝑦 ) )
20	15 16 19	3imtr4i	⊢ ( 𝑥 ∈ ( ⊥ ‘ ( ⊥ ‘ { 𝐴 } ) ) → 𝑥 ∈ ( span ‘ { 𝐴 } ) )
21	20	ssriv	⊢ ( ⊥ ‘ ( ⊥ ‘ { 𝐴 } ) ) ⊆ ( span ‘ { 𝐴 } )
22	4 21	eqssi	⊢ ( span ‘ { 𝐴 } ) = ( ⊥ ‘ ( ⊥ ‘ { 𝐴 } ) )