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 32696

Description: Lemma for dath 32734. 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 32648	. . 3
6	5	3ad2ant1 1018	. 2 $/\$ $/\$
7		dalem.ps	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
8	7	dalemclccjdd 32686	. . . . . . . . . 10 $.\/$
9	8	3ad2ant3 1020	. . . . . . . . 9 $/\$ $/\$ $.\/$
10	9	adantr 463	. . . . . . . 8 $/\$ $/\$ $/\$ $.\/$
11		simpr 459	. . . . . . . . . 10 $/\$ $/\$ $/\$
12		dalem23.g	. . . . . . . . . . . . 13 $.\/$ $./\$ $.\/$
13	1	dalemkelat 32622	. . . . . . . . . . . . . . 15
14	13	3ad2ant1 1018	. . . . . . . . . . . . . 14 $/\$ $/\$
15	1	dalemkehl 32621	. . . . . . . . . . . . . . . 16
16	15	3ad2ant1 1018	. . . . . . . . . . . . . . 15 $/\$ $/\$
17	7	dalemccea 32681	. . . . . . . . . . . . . . . 16
18	17	3ad2ant3 1020	. . . . . . . . . . . . . . 15 $/\$ $/\$
19	1	dalempea 32624	. . . . . . . . . . . . . . . 16
20	19	3ad2ant1 1018	. . . . . . . . . . . . . . 15 $/\$ $/\$
21		eqid 2402	. . . . . . . . . . . . . . . 16
22	21, 3, 4	hlatjcl 32365	. . . . . . . . . . . . . . 15 $/\$ $/\$ $.\/$
23	16, 18, 20, 22	syl3anc 1230	. . . . . . . . . . . . . 14 $/\$ $/\$ $.\/$
24	7	dalemddea 32682	. . . . . . . . . . . . . . . 16
25	24	3ad2ant3 1020	. . . . . . . . . . . . . . 15 $/\$ $/\$
26	1	dalemsea 32627	. . . . . . . . . . . . . . . 16
27	26	3ad2ant1 1018	. . . . . . . . . . . . . . 15 $/\$ $/\$
28	21, 3, 4	hlatjcl 32365	. . . . . . . . . . . . . . 15 $/\$ $/\$ $.\/$
29	16, 25, 27, 28	syl3anc 1230	. . . . . . . . . . . . . 14 $/\$ $/\$ $.\/$
30		dalem23.m	. . . . . . . . . . . . . . 15 $./\$
31	21, 2, 30	latmle2 15923	. . . . . . . . . . . . . 14 $/\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$
32	14, 23, 29, 31	syl3anc 1230	. . . . . . . . . . . . 13 $/\$ $/\$ $.\/$ $./\$ $.\/$ $.\/$
33	12, 32	syl5eqbr 4427	. . . . . . . . . . . 12 $/\$ $/\$ $.\/$
34	3, 4	hlatjcom 32366	. . . . . . . . . . . . 13 $/\$ $/\$ $.\/$ $.\/$
35	16, 25, 27, 34	syl3anc 1230	. . . . . . . . . . . 12 $/\$ $/\$ $.\/$ $.\/$
36	33, 35	breqtrd 4418	. . . . . . . . . . 11 $/\$ $/\$ $.\/$
37	36	adantr 463	. . . . . . . . . 10 $/\$ $/\$ $/\$ $.\/$
38	11, 37	eqbrtrd 4414	. . . . . . . . 9 $/\$ $/\$ $/\$ $.\/$
39	2, 3, 4	hlatlej2 32374	. . . . . . . . . . 11 $/\$ $/\$ $.\/$
40	16, 27, 25, 39	syl3anc 1230	. . . . . . . . . 10 $/\$ $/\$ $.\/$
41	40	adantr 463	. . . . . . . . 9 $/\$ $/\$ $/\$ $.\/$
42	7, 4	dalemcceb 32687	. . . . . . . . . . . 12
43	42	3ad2ant3 1020	. . . . . . . . . . 11 $/\$ $/\$
44	21, 4	atbase 32288	. . . . . . . . . . . . 13
45	24, 44	syl 17	. . . . . . . . . . . 12
46	45	3ad2ant3 1020	. . . . . . . . . . 11 $/\$ $/\$
47	21, 3, 4	hlatjcl 32365	. . . . . . . . . . . 12 $/\$ $/\$ $.\/$
48	16, 27, 25, 47	syl3anc 1230	. . . . . . . . . . 11 $/\$ $/\$ $.\/$
49	21, 2, 3	latjle12 15908	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$
50	14, 43, 46, 48, 49	syl13anc 1232	. . . . . . . . . 10 $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$
51	50	adantr 463	. . . . . . . . 9 $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$
52	38, 41, 51	mpbi2and 922	. . . . . . . 8 $/\$ $/\$ $/\$ $.\/$ $.\/$
53	1, 4	dalemceb 32636	. . . . . . . . . . 11
54	53	3ad2ant1 1018	. . . . . . . . . 10 $/\$ $/\$
55	21, 3, 4	hlatjcl 32365	. . . . . . . . . . 11 $/\$ $/\$ $.\/$
56	16, 18, 25, 55	syl3anc 1230	. . . . . . . . . 10 $/\$ $/\$ $.\/$
57	21, 2	lattr 15902	. . . . . . . . . 10 $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$
58	14, 54, 56, 48, 57	syl13anc 1232	. . . . . . . . 9 $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$
59	58	adantr 463	. . . . . . . 8 $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$
60	10, 52, 59	mp2and 677	. . . . . . 7 $/\$ $/\$ $/\$ $.\/$
61		dalem23.o	. . . . . . . . . . 11
62	1, 61	dalemyeb 32647	. . . . . . . . . 10
63	62	3ad2ant1 1018	. . . . . . . . 9 $/\$ $/\$
64	21, 2, 30	latmlem1 15927	. . . . . . . . 9 $/\$ $/\$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $./\$
65	14, 54, 48, 63, 64	syl13anc 1232	. . . . . . . 8 $/\$ $/\$ $.\/$ $./\$ $.\/$ $./\$
66	65	adantr 463	. . . . . . 7 $/\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $./\$
67	60, 66	mpd 15	. . . . . 6 $/\$ $/\$ $/\$ $./\$ $.\/$ $./\$
68		dalem23.y	. . . . . . . . . 10 $.\/$ $.\/$
69		dalem23.z	. . . . . . . . . 10 $.\/$ $.\/$
70	1, 2, 3, 4, 61, 68, 69	dalem17 32678	. . . . . . . . 9 $/\$
71	70	3adant3 1017	. . . . . . . 8 $/\$ $/\$
72	21, 2, 30	latleeqm1 15925	. . . . . . . . 9 $/\$ $/\$ $./\$
73	14, 54, 63, 72	syl3anc 1230	. . . . . . . 8 $/\$ $/\$ $./\$
74	71, 73	mpbid 210	. . . . . . 7 $/\$ $/\$ $./\$
75	74	adantr 463	. . . . . 6 $/\$ $/\$ $/\$ $./\$
76	1, 2, 3, 4, 69	dalemsly 32653	. . . . . . . . 9 $/\$
77	76	3adant3 1017	. . . . . . . 8 $/\$ $/\$
78	7	dalem-ddly 32684	. . . . . . . . 9
79	78	3ad2ant3 1020	. . . . . . . 8 $/\$ $/\$
80	21, 2, 3, 30, 4	2atjm 32443	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$
81	16, 27, 25, 63, 77, 79, 80	syl132anc 1248	. . . . . . 7 $/\$ $/\$ $.\/$ $./\$
82	81	adantr 463	. . . . . 6 $/\$ $/\$ $/\$ $.\/$ $./\$
83	67, 75, 82	3brtr3d 4423	. . . . 5 $/\$ $/\$ $/\$
84		hlatl 32359	. . . . . . . . 9
85	15, 84	syl 17	. . . . . . . 8
86	1, 2, 3, 4, 61, 68	dalemcea 32658	. . . . . . . 8
87	2, 4	atcmp 32310	. . . . . . . 8 $/\$ $/\$
88	85, 86, 26, 87	syl3anc 1230	. . . . . . 7
89	88	3ad2ant1 1018	. . . . . 6 $/\$ $/\$
90	89	adantr 463	. . . . 5 $/\$ $/\$ $/\$
91	83, 90	mpbid 210	. . . 4 $/\$ $/\$ $/\$
92	91	ex 432	. . 3 $/\$ $/\$
93	92	necon3d 2627	. 2 $/\$ $/\$
94	6, 93	mpd 15	1 $/\$ $/\$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 184 $/\$ wa 367 $/\$ w3a 974

wceq 1405

wcel 1842

wne 2598 class class class wbr 4394

cfv 5525 (class class class)co 6234

cbs 14733

cple 14808

cjn 15789

cmee 15790

clat 15891

catm 32262

cal 32263

chlt 32349

clpl 32490

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1639 ax-4 1652 ax-5 1725 ax-6 1771 ax-7 1814 ax-8 1844 ax-9 1846 ax-10 1861 ax-11 1866 ax-12 1878 ax-13 2026 ax-ext 2380 ax-rep 4506 ax-sep 4516 ax-nul 4524 ax-pow 4571 ax-pr 4629 ax-un 6530

This theorem depends on definitions: df-bi 185 df-or 368 df-an 369 df-3an 976 df-tru 1408 df-ex 1634 df-nf 1638 df-sb 1764 df-eu 2242 df-mo 2243 df-clab 2388 df-cleq 2394 df-clel 2397 df-nfc 2552 df-ne 2600 df-ral 2758 df-rex 2759 df-reu 2760 df-rab 2762 df-v 3060 df-sbc 3277 df-csb 3373 df-dif 3416 df-un 3418 df-in 3420 df-ss 3427 df-nul 3738 df-if 3885 df-pw 3956 df-sn 3972 df-pr 3974 df-op 3978 df-uni 4191 df-iun 4272 df-br 4395 df-opab 4453 df-mpt 4454 df-id 4737 df-xp 4948 df-rel 4949 df-cnv 4950 df-co 4951 df-dm 4952 df-rn 4953 df-res 4954 df-ima 4955 df-iota 5489 df-fun 5527 df-fn 5528 df-f 5529 df-f1 5530 df-fo 5531 df-f1o 5532 df-fv 5533 df-riota 6196 df-ov 6237 df-oprab 6238 df-preset 15773 df-poset 15791 df-plt 15804 df-lub 15820 df-glb 15821 df-join 15822 df-meet 15823 df-p0 15885 df-lat 15892 df-clat 15954 df-oposet 32175 df-ol 32177 df-oml 32178 df-covers 32265 df-ats 32266 df-atl 32297 df-cvlat 32321 df-hlat 32350 df-llines 32496 df-lplanes 32497

This theorem is referenced by: dalem28 32698 dalem31N 32701

W3C validator