Theorem sh1dle

Description: A 1-dimensional subspace is less than or equal to any subspace containing its generating vector. (Contributed by NM, 24-Nov-2004) (New usage is discouraged.)

	Ref	Expression
Assertion	sh1dle	$$⊢\left(A\in {\mathbf{S}}_{\mathscr{H}}\wedge B\in A\right)\to \perp \left(\perp \left(\left\{B\right\}\right)\right)\subseteq A$$

Proof

Step	Hyp	Ref	Expression
1		shel	$$⊢\left(A\in {\mathbf{S}}_{\mathscr{H}}\wedge B\in A\right)\to B\in \mathscr{H}$$
2		spansn	$$⊢B\in \mathscr{H}\to \mathrm{span}\left(\left\{B\right\}\right)=\perp \left(\perp \left(\left\{B\right\}\right)\right)$$
3	1 2	syl	$$⊢\left(A\in {\mathbf{S}}_{\mathscr{H}}\wedge B\in A\right)\to \mathrm{span}\left(\left\{B\right\}\right)=\perp \left(\perp \left(\left\{B\right\}\right)\right)$$
4		spansnss	$$⊢\left(A\in {\mathbf{S}}_{\mathscr{H}}\wedge B\in A\right)\to \mathrm{span}\left(\left\{B\right\}\right)\subseteq A$$
5	3 4	eqsstrrd	$$⊢\left(A\in {\mathbf{S}}_{\mathscr{H}}\wedge B\in A\right)\to \perp \left(\perp \left(\left\{B\right\}\right)\right)\subseteq A$$