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

Theorem dalem24 30556
 Description: Lemma for dath 30595. Show that auxiliary atom is outside of plane . (Contributed by NM, 2-Aug-2012.)
Hypotheses
Ref Expression
dalem.ph
dalem.l
dalem.j
dalem.a
dalem.ps
dalem23.m
dalem23.o
dalem23.y
dalem23.z
dalem23.g
Assertion
Ref Expression
dalem24

Proof of Theorem dalem24
StepHypRef Expression
1 dalem23.g . . . . 5
21oveq1i 6093 . . . 4
3 dalem.ph . . . . . . . 8
43dalemkehl 30482 . . . . . . 7
5 hlol 30221 . . . . . . 7
64, 5syl 16 . . . . . 6
763ad2ant1 979 . . . . 5
843ad2ant1 979 . . . . . 6
9 dalem.ps . . . . . . . 8
109dalemccea 30542 . . . . . . 7
11103ad2ant3 981 . . . . . 6
123dalempea 30485 . . . . . . 7
13123ad2ant1 979 . . . . . 6
14 eqid 2438 . . . . . . 7
15 dalem.j . . . . . . 7
16 dalem.a . . . . . . 7
1714, 15, 16hlatjcl 30226 . . . . . 6
188, 11, 13, 17syl3anc 1185 . . . . 5
199dalemddea 30543 . . . . . . 7
20193ad2ant3 981 . . . . . 6
213dalemsea 30488 . . . . . . 7
22213ad2ant1 979 . . . . . 6
2314, 15, 16hlatjcl 30226 . . . . . 6
248, 20, 22, 23syl3anc 1185 . . . . 5
25 dalem23.o . . . . . . 7
263, 25dalemyeb 30508 . . . . . 6
27263ad2ant1 979 . . . . 5
28 dalem23.m . . . . . 6
2914, 28latmmdir 30095 . . . . 5
307, 18, 24, 27, 29syl13anc 1187 . . . 4
312, 30syl5eq 2482 . . 3
3215, 16hlatjcom 30227 . . . . . . 7
338, 11, 13, 32syl3anc 1185 . . . . . 6
3433oveq1d 6098 . . . . 5
35 dalem.l . . . . . . . 8
36 dalem23.y . . . . . . . 8
373, 35, 15, 16, 25, 36dalemply 30513 . . . . . . 7
38373ad2ant1 979 . . . . . 6
399dalem-ccly 30544 . . . . . . 7
40393ad2ant3 981 . . . . . 6
4114, 35, 15, 28, 162atjm 30304 . . . . . 6
428, 13, 11, 27, 38, 40, 41syl132anc 1203 . . . . 5
4334, 42eqtrd 2470 . . . 4
4415, 16hlatjcom 30227 . . . . . . 7
458, 20, 22, 44syl3anc 1185 . . . . . 6
4645oveq1d 6098 . . . . 5
47 dalem23.z . . . . . . . 8
483, 35, 15, 16, 47dalemsly 30514 . . . . . . 7
49483adant3 978 . . . . . 6
509dalem-ddly 30545 . . . . . . 7
51503ad2ant3 981 . . . . . 6
5214, 35, 15, 28, 162atjm 30304 . . . . . 6
538, 22, 20, 27, 49, 51, 52syl132anc 1203 . . . . 5
5446, 53eqtrd 2470 . . . 4
5543, 54oveq12d 6101 . . 3
563, 35, 15, 16, 25, 36dalempnes 30510 . . . . 5
57 hlatl 30220 . . . . . . 7
584, 57syl 16 . . . . . 6
59 eqid 2438 . . . . . . 7
6028, 59, 16atnem0 30178 . . . . . 6
6158, 12, 21, 60syl3anc 1185 . . . . 5
6256, 61mpbid 203 . . . 4