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

Theorem hdmap1valc 35807
 Description: Connect the value of the preliminary map from vectors to functionals to the hypothesis used by earlier theorems. Note: the hypothesis could be the more general but the former will be easier to use. TODO: use the function directly in those theorems, so this theorem becomes unnecessary? TODO: The hdmap1cbv 35806 is probably unnecessary, but it would mean different \$d's later on. (Contributed by NM, 15-May-2015.)
Hypotheses
Ref Expression
hdmap1valc.h
hdmap1valc.u
hdmap1valc.v
hdmap1valc.s
hdmap1valc.o
hdmap1valc.n
hdmap1valc.c LCDual
hdmap1valc.d
hdmap1valc.r
hdmap1valc.q
hdmap1valc.j
hdmap1valc.m mapd
hdmap1valc.i HDMap1
hdmap1valc.k
hdmap1valc.x
hdmap1valc.f
hdmap1valc.y
hdmap1valc.l
Assertion
Ref Expression
hdmap1valc
Distinct variable groups:   ,   ,,   ,,   ,,   ,,   ,,   ,,   ,
Allowed substitution hints:   (,)   (,)   ()   (,)   (,)   (,)   (,)   (,)   (,)   (,)   (,)   (,)   (,)   ()

Proof of Theorem hdmap1valc
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 hdmap1valc.h . . 3
2 hdmap1valc.u . . 3
3 hdmap1valc.v . . 3
4 hdmap1valc.s . . 3
5 hdmap1valc.o . . 3
6 hdmap1valc.n . . 3
7 hdmap1valc.c . . 3 LCDual
8 hdmap1valc.d . . 3
9 hdmap1valc.r . . 3
10 hdmap1valc.q . . 3
11 hdmap1valc.j . . 3
12 hdmap1valc.m . . 3 mapd
13 hdmap1valc.i . . 3 HDMap1
14 hdmap1valc.k . . 3
15 hdmap1valc.x . . . 4