Theorem lspindp2l

Description: Alternate way to say 3 vectors are mutually independent (rotate left). (Contributed by NM, 10-May-2015)

	Ref	Expression
Hypotheses	lspindp1.v	$$⊢V={\mathrm{Base}}_W$$
	lspindp1.o	$$⊢\underset{\dot{}}{0}=0_W$$
	lspindp1.n	$$⊢N=\mathrm{LSpan}\left(W\right)$$
	lspindp1.w	$$⊢\phi \to W\in \mathrm{LVec}$$
	lspindp1.y	$$⊢\phi \to X\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
	lspindp1.z	$$⊢\phi \to Y\in V$$
	lspindp1.x	$$⊢\phi \to Z\in V$$
	lspindp1.q	$$⊢\phi \to N\left(\left\{X\right\}\right)\ne N\left(\left\{Y\right\}\right)$$
	lspindp1.e	$$⊢\phi \to \neg Z\in N\left(\left\{X,Y\right\}\right)$$
Assertion	lspindp2l	$$⊢\phi \to \left(N\left(\left\{Y\right\}\right)\ne N\left(\left\{Z\right\}\right)\wedge \neg X\in N\left(\left\{Y,Z\right\}\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		lspindp1.v	$$⊢V={\mathrm{Base}}_W$$
2		lspindp1.o	$$⊢\underset{\dot{}}{0}=0_W$$
3		lspindp1.n	$$⊢N=\mathrm{LSpan}\left(W\right)$$
4		lspindp1.w	$$⊢\phi \to W\in \mathrm{LVec}$$
5		lspindp1.y	$$⊢\phi \to X\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
6		lspindp1.z	$$⊢\phi \to Y\in V$$
7		lspindp1.x	$$⊢\phi \to Z\in V$$
8		lspindp1.q	$$⊢\phi \to N\left(\left\{X\right\}\right)\ne N\left(\left\{Y\right\}\right)$$
9		lspindp1.e	$$⊢\phi \to \neg Z\in N\left(\left\{X,Y\right\}\right)$$
10	1 2 3 4 5 6 7 8 9	lspindp1	$$⊢\phi \to \left(N\left(\left\{Z\right\}\right)\ne N\left(\left\{Y\right\}\right)\wedge \neg X\in N\left(\left\{Z,Y\right\}\right)\right)$$
11	10	simpld	$$⊢\phi \to N\left(\left\{Z\right\}\right)\ne N\left(\left\{Y\right\}\right)$$
12	11	necomd	$$⊢\phi \to N\left(\left\{Y\right\}\right)\ne N\left(\left\{Z\right\}\right)$$
13	10	simprd	$$⊢\phi \to \neg X\in N\left(\left\{Z,Y\right\}\right)$$
14		prcom	$$⊢\left\{Z,Y\right\}=\left\{Y,Z\right\}$$
15	14	fveq2i	$$⊢N\left(\left\{Z,Y\right\}\right)=N\left(\left\{Y,Z\right\}\right)$$
16	15	eleq2i	$$⊢X\in N\left(\left\{Z,Y\right\}\right)\leftrightarrow X\in N\left(\left\{Y,Z\right\}\right)$$
17	13 16	sylnib	$$⊢\phi \to \neg X\in N\left(\left\{Y,Z\right\}\right)$$
18	12 17	jca	$$⊢\phi \to \left(N\left(\left\{Y\right\}\right)\ne N\left(\left\{Z\right\}\right)\wedge \neg X\in N\left(\left\{Y,Z\right\}\right)\right)$$