Theorem mapdindp4

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	mapdindp4	$$⊢\phi \to \neg Z\in N\left(\left\{X,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	lmodvacl	$$⊢\left(W\in \mathrm{LMod}\wedge w\in V\wedge Y\in V\right)\to w\underset{\dot{}}{+}Y\in V$$
18	14 15 16 17	syl3anc	$$⊢\phi \to w\underset{\dot{}}{+}Y\in V$$
19	6	eldifad	$$⊢\phi \to X\in V$$
20	1 4 5 15 19 16 12	lspindpi	$$⊢\phi \to \left(N\left(\left\{w\right\}\right)\ne N\left(\left\{X\right\}\right)\wedge N\left(\left\{w\right\}\right)\ne N\left(\left\{Y\right\}\right)\right)$$
21	20	simprd	$$⊢\phi \to N\left(\left\{w\right\}\right)\ne N\left(\left\{Y\right\}\right)$$
22	21	necomd	$$⊢\phi \to N\left(\left\{Y\right\}\right)\ne N\left(\left\{w\right\}\right)$$
23	1 2 3 4 5 16 9 22	lspindp3	$$⊢\phi \to N\left(\left\{Y\right\}\right)\ne N\left(\left\{Y\underset{\dot{}}{+}w\right\}\right)$$
24	1 2	lmodcom	$$⊢\left(W\in \mathrm{LMod}\wedge w\in V\wedge Y\in V\right)\to w\underset{\dot{}}{+}Y=Y\underset{\dot{}}{+}w$$
25	14 15 16 24	syl3anc	$$⊢\phi \to w\underset{\dot{}}{+}Y=Y\underset{\dot{}}{+}w$$
26	25	sneqd	$$⊢\phi \to \left\{w\underset{\dot{}}{+}Y\right\}=\left\{Y\underset{\dot{}}{+}w\right\}$$
27	26	fveq2d	$$⊢\phi \to N\left(\left\{w\underset{\dot{}}{+}Y\right\}\right)=N\left(\left\{Y\underset{\dot{}}{+}w\right\}\right)$$
28	23 27	neeqtrrd	$$⊢\phi \to N\left(\left\{Y\right\}\right)\ne N\left(\left\{w\underset{\dot{}}{+}Y\right\}\right)$$
29	10 28	eqnetrrd	$$⊢\phi \to N\left(\left\{Z\right\}\right)\ne N\left(\left\{w\underset{\dot{}}{+}Y\right\}\right)$$
30	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)$$
31	30	simprd	$$⊢\phi \to \neg X\in N\left(\left\{w,Y\right\}\right)$$
32		eqid	$$⊢\mathrm{LSSum}\left(W\right)=\mathrm{LSSum}\left(W\right)$$
33	8	eldifad	$$⊢\phi \to Z\in V$$
34	1 4 32 14 33 18	lsmpr	$$⊢\phi \to N\left(\left\{Z,w\underset{\dot{}}{+}Y\right\}\right)=N\left(\left\{Z\right\}\right)\mathrm{LSSum}\left(W\right)N\left(\left\{w\underset{\dot{}}{+}Y\right\}\right)$$
35	1 2	lmodcom	$$⊢\left(W\in \mathrm{LMod}\wedge Y\in V\wedge w\in V\right)\to Y\underset{\dot{}}{+}w=w\underset{\dot{}}{+}Y$$
36	14 16 15 35	syl3anc	$$⊢\phi \to Y\underset{\dot{}}{+}w=w\underset{\dot{}}{+}Y$$
37	36	preq2d	$$⊢\phi \to \left\{Y,Y\underset{\dot{}}{+}w\right\}=\left\{Y,w\underset{\dot{}}{+}Y\right\}$$
38	37	fveq2d	$$⊢\phi \to N\left(\left\{Y,Y\underset{\dot{}}{+}w\right\}\right)=N\left(\left\{Y,w\underset{\dot{}}{+}Y\right\}\right)$$
39	1 2 4 14 16 15	lspprabs	$$⊢\phi \to N\left(\left\{Y,Y\underset{\dot{}}{+}w\right\}\right)=N\left(\left\{Y,w\right\}\right)$$
40	1 4 32 14 16 18	lsmpr	$$⊢\phi \to N\left(\left\{Y,w\underset{\dot{}}{+}Y\right\}\right)=N\left(\left\{Y\right\}\right)\mathrm{LSSum}\left(W\right)N\left(\left\{w\underset{\dot{}}{+}Y\right\}\right)$$
41	38 39 40	3eqtr3rd	$$⊢\phi \to N\left(\left\{Y\right\}\right)\mathrm{LSSum}\left(W\right)N\left(\left\{w\underset{\dot{}}{+}Y\right\}\right)=N\left(\left\{Y,w\right\}\right)$$
42	10	oveq1d	$$⊢\phi \to N\left(\left\{Y\right\}\right)\mathrm{LSSum}\left(W\right)N\left(\left\{w\underset{\dot{}}{+}Y\right\}\right)=N\left(\left\{Z\right\}\right)\mathrm{LSSum}\left(W\right)N\left(\left\{w\underset{\dot{}}{+}Y\right\}\right)$$
43		prcom	$$⊢\left\{Y,w\right\}=\left\{w,Y\right\}$$
44	43	fveq2i	$$⊢N\left(\left\{Y,w\right\}\right)=N\left(\left\{w,Y\right\}\right)$$
45	44	a1i	$$⊢\phi \to N\left(\left\{Y,w\right\}\right)=N\left(\left\{w,Y\right\}\right)$$
46	41 42 45	3eqtr3d	$$⊢\phi \to N\left(\left\{Z\right\}\right)\mathrm{LSSum}\left(W\right)N\left(\left\{w\underset{\dot{}}{+}Y\right\}\right)=N\left(\left\{w,Y\right\}\right)$$
47	34 46	eqtrd	$$⊢\phi \to N\left(\left\{Z,w\underset{\dot{}}{+}Y\right\}\right)=N\left(\left\{w,Y\right\}\right)$$
48	31 47	neleqtrrd	$$⊢\phi \to \neg X\in N\left(\left\{Z,w\underset{\dot{}}{+}Y\right\}\right)$$
49	1 3 4 5 8 18 19 29 48	lspindp1	$$⊢\phi \to \left(N\left(\left\{X\right\}\right)\ne N\left(\left\{w\underset{\dot{}}{+}Y\right\}\right)\wedge \neg Z\in N\left(\left\{X,w\underset{\dot{}}{+}Y\right\}\right)\right)$$
50	49	simprd	$$⊢\phi \to \neg Z\in N\left(\left\{X,w\underset{\dot{}}{+}Y\right\}\right)$$