Mathbox for Norm Megill < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  hdmapeveclem Structured version   Unicode version

Theorem hdmapeveclem 32697
 Description: Lemma for hdmapevec 32698. TODO: combine with hdmapevec 32698 if it shortens overall. (Contributed by NM, 16-May-2015.)
Hypotheses
Ref Expression
hdmapevec.h
hdmapevec.e
hdmapevec.j HVMap
hdmapevec.s HDMap
hdmapevec.k
hdmapevec.u
hdmapevec.v
hdmapevec.n
hdmapevec.c LCDual
hdmapevec.d
hdmapevec.i HDMap1
hdmapevec.x
hdmapevec.ne
Assertion
Ref Expression
hdmapeveclem

Proof of Theorem hdmapeveclem
StepHypRef Expression
1 hdmapevec.h . . 3
2 hdmapevec.e . . 3
3 hdmapevec.u . . 3
4 hdmapevec.v . . 3
5 hdmapevec.n . . 3
6 hdmapevec.c . . 3 LCDual
7 hdmapevec.d . . 3
8 hdmapevec.j . . 3 HVMap
9 hdmapevec.i . . 3 HDMap1
10 hdmapevec.s . . 3 HDMap
11 hdmapevec.k . . 3
12 eqid 2438 . . . . 5
13 eqid 2438 . . . . 5
14 eqid 2438 . . . . 5
151, 12, 13, 3, 4, 14, 2, 11dvheveccl 31972 . . . 4
17 hdmapevec.x . . 3
18 hdmapevec.ne . . 3
191, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 16, 17, 18hdmapval2 32695 . 2
20 eqid 2438 . . 3
21 eqid 2438 . . 3 mapd mapd
22 eqid 2438 . . . . 5
231, 3, 4, 14, 6, 7, 22, 8, 11, 15hvmapcl2 32626 . . . 4