Theorem hdmap1l6k

Description: Lemmma for hdmap1l6 . Eliminate nonzero vector requirement. (Contributed by NM, 1-May-2015)

	Ref	Expression
Hypotheses	hdmap1l6.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	hdmap1l6.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
	hdmap1l6.v	$$⊢V={\mathrm{Base}}_U$$
	hdmap1l6.p	$$⊢\underset{\dot{}}{+}={+}_U$$
	hdmap1l6.s	$$⊢\underset{\dot{}}{-}={-}_U$$
	hdmap1l6c.o	$$⊢\underset{\dot{}}{0}=0_U$$
	hdmap1l6.n	$$⊢N=\mathrm{LSpan}\left(U\right)$$
	hdmap1l6.c	$$⊢C=\mathrm{LCDual}\left(K\right)\left(W\right)$$
	hdmap1l6.d	$$⊢D={\mathrm{Base}}_C$$
	hdmap1l6.a	$$⊢\underset{\dot{}}{✚}={+}_C$$
	hdmap1l6.r	$$⊢R={-}_C$$
	hdmap1l6.q	$$⊢Q=0_C$$
	hdmap1l6.l	$$⊢L=\mathrm{LSpan}\left(C\right)$$
	hdmap1l6.m	$$⊢M=\mathrm{mapd}\left(K\right)\left(W\right)$$
	hdmap1l6.i	$$⊢I=\mathrm{HDMap1}\left(K\right)\left(W\right)$$
	hdmap1l6.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
	hdmap1l6.f	$$⊢\phi \to F\in D$$
	hdmap1l6cl.x	$$⊢\phi \to X\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
	hdmap1l6.mn	$$⊢\phi \to M\left(N\left(\left\{X\right\}\right)\right)=L\left(\left\{F\right\}\right)$$
	hdmap1l6k.y	$$⊢\phi \to Y\in V$$
	hdmap1l6k.z	$$⊢\phi \to Z\in V$$
	hdmap1l6k.xn	$$⊢\phi \to \neg X\in N\left(\left\{Y,Z\right\}\right)$$
Assertion	hdmap1l6k	$$⊢\phi \to I\left(⟨X,F,Y\underset{\dot{}}{+}Z⟩\right)=I\left(⟨X,F,Y⟩\right)\underset{\dot{}}{✚}I\left(⟨X,F,Z⟩\right)$$

Proof

Step	Hyp	Ref	Expression
1		hdmap1l6.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
2		hdmap1l6.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
3		hdmap1l6.v	$$⊢V={\mathrm{Base}}_U$$
4		hdmap1l6.p	$$⊢\underset{\dot{}}{+}={+}_U$$
5		hdmap1l6.s	$$⊢\underset{\dot{}}{-}={-}_U$$
6		hdmap1l6c.o	$$⊢\underset{\dot{}}{0}=0_U$$
7		hdmap1l6.n	$$⊢N=\mathrm{LSpan}\left(U\right)$$
8		hdmap1l6.c	$$⊢C=\mathrm{LCDual}\left(K\right)\left(W\right)$$
9		hdmap1l6.d	$$⊢D={\mathrm{Base}}_C$$
10		hdmap1l6.a	$$⊢\underset{\dot{}}{✚}={+}_C$$
11		hdmap1l6.r	$$⊢R={-}_C$$
12		hdmap1l6.q	$$⊢Q=0_C$$
13		hdmap1l6.l	$$⊢L=\mathrm{LSpan}\left(C\right)$$
14		hdmap1l6.m	$$⊢M=\mathrm{mapd}\left(K\right)\left(W\right)$$
15		hdmap1l6.i	$$⊢I=\mathrm{HDMap1}\left(K\right)\left(W\right)$$
16		hdmap1l6.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
17		hdmap1l6.f	$$⊢\phi \to F\in D$$
18		hdmap1l6cl.x	$$⊢\phi \to X\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
19		hdmap1l6.mn	$$⊢\phi \to M\left(N\left(\left\{X\right\}\right)\right)=L\left(\left\{F\right\}\right)$$
20		hdmap1l6k.y	$$⊢\phi \to Y\in V$$
21		hdmap1l6k.z	$$⊢\phi \to Z\in V$$
22		hdmap1l6k.xn	$$⊢\phi \to \neg X\in N\left(\left\{Y,Z\right\}\right)$$
23	16	adantr	$$⊢\left(\phi \wedge Y=\underset{\dot{}}{0}\right)\to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
24	17	adantr	$$⊢\left(\phi \wedge Y=\underset{\dot{}}{0}\right)\to F\in D$$
25	18	adantr	$$⊢\left(\phi \wedge Y=\underset{\dot{}}{0}\right)\to X\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
26	19	adantr	$$⊢\left(\phi \wedge Y=\underset{\dot{}}{0}\right)\to M\left(N\left(\left\{X\right\}\right)\right)=L\left(\left\{F\right\}\right)$$
27		simpr	$$⊢\left(\phi \wedge Y=\underset{\dot{}}{0}\right)\to Y=\underset{\dot{}}{0}$$
28	21	adantr	$$⊢\left(\phi \wedge Y=\underset{\dot{}}{0}\right)\to Z\in V$$
29	22	adantr	$$⊢\left(\phi \wedge Y=\underset{\dot{}}{0}\right)\to \neg X\in N\left(\left\{Y,Z\right\}\right)$$
30	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 23 24 25 26 27 28 29	hdmap1l6b	$$⊢\left(\phi \wedge Y=\underset{\dot{}}{0}\right)\to I\left(⟨X,F,Y\underset{\dot{}}{+}Z⟩\right)=I\left(⟨X,F,Y⟩\right)\underset{\dot{}}{✚}I\left(⟨X,F,Z⟩\right)$$
31	16	adantr	$$⊢\left(\phi \wedge Z=\underset{\dot{}}{0}\right)\to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
32	17	adantr	$$⊢\left(\phi \wedge Z=\underset{\dot{}}{0}\right)\to F\in D$$
33	18	adantr	$$⊢\left(\phi \wedge Z=\underset{\dot{}}{0}\right)\to X\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
34	19	adantr	$$⊢\left(\phi \wedge Z=\underset{\dot{}}{0}\right)\to M\left(N\left(\left\{X\right\}\right)\right)=L\left(\left\{F\right\}\right)$$
35	20	adantr	$$⊢\left(\phi \wedge Z=\underset{\dot{}}{0}\right)\to Y\in V$$
36		simpr	$$⊢\left(\phi \wedge Z=\underset{\dot{}}{0}\right)\to Z=\underset{\dot{}}{0}$$
37	22	adantr	$$⊢\left(\phi \wedge Z=\underset{\dot{}}{0}\right)\to \neg X\in N\left(\left\{Y,Z\right\}\right)$$
38	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 31 32 33 34 35 36 37	hdmap1l6c	$$⊢\left(\phi \wedge Z=\underset{\dot{}}{0}\right)\to I\left(⟨X,F,Y\underset{\dot{}}{+}Z⟩\right)=I\left(⟨X,F,Y⟩\right)\underset{\dot{}}{✚}I\left(⟨X,F,Z⟩\right)$$
39	16	adantr	$$⊢\left(\phi \wedge \left(Y\ne \underset{\dot{}}{0}\wedge Z\ne \underset{\dot{}}{0}\right)\right)\to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
40	17	adantr	$$⊢\left(\phi \wedge \left(Y\ne \underset{\dot{}}{0}\wedge Z\ne \underset{\dot{}}{0}\right)\right)\to F\in D$$
41	18	adantr	$$⊢\left(\phi \wedge \left(Y\ne \underset{\dot{}}{0}\wedge Z\ne \underset{\dot{}}{0}\right)\right)\to X\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
42	19	adantr	$$⊢\left(\phi \wedge \left(Y\ne \underset{\dot{}}{0}\wedge Z\ne \underset{\dot{}}{0}\right)\right)\to M\left(N\left(\left\{X\right\}\right)\right)=L\left(\left\{F\right\}\right)$$
43	22	adantr	$$⊢\left(\phi \wedge \left(Y\ne \underset{\dot{}}{0}\wedge Z\ne \underset{\dot{}}{0}\right)\right)\to \neg X\in N\left(\left\{Y,Z\right\}\right)$$
44	20	adantr	$$⊢\left(\phi \wedge \left(Y\ne \underset{\dot{}}{0}\wedge Z\ne \underset{\dot{}}{0}\right)\right)\to Y\in V$$
45		simprl	$$⊢\left(\phi \wedge \left(Y\ne \underset{\dot{}}{0}\wedge Z\ne \underset{\dot{}}{0}\right)\right)\to Y\ne \underset{\dot{}}{0}$$
46		eldifsn	$$⊢Y\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)\leftrightarrow \left(Y\in V\wedge Y\ne \underset{\dot{}}{0}\right)$$
47	44 45 46	sylanbrc	$$⊢\left(\phi \wedge \left(Y\ne \underset{\dot{}}{0}\wedge Z\ne \underset{\dot{}}{0}\right)\right)\to Y\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
48	21	adantr	$$⊢\left(\phi \wedge \left(Y\ne \underset{\dot{}}{0}\wedge Z\ne \underset{\dot{}}{0}\right)\right)\to Z\in V$$
49		simprr	$$⊢\left(\phi \wedge \left(Y\ne \underset{\dot{}}{0}\wedge Z\ne \underset{\dot{}}{0}\right)\right)\to Z\ne \underset{\dot{}}{0}$$
50		eldifsn	$$⊢Z\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)\leftrightarrow \left(Z\in V\wedge Z\ne \underset{\dot{}}{0}\right)$$
51	48 49 50	sylanbrc	$$⊢\left(\phi \wedge \left(Y\ne \underset{\dot{}}{0}\wedge Z\ne \underset{\dot{}}{0}\right)\right)\to Z\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
52	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 39 40 41 42 43 47 51	hdmap1l6j	$$⊢\left(\phi \wedge \left(Y\ne \underset{\dot{}}{0}\wedge Z\ne \underset{\dot{}}{0}\right)\right)\to I\left(⟨X,F,Y\underset{\dot{}}{+}Z⟩\right)=I\left(⟨X,F,Y⟩\right)\underset{\dot{}}{✚}I\left(⟨X,F,Z⟩\right)$$
53	30 38 52	pm2.61da2ne	$$⊢\phi \to I\left(⟨X,F,Y\underset{\dot{}}{+}Z⟩\right)=I\left(⟨X,F,Y⟩\right)\underset{\dot{}}{✚}I\left(⟨X,F,Z⟩\right)$$