Theorem ellspsn3

Description: A member of the span of the singleton of a vector is a member of a subspace containing the vector. ( elspansn3 analog.) (Contributed by NM, 4-Jul-2014)

	Ref	Expression
Hypotheses	lspsnss.s	$$⊢S=\mathrm{LSubSp}\left(W\right)$$
	lspsnss.n	$$⊢N=\mathrm{LSpan}\left(W\right)$$
	ellspsn3.w	$$⊢\phi \to W\in \mathrm{LMod}$$
	ellspsn3.u	$$⊢\phi \to U\in S$$
	ellspsn3.x	$$⊢\phi \to X\in U$$
	ellspsn3.y	$$⊢\phi \to Y\in N\left(\left\{X\right\}\right)$$
Assertion	ellspsn3	$$⊢\phi \to Y\in U$$

Proof

Step	Hyp	Ref	Expression
1		lspsnss.s	$$⊢S=\mathrm{LSubSp}\left(W\right)$$
2		lspsnss.n	$$⊢N=\mathrm{LSpan}\left(W\right)$$
3		ellspsn3.w	$$⊢\phi \to W\in \mathrm{LMod}$$
4		ellspsn3.u	$$⊢\phi \to U\in S$$
5		ellspsn3.x	$$⊢\phi \to X\in U$$
6		ellspsn3.y	$$⊢\phi \to Y\in N\left(\left\{X\right\}\right)$$
7	1 2	lspsnss	$$⊢\left(W\in \mathrm{LMod}\wedge U\in S\wedge X\in U\right)\to N\left(\left\{X\right\}\right)\subseteq U$$
8	3 4 5 7	syl3anc	$$⊢\phi \to N\left(\left\{X\right\}\right)\subseteq U$$
9	8 6	sseldd	$$⊢\phi \to Y\in U$$