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

Metamath Proof Explorer

Theorem spansn

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

Ref Expression
Assertion spansn ( 𝐴 ∈ ℋ → ( span ‘ { 𝐴 } ) = ( ⊥ ‘ ( ⊥ ‘ { 𝐴 } ) ) )

Proof

Step Hyp Ref Expression
1 sneq ⊢ ( 𝐴 = if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) → { 𝐴 } = { if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) } )
2 1 fveq2d ⊢ ( 𝐴 = if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) → ( span ‘ { 𝐴 } ) = ( span ‘ { if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) } ) )
3 1 fveq2d ⊢ ( 𝐴 = if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) → ( ⊥ ‘ { 𝐴 } ) = ( ⊥ ‘ { if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) } ) )
4 3 fveq2d ⊢ ( 𝐴 = if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) → ( ⊥ ‘ ( ⊥ ‘ { 𝐴 } ) ) = ( ⊥ ‘ ( ⊥ ‘ { if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) } ) ) )
5 2 4 eqeq12d ⊢ ( 𝐴 = if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) → ( ( span ‘ { 𝐴 } ) = ( ⊥ ‘ ( ⊥ ‘ { 𝐴 } ) ) ↔ ( span ‘ { if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) } ) = ( ⊥ ‘ ( ⊥ ‘ { if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) } ) ) ) )
6 ifhvhv0 ⊢ if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) ∈ ℋ
7 6 spansni ⊢ ( span ‘ { if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) } ) = ( ⊥ ‘ ( ⊥ ‘ { if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) } ) )
8 5 7 dedth ⊢ ( 𝐴 ∈ ℋ → ( span ‘ { 𝐴 } ) = ( ⊥ ‘ ( ⊥ ‘ { 𝐴 } ) ) )