Theorem mapdpglem30a

Description: Lemma for mapdpg . (Contributed by NM, 22-Mar-2015)

	Ref	Expression
Hypotheses	mapdpg.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	mapdpg.m	$$⊢M=\mathrm{mapd}\left(K\right)\left(W\right)$$
	mapdpg.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
	mapdpg.v	$$⊢V={\mathrm{Base}}_U$$
	mapdpg.s	$$⊢\underset{\dot{}}{-}={-}_U$$
	mapdpg.z	$$⊢\underset{\dot{}}{0}=0_U$$
	mapdpg.n	$$⊢N=\mathrm{LSpan}\left(U\right)$$
	mapdpg.c	$$⊢C=\mathrm{LCDual}\left(K\right)\left(W\right)$$
	mapdpg.f	$$⊢F={\mathrm{Base}}_C$$
	mapdpg.r	$$⊢R={-}_C$$
	mapdpg.j	$$⊢J=\mathrm{LSpan}\left(C\right)$$
	mapdpg.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
	mapdpg.x	$$⊢\phi \to X\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
	mapdpg.y	$$⊢\phi \to Y\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
	mapdpg.g	$$⊢\phi \to G\in F$$
	mapdpg.ne	$$⊢\phi \to N\left(\left\{X\right\}\right)\ne N\left(\left\{Y\right\}\right)$$
	mapdpg.e	$$⊢\phi \to M\left(N\left(\left\{X\right\}\right)\right)=J\left(\left\{G\right\}\right)$$
Assertion	mapdpglem30a	$$⊢\phi \to G\ne 0_C$$

Proof

Step	Hyp	Ref	Expression
1		mapdpg.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
2		mapdpg.m	$$⊢M=\mathrm{mapd}\left(K\right)\left(W\right)$$
3		mapdpg.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
4		mapdpg.v	$$⊢V={\mathrm{Base}}_U$$
5		mapdpg.s	$$⊢\underset{\dot{}}{-}={-}_U$$
6		mapdpg.z	$$⊢\underset{\dot{}}{0}=0_U$$
7		mapdpg.n	$$⊢N=\mathrm{LSpan}\left(U\right)$$
8		mapdpg.c	$$⊢C=\mathrm{LCDual}\left(K\right)\left(W\right)$$
9		mapdpg.f	$$⊢F={\mathrm{Base}}_C$$
10		mapdpg.r	$$⊢R={-}_C$$
11		mapdpg.j	$$⊢J=\mathrm{LSpan}\left(C\right)$$
12		mapdpg.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
13		mapdpg.x	$$⊢\phi \to X\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
14		mapdpg.y	$$⊢\phi \to Y\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
15		mapdpg.g	$$⊢\phi \to G\in F$$
16		mapdpg.ne	$$⊢\phi \to N\left(\left\{X\right\}\right)\ne N\left(\left\{Y\right\}\right)$$
17		mapdpg.e	$$⊢\phi \to M\left(N\left(\left\{X\right\}\right)\right)=J\left(\left\{G\right\}\right)$$
18		eqid	$$⊢\mathrm{LSAtoms}\left(U\right)=\mathrm{LSAtoms}\left(U\right)$$
19		eqid	$$⊢\mathrm{LSAtoms}\left(C\right)=\mathrm{LSAtoms}\left(C\right)$$
20	1 3 12	dvhlmod	$$⊢\phi \to U\in \mathrm{LMod}$$
21	4 7 6 18 20 13	lsatlspsn	$$⊢\phi \to N\left(\left\{X\right\}\right)\in \mathrm{LSAtoms}\left(U\right)$$
22	1 2 3 18 8 19 12 21	mapdat	$$⊢\phi \to M\left(N\left(\left\{X\right\}\right)\right)\in \mathrm{LSAtoms}\left(C\right)$$
23	17 22	eqeltrrd	$$⊢\phi \to J\left(\left\{G\right\}\right)\in \mathrm{LSAtoms}\left(C\right)$$
24		eqid	$$⊢0_C=0_C$$
25	1 8 12	lcdlmod	$$⊢\phi \to C\in \mathrm{LMod}$$
26	9 11 24 19 25 15	lsatspn0	$$⊢\phi \to \left(J\left(\left\{G\right\}\right)\in \mathrm{LSAtoms}\left(C\right)\leftrightarrow G\ne 0_C\right)$$
27	23 26	mpbid	$$⊢\phi \to G\ne 0_C$$