Metamath Proof Explorer

Theorem spansnid

Description: A vector belongs to the span of its singleton. (Contributed by NM, 3-Jun-2004) (New usage is discouraged.)

Ref Expression
Assertion spansnid 
|- ( A e. ~H -> A e. ( span ` { A } ) )

Proof

Step Hyp Ref Expression
1 h1did 
 |-  ( A e. ~H -> A e. ( _|_ ` ( _|_ ` { A } ) ) )
2 spansn 
 |-  ( A e. ~H -> ( span ` { A } ) = ( _|_ ` ( _|_ ` { A } ) ) )
3 1 2 eleqtrrd 
 |-  ( A e. ~H -> A e. ( span ` { A } ) )