Theorem mapdindp3

Description: Vector independence lemma. (Contributed by NM, 29-Apr-2015)

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

Proof

Step	Hyp	Ref	Expression
1		mapdindp1.v	$$⊢V={\mathrm{Base}}_W$$
2		mapdindp1.p	$$⊢\underset{\dot{}}{+}={+}_W$$
3		mapdindp1.o	$$⊢\underset{\dot{}}{0}=0_W$$
4		mapdindp1.n	$$⊢N=\mathrm{LSpan}\left(W\right)$$
5		mapdindp1.w	$$⊢\phi \to W\in \mathrm{LVec}$$
6		mapdindp1.x	$$⊢\phi \to X\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
7		mapdindp1.y	$$⊢\phi \to Y\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
8		mapdindp1.z	$$⊢\phi \to Z\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
9		mapdindp1.W	$$⊢\phi \to w\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
10		mapdindp1.e	$$⊢\phi \to N\left(\left\{Y\right\}\right)=N\left(\left\{Z\right\}\right)$$
11		mapdindp1.ne	$$⊢\phi \to N\left(\left\{X\right\}\right)\ne N\left(\left\{Y\right\}\right)$$
12		mapdindp1.f	$$⊢\phi \to \neg w\in N\left(\left\{X,Y\right\}\right)$$
13		lveclmod	$$⊢W\in \mathrm{LVec}\to W\in \mathrm{LMod}$$
14	5 13	syl	$$⊢\phi \to W\in \mathrm{LMod}$$
15	9	eldifad	$$⊢\phi \to w\in V$$
16	7	eldifad	$$⊢\phi \to Y\in V$$
17	1 2 4	lspvadd	$$⊢\left(W\in \mathrm{LMod}\wedge w\in V\wedge Y\in V\right)\to N\left(\left\{w\underset{\dot{}}{+}Y\right\}\right)\subseteq N\left(\left\{w,Y\right\}\right)$$
18	14 15 16 17	syl3anc	$$⊢\phi \to N\left(\left\{w\underset{\dot{}}{+}Y\right\}\right)\subseteq N\left(\left\{w,Y\right\}\right)$$
19	1 3 4 5 6 16 15 11 12	lspindp1	$$⊢\phi \to \left(N\left(\left\{w\right\}\right)\ne N\left(\left\{Y\right\}\right)\wedge \neg X\in N\left(\left\{w,Y\right\}\right)\right)$$
20	19	simprd	$$⊢\phi \to \neg X\in N\left(\left\{w,Y\right\}\right)$$
21	18 20	ssneldd	$$⊢\phi \to \neg X\in N\left(\left\{w\underset{\dot{}}{+}Y\right\}\right)$$
22	6	eldifad	$$⊢\phi \to X\in V$$
23	1 4	lspsnid	$$⊢\left(W\in \mathrm{LMod}\wedge X\in V\right)\to X\in N\left(\left\{X\right\}\right)$$
24	14 22 23	syl2anc	$$⊢\phi \to X\in N\left(\left\{X\right\}\right)$$
25		eleq2	$$⊢N\left(\left\{X\right\}\right)=N\left(\left\{w\underset{\dot{}}{+}Y\right\}\right)\to \left(X\in N\left(\left\{X\right\}\right)\leftrightarrow X\in N\left(\left\{w\underset{\dot{}}{+}Y\right\}\right)\right)$$
26	24 25	syl5ibcom	$$⊢\phi \to \left(N\left(\left\{X\right\}\right)=N\left(\left\{w\underset{\dot{}}{+}Y\right\}\right)\to X\in N\left(\left\{w\underset{\dot{}}{+}Y\right\}\right)\right)$$
27	26	necon3bd	$$⊢\phi \to \left(\neg X\in N\left(\left\{w\underset{\dot{}}{+}Y\right\}\right)\to N\left(\left\{X\right\}\right)\ne N\left(\left\{w\underset{\dot{}}{+}Y\right\}\right)\right)$$
28	21 27	mpd	$$⊢\phi \to N\left(\left\{X\right\}\right)\ne N\left(\left\{w\underset{\dot{}}{+}Y\right\}\right)$$