Theorem lspprss

Description: The span of a pair of vectors in a subspace belongs to the subspace. (Contributed by NM, 12-Jan-2015)

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

Proof

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