dalem25 - Mathbox for Norm Megill

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

Theorem dalem25 33232

Description: Lemma for dath 33270. Show that the dummy center of perspectivity

is different from auxiliary atom

. (Contributed by NM, 3-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
dalem25	$/\$ $/\$

**Proof of Theorem dalem25**
Step	Hyp	Ref	Expression
1		dalem.ph	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$
2		dalem.l	. . . 4
3		dalem.j	. . . 4 $.\/$
4		dalem.a	. . . 4
5	1, 2, 3, 4	dalemcnes 33184	. . 3
6	5	3ad2ant1 1026	. 2 $/\$ $/\$
7		dalem.ps	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
8	7	dalemclccjdd 33222	. . . . . . . . . 10 $.\/$
9	8	3ad2ant3 1028	. . . . . . . . 9 $/\$ $/\$ $.\/$
10	9	adantr 466	. . . . . . . 8 $/\$ $/\$ $/\$ $.\/$
11		simpr 462	. . . . . . . . . 10 $/\$ $/\$ $/\$
12		dalem23.g	. . . . . . . . . . . . 13 $.\/$ $./\$ $.\/$
13	1	dalemkelat 33158	. . . . . . . . . . . . . . 15
14	13	3ad2ant1 1026	. . . . . . . . . . . . . 14 $/\$ $/\$
15	1	dalemkehl 33157	. . . . . . . . . . . . . . . 16
16	15	3ad2ant1 1026	. . . . . . . . . . . . . . 15 $/\$ $/\$
17	7	dalemccea 33217	. . . . . . . . . . . . . . . 16
18	17	3ad2ant3 1028	. . . . . . . . . . . . . . 15 $/\$ $/\$
19	1	dalempea 33160	. . . . . . . . . . . . . . . 16
20	19	3ad2ant1 1026	. . . . . . . . . . . . . . 15 $/\$ $/\$
21		eqid 2422	. . . . . . . . . . . . . . . 16
22	21, 3, 4	hlatjcl 32901	. . . . . . . . . . . . . . 15 $/\$ $/\$ $.\/$
23	16, 18, 20, 22	syl3anc 1264	. . . . . . . . . . . . . 14 $/\$ $/\$ $.\/$
24	7	dalemddea 33218	. . . . . . . . . . . . . . . 16
25	24	3ad2ant3 1028	. . . . . . . . . . . . . . 15 $/\$ $/\$
26	1	dalemsea 33163	. . . . . . . . . . . . . . . 16
27	26	3ad2ant1 1026	. . . . . . . . . . . . . . 15 $/\$ $/\$
28	21, 3, 4	hlatjcl 32901	. . . . . . . . . . . . . . 15 $/\$ $/\$ $.\/$
29	16, 25, 27, 28	syl3anc 1264	. . . . . . . . . . . . . 14 $/\$ $/\$ $.\/$
30		dalem23.m	. . . . . . . . . . . . . . 15 $./\$
31	21, 2, 30	latmle2 16322	. . . . . . . . . . . . . 14 $/\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$
32	14, 23, 29, 31	syl3anc 1264	. . . . . . . . . . . . 13 $/\$ $/\$ $.\/$ $./\$ $.\/$ $.\/$
33	12, 32	syl5eqbr 4457	. . . . . . . . . . . 12 $/\$ $/\$ $.\/$
34	3, 4	hlatjcom 32902	. . . . . . . . . . . . 13 $/\$ $/\$ $.\/$ $.\/$
35	16, 25, 27, 34	syl3anc 1264	. . . . . . . . . . . 12 $/\$ $/\$ $.\/$ $.\/$
36	33, 35	breqtrd 4448	. . . . . . . . . . 11 $/\$ $/\$ $.\/$
37	36	adantr 466	. . . . . . . . . 10 $/\$ $/\$ $/\$ $.\/$
38	11, 37	eqbrtrd 4444	. . . . . . . . 9 $/\$ $/\$ $/\$ $.\/$
39	2, 3, 4	hlatlej2 32910	. . . . . . . . . . 11 $/\$ $/\$ $.\/$
40	16, 27, 25, 39	syl3anc 1264	. . . . . . . . . 10 $/\$ $/\$ $.\/$
41	40	adantr 466	. . . . . . . . 9 $/\$ $/\$ $/\$ $.\/$
42	7, 4	dalemcceb 33223	. . . . . . . . . . . 12
43	42	3ad2ant3 1028	. . . . . . . . . . 11 $/\$ $/\$
44	21, 4	atbase 32824	. . . . . . . . . . . . 13
45	24, 44	syl 17	. . . . . . . . . . . 12
46	45	3ad2ant3 1028	. . . . . . . . . . 11 $/\$ $/\$
47	21, 3, 4	hlatjcl 32901	. . . . . . . . . . . 12 $/\$ $/\$ $.\/$
48	16, 27, 25, 47	syl3anc 1264	. . . . . . . . . . 11 $/\$ $/\$ $.\/$
49	21, 2, 3	latjle12 16307	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$
50	14, 43, 46, 48, 49	syl13anc 1266	. . . . . . . . . 10 $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$
51	50	adantr 466	. . . . . . . . 9 $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$
52	38, 41, 51	mpbi2and 929	. . . . . . . 8 $/\$ $/\$ $/\$ $.\/$ $.\/$
53	1, 4	dalemceb 33172	. . . . . . . . . . 11
54	53	3ad2ant1 1026	. . . . . . . . . 10 $/\$ $/\$
55	21, 3, 4	hlatjcl 32901	. . . . . . . . . . 11 $/\$ $/\$ $.\/$
56	16, 18, 25, 55	syl3anc 1264	. . . . . . . . . 10 $/\$ $/\$ $.\/$
57	21, 2	lattr 16301	. . . . . . . . . 10 $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$
58	14, 54, 56, 48, 57	syl13anc 1266	. . . . . . . . 9 $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$
59	58	adantr 466	. . . . . . . 8 $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$
60	10, 52, 59	mp2and 683	. . . . . . 7 $/\$ $/\$ $/\$ $.\/$
61		dalem23.o	. . . . . . . . . . 11
62	1, 61	dalemyeb 33183	. . . . . . . . . 10
63	62	3ad2ant1 1026	. . . . . . . . 9 $/\$ $/\$
64	21, 2, 30	latmlem1 16326	. . . . . . . . 9 $/\$ $/\$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $./\$
65	14, 54, 48, 63, 64	syl13anc 1266	. . . . . . . 8 $/\$ $/\$ $.\/$ $./\$ $.\/$ $./\$
66	65	adantr 466	. . . . . . 7 $/\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $./\$
67	60, 66	mpd 15	. . . . . 6 $/\$ $/\$ $/\$ $./\$ $.\/$ $./\$
68		dalem23.y	. . . . . . . . . 10 $.\/$ $.\/$
69		dalem23.z	. . . . . . . . . 10 $.\/$ $.\/$
70	1, 2, 3, 4, 61, 68, 69	dalem17 33214	. . . . . . . . 9 $/\$
71	70	3adant3 1025	. . . . . . . 8 $/\$ $/\$
72	21, 2, 30	latleeqm1 16324	. . . . . . . . 9 $/\$ $/\$ $./\$
73	14, 54, 63, 72	syl3anc 1264	. . . . . . . 8 $/\$ $/\$ $./\$
74	71, 73	mpbid 213	. . . . . . 7 $/\$ $/\$ $./\$
75	74	adantr 466	. . . . . 6 $/\$ $/\$ $/\$ $./\$
76	1, 2, 3, 4, 69	dalemsly 33189	. . . . . . . . 9 $/\$
77	76	3adant3 1025	. . . . . . . 8 $/\$ $/\$
78	7	dalem-ddly 33220	. . . . . . . . 9
79	78	3ad2ant3 1028	. . . . . . . 8 $/\$ $/\$
80	21, 2, 3, 30, 4	2atjm 32979	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$
81	16, 27, 25, 63, 77, 79, 80	syl132anc 1282	. . . . . . 7 $/\$ $/\$ $.\/$ $./\$
82	81	adantr 466	. . . . . 6 $/\$ $/\$ $/\$ $.\/$ $./\$
83	67, 75, 82	3brtr3d 4453	. . . . 5 $/\$ $/\$ $/\$
84		hlatl 32895	. . . . . . . . 9
85	15, 84	syl 17	. . . . . . . 8
86	1, 2, 3, 4, 61, 68	dalemcea 33194	. . . . . . . 8
87	2, 4	atcmp 32846	. . . . . . . 8 $/\$ $/\$
88	85, 86, 26, 87	syl3anc 1264	. . . . . . 7
89	88	3ad2ant1 1026	. . . . . 6 $/\$ $/\$
90	89	adantr 466	. . . . 5 $/\$ $/\$ $/\$
91	83, 90	mpbid 213	. . . 4 $/\$ $/\$ $/\$
92	91	ex 435	. . 3 $/\$ $/\$
93	92	necon3d 2644	. 2 $/\$ $/\$
94	6, 93	mpd 15	1 $/\$ $/\$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

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

wceq 1437

wcel 1872

wne 2614 class class class wbr 4423

cfv 5601 (class class class)co 6305

cbs 15120

cple 15196

cjn 16188

cmee 16189

clat 16290

catm 32798

cal 32799

chlt 32885

clpl 33026

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1663 ax-4 1676 ax-5 1752 ax-6 1798 ax-7 1843 ax-8 1874 ax-9 1876 ax-10 1891 ax-11 1896 ax-12 1909 ax-13 2057 ax-ext 2401 ax-rep 4536 ax-sep 4546 ax-nul 4555 ax-pow 4602 ax-pr 4660 ax-un 6597

This theorem depends on definitions: df-bi 188 df-or 371 df-an 372 df-3an 984 df-tru 1440 df-ex 1658 df-nf 1662 df-sb 1791 df-eu 2273 df-mo 2274 df-clab 2408 df-cleq 2414 df-clel 2417 df-nfc 2568 df-ne 2616 df-ral 2776 df-rex 2777 df-reu 2778 df-rab 2780 df-v 3082 df-sbc 3300 df-csb 3396 df-dif 3439 df-un 3441 df-in 3443 df-ss 3450 df-nul 3762 df-if 3912 df-pw 3983 df-sn 3999 df-pr 4001 df-op 4005 df-uni 4220 df-iun 4301 df-br 4424 df-opab 4483 df-mpt 4484 df-id 4768 df-xp 4859 df-rel 4860 df-cnv 4861 df-co 4862 df-dm 4863 df-rn 4864 df-res 4865 df-ima 4866 df-iota 5565 df-fun 5603 df-fn 5604 df-f 5605 df-f1 5606 df-fo 5607 df-f1o 5608 df-fv 5609 df-riota 6267 df-ov 6308 df-oprab 6309 df-preset 16172 df-poset 16190 df-plt 16203 df-lub 16219 df-glb 16220 df-join 16221 df-meet 16222 df-p0 16284 df-lat 16291 df-clat 16353 df-oposet 32711 df-ol 32713 df-oml 32714 df-covers 32801 df-ats 32802 df-atl 32833 df-cvlat 32857 df-hlat 32886 df-llines 33032 df-lplanes 33033

This theorem is referenced by: dalem28 33234 dalem31N 33237

W3C validator