Theorem lspprid1

Description: A member of a pair of vectors belongs to their span. (Contributed by NM, 14-May-2015)

	Ref	Expression
Hypotheses	lspprid.v	$$⊢V={\mathrm{Base}}_W$$
	lspprid.n	$$⊢N=\mathrm{LSpan}\left(W\right)$$
	lspprid.w	$$⊢\phi \to W\in \mathrm{LMod}$$
	lspprid.x	$$⊢\phi \to X\in V$$
	lspprid.y	$$⊢\phi \to Y\in V$$
Assertion	lspprid1	$$⊢\phi \to X\in N\left(\left\{X,Y\right\}\right)$$

Proof

Step	Hyp	Ref	Expression
1		lspprid.v	$$⊢V={\mathrm{Base}}_W$$
2		lspprid.n	$$⊢N=\mathrm{LSpan}\left(W\right)$$
3		lspprid.w	$$⊢\phi \to W\in \mathrm{LMod}$$
4		lspprid.x	$$⊢\phi \to X\in V$$
5		lspprid.y	$$⊢\phi \to Y\in V$$
6	4 5	prssd	$$⊢\phi \to \left\{X,Y\right\}\subseteq V$$
7		snsspr1	$$⊢\left\{X\right\}\subseteq \left\{X,Y\right\}$$
8	7	a1i	$$⊢\phi \to \left\{X\right\}\subseteq \left\{X,Y\right\}$$
9	1 2	lspss	$$⊢\left(W\in \mathrm{LMod}\wedge \left\{X,Y\right\}\subseteq V\wedge \left\{X\right\}\subseteq \left\{X,Y\right\}\right)\to N\left(\left\{X\right\}\right)\subseteq N\left(\left\{X,Y\right\}\right)$$
10	3 6 8 9	syl3anc	$$⊢\phi \to N\left(\left\{X\right\}\right)\subseteq N\left(\left\{X,Y\right\}\right)$$
11		eqid	$$⊢\mathrm{LSubSp}\left(W\right)=\mathrm{LSubSp}\left(W\right)$$
12	1 11 2 3 4 5	lspprcl	$$⊢\phi \to N\left(\left\{X,Y\right\}\right)\in \mathrm{LSubSp}\left(W\right)$$
13	1 11 2 3 12 4	ellspsn5b	$$⊢\phi \to \left(X\in N\left(\left\{X,Y\right\}\right)\leftrightarrow N\left(\left\{X\right\}\right)\subseteq N\left(\left\{X,Y\right\}\right)\right)$$
14	10 13	mpbird	$$⊢\phi \to X\in N\left(\left\{X,Y\right\}\right)$$