Metamath Proof Explorer

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 ⊢ φ → K ∈ HL ∧ W ∈ H
mapdindp.f ⊢ φ → F ∈ D
mapdindp.mx ⊢ φ → M ⁡ N ⁡ X = J ⁡ F
mapdindp.x ⊢ φ → X ∈ V
mapdindp.y ⊢ φ → Y ∈ V
mapdindp.g ⊢ φ → G ∈ D
mapdindp.my ⊢ φ → M ⁡ N ⁡ Y = J ⁡ G
mapdncol.q ⊢ φ → N ⁡ X ≠ N ⁡ Y
Assertion mapdncol ⊢ φ → 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 ⊢ φ → K ∈ HL ∧ W ∈ H
10 mapdindp.f ⊢ φ → F ∈ D
11 mapdindp.mx ⊢ φ → M ⁡ N ⁡ X = J ⁡ F
12 mapdindp.x ⊢ φ → X ∈ V
13 mapdindp.y ⊢ φ → Y ∈ V
14 mapdindp.g ⊢ φ → G ∈ D
15 mapdindp.my ⊢ φ → M ⁡ N ⁡ Y = J ⁡ G
16 mapdncol.q ⊢ φ → N ⁡ X ≠ N ⁡ Y
17 eqid ⊢ LSubSp ⁡ U = LSubSp ⁡ U
18 1 3 9 dvhlmod ⊢ φ → U ∈ LMod
19 4 17 5 lspsncl ⊢ U ∈ LMod ∧ X ∈ V → N ⁡ X ∈ LSubSp ⁡ U
20 18 12 19 syl2anc ⊢ φ → N ⁡ X ∈ LSubSp ⁡ U
21 4 17 5 lspsncl ⊢ U ∈ LMod ∧ Y ∈ V → N ⁡ Y ∈ LSubSp ⁡ U
22 18 13 21 syl2anc ⊢ φ → N ⁡ Y ∈ LSubSp ⁡ U
23 1 3 17 2 9 20 22 mapd11 ⊢ φ → M ⁡ N ⁡ X = M ⁡ N ⁡ Y ↔ N ⁡ X = N ⁡ Y
24 23 necon3bid ⊢ φ → M ⁡ N ⁡ X ≠ M ⁡ N ⁡ Y ↔ N ⁡ X ≠ N ⁡ Y
25 16 24 mpbird ⊢ φ → M ⁡ N ⁡ X ≠ M ⁡ N ⁡ Y
26 25 11 15 3netr3d ⊢ φ → J ⁡ F ≠ J ⁡ G