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

Theorem hdmap1eq2 32666
 Description: Convert mapdheq2 32589 to use HDMap1 function. (Contributed by NM, 16-May-2015.)
Hypotheses
Ref Expression
hdmap1eq2.h
hdmap1eq2.u
hdmap1eq2.v
hdmap1eq2.o
hdmap1eq2.n
hdmap1eq2.c LCDual
hdmap1eq2.d
hdmap1eq2.l
hdmap1eq2.m mapd
hdmap1eq2.i HDMap1
hdmap1eq2.k
hdmap1eq2.f
hdmap1eq2.mn
hdmap1eq2.ne
hdmap1eq2.x
hdmap1eq2.y
hdmap1eq2.e
Assertion
Ref Expression
hdmap1eq2

Proof of Theorem hdmap1eq2
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 hdmap1eq2.h . . 3
2 hdmap1eq2.u . . 3
3 hdmap1eq2.v . . 3
4 eqid 2438 . . 3
5 hdmap1eq2.o . . 3
6 hdmap1eq2.n . . 3
7 hdmap1eq2.c . . 3 LCDual
8 hdmap1eq2.d . . 3
9 eqid 2438 . . 3
10 eqid 2438 . . 3
11 hdmap1eq2.l . . 3
12 hdmap1eq2.m . . 3 mapd
13 hdmap1eq2.i . . 3 HDMap1
14 hdmap1eq2.k . . 3
15 hdmap1eq2.y . . 3
16 hdmap1eq2.e . . . 4
17 hdmap1eq2.f . . . . 5
18 hdmap1eq2.mn . . . . 5
19 hdmap1eq2.ne . . . . 5
20 hdmap1eq2.x . . . . 5
2115eldifad 3334 . . . . 5
221, 2, 3, 5, 6, 7, 8, 11, 12, 13, 14, 17, 18, 19, 20, 21hdmap1cl 32665 . . . 4
2316, 22eqeltrrd 2513 . . 3