Theorem ellspsn5b

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

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

Proof

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