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 
|- ( A e. ~H -> ( span ` { A } ) = ( _|_ ` ( _|_ ` { A } ) ) )

Proof

Step Hyp Ref Expression
1 sneq 
 |-  ( A = if ( A e. ~H , A , 0h ) -> { A } = { if ( A e. ~H , A , 0h ) } )
2 1 fveq2d 
 |-  ( A = if ( A e. ~H , A , 0h ) -> ( span ` { A } ) = ( span ` { if ( A e. ~H , A , 0h ) } ) )
3 1 fveq2d 
 |-  ( A = if ( A e. ~H , A , 0h ) -> ( _|_ ` { A } ) = ( _|_ ` { if ( A e. ~H , A , 0h ) } ) )
4 3 fveq2d 
 |-  ( A = if ( A e. ~H , A , 0h ) -> ( _|_ ` ( _|_ ` { A } ) ) = ( _|_ ` ( _|_ ` { if ( A e. ~H , A , 0h ) } ) ) )
5 2 4 eqeq12d 
 |-  ( A = if ( A e. ~H , A , 0h ) -> ( ( span ` { A } ) = ( _|_ ` ( _|_ ` { A } ) ) <-> ( span ` { if ( A e. ~H , A , 0h ) } ) = ( _|_ ` ( _|_ ` { if ( A e. ~H , A , 0h ) } ) ) ) )
6 ifhvhv0 
 |-  if ( A e. ~H , A , 0h ) e. ~H
7 6 spansni 
 |-  ( span ` { if ( A e. ~H , A , 0h ) } ) = ( _|_ ` ( _|_ ` { if ( A e. ~H , A , 0h ) } ) )
8 5 7 dedth 
 |-  ( A e. ~H -> ( span ` { A } ) = ( _|_ ` ( _|_ ` { A } ) ) )