Theorem mapdn0

Description: Transfer nonzero property from domain to range of projectivity mapd . (Contributed by NM, 12-Apr-2015)

	Ref	Expression
Hypotheses	mapdindp.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	mapdindp.m	$$⊢M=\mathrm{mapd}\left(K\right)\left(W\right)$$
	mapdindp.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
	mapdindp.v	$$⊢V={\mathrm{Base}}_U$$
	mapdindp.n	$$⊢N=\mathrm{LSpan}\left(U\right)$$
	mapdindp.c	$$⊢C=\mathrm{LCDual}\left(K\right)\left(W\right)$$
	mapdindp.d	$$⊢D={\mathrm{Base}}_C$$
	mapdindp.j	$$⊢J=\mathrm{LSpan}\left(C\right)$$
	mapdindp.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
	mapdindp.f	$$⊢\phi \to F\in D$$
	mapdindp.mx	$$⊢\phi \to M\left(N\left(\left\{X\right\}\right)\right)=J\left(\left\{F\right\}\right)$$
	mapdn0.o	$$⊢\underset{\dot{}}{0}=0_U$$
	mapdn0.z	$$⊢Z=0_C$$
	mapdn0.x	$$⊢\phi \to X\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
Assertion	mapdn0	$$⊢\phi \to F\in \left(D\setminus \left\{Z\right\}\right)$$

Proof

Step	Hyp	Ref	Expression
1		mapdindp.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
2		mapdindp.m	$$⊢M=\mathrm{mapd}\left(K\right)\left(W\right)$$
3		mapdindp.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
4		mapdindp.v	$$⊢V={\mathrm{Base}}_U$$
5		mapdindp.n	$$⊢N=\mathrm{LSpan}\left(U\right)$$
6		mapdindp.c	$$⊢C=\mathrm{LCDual}\left(K\right)\left(W\right)$$
7		mapdindp.d	$$⊢D={\mathrm{Base}}_C$$
8		mapdindp.j	$$⊢J=\mathrm{LSpan}\left(C\right)$$
9		mapdindp.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
10		mapdindp.f	$$⊢\phi \to F\in D$$
11		mapdindp.mx	$$⊢\phi \to M\left(N\left(\left\{X\right\}\right)\right)=J\left(\left\{F\right\}\right)$$
12		mapdn0.o	$$⊢\underset{\dot{}}{0}=0_U$$
13		mapdn0.z	$$⊢Z=0_C$$
14		mapdn0.x	$$⊢\phi \to X\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
15		eldifsni	$$⊢X\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)\to X\ne \underset{\dot{}}{0}$$
16	14 15	syl	$$⊢\phi \to X\ne \underset{\dot{}}{0}$$
17		sneq	$$⊢F=Z\to \left\{F\right\}=\left\{Z\right\}$$
18	17	fveq2d	$$⊢F=Z\to J\left(\left\{F\right\}\right)=J\left(\left\{Z\right\}\right)$$
19	11 18	sylan9eq	$$⊢\left(\phi \wedge F=Z\right)\to M\left(N\left(\left\{X\right\}\right)\right)=J\left(\left\{Z\right\}\right)$$
20	1 2 3 12 6 13 9	mapd0	$$⊢\phi \to M\left(\left\{\underset{\dot{}}{0}\right\}\right)=\left\{Z\right\}$$
21	1 6 9	lcdlmod	$$⊢\phi \to C\in \mathrm{LMod}$$
22	13 8	lspsn0	$$⊢C\in \mathrm{LMod}\to J\left(\left\{Z\right\}\right)=\left\{Z\right\}$$
23	21 22	syl	$$⊢\phi \to J\left(\left\{Z\right\}\right)=\left\{Z\right\}$$
24	20 23	eqtr4d	$$⊢\phi \to M\left(\left\{\underset{\dot{}}{0}\right\}\right)=J\left(\left\{Z\right\}\right)$$
25	24	adantr	$$⊢\left(\phi \wedge F=Z\right)\to M\left(\left\{\underset{\dot{}}{0}\right\}\right)=J\left(\left\{Z\right\}\right)$$
26	19 25	eqtr4d	$$⊢\left(\phi \wedge F=Z\right)\to M\left(N\left(\left\{X\right\}\right)\right)=M\left(\left\{\underset{\dot{}}{0}\right\}\right)$$
27	26	ex	$$⊢\phi \to \left(F=Z\to M\left(N\left(\left\{X\right\}\right)\right)=M\left(\left\{\underset{\dot{}}{0}\right\}\right)\right)$$
28		eqid	$$⊢\mathrm{LSubSp}\left(U\right)=\mathrm{LSubSp}\left(U\right)$$
29	1 3 9	dvhlmod	$$⊢\phi \to U\in \mathrm{LMod}$$
30	14	eldifad	$$⊢\phi \to X\in V$$
31	4 28 5	lspsncl	$$⊢\left(U\in \mathrm{LMod}\wedge X\in V\right)\to N\left(\left\{X\right\}\right)\in \mathrm{LSubSp}\left(U\right)$$
32	29 30 31	syl2anc	$$⊢\phi \to N\left(\left\{X\right\}\right)\in \mathrm{LSubSp}\left(U\right)$$
33	12 28	lsssn0	$$⊢U\in \mathrm{LMod}\to \left\{\underset{\dot{}}{0}\right\}\in \mathrm{LSubSp}\left(U\right)$$
34	29 33	syl	$$⊢\phi \to \left\{\underset{\dot{}}{0}\right\}\in \mathrm{LSubSp}\left(U\right)$$
35	1 3 28 2 9 32 34	mapd11	$$⊢\phi \to \left(M\left(N\left(\left\{X\right\}\right)\right)=M\left(\left\{\underset{\dot{}}{0}\right\}\right)\leftrightarrow N\left(\left\{X\right\}\right)=\left\{\underset{\dot{}}{0}\right\}\right)$$
36	4 12 5	lspsneq0	$$⊢\left(U\in \mathrm{LMod}\wedge X\in V\right)\to \left(N\left(\left\{X\right\}\right)=\left\{\underset{\dot{}}{0}\right\}\leftrightarrow X=\underset{\dot{}}{0}\right)$$
37	29 30 36	syl2anc	$$⊢\phi \to \left(N\left(\left\{X\right\}\right)=\left\{\underset{\dot{}}{0}\right\}\leftrightarrow X=\underset{\dot{}}{0}\right)$$
38	35 37	bitrd	$$⊢\phi \to \left(M\left(N\left(\left\{X\right\}\right)\right)=M\left(\left\{\underset{\dot{}}{0}\right\}\right)\leftrightarrow X=\underset{\dot{}}{0}\right)$$
39	27 38	sylibd	$$⊢\phi \to \left(F=Z\to X=\underset{\dot{}}{0}\right)$$
40	39	necon3d	$$⊢\phi \to \left(X\ne \underset{\dot{}}{0}\to F\ne Z\right)$$
41	16 40	mpd	$$⊢\phi \to F\ne Z$$
42		eldifsn	$$⊢F\in \left(D\setminus \left\{Z\right\}\right)\leftrightarrow \left(F\in D\wedge F\ne Z\right)$$
43	10 41 42	sylanbrc	$$⊢\phi \to F\in \left(D\setminus \left\{Z\right\}\right)$$