mapdncol

Description: Transfer non-colinearity from domain to range of projectivity mapd . (Contributed by NM, 11-Apr-2015)

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		mapdindp.x	$⊢ φ \to X \in V$
13		mapdindp.y	$⊢ φ \to Y \in V$
14		mapdindp.g	$⊢ φ \to G \in D$
15		mapdindp.my	$⊢ φ \to M (N (\{Y\})) = J (\{G\})$
16		mapdncol.q	$⊢ φ \to N (\{X\}) \neq N (\{Y\})$
17		eqid	$⊢ LSubSp (U) = LSubSp (U)$
18	1 3 9	dvhlmod	$⊢ φ \to U \in LMod$
19	4 17 5	lspsncl	$⊢ (U \in LMod \land X \in V) \to N (\{X\}) \in LSubSp (U)$
20	18 12 19	syl2anc	$⊢ φ \to N (\{X\}) \in LSubSp (U)$
21	4 17 5	lspsncl	$⊢ (U \in LMod \land Y \in V) \to N (\{Y\}) \in LSubSp (U)$
22	18 13 21	syl2anc	$⊢ φ \to N (\{Y\}) \in LSubSp (U)$
23	1 3 17 2 9 20 22	mapd11	$⊢ φ \to (M (N (\{X\})) = M (N (\{Y\})) \leftrightarrow N (\{X\}) = N (\{Y\}))$
24	23	necon3bid	$⊢ φ \to (M (N (\{X\})) \neq M (N (\{Y\})) \leftrightarrow N (\{X\}) \neq N (\{Y\}))$
25	16 24	mpbird	$⊢ φ \to M (N (\{X\})) \neq M (N (\{Y\}))$
26	25 11 15	3netr3d	$⊢ φ \to J (\{F\}) \neq J (\{G\})$

Metamath Proof Explorer