Theorem spansna

Description: The span of the singleton of a vector is an atom. (Contributed by NM, 18-Dec-2004) (New usage is discouraged.)

	Ref	Expression
Assertion	spansna	$$⊢\left(A\in \mathscr{H}\wedge A\ne 0_{ℎ}\right)\to \mathrm{span}\left(\left\{A\right\}\right)\in \mathrm{HAtoms}$$

Proof

Step	Hyp	Ref	Expression
1		spansn	$$⊢A\in \mathscr{H}\to \mathrm{span}\left(\left\{A\right\}\right)=\perp \left(\perp \left(\left\{A\right\}\right)\right)$$
2	1	adantr	$$⊢\left(A\in \mathscr{H}\wedge A\ne 0_{ℎ}\right)\to \mathrm{span}\left(\left\{A\right\}\right)=\perp \left(\perp \left(\left\{A\right\}\right)\right)$$
3		h1da	$$⊢\left(A\in \mathscr{H}\wedge A\ne 0_{ℎ}\right)\to \perp \left(\perp \left(\left\{A\right\}\right)\right)\in \mathrm{HAtoms}$$
4	2 3	eqeltrd	$$⊢\left(A\in \mathscr{H}\wedge A\ne 0_{ℎ}\right)\to \mathrm{span}\left(\left\{A\right\}\right)\in \mathrm{HAtoms}$$