dalem21 - Mathbox for Norm Megill

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

Theorem dalem21 33012

Description: Lemma for dath 33054. Show that lines

and

intersect at an atom. (Contributed by NM, 2-Aug-2012.)

**Hypotheses**
Ref	Expression
dalem.ph	$/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$
dalem.l
dalem.j	$.\/$
dalem.a
dalem.ps	$/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
dalem21.m	$./\$
dalem21.o
dalem21.y	$.\/$ $.\/$
dalem21.z	$.\/$ $.\/$

**Assertion**
Ref	Expression
dalem21	$/\$ $/\$ $.\/$ $./\$ $.\/$

**Proof of Theorem dalem21**
Step	Hyp	Ref	Expression
1		dalem.ph	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$
2	1	dalemkehl 32941	. . 3
3	2	3ad2ant1 1026	. 2 $/\$ $/\$
4		dalem.l	. . . 4
5		dalem.j	. . . 4 $.\/$
6		dalem.a	. . . 4
7		dalem.ps	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
8	1, 4, 5, 6, 7	dalemcjden 33010	. . 3 $/\$ $.\/$
9	8	3adant2 1024	. 2 $/\$ $/\$ $.\/$
10		dalem21.o	. . . 4
11		dalem21.y	. . . 4 $.\/$ $.\/$
12	1, 4, 5, 6, 10, 11	dalempjsen 32971	. . 3 $.\/$
13	12	3ad2ant1 1026	. 2 $/\$ $/\$ $.\/$
14	1, 4, 5, 6, 10, 11	dalemply 32972	. . . . . . 7
15	14	adantr 466	. . . . . 6 $/\$
16		dalem21.z	. . . . . . 7 $.\/$ $.\/$
17	1, 4, 5, 6, 16	dalemsly 32973	. . . . . 6 $/\$
18	1	dalemkelat 32942	. . . . . . . 8
19	1, 6	dalempeb 32957	. . . . . . . 8
20	1, 6	dalemseb 32960	. . . . . . . 8
21	1, 10	dalemyeb 32967	. . . . . . . 8
22		eqid 2420	. . . . . . . . 9
23	22, 4, 5	latjle12 16260	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $.\/$
24	18, 19, 20, 21, 23	syl13anc 1266	. . . . . . 7 $/\$ $.\/$
25	24	adantr 466	. . . . . 6 $/\$ $/\$ $.\/$
26	15, 17, 25	mpbi2and 929	. . . . 5 $/\$ $.\/$
27	26	3adant3 1025	. . . 4 $/\$ $/\$ $.\/$
28	7	dalem-ccly 33003	. . . . . . 7
29	28	adantl 467	. . . . . 6 $/\$
30	18	adantr 466	. . . . . . . 8 $/\$
31	7, 6	dalemcceb 33007	. . . . . . . . 9
32	31	adantl 467	. . . . . . . 8 $/\$
33	7	dalemddea 33002	. . . . . . . . . 10
34	22, 6	atbase 32608	. . . . . . . . . 10
35	33, 34	syl 17	. . . . . . . . 9
36	35	adantl 467	. . . . . . . 8 $/\$
37	22, 4, 5	latlej1 16258	. . . . . . . 8 $/\$ $/\$ $.\/$
38	30, 32, 36, 37	syl3anc 1264	. . . . . . 7 $/\$ $.\/$
39		eqid 2420	. . . . . . . . . 10
40	22, 39	llnbase 32827	. . . . . . . . 9 $.\/$ $.\/$
41	8, 40	syl 17	. . . . . . . 8 $/\$ $.\/$
42	21	adantr 466	. . . . . . . 8 $/\$
43	22, 4	lattr 16254	. . . . . . . 8 $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$
44	30, 32, 41, 42, 43	syl13anc 1266	. . . . . . 7 $/\$ $.\/$ $/\$ $.\/$
45	38, 44	mpand 679	. . . . . 6 $/\$ $.\/$
46	29, 45	mtod 180	. . . . 5 $/\$ $.\/$
47	46	3adant2 1024	. . . 4 $/\$ $/\$ $.\/$
48		nbrne2 4435	. . . 4 $.\/$ $/\$ $.\/$ $.\/$ $.\/$
49	27, 47, 48	syl2anc 665	. . 3 $/\$ $/\$ $.\/$ $.\/$
50	49	necomd 2693	. 2 $/\$ $/\$ $.\/$ $.\/$
51		hlatl 32679	. . . . . 6
52	2, 51	syl 17	. . . . 5
53	52	adantr 466	. . . 4 $/\$
54	1	dalempea 32944	. . . . . . 7
55	1	dalemsea 32947	. . . . . . 7
56	22, 5, 6	hlatjcl 32685	. . . . . . 7 $/\$ $/\$ $.\/$
57	2, 54, 55, 56	syl3anc 1264	. . . . . 6 $.\/$
58	57	adantr 466	. . . . 5 $/\$ $.\/$
59		dalem21.m	. . . . . 6 $./\$
60	22, 59	latmcl 16250	. . . . 5 $/\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $.\/$
61	30, 41, 58, 60	syl3anc 1264	. . . 4 $/\$ $.\/$ $./\$ $.\/$
62	1, 4, 5, 6, 10, 11	dalemcea 32978	. . . . 5
63	62	adantr 466	. . . 4 $/\$
64	7	dalemclccjdd 33006	. . . . . 6 $.\/$
65	64	adantl 467	. . . . 5 $/\$ $.\/$
66	1	dalemclpjs 32952	. . . . . 6 $.\/$
67	66	adantr 466	. . . . 5 $/\$ $.\/$
68	1, 6	dalemceb 32956	. . . . . . 7
69	68	adantr 466	. . . . . 6 $/\$
70	22, 4, 59	latlem12 16276	. . . . . 6 $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $.\/$
71	30, 69, 41, 58, 70	syl13anc 1266	. . . . 5 $/\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $.\/$
72	65, 67, 71	mpbi2and 929	. . . 4 $/\$ $.\/$ $./\$ $.\/$
73		eqid 2420	. . . . 5
74	22, 4, 73, 6	atlen0 32629	. . . 4 $/\$ $.\/$ $./\$ $.\/$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$
75	53, 61, 63, 72, 74	syl31anc 1267	. . 3 $/\$ $.\/$ $./\$ $.\/$
76	75	3adant2 1024	. 2 $/\$ $/\$ $.\/$ $./\$ $.\/$
77	59, 73, 6, 39	2llnmat 32842	. 2 $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$
78	3, 9, 13, 50, 76, 77	syl32anc 1272	1 $/\$ $/\$ $.\/$ $./\$ $.\/$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 187 $/\$ wa 370 $/\$ w3a 982

wceq 1437

wcel 1867

wne 2616 class class class wbr 4417

cfv 5592 (class class class)co 6296

cbs 15081

cple 15157

cjn 16141

cmee 16142

cp0 16235

clat 16243

catm 32582

cal 32583

chlt 32669

clln 32809

clpl 32810

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1665 ax-4 1678 ax-5 1748 ax-6 1794 ax-7 1838 ax-8 1869 ax-9 1871 ax-10 1886 ax-11 1891 ax-12 1904 ax-13 2052 ax-ext 2398 ax-rep 4529 ax-sep 4539 ax-nul 4547 ax-pow 4594 ax-pr 4652 ax-un 6588

This theorem depends on definitions: df-bi 188 df-or 371 df-an 372 df-3an 984 df-tru 1440 df-ex 1660 df-nf 1664 df-sb 1787 df-eu 2267 df-mo 2268 df-clab 2406 df-cleq 2412 df-clel 2415 df-nfc 2570 df-ne 2618 df-ral 2778 df-rex 2779 df-reu 2780 df-rab 2782 df-v 3080 df-sbc 3297 df-csb 3393 df-dif 3436 df-un 3438 df-in 3440 df-ss 3447 df-nul 3759 df-if 3907 df-pw 3978 df-sn 3994 df-pr 3996 df-op 4000 df-uni 4214 df-iun 4295 df-br 4418 df-opab 4476 df-mpt 4477 df-id 4760 df-xp 4851 df-rel 4852 df-cnv 4853 df-co 4854 df-dm 4855 df-rn 4856 df-res 4857 df-ima 4858 df-iota 5556 df-fun 5594 df-fn 5595 df-f 5596 df-f1 5597 df-fo 5598 df-f1o 5599 df-fv 5600 df-riota 6258 df-ov 6299 df-oprab 6300 df-preset 16125 df-poset 16143 df-plt 16156 df-lub 16172 df-glb 16173 df-join 16174 df-meet 16175 df-p0 16237 df-lat 16244 df-clat 16306 df-oposet 32495 df-ol 32497 df-oml 32498 df-covers 32585 df-ats 32586 df-atl 32617 df-cvlat 32641 df-hlat 32670 df-llines 32816 df-lplanes 32817

This theorem is referenced by: dalem22 33013

W3C validator