h1dn0

Description: A nonzero vector generates a (nonzero) 1-dimensional subspace. (Contributed by NM, 22-Jul-2001) (New usage is discouraged.)

		Ref	Expression
	Assertion	h1dn0	$⊢ (A \in ℋ \land A \neq 0_{ℎ}) \to ⊥ (⊥ (\{A\})) \neq 0_{ℋ}$

Step	Hyp	Ref	Expression
1		h1did	$⊢ A \in ℋ \to A \in ⊥ (⊥ (\{A\}))$
2		eleq2	$⊢ ⊥ (⊥ (\{A\})) = 0_{ℋ} \to (A \in ⊥ (⊥ (\{A\})) \leftrightarrow A \in 0_{ℋ})$
3	1 2	syl5ibcom	$⊢ A \in ℋ \to (⊥ (⊥ (\{A\})) = 0_{ℋ} \to A \in 0_{ℋ})$
4		elch0	$⊢ A \in 0_{ℋ} \leftrightarrow A = 0_{ℎ}$
5	3 4	syl6ib	$⊢ A \in ℋ \to (⊥ (⊥ (\{A\})) = 0_{ℋ} \to A = 0_{ℎ})$
6	5	necon3d	$⊢ A \in ℋ \to (A \neq 0_{ℎ} \to ⊥ (⊥ (\{A\})) \neq 0_{ℋ})$
7	6	imp	$⊢ (A \in ℋ \land A \neq 0_{ℎ}) \to ⊥ (⊥ (\{A\})) \neq 0_{ℋ}$

Metamath Proof Explorer