Theorem hdmap1l6b0N

Description: Lemmma for hdmap1l6 . (Contributed by NM, 23-Apr-2015) (New usage is discouraged.)

	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)$$
	hdmap1l6b0.y	$$⊢\phi \to Y\in V$$
	hdmap1l6b0.z	$$⊢\phi \to Z\in V$$
	hdmap1l6b0.ne	$$⊢\phi \to N\left(\left\{X\right\}\right)\cap N\left(\left\{Y,Z\right\}\right)=\left\{\underset{\dot{}}{0}\right\}$$
Assertion	hdmap1l6b0N	$$⊢\phi \to \neg X\in N\left(\left\{Y,Z\right\}\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		hdmap1l6b0.y	$$⊢\phi \to Y\in V$$
21		hdmap1l6b0.z	$$⊢\phi \to Z\in V$$
22		hdmap1l6b0.ne	$$⊢\phi \to N\left(\left\{X\right\}\right)\cap N\left(\left\{Y,Z\right\}\right)=\left\{\underset{\dot{}}{0}\right\}$$
23		eqid	$$⊢\mathrm{LSubSp}\left(U\right)=\mathrm{LSubSp}\left(U\right)$$
24	1 2 16	dvhlvec	$$⊢\phi \to U\in \mathrm{LVec}$$
25	1 2 16	dvhlmod	$$⊢\phi \to U\in \mathrm{LMod}$$
26	3 23 7 25 20 21	lspprcl	$$⊢\phi \to N\left(\left\{Y,Z\right\}\right)\in \mathrm{LSubSp}\left(U\right)$$
27	3 6 7 23 24 26 18	lspdisjb	$$⊢\phi \to \left(\neg X\in N\left(\left\{Y,Z\right\}\right)\leftrightarrow N\left(\left\{X\right\}\right)\cap N\left(\left\{Y,Z\right\}\right)=\left\{\underset{\dot{}}{0}\right\}\right)$$
28	22 27	mpbird	$$⊢\phi \to \neg X\in N\left(\left\{Y,Z\right\}\right)$$