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 ‘ { 𝐴 } ) = ( ⊥ ‘ ( ⊥ ‘ { 𝐴 } ) ) )