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 } ) ) )