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	⊢ ( 𝐴 ∈ ℋ → 𝐴 ∈ ( span ‘ { 𝐴 } ) )

Proof

Step	Hyp	Ref	Expression
1		h1did	⊢ ( 𝐴 ∈ ℋ → 𝐴 ∈ ( ⊥ ‘ ( ⊥ ‘ { 𝐴 } ) ) )
2		spansn	⊢ ( 𝐴 ∈ ℋ → ( span ‘ { 𝐴 } ) = ( ⊥ ‘ ( ⊥ ‘ { 𝐴 } ) ) )
3	1 2	eleqtrrd	⊢ ( 𝐴 ∈ ℋ → 𝐴 ∈ ( span ‘ { 𝐴 } ) )