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

Theorem mapdh8j 31978
 Description: Part of Part (8) in [Baer] p. 48. (Contributed by NM, 13-May-2015.)
Hypotheses
Ref Expression
mapdh8a.h
mapdh8a.u
mapdh8a.v
mapdh8a.s
mapdh8a.o
mapdh8a.n
mapdh8a.c LCDual
mapdh8a.d
mapdh8a.r
mapdh8a.q
mapdh8a.j
mapdh8a.m mapd
mapdh8a.i
mapdh8a.k
mapdh8h.f
mapdh8h.mn
mapdh8i.x
mapdh8i.y
mapdh8i.z
mapdh8i.xy
mapdh8i.xz
mapdh8i.yt
mapdh8i.zt
mapdh8j.t
Assertion
Ref Expression
mapdh8j
Distinct variable groups:   ,,   ,,   ,   ,,   ,,   ,   ,,   ,,   ,,   ,   ,,   ,   ,,   ,   ,,   ,,   ,,   ,   ,
Allowed substitution hints:   ()   ()   ()   ()   (,)   (,)   ()   (,)

Proof of Theorem mapdh8j
StepHypRef Expression
1 mapdh8a.h . . 3
2 mapdh8a.u . . 3
3 mapdh8a.v . . 3
4 mapdh8a.s . . 3
5 mapdh8a.o . . 3
6 mapdh8a.n . . 3
7 mapdh8a.c . . 3 LCDual
8 mapdh8a.d . . 3
9 mapdh8a.r . . 3
10 mapdh8a.q . . 3
11 mapdh8a.j . . 3
12 mapdh8a.m . . 3 mapd
13 mapdh8a.i . . 3
14 mapdh8a.k . . . 4
16 mapdh8h.f . . . 4
18 mapdh8h.mn . . . 4
20 eqidd 2284 . . 3
21 eqidd 2284 . . 3
22 mapdh8i.x . . . 4
24 mapdh8i.y . . . 4
26 mapdh8i.z . . . 4
28 mapdh8j.t . . . 4
30 simpr 447 . . 3
31 mapdh8i.xy . . . 4
33 mapdh8i.xz . . . 4
351, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 15, 17, 19, 20, 21, 23, 25, 27, 29, 30, 32, 34mapdh8ad 31969 . 2