Metamath Proof Explorer

Theorem mapdindp

Description: Transfer (part of) vector independence condition 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 ⊢ ( 𝜑 → ( 𝑀 ‘ ( 𝑁 ‘ { 𝑌 } ) ) = ( 𝐽 ‘ { 𝐺 } ) )
mapdindp.z ⊢ ( 𝜑 → 𝑍 ∈ 𝑉 )
mapdindp.e ⊢ ( 𝜑 → 𝐸 ∈ 𝐷 )
mapdindp.mg ⊢ ( 𝜑 → ( 𝑀 ‘ ( 𝑁 ‘ { 𝑍 } ) ) = ( 𝐽 ‘ { 𝐸 } ) )
mapdindp.xn ⊢ ( 𝜑 → ¬ 𝑋 ∈ ( 𝑁 ‘ { 𝑌 , 𝑍 } ) )
Assertion mapdindp ( 𝜑 → ¬ 𝐹 ∈ ( 𝐽 ‘ { 𝐺 , 𝐸 } ) )

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 mapdindp.z ⊢ ( 𝜑 → 𝑍 ∈ 𝑉 )
17 mapdindp.e ⊢ ( 𝜑 → 𝐸 ∈ 𝐷 )
18 mapdindp.mg ⊢ ( 𝜑 → ( 𝑀 ‘ ( 𝑁 ‘ { 𝑍 } ) ) = ( 𝐽 ‘ { 𝐸 } ) )
19 mapdindp.xn ⊢ ( 𝜑 → ¬ 𝑋 ∈ ( 𝑁 ‘ { 𝑌 , 𝑍 } ) )
20 eqid ⊢ ( LSubSp ‘ 𝐶 ) = ( LSubSp ‘ 𝐶 )
21 1 6 9 lcdlmod ⊢ ( 𝜑 → 𝐶 ∈ LMod )
22 7 20 8 21 14 17 lspprcl ⊢ ( 𝜑 → ( 𝐽 ‘ { 𝐺 , 𝐸 } ) ∈ ( LSubSp ‘ 𝐶 ) )
23 7 20 8 21 22 10 ellspsn5b ⊢ ( 𝜑 → ( 𝐹 ∈ ( 𝐽 ‘ { 𝐺 , 𝐸 } ) ↔ ( 𝐽 ‘ { 𝐹 } ) ⊆ ( 𝐽 ‘ { 𝐺 , 𝐸 } ) ) )
24 eqid ⊢ ( LSubSp ‘ 𝑈 ) = ( LSubSp ‘ 𝑈 )
25 1 3 9 dvhlmod ⊢ ( 𝜑 → 𝑈 ∈ LMod )
26 4 24 5 25 13 16 lspprcl ⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑌 , 𝑍 } ) ∈ ( LSubSp ‘ 𝑈 ) )
27 4 24 5 25 26 12 ellspsn5b ⊢ ( 𝜑 → ( 𝑋 ∈ ( 𝑁 ‘ { 𝑌 , 𝑍 } ) ↔ ( 𝑁 ‘ { 𝑋 } ) ⊆ ( 𝑁 ‘ { 𝑌 , 𝑍 } ) ) )
28 4 24 5 lspsncl ⊢ ( ( 𝑈 ∈ LMod ∧ 𝑋 ∈ 𝑉 ) → ( 𝑁 ‘ { 𝑋 } ) ∈ ( LSubSp ‘ 𝑈 ) )
29 25 12 28 syl2anc ⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑋 } ) ∈ ( LSubSp ‘ 𝑈 ) )
30 1 3 24 2 9 29 26 mapdord ⊢ ( 𝜑 → ( ( 𝑀 ‘ ( 𝑁 ‘ { 𝑋 } ) ) ⊆ ( 𝑀 ‘ ( 𝑁 ‘ { 𝑌 , 𝑍 } ) ) ↔ ( 𝑁 ‘ { 𝑋 } ) ⊆ ( 𝑁 ‘ { 𝑌 , 𝑍 } ) ) )
31 eqid ⊢ ( LSSum ‘ 𝑈 ) = ( LSSum ‘ 𝑈 )
32 4 5 31 25 13 16 lsmpr ⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑌 , 𝑍 } ) = ( ( 𝑁 ‘ { 𝑌 } ) ( LSSum ‘ 𝑈 ) ( 𝑁 ‘ { 𝑍 } ) ) )
33 32 fveq2d ⊢ ( 𝜑 → ( 𝑀 ‘ ( 𝑁 ‘ { 𝑌 , 𝑍 } ) ) = ( 𝑀 ‘ ( ( 𝑁 ‘ { 𝑌 } ) ( LSSum ‘ 𝑈 ) ( 𝑁 ‘ { 𝑍 } ) ) ) )
34 eqid ⊢ ( LSSum ‘ 𝐶 ) = ( LSSum ‘ 𝐶 )
35 4 24 5 lspsncl ⊢ ( ( 𝑈 ∈ LMod ∧ 𝑌 ∈ 𝑉 ) → ( 𝑁 ‘ { 𝑌 } ) ∈ ( LSubSp ‘ 𝑈 ) )
36 25 13 35 syl2anc ⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑌 } ) ∈ ( LSubSp ‘ 𝑈 ) )
37 4 24 5 lspsncl ⊢ ( ( 𝑈 ∈ LMod ∧ 𝑍 ∈ 𝑉 ) → ( 𝑁 ‘ { 𝑍 } ) ∈ ( LSubSp ‘ 𝑈 ) )
38 25 16 37 syl2anc ⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑍 } ) ∈ ( LSubSp ‘ 𝑈 ) )
39 1 2 3 24 31 6 34 9 36 38 mapdlsm ⊢ ( 𝜑 → ( 𝑀 ‘ ( ( 𝑁 ‘ { 𝑌 } ) ( LSSum ‘ 𝑈 ) ( 𝑁 ‘ { 𝑍 } ) ) ) = ( ( 𝑀 ‘ ( 𝑁 ‘ { 𝑌 } ) ) ( LSSum ‘ 𝐶 ) ( 𝑀 ‘ ( 𝑁 ‘ { 𝑍 } ) ) ) )
40 15 18 oveq12d ⊢ ( 𝜑 → ( ( 𝑀 ‘ ( 𝑁 ‘ { 𝑌 } ) ) ( LSSum ‘ 𝐶 ) ( 𝑀 ‘ ( 𝑁 ‘ { 𝑍 } ) ) ) = ( ( 𝐽 ‘ { 𝐺 } ) ( LSSum ‘ 𝐶 ) ( 𝐽 ‘ { 𝐸 } ) ) )
41 33 39 40 3eqtrd ⊢ ( 𝜑 → ( 𝑀 ‘ ( 𝑁 ‘ { 𝑌 , 𝑍 } ) ) = ( ( 𝐽 ‘ { 𝐺 } ) ( LSSum ‘ 𝐶 ) ( 𝐽 ‘ { 𝐸 } ) ) )
42 7 8 34 21 14 17 lsmpr ⊢ ( 𝜑 → ( 𝐽 ‘ { 𝐺 , 𝐸 } ) = ( ( 𝐽 ‘ { 𝐺 } ) ( LSSum ‘ 𝐶 ) ( 𝐽 ‘ { 𝐸 } ) ) )
43 41 42 eqtr4d ⊢ ( 𝜑 → ( 𝑀 ‘ ( 𝑁 ‘ { 𝑌 , 𝑍 } ) ) = ( 𝐽 ‘ { 𝐺 , 𝐸 } ) )
44 11 43 sseq12d ⊢ ( 𝜑 → ( ( 𝑀 ‘ ( 𝑁 ‘ { 𝑋 } ) ) ⊆ ( 𝑀 ‘ ( 𝑁 ‘ { 𝑌 , 𝑍 } ) ) ↔ ( 𝐽 ‘ { 𝐹 } ) ⊆ ( 𝐽 ‘ { 𝐺 , 𝐸 } ) ) )
45 27 30 44 3bitr2rd ⊢ ( 𝜑 → ( ( 𝐽 ‘ { 𝐹 } ) ⊆ ( 𝐽 ‘ { 𝐺 , 𝐸 } ) ↔ 𝑋 ∈ ( 𝑁 ‘ { 𝑌 , 𝑍 } ) ) )
46 23 45 bitrd ⊢ ( 𝜑 → ( 𝐹 ∈ ( 𝐽 ‘ { 𝐺 , 𝐸 } ) ↔ 𝑋 ∈ ( 𝑁 ‘ { 𝑌 , 𝑍 } ) ) )
47 19 46 mtbird ⊢ ( 𝜑 → ¬ 𝐹 ∈ ( 𝐽 ‘ { 𝐺 , 𝐸 } ) )