mapdn0

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

	Ref	Expression
Hypotheses	mapdindp.h	$⊢ H = LHyp (K)$
	mapdindp.m	$⊢ M = mapd (K) (W)$
	mapdindp.u	$⊢ U = DVecH (K) (W)$
	mapdindp.v	$⊢ V = {Base}_{U}$
	mapdindp.n	$⊢ N = LSpan (U)$
	mapdindp.c	$⊢ C = LCDual (K) (W)$
	mapdindp.d	$⊢ D = {Base}_{C}$
	mapdindp.j	$⊢ J = LSpan (C)$
	mapdindp.k	$⊢ φ \to (K \in HL \land W \in H)$
	mapdindp.f	$⊢ φ \to F \in D$
	mapdindp.mx	$⊢ φ \to M (N (\{X\})) = J (\{F\})$
	mapdn0.o	$⊢ \underset{˙}{0} = 0_{U}$
	mapdn0.z	$⊢ Z = 0_{C}$
	mapdn0.x	$⊢ φ \to X \in (V ∖ \{\underset{˙}{0}\})$
Assertion	mapdn0	$⊢ φ \to F \in (D ∖ \{Z\})$

Proof

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

Metamath Proof Explorer

Theorem mapdn0

Proof