Theorem lspindp1

Description: Alternate way to say 3 vectors are mutually independent (swap 1st and 2nd). (Contributed by NM, 11-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}$$
	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	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)$$

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	5	eldifad	$$⊢\phi \to X\in V$$
11	1 3 4 7 10 6 9	lspindpi	$$⊢\phi \to \left(N\left(\left\{Z\right\}\right)\ne N\left(\left\{X\right\}\right)\wedge N\left(\left\{Z\right\}\right)\ne N\left(\left\{Y\right\}\right)\right)$$
12	11	simprd	$$⊢\phi \to N\left(\left\{Z\right\}\right)\ne N\left(\left\{Y\right\}\right)$$
13	4	adantr	$$⊢\left(\phi \wedge X\in N\left(\left\{Z,Y\right\}\right)\right)\to W\in \mathrm{LVec}$$
14	5	adantr	$$⊢\left(\phi \wedge X\in N\left(\left\{Z,Y\right\}\right)\right)\to X\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
15	7	adantr	$$⊢\left(\phi \wedge X\in N\left(\left\{Z,Y\right\}\right)\right)\to Z\in V$$
16	6	adantr	$$⊢\left(\phi \wedge X\in N\left(\left\{Z,Y\right\}\right)\right)\to Y\in V$$
17	8	adantr	$$⊢\left(\phi \wedge X\in N\left(\left\{Z,Y\right\}\right)\right)\to N\left(\left\{X\right\}\right)\ne N\left(\left\{Y\right\}\right)$$
18		simpr	$$⊢\left(\phi \wedge X\in N\left(\left\{Z,Y\right\}\right)\right)\to X\in N\left(\left\{Z,Y\right\}\right)$$
19	1 2 3 13 14 15 16 17 18	lspexch	$$⊢\left(\phi \wedge X\in N\left(\left\{Z,Y\right\}\right)\right)\to Z\in N\left(\left\{X,Y\right\}\right)$$
20	9 19	mtand	$$⊢\phi \to \neg X\in N\left(\left\{Z,Y\right\}\right)$$
21	12 20	jca	$$⊢\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)$$