This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝐴 ∈ ℋ
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 biimtrrid ⊢ ( ( 𝑧 ∈ ℂ ∧ 𝑦 ∈ 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 ‘ { 𝐴 } ) = ( ⊥ ‘ ( ⊥ ‘ { 𝐴 } ) )