Theorem mapdindp2

Description: Vector independence lemma. (Contributed by NM, 1-May-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	mapdindp2	$$⊢\phi \to \neg w\in N\left(\left\{X,Y\underset{\dot{}}{+}Z\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		preq2	$$⊢Y\underset{\dot{}}{+}Z=\underset{\dot{}}{0}\to \left\{X,Y\underset{\dot{}}{+}Z\right\}=\left\{X,\underset{\dot{}}{0}\right\}$$
14	13	fveq2d	$$⊢Y\underset{\dot{}}{+}Z=\underset{\dot{}}{0}\to N\left(\left\{X,Y\underset{\dot{}}{+}Z\right\}\right)=N\left(\left\{X,\underset{\dot{}}{0}\right\}\right)$$
15		lveclmod	$$⊢W\in \mathrm{LVec}\to W\in \mathrm{LMod}$$
16	5 15	syl	$$⊢\phi \to W\in \mathrm{LMod}$$
17	6	eldifad	$$⊢\phi \to X\in V$$
18	1 3 4 16 17	lsppr0	$$⊢\phi \to N\left(\left\{X,\underset{\dot{}}{0}\right\}\right)=N\left(\left\{X\right\}\right)$$
19	14 18	sylan9eqr	$$⊢\left(\phi \wedge Y\underset{\dot{}}{+}Z=\underset{\dot{}}{0}\right)\to N\left(\left\{X,Y\underset{\dot{}}{+}Z\right\}\right)=N\left(\left\{X\right\}\right)$$
20	7	eldifad	$$⊢\phi \to Y\in V$$
21		prssi	$$⊢\left(X\in V\wedge Y\in V\right)\to \left\{X,Y\right\}\subseteq V$$
22	17 20 21	syl2anc	$$⊢\phi \to \left\{X,Y\right\}\subseteq V$$
23		snsspr1	$$⊢\left\{X\right\}\subseteq \left\{X,Y\right\}$$
24	23	a1i	$$⊢\phi \to \left\{X\right\}\subseteq \left\{X,Y\right\}$$
25	1 4	lspss	$$⊢\left(W\in \mathrm{LMod}\wedge \left\{X,Y\right\}\subseteq V\wedge \left\{X\right\}\subseteq \left\{X,Y\right\}\right)\to N\left(\left\{X\right\}\right)\subseteq N\left(\left\{X,Y\right\}\right)$$
26	16 22 24 25	syl3anc	$$⊢\phi \to N\left(\left\{X\right\}\right)\subseteq N\left(\left\{X,Y\right\}\right)$$
27	26	adantr	$$⊢\left(\phi \wedge Y\underset{\dot{}}{+}Z=\underset{\dot{}}{0}\right)\to N\left(\left\{X\right\}\right)\subseteq N\left(\left\{X,Y\right\}\right)$$
28	19 27	eqsstrd	$$⊢\left(\phi \wedge Y\underset{\dot{}}{+}Z=\underset{\dot{}}{0}\right)\to N\left(\left\{X,Y\underset{\dot{}}{+}Z\right\}\right)\subseteq N\left(\left\{X,Y\right\}\right)$$
29	12	adantr	$$⊢\left(\phi \wedge Y\underset{\dot{}}{+}Z=\underset{\dot{}}{0}\right)\to \neg w\in N\left(\left\{X,Y\right\}\right)$$
30	28 29	ssneldd	$$⊢\left(\phi \wedge Y\underset{\dot{}}{+}Z=\underset{\dot{}}{0}\right)\to \neg w\in N\left(\left\{X,Y\underset{\dot{}}{+}Z\right\}\right)$$
31	12	adantr	$$⊢\left(\phi \wedge Y\underset{\dot{}}{+}Z\ne \underset{\dot{}}{0}\right)\to \neg w\in N\left(\left\{X,Y\right\}\right)$$
32	5	adantr	$$⊢\left(\phi \wedge Y\underset{\dot{}}{+}Z\ne \underset{\dot{}}{0}\right)\to W\in \mathrm{LVec}$$
33	6	adantr	$$⊢\left(\phi \wedge Y\underset{\dot{}}{+}Z\ne \underset{\dot{}}{0}\right)\to X\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
34	7	adantr	$$⊢\left(\phi \wedge Y\underset{\dot{}}{+}Z\ne \underset{\dot{}}{0}\right)\to Y\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
35	8	adantr	$$⊢\left(\phi \wedge Y\underset{\dot{}}{+}Z\ne \underset{\dot{}}{0}\right)\to Z\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
36	9	adantr	$$⊢\left(\phi \wedge Y\underset{\dot{}}{+}Z\ne \underset{\dot{}}{0}\right)\to w\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
37	10	adantr	$$⊢\left(\phi \wedge Y\underset{\dot{}}{+}Z\ne \underset{\dot{}}{0}\right)\to N\left(\left\{Y\right\}\right)=N\left(\left\{Z\right\}\right)$$
38	11	adantr	$$⊢\left(\phi \wedge Y\underset{\dot{}}{+}Z\ne \underset{\dot{}}{0}\right)\to N\left(\left\{X\right\}\right)\ne N\left(\left\{Y\right\}\right)$$
39		simpr	$$⊢\left(\phi \wedge Y\underset{\dot{}}{+}Z\ne \underset{\dot{}}{0}\right)\to Y\underset{\dot{}}{+}Z\ne \underset{\dot{}}{0}$$
40	1 2 3 4 32 33 34 35 36 37 38 31 39	mapdindp0	$$⊢\left(\phi \wedge Y\underset{\dot{}}{+}Z\ne \underset{\dot{}}{0}\right)\to N\left(\left\{Y\underset{\dot{}}{+}Z\right\}\right)=N\left(\left\{Y\right\}\right)$$
41	40	oveq2d	$$⊢\left(\phi \wedge Y\underset{\dot{}}{+}Z\ne \underset{\dot{}}{0}\right)\to N\left(\left\{X\right\}\right)\mathrm{LSSum}\left(W\right)N\left(\left\{Y\underset{\dot{}}{+}Z\right\}\right)=N\left(\left\{X\right\}\right)\mathrm{LSSum}\left(W\right)N\left(\left\{Y\right\}\right)$$
42		eqid	$$⊢\mathrm{LSSum}\left(W\right)=\mathrm{LSSum}\left(W\right)$$
43	8	eldifad	$$⊢\phi \to Z\in V$$
44	1 2	lmodvacl	$$⊢\left(W\in \mathrm{LMod}\wedge Y\in V\wedge Z\in V\right)\to Y\underset{\dot{}}{+}Z\in V$$
45	16 20 43 44	syl3anc	$$⊢\phi \to Y\underset{\dot{}}{+}Z\in V$$
46	1 4 42 16 17 45	lsmpr	$$⊢\phi \to N\left(\left\{X,Y\underset{\dot{}}{+}Z\right\}\right)=N\left(\left\{X\right\}\right)\mathrm{LSSum}\left(W\right)N\left(\left\{Y\underset{\dot{}}{+}Z\right\}\right)$$
47	46	adantr	$$⊢\left(\phi \wedge Y\underset{\dot{}}{+}Z\ne \underset{\dot{}}{0}\right)\to N\left(\left\{X,Y\underset{\dot{}}{+}Z\right\}\right)=N\left(\left\{X\right\}\right)\mathrm{LSSum}\left(W\right)N\left(\left\{Y\underset{\dot{}}{+}Z\right\}\right)$$
48	1 4 42 16 17 20	lsmpr	$$⊢\phi \to N\left(\left\{X,Y\right\}\right)=N\left(\left\{X\right\}\right)\mathrm{LSSum}\left(W\right)N\left(\left\{Y\right\}\right)$$
49	48	adantr	$$⊢\left(\phi \wedge Y\underset{\dot{}}{+}Z\ne \underset{\dot{}}{0}\right)\to N\left(\left\{X,Y\right\}\right)=N\left(\left\{X\right\}\right)\mathrm{LSSum}\left(W\right)N\left(\left\{Y\right\}\right)$$
50	41 47 49	3eqtr4d	$$⊢\left(\phi \wedge Y\underset{\dot{}}{+}Z\ne \underset{\dot{}}{0}\right)\to N\left(\left\{X,Y\underset{\dot{}}{+}Z\right\}\right)=N\left(\left\{X,Y\right\}\right)$$
51	31 50	neleqtrrd	$$⊢\left(\phi \wedge Y\underset{\dot{}}{+}Z\ne \underset{\dot{}}{0}\right)\to \neg w\in N\left(\left\{X,Y\underset{\dot{}}{+}Z\right\}\right)$$
52	30 51	pm2.61dane	$$⊢\phi \to \neg w\in N\left(\left\{X,Y\underset{\dot{}}{+}Z\right\}\right)$$