dalem5 - Mathbox for Norm Megill

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

Theorem dalem5 33630

Description: Lemma for dath 33699. Atom

(in plane

) belongs to the 3-dimensional volume formed by

and

. (Contributed by NM, 21-Jul-2012.)

**Hypotheses**
Ref	Expression
dalema.ph	$/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$
dalemc.l
dalemc.j	$.\/$
dalemc.a
dalem5.o
dalem5.y	$.\/$ $.\/$
dalem5.w	$.\/$

**Assertion**
Ref	Expression
dalem5

**Proof of Theorem dalem5**
Step	Hyp	Ref	Expression
1		eqid 2452	. 2
2		dalemc.l	. 2
3		dalema.ph	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$
4	3	dalemkelat 33587	. 2
5		dalemc.a	. . 3
6	3, 5	dalemueb 33607	. 2
7	3	dalemkehl 33586	. . 3
8	3	dalemrea 33591	. . 3
9		dalemc.j	. . . 4 $.\/$
10		dalem5.o	. . . 4
11		dalem5.y	. . . 4 $.\/$ $.\/$
12	3, 2, 9, 5, 10, 11	dalemcea 33623	. . 3
13	1, 9, 5	hlatjcl 33330	. . 3 $/\$ $/\$ $.\/$
14	7, 8, 12, 13	syl3anc 1219	. 2 $.\/$
15		dalem5.w	. . 3 $.\/$
16	3, 10	dalemyeb 33612	. . . 4
17	3, 5	dalemceb 33601	. . . 4
18	1, 9	latjcl 15335	. . . 4 $/\$ $/\$ $.\/$
19	4, 16, 17, 18	syl3anc 1219	. . 3 $.\/$
20	15, 19	syl5eqel 2544	. 2
21	3	dalemclrju 33599	. . 3 $.\/$
22	3	dalemuea 33594	. . . 4
23	3	dalempea 33589	. . . . 5
24		simp313 1137	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
25	3, 24	sylbi 195	. . . . 5 $.\/$
26	2, 9, 5	atnlej1 33342	. . . . 5 $/\$ $/\$ $/\$ $/\$ $.\/$
27	7, 12, 8, 23, 25, 26	syl131anc 1232	. . . 4
28	2, 9, 5	hlatexch1 33358	. . . 4 $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
29	7, 12, 22, 8, 27, 28	syl131anc 1232	. . 3 $.\/$ $.\/$
30	21, 29	mpd 15	. 2 $.\/$
31	3, 9, 5	dalempjqeb 33608	. . . . . 6 $.\/$
32	3, 5	dalemreb 33604	. . . . . 6
33	1, 2, 9	latlej2 15345	. . . . . 6 $/\$ $.\/$ $/\$ $.\/$ $.\/$
34	4, 31, 32, 33	syl3anc 1219	. . . . 5 $.\/$ $.\/$
35	34, 11	syl6breqr 4435	. . . 4
36	1, 2, 9	latjlej1 15349	. . . . 5 $/\$ $/\$ $/\$ $.\/$ $.\/$
37	4, 32, 16, 17, 36	syl13anc 1221	. . . 4 $.\/$ $.\/$
38	35, 37	mpd 15	. . 3 $.\/$ $.\/$
39	38, 15	syl6breqr 4435	. 2 $.\/$
40	1, 2, 4, 6, 14, 20, 30, 39	lattrd 15342	1

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 184 $/\$ wa 369 $/\$ w3a 965

wceq 1370

wcel 1758

wne 2645 class class class wbr 4395

cfv 5521 (class class class)co 6195

cbs 14287

cple 14359

cjn 15228

clat 15329

catm 33227

chlt 33314

clpl 33455

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1592 ax-4 1603 ax-5 1671 ax-6 1710 ax-7 1730 ax-8 1760 ax-9 1762 ax-10 1777 ax-11 1782 ax-12 1794 ax-13 1954 ax-ext 2431 ax-rep 4506 ax-sep 4516 ax-nul 4524 ax-pow 4573 ax-pr 4634 ax-un 6477

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3an 967 df-tru 1373 df-ex 1588 df-nf 1591 df-sb 1703 df-eu 2265 df-mo 2266 df-clab 2438 df-cleq 2444 df-clel 2447 df-nfc 2602 df-ne 2647 df-ral 2801 df-rex 2802 df-reu 2803 df-rab 2805 df-v 3074 df-sbc 3289 df-csb 3391 df-dif 3434 df-un 3436 df-in 3438 df-ss 3445 df-nul 3741 df-if 3895 df-pw 3965 df-sn 3981 df-pr 3983 df-op 3987 df-uni 4195 df-iun 4276 df-br 4396 df-opab 4454 df-mpt 4455 df-id 4739 df-xp 4949 df-rel 4950 df-cnv 4951 df-co 4952 df-dm 4953 df-rn 4954 df-res 4955 df-ima 4956 df-iota 5484 df-fun 5523 df-fn 5524 df-f 5525 df-f1 5526 df-fo 5527 df-f1o 5528 df-fv 5529 df-riota 6156 df-ov 6198 df-oprab 6199 df-poset 15230 df-plt 15242 df-lub 15258 df-glb 15259 df-join 15260 df-meet 15261 df-p0 15323 df-lat 15330 df-clat 15392 df-oposet 33140 df-ol 33142 df-oml 33143 df-covers 33230 df-ats 33231 df-atl 33262 df-cvlat 33286 df-hlat 33315 df-llines 33461 df-lplanes 33462

This theorem is referenced by: dalem6 33631 dalem8 33633

W3C validator