Theorem lspprid2

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	lspprid2	$$⊢\phi \to Y\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	1 2 3 5 4	lspprid1	$$⊢\phi \to Y\in N\left(\left\{Y,X\right\}\right)$$
7		prcom	$$⊢\left\{Y,X\right\}=\left\{X,Y\right\}$$
8	7	fveq2i	$$⊢N\left(\left\{Y,X\right\}\right)=N\left(\left\{X,Y\right\}\right)$$
9	6 8	eleqtrdi	$$⊢\phi \to Y\in N\left(\left\{X,Y\right\}\right)$$