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

Theorem dalem44 33256
 Description: Lemma for dath 33276. Dummy center of perspectivity lies outside of plane . (Contributed by NM, 16-Aug-2012.)
Hypotheses
Ref Expression
dalem.ph
dalem.l
dalem.j
dalem.a
dalem.ps
dalem44.m
dalem44.o
dalem44.y
dalem44.z
dalem44.g
dalem44.h
dalem44.i
Assertion
Ref Expression
dalem44

Proof of Theorem dalem44
StepHypRef Expression
1 dalem.ph . . . 4
2 dalem.l . . . 4
3 dalem.j . . . 4
4 dalem.a . . . 4
5 dalem.ps . . . 4
6 dalem44.m . . . 4
7 dalem44.o . . . 4
8 dalem44.y . . . 4
9 dalem44.z . . . 4
10 dalem44.g . . . 4
11 dalem44.h . . . 4
12 dalem44.i . . . 4
131, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12dalem43 33255 . . 3
1413necomd 2696 . 2
151dalemkelat 33164 . . . . . . 7
16153ad2ant1 1027 . . . . . 6
175, 4dalemcceb 33229 . . . . . . 7
18173ad2ant3 1029 . . . . . 6
191, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12dalem42 33254 . . . . . . 7
20 eqid 2423 . . . . . . . 8
2120, 7lplnbase 33074 . . . . . . 7
2219, 21syl 17 . . . . . 6
2320, 2, 3latleeqj1 16314 . . . . . 6
2416, 18, 22, 23syl3anc 1265 . . . . 5
251, 2, 3, 4, 5, 6, 7, 8, 9, 10dalem28 33240 . . . . . . . . . . . 12
261dalemkehl 33163 . . . . . . . . . . . . . 14
27263ad2ant1 1027 . . . . . . . . . . . . 13
285dalemccea 33223 . . . . . . . . . . . . . 14
29283ad2ant3 1029 . . . . . . . . . . . . 13
301, 2, 3, 4, 5, 6, 7, 8, 9, 10dalem23 33236 . . . . . . . . . . . . 13
313, 4hlatjcom 32908 . . . . . . . . . . . . 13
3227, 29, 30, 31syl3anc 1265 . . . . . . . . . . . 12
3325, 32breqtrrd 4456 . . . . . . . . . . 11
341, 2, 3, 4, 5, 6, 7, 8, 9, 11dalem33 33245 . . . . . . . . . . . 12
351, 2, 3, 4, 5, 6, 7, 8, 9, 11dalem29 33241 . . . . . . . . . . . . 13
363, 4hlatjcom 32908 . . . . . . . . . . . . 13
3727, 29, 35, 36syl3anc 1265 . . . . . . . . . . . 12
3834, 37breqtrrd 4456 . . . . . . . . . . 11
391, 4dalempeb 33179 . . . . . . . . . . . . 13
40393ad2ant1 1027 . . . . . . . . . . . 12
4120, 3, 4hlatjcl 32907 . . . . . . . . . . . . 13
4227, 29, 30, 41syl3anc 1265 . . . . . . . . . . . 12
431, 4dalemqeb 33180 . . . . . . . . . . . . 13
44433ad2ant1 1027 . . . . . . . . . . . 12
4520, 3, 4hlatjcl 32907 . . . . . . . . . . . . 13
4627, 29, 35, 45syl3anc 1265 . . . . . . . . . . . 12
4720, 2, 3latjlej12 16318 . . . . . . . . . . . 12
4816, 40, 42, 44, 46, 47syl122anc 1274 . . . . . . . . . . 11
4933, 38, 48mp2and 684 . . . . . . . . . 10
5020, 4atbase 32830 . . . . . . . . . . . 12
5130, 50syl 17 . . . . . . . . . . 11
5220, 4atbase 32830 . . . . . . . . . . . 12
5335, 52syl 17 . . . . . . . . . . 11
5420, 3latjjdi 16354 . . . . . . . . . . 11
5516, 18, 51, 53, 54syl13anc 1267 . . . . . . . . . 10
5649, 55breqtrrd 4456 . . . . . . . . 9
571, 2, 3, 4, 5, 6, 7, 8, 9, 12dalem37 33249 . . . . . . . . . 10
581, 2, 3, 4, 5, 6, 7, 8, 9, 12dalem34 33246 . . . . . . . . . . 11
593, 4hlatjcom 32908 . . . . . . . . . . 11
6027, 29, 58, 59syl3anc 1265 . . . . . . . . . 10
6157, 60breqtrrd 4456 . . . . . . . . 9
621, 3, 4dalempjqeb 33185 . . . . . . . . . . 11
63623ad2ant1 1027 . . . . . . . . . 10
6420, 3, 4hlatjcl 32907 . . . . . . . . . . . 12
6527, 30, 35, 64syl3anc 1265 . . . . . . . . . . 11
6620, 3latjcl 16302 . . . . . . . . . . 11
6716, 18, 65, 66syl3anc 1265 . . . . . . . . . 10
681, 4dalemreb 33181 . . . . . . . . . . 11
69683ad2ant1 1027 . . . . . . . . . 10
7020, 3, 4hlatjcl 32907 . . . . . . . . . . 11
7127, 29, 58, 70syl3anc 1265 . . . . . . . . . 10
7220, 2, 3latjlej12 16318 . . . . . . . . . 10
7316, 63, 67, 69, 71, 72syl122anc 1274 . . . . . . . . 9
7456, 61, 73mp2and 684 . . . . . . . 8
7520, 4atbase 32830 . . . . . . . . . 10
7658, 75syl 17 . . . . . . . . 9
7720, 3latjjdi 16354 . . . . . . . . 9
7816, 18, 65, 76, 77syl13anc 1267 . . . . . . . 8
7974, 78breqtrrd 4456 . . . . . . 7
808, 79syl5eqbr 4463 . . . . . 6
81 breq2 4433 . . . . . 6
8280, 81syl5ibcom 224 . . . . 5
8324, 82sylbid 219 . . . 4
841dalemyeo 33172 . . . . . 6
85843ad2ant1 1027 . . . . 5
862, 7lplncmp 33102 . . . . 5
8727, 85, 19, 86syl3anc 1265 . . . 4
8883, 87sylibd 218 . . 3