Theorem lsmelpr

Description: Two ways to say that a vector belongs to the span of a pair of vectors. (Contributed by NM, 14-Jan-2015)

	Ref	Expression
Hypotheses	lsmelpr.v	$$⊢V={\mathrm{Base}}_W$$
	lsmelpr.n	$$⊢N=\mathrm{LSpan}\left(W\right)$$
	lsmelpr.p	$$⊢\underset{\dot{}}{\oplus }=\mathrm{LSSum}\left(W\right)$$
	lsmelpr.w	$$⊢\phi \to W\in \mathrm{LMod}$$
	lsmelpr.x	$$⊢\phi \to X\in V$$
	lsmelpr.y	$$⊢\phi \to Y\in V$$
	lsmelpr.z	$$⊢\phi \to Z\in V$$
Assertion	lsmelpr	$$⊢\phi \to \left(X\in N\left(\left\{Y,Z\right\}\right)\leftrightarrow N\left(\left\{X\right\}\right)\subseteq N\left(\left\{Y\right\}\right)\underset{\dot{}}{\oplus }N\left(\left\{Z\right\}\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		lsmelpr.v	$$⊢V={\mathrm{Base}}_W$$
2		lsmelpr.n	$$⊢N=\mathrm{LSpan}\left(W\right)$$
3		lsmelpr.p	$$⊢\underset{\dot{}}{\oplus }=\mathrm{LSSum}\left(W\right)$$
4		lsmelpr.w	$$⊢\phi \to W\in \mathrm{LMod}$$
5		lsmelpr.x	$$⊢\phi \to X\in V$$
6		lsmelpr.y	$$⊢\phi \to Y\in V$$
7		lsmelpr.z	$$⊢\phi \to Z\in V$$
8		eqid	$$⊢\mathrm{LSubSp}\left(W\right)=\mathrm{LSubSp}\left(W\right)$$
9	1 8 2 4 6 7	lspprcl	$$⊢\phi \to N\left(\left\{Y,Z\right\}\right)\in \mathrm{LSubSp}\left(W\right)$$
10	1 8 2 4 9 5	ellspsn5b	$$⊢\phi \to \left(X\in N\left(\left\{Y,Z\right\}\right)\leftrightarrow N\left(\left\{X\right\}\right)\subseteq N\left(\left\{Y,Z\right\}\right)\right)$$
11	1 2 3 4 6 7	lsmpr	$$⊢\phi \to N\left(\left\{Y,Z\right\}\right)=N\left(\left\{Y\right\}\right)\underset{\dot{}}{\oplus }N\left(\left\{Z\right\}\right)$$
12	11	sseq2d	$$⊢\phi \to \left(N\left(\left\{X\right\}\right)\subseteq N\left(\left\{Y,Z\right\}\right)\leftrightarrow N\left(\left\{X\right\}\right)\subseteq N\left(\left\{Y\right\}\right)\underset{\dot{}}{\oplus }N\left(\left\{Z\right\}\right)\right)$$
13	10 12	bitrd	$$⊢\phi \to \left(X\in N\left(\left\{Y,Z\right\}\right)\leftrightarrow N\left(\left\{X\right\}\right)\subseteq N\left(\left\{Y\right\}\right)\underset{\dot{}}{\oplus }N\left(\left\{Z\right\}\right)\right)$$