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

Theorem hdmapinvlem2 32658
 Description: Line 28 in [Baer] p. 110, 0 = f(w,u). (Contributed by NM, 11-Jun-2015.)
Hypotheses
Ref Expression
hdmapinvlem1.h
hdmapinvlem1.e
hdmapinvlem1.o
hdmapinvlem1.u
hdmapinvlem1.v
hdmapinvlem1.r Scalar
hdmapinvlem1.b
hdmapinvlem1.t
hdmapinvlem1.z
hdmapinvlem1.s HDMap
hdmapinvlem1.k
hdmapinvlem1.c
Assertion
Ref Expression
hdmapinvlem2

Proof of Theorem hdmapinvlem2
StepHypRef Expression
1 hdmapinvlem1.h . . 3
2 hdmapinvlem1.e . . 3
3 hdmapinvlem1.o . . 3
4 hdmapinvlem1.u . . 3
5 hdmapinvlem1.v . . 3
6 hdmapinvlem1.r . . 3 Scalar
7 hdmapinvlem1.b . . 3
8 hdmapinvlem1.t . . 3
9 hdmapinvlem1.z . . 3
10 hdmapinvlem1.s . . 3 HDMap
11 hdmapinvlem1.k . . 3
12 hdmapinvlem1.c . . 3
131, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12hdmapinvlem1 32657 . 2
14 eqid 2436 . . . . 5
15 eqid 2436 . . . . 5
16 eqid 2436 . . . . 5
171, 14, 15, 4, 5, 16, 2, 11dvheveccl 31848 . . . 4