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