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 \in ℋ \to A \in span (\{A\})$

Step	Hyp	Ref	Expression
1		h1did	$⊢ A \in ℋ \to A \in ⊥ (⊥ (\{A\}))$
2		spansn	$⊢ A \in ℋ \to span (\{A\}) = ⊥ (⊥ (\{A\}))$
3	1 2	eleqtrrd	$⊢ A \in ℋ \to A \in span (\{A\})$