Metamath Proof Explorer


Theorem hdmap10lem

Description: Lemma for hdmap10 . (Contributed by NM, 17-May-2015)

Ref Expression
Hypotheses hdmap10.h 𝐻 = ( LHyp ‘ 𝐾 )
hdmap10.u 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
hdmap10.v 𝑉 = ( Base ‘ 𝑈 )
hdmap10.n 𝑁 = ( LSpan ‘ 𝑈 )
hdmap10.c 𝐶 = ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 )
hdmap10.l 𝐿 = ( LSpan ‘ 𝐶 )
hdmap10.m 𝑀 = ( ( mapd ‘ 𝐾 ) ‘ 𝑊 )
hdmap10.s 𝑆 = ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 )
hdmap10.k ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) )
hdmap10.e 𝐸 = ⟨ ( I ↾ ( Base ‘ 𝐾 ) ) , ( I ↾ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) ⟩
hdmap10.o 0 = ( 0g𝑈 )
hdmap10.d 𝐷 = ( Base ‘ 𝐶 )
hdmap10.j 𝐽 = ( ( HVMap ‘ 𝐾 ) ‘ 𝑊 )
hdmap10.i 𝐼 = ( ( HDMap1 ‘ 𝐾 ) ‘ 𝑊 )
hdmap10lem.t ( 𝜑𝑇 ∈ ( 𝑉 ∖ { 0 } ) )
Assertion hdmap10lem ( 𝜑 → ( 𝑀 ‘ ( 𝑁 ‘ { 𝑇 } ) ) = ( 𝐿 ‘ { ( 𝑆𝑇 ) } ) )

Proof

Step Hyp Ref Expression
1 hdmap10.h 𝐻 = ( LHyp ‘ 𝐾 )
2 hdmap10.u 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
3 hdmap10.v 𝑉 = ( Base ‘ 𝑈 )
4 hdmap10.n 𝑁 = ( LSpan ‘ 𝑈 )
5 hdmap10.c 𝐶 = ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 )
6 hdmap10.l 𝐿 = ( LSpan ‘ 𝐶 )
7 hdmap10.m 𝑀 = ( ( mapd ‘ 𝐾 ) ‘ 𝑊 )
8 hdmap10.s 𝑆 = ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 )
9 hdmap10.k ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) )
10 hdmap10.e 𝐸 = ⟨ ( I ↾ ( Base ‘ 𝐾 ) ) , ( I ↾ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) ⟩
11 hdmap10.o 0 = ( 0g𝑈 )
12 hdmap10.d 𝐷 = ( Base ‘ 𝐶 )
13 hdmap10.j 𝐽 = ( ( HVMap ‘ 𝐾 ) ‘ 𝑊 )
14 hdmap10.i 𝐼 = ( ( HDMap1 ‘ 𝐾 ) ‘ 𝑊 )
15 hdmap10lem.t ( 𝜑𝑇 ∈ ( 𝑉 ∖ { 0 } ) )
16 eqid ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
17 eqid ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
18 1 16 17 2 3 11 10 9 dvheveccl ( 𝜑𝐸 ∈ ( 𝑉 ∖ { 0 } ) )
19 18 eldifad ( 𝜑𝐸𝑉 )
20 15 eldifad ( 𝜑𝑇𝑉 )
21 1 2 3 4 9 19 20 dvh3dim ( 𝜑 → ∃ 𝑥𝑉 ¬ 𝑥 ∈ ( 𝑁 ‘ { 𝐸 , 𝑇 } ) )
22 9 3ad2ant1 ( ( 𝜑𝑥𝑉 ∧ ¬ 𝑥 ∈ ( 𝑁 ‘ { 𝐸 , 𝑇 } ) ) → ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) )
23 20 3ad2ant1 ( ( 𝜑𝑥𝑉 ∧ ¬ 𝑥 ∈ ( 𝑁 ‘ { 𝐸 , 𝑇 } ) ) → 𝑇𝑉 )
24 simp2 ( ( 𝜑𝑥𝑉 ∧ ¬ 𝑥 ∈ ( 𝑁 ‘ { 𝐸 , 𝑇 } ) ) → 𝑥𝑉 )
25 eqid ( LSubSp ‘ 𝑈 ) = ( LSubSp ‘ 𝑈 )
26 1 2 9 dvhlmod ( 𝜑𝑈 ∈ LMod )
27 3 25 4 26 19 20 lspprcl ( 𝜑 → ( 𝑁 ‘ { 𝐸 , 𝑇 } ) ∈ ( LSubSp ‘ 𝑈 ) )
28 3 4 26 19 20 lspprid1 ( 𝜑𝐸 ∈ ( 𝑁 ‘ { 𝐸 , 𝑇 } ) )
29 25 4 26 27 28 lspsnel5a ( 𝜑 → ( 𝑁 ‘ { 𝐸 } ) ⊆ ( 𝑁 ‘ { 𝐸 , 𝑇 } ) )
30 3 4 26 19 20 lspprid2 ( 𝜑𝑇 ∈ ( 𝑁 ‘ { 𝐸 , 𝑇 } ) )
31 25 4 26 27 30 lspsnel5a ( 𝜑 → ( 𝑁 ‘ { 𝑇 } ) ⊆ ( 𝑁 ‘ { 𝐸 , 𝑇 } ) )
32 29 31 unssd ( 𝜑 → ( ( 𝑁 ‘ { 𝐸 } ) ∪ ( 𝑁 ‘ { 𝑇 } ) ) ⊆ ( 𝑁 ‘ { 𝐸 , 𝑇 } ) )
33 32 sseld ( 𝜑 → ( 𝑥 ∈ ( ( 𝑁 ‘ { 𝐸 } ) ∪ ( 𝑁 ‘ { 𝑇 } ) ) → 𝑥 ∈ ( 𝑁 ‘ { 𝐸 , 𝑇 } ) ) )
34 33 con3dimp ( ( 𝜑 ∧ ¬ 𝑥 ∈ ( 𝑁 ‘ { 𝐸 , 𝑇 } ) ) → ¬ 𝑥 ∈ ( ( 𝑁 ‘ { 𝐸 } ) ∪ ( 𝑁 ‘ { 𝑇 } ) ) )
35 34 3adant2 ( ( 𝜑𝑥𝑉 ∧ ¬ 𝑥 ∈ ( 𝑁 ‘ { 𝐸 , 𝑇 } ) ) → ¬ 𝑥 ∈ ( ( 𝑁 ‘ { 𝐸 } ) ∪ ( 𝑁 ‘ { 𝑇 } ) ) )
36 1 10 2 3 4 5 12 13 14 8 22 23 24 35 hdmapval2 ( ( 𝜑𝑥𝑉 ∧ ¬ 𝑥 ∈ ( 𝑁 ‘ { 𝐸 , 𝑇 } ) ) → ( 𝑆𝑇 ) = ( 𝐼 ‘ ⟨ 𝑥 , ( 𝐼 ‘ ⟨ 𝐸 , ( 𝐽𝐸 ) , 𝑥 ⟩ ) , 𝑇 ⟩ ) )
37 36 eqcomd ( ( 𝜑𝑥𝑉 ∧ ¬ 𝑥 ∈ ( 𝑁 ‘ { 𝐸 , 𝑇 } ) ) → ( 𝐼 ‘ ⟨ 𝑥 , ( 𝐼 ‘ ⟨ 𝐸 , ( 𝐽𝐸 ) , 𝑥 ⟩ ) , 𝑇 ⟩ ) = ( 𝑆𝑇 ) )
38 eqid ( -g𝑈 ) = ( -g𝑈 )
39 eqid ( -g𝐶 ) = ( -g𝐶 )
40 26 3ad2ant1 ( ( 𝜑𝑥𝑉 ∧ ¬ 𝑥 ∈ ( 𝑁 ‘ { 𝐸 , 𝑇 } ) ) → 𝑈 ∈ LMod )
41 27 3ad2ant1 ( ( 𝜑𝑥𝑉 ∧ ¬ 𝑥 ∈ ( 𝑁 ‘ { 𝐸 , 𝑇 } ) ) → ( 𝑁 ‘ { 𝐸 , 𝑇 } ) ∈ ( LSubSp ‘ 𝑈 ) )
42 simp3 ( ( 𝜑𝑥𝑉 ∧ ¬ 𝑥 ∈ ( 𝑁 ‘ { 𝐸 , 𝑇 } ) ) → ¬ 𝑥 ∈ ( 𝑁 ‘ { 𝐸 , 𝑇 } ) )
43 11 25 40 41 24 42 lssneln0 ( ( 𝜑𝑥𝑉 ∧ ¬ 𝑥 ∈ ( 𝑁 ‘ { 𝐸 , 𝑇 } ) ) → 𝑥 ∈ ( 𝑉 ∖ { 0 } ) )
44 eqid ( 0g𝐶 ) = ( 0g𝐶 )
45 1 2 3 11 5 12 44 13 9 18 hvmapcl2 ( 𝜑 → ( 𝐽𝐸 ) ∈ ( 𝐷 ∖ { ( 0g𝐶 ) } ) )
46 45 eldifad ( 𝜑 → ( 𝐽𝐸 ) ∈ 𝐷 )
47 46 3ad2ant1 ( ( 𝜑𝑥𝑉 ∧ ¬ 𝑥 ∈ ( 𝑁 ‘ { 𝐸 , 𝑇 } ) ) → ( 𝐽𝐸 ) ∈ 𝐷 )
48 1 2 3 11 4 5 6 7 13 9 18 mapdhvmap ( 𝜑 → ( 𝑀 ‘ ( 𝑁 ‘ { 𝐸 } ) ) = ( 𝐿 ‘ { ( 𝐽𝐸 ) } ) )
49 48 3ad2ant1 ( ( 𝜑𝑥𝑉 ∧ ¬ 𝑥 ∈ ( 𝑁 ‘ { 𝐸 , 𝑇 } ) ) → ( 𝑀 ‘ ( 𝑁 ‘ { 𝐸 } ) ) = ( 𝐿 ‘ { ( 𝐽𝐸 ) } ) )
50 1 2 9 dvhlvec ( 𝜑𝑈 ∈ LVec )
51 50 3ad2ant1 ( ( 𝜑𝑥𝑉 ∧ ¬ 𝑥 ∈ ( 𝑁 ‘ { 𝐸 , 𝑇 } ) ) → 𝑈 ∈ LVec )
52 19 3ad2ant1 ( ( 𝜑𝑥𝑉 ∧ ¬ 𝑥 ∈ ( 𝑁 ‘ { 𝐸 , 𝑇 } ) ) → 𝐸𝑉 )
53 3 4 51 24 52 23 42 lspindpi ( ( 𝜑𝑥𝑉 ∧ ¬ 𝑥 ∈ ( 𝑁 ‘ { 𝐸 , 𝑇 } ) ) → ( ( 𝑁 ‘ { 𝑥 } ) ≠ ( 𝑁 ‘ { 𝐸 } ) ∧ ( 𝑁 ‘ { 𝑥 } ) ≠ ( 𝑁 ‘ { 𝑇 } ) ) )
54 53 simpld ( ( 𝜑𝑥𝑉 ∧ ¬ 𝑥 ∈ ( 𝑁 ‘ { 𝐸 , 𝑇 } ) ) → ( 𝑁 ‘ { 𝑥 } ) ≠ ( 𝑁 ‘ { 𝐸 } ) )
55 54 necomd ( ( 𝜑𝑥𝑉 ∧ ¬ 𝑥 ∈ ( 𝑁 ‘ { 𝐸 , 𝑇 } ) ) → ( 𝑁 ‘ { 𝐸 } ) ≠ ( 𝑁 ‘ { 𝑥 } ) )
56 18 3ad2ant1 ( ( 𝜑𝑥𝑉 ∧ ¬ 𝑥 ∈ ( 𝑁 ‘ { 𝐸 , 𝑇 } ) ) → 𝐸 ∈ ( 𝑉 ∖ { 0 } ) )
57 1 2 3 11 4 5 12 6 7 14 22 47 49 55 56 24 hdmap1cl ( ( 𝜑𝑥𝑉 ∧ ¬ 𝑥 ∈ ( 𝑁 ‘ { 𝐸 , 𝑇 } ) ) → ( 𝐼 ‘ ⟨ 𝐸 , ( 𝐽𝐸 ) , 𝑥 ⟩ ) ∈ 𝐷 )
58 15 3ad2ant1 ( ( 𝜑𝑥𝑉 ∧ ¬ 𝑥 ∈ ( 𝑁 ‘ { 𝐸 , 𝑇 } ) ) → 𝑇 ∈ ( 𝑉 ∖ { 0 } ) )
59 1 2 3 5 12 8 9 20 hdmapcl ( 𝜑 → ( 𝑆𝑇 ) ∈ 𝐷 )
60 59 3ad2ant1 ( ( 𝜑𝑥𝑉 ∧ ¬ 𝑥 ∈ ( 𝑁 ‘ { 𝐸 , 𝑇 } ) ) → ( 𝑆𝑇 ) ∈ 𝐷 )
61 53 simprd ( ( 𝜑𝑥𝑉 ∧ ¬ 𝑥 ∈ ( 𝑁 ‘ { 𝐸 , 𝑇 } ) ) → ( 𝑁 ‘ { 𝑥 } ) ≠ ( 𝑁 ‘ { 𝑇 } ) )
62 eqid ( 𝐼 ‘ ⟨ 𝐸 , ( 𝐽𝐸 ) , 𝑥 ⟩ ) = ( 𝐼 ‘ ⟨ 𝐸 , ( 𝐽𝐸 ) , 𝑥 ⟩ )
63 1 2 3 38 11 4 5 12 39 6 7 14 22 56 47 43 57 55 49 hdmap1eq ( ( 𝜑𝑥𝑉 ∧ ¬ 𝑥 ∈ ( 𝑁 ‘ { 𝐸 , 𝑇 } ) ) → ( ( 𝐼 ‘ ⟨ 𝐸 , ( 𝐽𝐸 ) , 𝑥 ⟩ ) = ( 𝐼 ‘ ⟨ 𝐸 , ( 𝐽𝐸 ) , 𝑥 ⟩ ) ↔ ( ( 𝑀 ‘ ( 𝑁 ‘ { 𝑥 } ) ) = ( 𝐿 ‘ { ( 𝐼 ‘ ⟨ 𝐸 , ( 𝐽𝐸 ) , 𝑥 ⟩ ) } ) ∧ ( 𝑀 ‘ ( 𝑁 ‘ { ( 𝐸 ( -g𝑈 ) 𝑥 ) } ) ) = ( 𝐿 ‘ { ( ( 𝐽𝐸 ) ( -g𝐶 ) ( 𝐼 ‘ ⟨ 𝐸 , ( 𝐽𝐸 ) , 𝑥 ⟩ ) ) } ) ) ) )
64 62 63 mpbii ( ( 𝜑𝑥𝑉 ∧ ¬ 𝑥 ∈ ( 𝑁 ‘ { 𝐸 , 𝑇 } ) ) → ( ( 𝑀 ‘ ( 𝑁 ‘ { 𝑥 } ) ) = ( 𝐿 ‘ { ( 𝐼 ‘ ⟨ 𝐸 , ( 𝐽𝐸 ) , 𝑥 ⟩ ) } ) ∧ ( 𝑀 ‘ ( 𝑁 ‘ { ( 𝐸 ( -g𝑈 ) 𝑥 ) } ) ) = ( 𝐿 ‘ { ( ( 𝐽𝐸 ) ( -g𝐶 ) ( 𝐼 ‘ ⟨ 𝐸 , ( 𝐽𝐸 ) , 𝑥 ⟩ ) ) } ) ) )
65 64 simpld ( ( 𝜑𝑥𝑉 ∧ ¬ 𝑥 ∈ ( 𝑁 ‘ { 𝐸 , 𝑇 } ) ) → ( 𝑀 ‘ ( 𝑁 ‘ { 𝑥 } ) ) = ( 𝐿 ‘ { ( 𝐼 ‘ ⟨ 𝐸 , ( 𝐽𝐸 ) , 𝑥 ⟩ ) } ) )
66 1 2 3 38 11 4 5 12 39 6 7 14 22 43 57 58 60 61 65 hdmap1eq ( ( 𝜑𝑥𝑉 ∧ ¬ 𝑥 ∈ ( 𝑁 ‘ { 𝐸 , 𝑇 } ) ) → ( ( 𝐼 ‘ ⟨ 𝑥 , ( 𝐼 ‘ ⟨ 𝐸 , ( 𝐽𝐸 ) , 𝑥 ⟩ ) , 𝑇 ⟩ ) = ( 𝑆𝑇 ) ↔ ( ( 𝑀 ‘ ( 𝑁 ‘ { 𝑇 } ) ) = ( 𝐿 ‘ { ( 𝑆𝑇 ) } ) ∧ ( 𝑀 ‘ ( 𝑁 ‘ { ( 𝑥 ( -g𝑈 ) 𝑇 ) } ) ) = ( 𝐿 ‘ { ( ( 𝐼 ‘ ⟨ 𝐸 , ( 𝐽𝐸 ) , 𝑥 ⟩ ) ( -g𝐶 ) ( 𝑆𝑇 ) ) } ) ) ) )
67 37 66 mpbid ( ( 𝜑𝑥𝑉 ∧ ¬ 𝑥 ∈ ( 𝑁 ‘ { 𝐸 , 𝑇 } ) ) → ( ( 𝑀 ‘ ( 𝑁 ‘ { 𝑇 } ) ) = ( 𝐿 ‘ { ( 𝑆𝑇 ) } ) ∧ ( 𝑀 ‘ ( 𝑁 ‘ { ( 𝑥 ( -g𝑈 ) 𝑇 ) } ) ) = ( 𝐿 ‘ { ( ( 𝐼 ‘ ⟨ 𝐸 , ( 𝐽𝐸 ) , 𝑥 ⟩ ) ( -g𝐶 ) ( 𝑆𝑇 ) ) } ) ) )
68 67 simpld ( ( 𝜑𝑥𝑉 ∧ ¬ 𝑥 ∈ ( 𝑁 ‘ { 𝐸 , 𝑇 } ) ) → ( 𝑀 ‘ ( 𝑁 ‘ { 𝑇 } ) ) = ( 𝐿 ‘ { ( 𝑆𝑇 ) } ) )
69 68 rexlimdv3a ( 𝜑 → ( ∃ 𝑥𝑉 ¬ 𝑥 ∈ ( 𝑁 ‘ { 𝐸 , 𝑇 } ) → ( 𝑀 ‘ ( 𝑁 ‘ { 𝑇 } ) ) = ( 𝐿 ‘ { ( 𝑆𝑇 ) } ) ) )
70 21 69 mpd ( 𝜑 → ( 𝑀 ‘ ( 𝑁 ‘ { 𝑇 } ) ) = ( 𝐿 ‘ { ( 𝑆𝑇 ) } ) )