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

Theorem dalem17 30477
 Description: Lemma for dath 30533. When planes and are equal, the center of perspectivity is in . (Contributed by NM, 1-Aug-2012.)
Hypotheses
Ref Expression
dalema.ph
dalemc.l
dalemc.j
dalemc.a
dalem17.o
dalem17.y
dalem17.z
Assertion
Ref Expression
dalem17

Proof of Theorem dalem17
StepHypRef Expression
1 dalema.ph . . . 4
21dalemclrju 30433 . . 3
41dalemkelat 30421 . . . . . 6
5 dalemc.j . . . . . . 7
6 dalemc.a . . . . . . 7
71, 5, 6dalempjqeb 30442 . . . . . 6
81, 6dalemreb 30438 . . . . . 6
9 eqid 2436 . . . . . . 7
10 dalemc.l . . . . . . 7
119, 10, 5latlej2 14490 . . . . . 6
124, 7, 8, 11syl3anc 1184 . . . . 5
13 dalem17.y . . . . 5
1412, 13syl6breqr 4252 . . . 4
161, 5, 6dalemsjteb 30443 . . . . . . 7
171, 6dalemueb 30441 . . . . . . 7
189, 10, 5latlej2 14490 . . . . . . 7
194, 16, 17, 18syl3anc 1184 . . . . . 6
20 dalem17.z . . . . . 6
2119, 20syl6breqr 4252 . . . . 5
2221adantr 452 . . . 4
23 simpr 448 . . . 4
2422, 23breqtrrd 4238 . . 3
25 dalem17.o . . . . . 6
261, 25dalemyeb 30446 . . . . 5
279, 10, 5latjle12 14491 . . . . 5
284, 8, 17, 26, 27syl13anc 1186 . . . 4