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

Theorem dalem60 30466
 Description: Lemma for dath 30470. is an axis of perspectivity (almost). (Contributed by NM, 11-Aug-2012.)
Hypotheses
Ref Expression
dalem.ph
dalem.l
dalem.j
dalem.a
dalem.ps
dalem60.m
dalem60.o
dalem60.y
dalem60.z
dalem60.d
dalem60.e
dalem60.g
dalem60.h
dalem60.i
dalem60.b1
Assertion
Ref Expression
dalem60

Proof of Theorem dalem60
StepHypRef Expression
1 dalem.ph . . . 4
2 dalem.l . . . 4
3 dalem.j . . . 4
4 dalem.a . . . 4
5 dalem.ps . . . 4
6 dalem60.m . . . 4
7 dalem60.o . . . 4
8 dalem60.y . . . 4
9 dalem60.z . . . 4
10 dalem60.d . . . 4
11 dalem60.g . . . 4
12 dalem60.h . . . 4
13 dalem60.i . . . 4
14 dalem60.b1 . . . 4
151, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14dalem57 30463 . . 3
16 dalem60.e . . . 4
171, 2, 3, 4, 5, 6, 7, 8, 9, 16, 11, 12, 13, 14dalem58 30464 . . 3
181dalemkelat 30358 . . . . 5
19183ad2ant1 978 . . . 4
201, 2, 3, 4, 6, 7, 8, 9, 10dalemdea 30396 . . . . . 6
21 eqid 2435 . . . . . . 7
2221, 4atbase 30024 . . . . . 6
2320, 22syl 16 . . . . 5
24233ad2ant1 978 . . . 4
251, 2, 3, 4, 6, 7, 8, 9, 16dalemeea 30397 . . . . . 6
2621, 4atbase 30024 . . . . . 6
2725, 26syl 16 . . . . 5
28273ad2ant1 978 . . . 4
29 eqid 2435 . . . . . 6
301, 2, 3, 4, 5, 6, 29, 7, 8, 9, 11, 12, 13, 14dalem53 30459 . . . . 5
3121, 29llnbase 30243 . . . . 5
3230, 31syl 16 . . . 4
3321, 2, 3latjle12 14483 . . . 4
3419, 24, 28, 32, 33syl13anc 1186 . . 3
3515, 17, 34mpbi2and 888 . 2
361dalemkehl 30357 . . . 4