Theorem ellspsn5

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

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

Proof

Step	Hyp	Ref	Expression
1		ellspsn5.s	$$⊢S=\mathrm{LSubSp}\left(W\right)$$
2		ellspsn5.n	$$⊢N=\mathrm{LSpan}\left(W\right)$$
3		ellspsn5.w	$$⊢\phi \to W\in \mathrm{LMod}$$
4		ellspsn5.a	$$⊢\phi \to U\in S$$
5		ellspsn5.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	ellspsn5b	$$⊢\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$$