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

Theorem hdmap14lem7 32602
 Description: Combine cases of . TODO: Can this be done at once in hdmap14lem3 32598, in order to get rid of hdmap14lem6 32601? Perhaps modify lspsneu 16187 to become instead of ? (Contributed by NM, 1-Jun-2015.)
Hypotheses
Ref Expression
hdmap14lem7.h
hdmap14lem7.u
hdmap14lem7.v
hdmap14lem7.t
hdmap14lem7.o
hdmap14lem7.r Scalar
hdmap14lem7.b
hdmap14lem7.c LCDual
hdmap14lem7.e
hdmap14lem7.p Scalar
hdmap14lem7.a
hdmap14lem7.s HDMap
hdmap14lem7.k
hdmap14lem7.x
hdmap14lem7.f
Assertion
Ref Expression
hdmap14lem7
Distinct variable groups:   ,   ,   ,   ,   ,   ,   ,   ,   ,   ,
Allowed substitution hints:   ()   ()   ()   ()   ()   ()   ()

Proof of Theorem hdmap14lem7
StepHypRef Expression
1 hdmap14lem7.h . . 3
2 hdmap14lem7.u . . 3
3 hdmap14lem7.v . . 3
4 hdmap14lem7.t . . 3
5 hdmap14lem7.o . . 3
6 hdmap14lem7.r . . 3 Scalar
7 hdmap14lem7.b . . 3
8 eqid 2435 . . 3
9 hdmap14lem7.c . . 3 LCDual
10 hdmap14lem7.e . . 3
11 eqid 2435 . . 3
12 hdmap14lem7.p . . 3 Scalar
13 hdmap14lem7.a . . 3
14 eqid 2435 . . 3
15 hdmap14lem7.s . . 3 HDMap
16 hdmap14lem7.k . . . 4
18 hdmap14lem7.x . . . 4