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 ellspsn5 ⊢ ( 𝜑 → ( 𝑁 ‘ { 𝐸 } ) ⊆ ( 𝑁 ‘ { 𝐸 , 𝑇 } ) )
30 3 4 26 19 20 lspprid2 ⊢ ( 𝜑 → 𝑇 ∈ ( 𝑁 ‘ { 𝐸 , 𝑇 } ) )
31 25 4 26 27 30 ellspsn5 ⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑇 } ) ⊆ ( 𝑁 ‘ { 𝐸 , 𝑇 } ) )
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 ⊢ ( 𝜑 → ( 𝑀 ‘ ( 𝑁 ‘ { 𝑇 } ) ) = ( 𝐿 ‘ { ( 𝑆 ‘ 𝑇 ) } ) )