Theorem lspsnel5a

Description: Relationship between a vector and the 1-dim (or 0-dim) subspace it generates. (Contributed by NM, 20-Feb-2015)

	Ref	Expression
Hypotheses	lspsnel5a.s	$$⊢S=\mathrm{LSubSp}\left(W\right)$$
	lspsnel5a.n	$$⊢N=\mathrm{LSpan}\left(W\right)$$
	lspsnel5a.w	$$⊢\phi \to W\in \mathrm{LMod}$$
	lspsnel5a.a	$$⊢\phi \to U\in S$$
	lspsnel5a.x	$$⊢\phi \to X\in U$$
Assertion	lspsnel5a	$$⊢\phi \to N\left(\left\{X\right\}\right)\subseteq U$$

Proof

Step	Hyp	Ref	Expression
1		lspsnel5a.s	$$⊢S=\mathrm{LSubSp}\left(W\right)$$
2		lspsnel5a.n	$$⊢N=\mathrm{LSpan}\left(W\right)$$
3		lspsnel5a.w	$$⊢\phi \to W\in \mathrm{LMod}$$
4		lspsnel5a.a	$$⊢\phi \to U\in S$$
5		lspsnel5a.x	$$⊢\phi \to X\in U$$
6		eqid	$$⊢{\mathrm{Base}}_W={\mathrm{Base}}_W$$
7	6 1	lssel	$$⊢\left(U\in S\wedge X\in U\right)\to X\in {\mathrm{Base}}_W$$
8	4 5 7	syl2anc	$$⊢\phi \to X\in {\mathrm{Base}}_W$$
9	6 1 2 3 4 8	lspsnel5	$$⊢\phi \to \left(X\in U\leftrightarrow N\left(\left\{X\right\}\right)\subseteq U\right)$$
10	5 9	mpbid	$$⊢\phi \to N\left(\left\{X\right\}\right)\subseteq U$$