Metamath Proof Explorer

Theorem h1did

Description: A generating vector belongs to the 1-dimensional subspace it generates. (Contributed by NM, 22-Jul-2001) (New usage is discouraged.)

		Ref	Expression
	Assertion	h1did	$⊢ A \in ℋ \to A \in ⊥ (⊥ (\{A\}))$

Step	Hyp	Ref	Expression
1		snssi	$⊢ A \in ℋ \to \{A\} \subseteq ℋ$
2		ococss	$⊢ \{A\} \subseteq ℋ \to \{A\} \subseteq ⊥ (⊥ (\{A\}))$
3	1 2	syl	$⊢ A \in ℋ \to \{A\} \subseteq ⊥ (⊥ (\{A\}))$
4		snssg	$⊢ A \in ℋ \to (A \in ⊥ (⊥ (\{A\})) \leftrightarrow \{A\} \subseteq ⊥ (⊥ (\{A\})))$
5	3 4	mpbird	$⊢ A \in ℋ \to A \in ⊥ (⊥ (\{A\}))$