Theorem lspsnel5

Description: Relationship between a vector and the 1-dim (or 0-dim) subspace it generates. (Contributed by NM, 8-Aug-2014)

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

Proof

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