Theorem lspindp2

Description: Alternate way to say 3 vectors are mutually independent (rotate right). (Contributed by NM, 12-Apr-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}$$
	lspindp2.x	$$⊢\phi \to X\in V$$
	lspindp2.y	$$⊢\phi \to Y\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
	lspindp2.z	$$⊢\phi \to Z\in V$$
	lspindp2.q	$$⊢\phi \to N\left(\left\{X\right\}\right)\ne N\left(\left\{Y\right\}\right)$$
	lspindp2.e	$$⊢\phi \to \neg Z\in N\left(\left\{X,Y\right\}\right)$$
Assertion	lspindp2	$$⊢\phi \to \left(N\left(\left\{Z\right\}\right)\ne N\left(\left\{X\right\}\right)\wedge \neg Y\in N\left(\left\{Z,X\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		lspindp2.x	$$⊢\phi \to X\in V$$
6		lspindp2.y	$$⊢\phi \to Y\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
7		lspindp2.z	$$⊢\phi \to Z\in V$$
8		lspindp2.q	$$⊢\phi \to N\left(\left\{X\right\}\right)\ne N\left(\left\{Y\right\}\right)$$
9		lspindp2.e	$$⊢\phi \to \neg Z\in N\left(\left\{X,Y\right\}\right)$$
10	8	necomd	$$⊢\phi \to N\left(\left\{Y\right\}\right)\ne N\left(\left\{X\right\}\right)$$
11		prcom	$$⊢\left\{X,Y\right\}=\left\{Y,X\right\}$$
12	11	fveq2i	$$⊢N\left(\left\{X,Y\right\}\right)=N\left(\left\{Y,X\right\}\right)$$
13	12	eleq2i	$$⊢Z\in N\left(\left\{X,Y\right\}\right)\leftrightarrow Z\in N\left(\left\{Y,X\right\}\right)$$
14	9 13	sylnib	$$⊢\phi \to \neg Z\in N\left(\left\{Y,X\right\}\right)$$
15	1 2 3 4 6 5 7 10 14	lspindp1	$$⊢\phi \to \left(N\left(\left\{Z\right\}\right)\ne N\left(\left\{X\right\}\right)\wedge \neg Y\in N\left(\left\{Z,X\right\}\right)\right)$$