# Metamath Proof Explorer

## Theorem hdmapeveclem

Description: Lemma for hdmapevec . TODO: combine with hdmapevec if it shortens overall. (Contributed by NM, 16-May-2015)

Ref Expression
Hypotheses hdmapevec.h 𝐻 = ( LHyp ‘ 𝐾 )
hdmapevec.e 𝐸 = ⟨ ( I ↾ ( Base ‘ 𝐾 ) ) , ( I ↾ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) ⟩
hdmapevec.j 𝐽 = ( ( HVMap ‘ 𝐾 ) ‘ 𝑊 )
hdmapevec.s 𝑆 = ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 )
hdmapevec.k ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) )
hdmapevec.u 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
hdmapevec.v 𝑉 = ( Base ‘ 𝑈 )
hdmapevec.n 𝑁 = ( LSpan ‘ 𝑈 )
hdmapevec.c 𝐶 = ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 )
hdmapevec.d 𝐷 = ( Base ‘ 𝐶 )
hdmapevec.i 𝐼 = ( ( HDMap1 ‘ 𝐾 ) ‘ 𝑊 )
hdmapevec.x ( 𝜑𝑋𝑉 )
hdmapevec.ne ( 𝜑 → ¬ 𝑋 ∈ ( ( 𝑁 ‘ { 𝐸 } ) ∪ ( 𝑁 ‘ { 𝐸 } ) ) )
Assertion hdmapeveclem ( 𝜑 → ( 𝑆𝐸 ) = ( 𝐽𝐸 ) )

### Proof

Step Hyp Ref Expression
1 hdmapevec.h 𝐻 = ( LHyp ‘ 𝐾 )
2 hdmapevec.e 𝐸 = ⟨ ( I ↾ ( Base ‘ 𝐾 ) ) , ( I ↾ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) ⟩
3 hdmapevec.j 𝐽 = ( ( HVMap ‘ 𝐾 ) ‘ 𝑊 )
4 hdmapevec.s 𝑆 = ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 )
5 hdmapevec.k ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) )
6 hdmapevec.u 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
7 hdmapevec.v 𝑉 = ( Base ‘ 𝑈 )
8 hdmapevec.n 𝑁 = ( LSpan ‘ 𝑈 )
9 hdmapevec.c 𝐶 = ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 )
10 hdmapevec.d 𝐷 = ( Base ‘ 𝐶 )
11 hdmapevec.i 𝐼 = ( ( HDMap1 ‘ 𝐾 ) ‘ 𝑊 )
12 hdmapevec.x ( 𝜑𝑋𝑉 )
13 hdmapevec.ne ( 𝜑 → ¬ 𝑋 ∈ ( ( 𝑁 ‘ { 𝐸 } ) ∪ ( 𝑁 ‘ { 𝐸 } ) ) )
14 eqid ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
15 eqid ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
16 eqid ( 0g𝑈 ) = ( 0g𝑈 )
17 1 14 15 6 7 16 2 5 dvheveccl ( 𝜑𝐸 ∈ ( 𝑉 ∖ { ( 0g𝑈 ) } ) )
18 17 eldifad ( 𝜑𝐸𝑉 )
19 1 2 6 7 8 9 10 3 11 4 5 18 12 13 hdmapval2 ( 𝜑 → ( 𝑆𝐸 ) = ( 𝐼 ‘ ⟨ 𝑋 , ( 𝐼 ‘ ⟨ 𝐸 , ( 𝐽𝐸 ) , 𝑋 ⟩ ) , 𝐸 ⟩ ) )
20 eqid ( LSpan ‘ 𝐶 ) = ( LSpan ‘ 𝐶 )
21 eqid ( ( mapd ‘ 𝐾 ) ‘ 𝑊 ) = ( ( mapd ‘ 𝐾 ) ‘ 𝑊 )
22 eqid ( 0g𝐶 ) = ( 0g𝐶 )
23 1 6 7 16 9 10 22 3 5 17 hvmapcl2 ( 𝜑 → ( 𝐽𝐸 ) ∈ ( 𝐷 ∖ { ( 0g𝐶 ) } ) )
24 23 eldifad ( 𝜑 → ( 𝐽𝐸 ) ∈ 𝐷 )
25 1 6 7 16 8 9 20 21 3 5 17 mapdhvmap ( 𝜑 → ( ( ( mapd ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑁 ‘ { 𝐸 } ) ) = ( ( LSpan ‘ 𝐶 ) ‘ { ( 𝐽𝐸 ) } ) )
26 1 6 5 dvhlmod ( 𝜑𝑈 ∈ LMod )
27 7 8 26 12 13 18 hdmaplem1 ( 𝜑 → ( 𝑁 ‘ { 𝑋 } ) ≠ ( 𝑁 ‘ { 𝐸 } ) )
28 27 necomd ( 𝜑 → ( 𝑁 ‘ { 𝐸 } ) ≠ ( 𝑁 ‘ { 𝑋 } ) )
29 7 8 26 12 13 18 16 hdmaplem3 ( 𝜑𝑋 ∈ ( 𝑉 ∖ { ( 0g𝑈 ) } ) )
30 eqidd ( 𝜑 → ( 𝐼 ‘ ⟨ 𝐸 , ( 𝐽𝐸 ) , 𝑋 ⟩ ) = ( 𝐼 ‘ ⟨ 𝐸 , ( 𝐽𝐸 ) , 𝑋 ⟩ ) )
31 1 6 7 16 8 9 10 20 21 11 5 24 25 28 17 29 30 hdmap1eq2 ( 𝜑 → ( 𝐼 ‘ ⟨ 𝑋 , ( 𝐼 ‘ ⟨ 𝐸 , ( 𝐽𝐸 ) , 𝑋 ⟩ ) , 𝐸 ⟩ ) = ( 𝐽𝐸 ) )
32 19 31 eqtrd ( 𝜑 → ( 𝑆𝐸 ) = ( 𝐽𝐸 ) )