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 ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
mapdindp.m ⊢ 𝑀 = ( ( mapd ‘ 𝐾 ) ‘ 𝑊 )
mapdindp.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
mapdindp.v ⊢ 𝑉 = ( Base ‘ 𝑈 )
mapdindp.n ⊢ 𝑁 = ( LSpan ‘ 𝑈 )
mapdindp.c ⊢ 𝐶 = ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 )
mapdindp.d ⊢ 𝐷 = ( Base ‘ 𝐶 )
mapdindp.j ⊢ 𝐽 = ( LSpan ‘ 𝐶 )
mapdindp.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
mapdindp.f ⊢ ( 𝜑 → 𝐹 ∈ 𝐷 )
mapdindp.mx ⊢ ( 𝜑 → ( 𝑀 ‘ ( 𝑁 ‘ { 𝑋 } ) ) = ( 𝐽 ‘ { 𝐹 } ) )
mapdindp.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
mapdindp.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑉 )
mapdindp.g ⊢ ( 𝜑 → 𝐺 ∈ 𝐷 )
mapdindp.my ⊢ ( 𝜑 → ( 𝑀 ‘ ( 𝑁 ‘ { 𝑌 } ) ) = ( 𝐽 ‘ { 𝐺 } ) )
mapdncol.q ⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑋 } ) ≠ ( 𝑁 ‘ { 𝑌 } ) )
Assertion mapdncol ( 𝜑 → ( 𝐽 ‘ { 𝐹 } ) ≠ ( 𝐽 ‘ { 𝐺 } ) )

Proof

Step Hyp Ref Expression
1 mapdindp.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2 mapdindp.m ⊢ 𝑀 = ( ( mapd ‘ 𝐾 ) ‘ 𝑊 )
3 mapdindp.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
4 mapdindp.v ⊢ 𝑉 = ( Base ‘ 𝑈 )
5 mapdindp.n ⊢ 𝑁 = ( LSpan ‘ 𝑈 )
6 mapdindp.c ⊢ 𝐶 = ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 )
7 mapdindp.d ⊢ 𝐷 = ( Base ‘ 𝐶 )
8 mapdindp.j ⊢ 𝐽 = ( LSpan ‘ 𝐶 )
9 mapdindp.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
10 mapdindp.f ⊢ ( 𝜑 → 𝐹 ∈ 𝐷 )
11 mapdindp.mx ⊢ ( 𝜑 → ( 𝑀 ‘ ( 𝑁 ‘ { 𝑋 } ) ) = ( 𝐽 ‘ { 𝐹 } ) )
12 mapdindp.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
13 mapdindp.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑉 )
14 mapdindp.g ⊢ ( 𝜑 → 𝐺 ∈ 𝐷 )
15 mapdindp.my ⊢ ( 𝜑 → ( 𝑀 ‘ ( 𝑁 ‘ { 𝑌 } ) ) = ( 𝐽 ‘ { 𝐺 } ) )
16 mapdncol.q ⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑋 } ) ≠ ( 𝑁 ‘ { 𝑌 } ) )
17 eqid ⊢ ( LSubSp ‘ 𝑈 ) = ( LSubSp ‘ 𝑈 )
18 1 3 9 dvhlmod ⊢ ( 𝜑 → 𝑈 ∈ LMod )
19 4 17 5 lspsncl ⊢ ( ( 𝑈 ∈ LMod ∧ 𝑋 ∈ 𝑉 ) → ( 𝑁 ‘ { 𝑋 } ) ∈ ( LSubSp ‘ 𝑈 ) )
20 18 12 19 syl2anc ⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑋 } ) ∈ ( LSubSp ‘ 𝑈 ) )
21 4 17 5 lspsncl ⊢ ( ( 𝑈 ∈ LMod ∧ 𝑌 ∈ 𝑉 ) → ( 𝑁 ‘ { 𝑌 } ) ∈ ( LSubSp ‘ 𝑈 ) )
22 18 13 21 syl2anc ⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑌 } ) ∈ ( LSubSp ‘ 𝑈 ) )
23 1 3 17 2 9 20 22 mapd11 ⊢ ( 𝜑 → ( ( 𝑀 ‘ ( 𝑁 ‘ { 𝑋 } ) ) = ( 𝑀 ‘ ( 𝑁 ‘ { 𝑌 } ) ) ↔ ( 𝑁 ‘ { 𝑋 } ) = ( 𝑁 ‘ { 𝑌 } ) ) )
24 23 necon3bid ⊢ ( 𝜑 → ( ( 𝑀 ‘ ( 𝑁 ‘ { 𝑋 } ) ) ≠ ( 𝑀 ‘ ( 𝑁 ‘ { 𝑌 } ) ) ↔ ( 𝑁 ‘ { 𝑋 } ) ≠ ( 𝑁 ‘ { 𝑌 } ) ) )
25 16 24 mpbird ⊢ ( 𝜑 → ( 𝑀 ‘ ( 𝑁 ‘ { 𝑋 } ) ) ≠ ( 𝑀 ‘ ( 𝑁 ‘ { 𝑌 } ) ) )
26 25 11 15 3netr3d ⊢ ( 𝜑 → ( 𝐽 ‘ { 𝐹 } ) ≠ ( 𝐽 ‘ { 𝐺 } ) )