Theorem 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	$$⊢\left(A\in \mathscr{H}\wedge A\ne 0_{ℎ}\right)\to \perp \left(\perp \left(\left\{A\right\}\right)\right)\ne 0_{\mathscr{H}}$$

Proof

Step	Hyp	Ref	Expression
1		h1did	$$⊢A\in \mathscr{H}\to A\in \perp \left(\perp \left(\left\{A\right\}\right)\right)$$
2		eleq2	$$⊢\perp \left(\perp \left(\left\{A\right\}\right)\right)=0_{\mathscr{H}}\to \left(A\in \perp \left(\perp \left(\left\{A\right\}\right)\right)\leftrightarrow A\in 0_{\mathscr{H}}\right)$$
3	1 2	syl5ibcom	$$⊢A\in \mathscr{H}\to \left(\perp \left(\perp \left(\left\{A\right\}\right)\right)=0_{\mathscr{H}}\to A\in 0_{\mathscr{H}}\right)$$
4		elch0	$$⊢A\in 0_{\mathscr{H}}\leftrightarrow A=0_{ℎ}$$
5	3 4	imbitrdi	$$⊢A\in \mathscr{H}\to \left(\perp \left(\perp \left(\left\{A\right\}\right)\right)=0_{\mathscr{H}}\to A=0_{ℎ}\right)$$
6	5	necon3d	$$⊢A\in \mathscr{H}\to \left(A\ne 0_{ℎ}\to \perp \left(\perp \left(\left\{A\right\}\right)\right)\ne 0_{\mathscr{H}}\right)$$
7	6	imp	$$⊢\left(A\in \mathscr{H}\wedge A\ne 0_{ℎ}\right)\to \perp \left(\perp \left(\left\{A\right\}\right)\right)\ne 0_{\mathscr{H}}$$