Theorem mapdncol

Description: Transfer non-colinearity from domain to range of projectivity mapd . (Contributed by NM, 11-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	|- ( ph -> ( K e. HL /\ W e. H ) )
	mapdindp.f	|- ( ph -> F e. D )
	mapdindp.mx	|- ( ph -> ( M ` ( N ` { X } ) ) = ( J ` { F } ) )
	mapdindp.x	|- ( ph -> X e. V )
	mapdindp.y	|- ( ph -> Y e. V )
	mapdindp.g	|- ( ph -> G e. D )
	mapdindp.my	|- ( ph -> ( M ` ( N ` { Y } ) ) = ( J ` { G } ) )
	mapdncol.q	|- ( ph -> ( N ` { X } ) =/= ( N ` { Y } ) )
Assertion	mapdncol	|- ( ph -> ( J ` { F } ) =/= ( J ` { G } ) )

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	|- ( ph -> ( K e. HL /\ W e. H ) )
10		mapdindp.f	|- ( ph -> F e. D )
11		mapdindp.mx	|- ( ph -> ( M ` ( N ` { X } ) ) = ( J ` { F } ) )
12		mapdindp.x	|- ( ph -> X e. V )
13		mapdindp.y	|- ( ph -> Y e. V )
14		mapdindp.g	|- ( ph -> G e. D )
15		mapdindp.my	|- ( ph -> ( M ` ( N ` { Y } ) ) = ( J ` { G } ) )
16		mapdncol.q	|- ( ph -> ( N ` { X } ) =/= ( N ` { Y } ) )
17		eqid	|- ( LSubSp ` U ) = ( LSubSp ` U )
18	1 3 9	dvhlmod	|- ( ph -> U e. LMod )
19	4 17 5	lspsncl	|- ( ( U e. LMod /\ X e. V ) -> ( N ` { X } ) e. ( LSubSp ` U ) )
20	18 12 19	syl2anc	|- ( ph -> ( N ` { X } ) e. ( LSubSp ` U ) )
21	4 17 5	lspsncl	|- ( ( U e. LMod /\ Y e. V ) -> ( N ` { Y } ) e. ( LSubSp ` U ) )
22	18 13 21	syl2anc	|- ( ph -> ( N ` { Y } ) e. ( LSubSp ` U ) )
23	1 3 17 2 9 20 22	mapd11	|- ( ph -> ( ( M ` ( N ` { X } ) ) = ( M ` ( N ` { Y } ) ) <-> ( N ` { X } ) = ( N ` { Y } ) ) )
24	23	necon3bid	|- ( ph -> ( ( M ` ( N ` { X } ) ) =/= ( M ` ( N ` { Y } ) ) <-> ( N ` { X } ) =/= ( N ` { Y } ) ) )
25	16 24	mpbird	|- ( ph -> ( M ` ( N ` { X } ) ) =/= ( M ` ( N ` { Y } ) ) )
26	25 11 15	3netr3d	|- ( ph -> ( J ` { F } ) =/= ( J ` { G } ) )