dalem25 - Mathbox for Norm Megill

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

Theorem dalem25 33309

Description: Lemma for dath 33347. 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 33261	. . 3
6	5	3ad2ant1 1035	. 2 $/\$ $/\$
7		dalem.ps	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
8	7	dalemclccjdd 33299	. . . . . . . . . 10 $.\/$
9	8	3ad2ant3 1037	. . . . . . . . 9 $/\$ $/\$ $.\/$
10	9	adantr 471	. . . . . . . 8 $/\$ $/\$ $/\$ $.\/$
11		simpr 467	. . . . . . . . . 10 $/\$ $/\$ $/\$
12		dalem23.g	. . . . . . . . . . . . 13 $.\/$ $./\$ $.\/$
13	1	dalemkelat 33235	. . . . . . . . . . . . . . 15
14	13	3ad2ant1 1035	. . . . . . . . . . . . . 14 $/\$ $/\$
15	1	dalemkehl 33234	. . . . . . . . . . . . . . . 16
16	15	3ad2ant1 1035	. . . . . . . . . . . . . . 15 $/\$ $/\$
17	7	dalemccea 33294	. . . . . . . . . . . . . . . 16
18	17	3ad2ant3 1037	. . . . . . . . . . . . . . 15 $/\$ $/\$
19	1	dalempea 33237	. . . . . . . . . . . . . . . 16
20	19	3ad2ant1 1035	. . . . . . . . . . . . . . 15 $/\$ $/\$
21		eqid 2462	. . . . . . . . . . . . . . . 16
22	21, 3, 4	hlatjcl 32978	. . . . . . . . . . . . . . 15 $/\$ $/\$ $.\/$
23	16, 18, 20, 22	syl3anc 1276	. . . . . . . . . . . . . 14 $/\$ $/\$ $.\/$
24	7	dalemddea 33295	. . . . . . . . . . . . . . . 16
25	24	3ad2ant3 1037	. . . . . . . . . . . . . . 15 $/\$ $/\$
26	1	dalemsea 33240	. . . . . . . . . . . . . . . 16
27	26	3ad2ant1 1035	. . . . . . . . . . . . . . 15 $/\$ $/\$
28	21, 3, 4	hlatjcl 32978	. . . . . . . . . . . . . . 15 $/\$ $/\$ $.\/$
29	16, 25, 27, 28	syl3anc 1276	. . . . . . . . . . . . . 14 $/\$ $/\$ $.\/$
30		dalem23.m	. . . . . . . . . . . . . . 15 $./\$
31	21, 2, 30	latmle2 16378	. . . . . . . . . . . . . 14 $/\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$
32	14, 23, 29, 31	syl3anc 1276	. . . . . . . . . . . . 13 $/\$ $/\$ $.\/$ $./\$ $.\/$ $.\/$
33	12, 32	syl5eqbr 4452	. . . . . . . . . . . 12 $/\$ $/\$ $.\/$
34	3, 4	hlatjcom 32979	. . . . . . . . . . . . 13 $/\$ $/\$ $.\/$ $.\/$
35	16, 25, 27, 34	syl3anc 1276	. . . . . . . . . . . 12 $/\$ $/\$ $.\/$ $.\/$
36	33, 35	breqtrd 4443	. . . . . . . . . . 11 $/\$ $/\$ $.\/$
37	36	adantr 471	. . . . . . . . . 10 $/\$ $/\$ $/\$ $.\/$
38	11, 37	eqbrtrd 4439	. . . . . . . . 9 $/\$ $/\$ $/\$ $.\/$
39	2, 3, 4	hlatlej2 32987	. . . . . . . . . . 11 $/\$ $/\$ $.\/$
40	16, 27, 25, 39	syl3anc 1276	. . . . . . . . . 10 $/\$ $/\$ $.\/$
41	40	adantr 471	. . . . . . . . 9 $/\$ $/\$ $/\$ $.\/$
42	7, 4	dalemcceb 33300	. . . . . . . . . . . 12
43	42	3ad2ant3 1037	. . . . . . . . . . 11 $/\$ $/\$
44	21, 4	atbase 32901	. . . . . . . . . . . . 13
45	24, 44	syl 17	. . . . . . . . . . . 12
46	45	3ad2ant3 1037	. . . . . . . . . . 11 $/\$ $/\$
47	21, 3, 4	hlatjcl 32978	. . . . . . . . . . . 12 $/\$ $/\$ $.\/$
48	16, 27, 25, 47	syl3anc 1276	. . . . . . . . . . 11 $/\$ $/\$ $.\/$
49	21, 2, 3	latjle12 16363	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$
50	14, 43, 46, 48, 49	syl13anc 1278	. . . . . . . . . 10 $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$
51	50	adantr 471	. . . . . . . . 9 $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$
52	38, 41, 51	mpbi2and 937	. . . . . . . 8 $/\$ $/\$ $/\$ $.\/$ $.\/$
53	1, 4	dalemceb 33249	. . . . . . . . . . 11
54	53	3ad2ant1 1035	. . . . . . . . . 10 $/\$ $/\$
55	21, 3, 4	hlatjcl 32978	. . . . . . . . . . 11 $/\$ $/\$ $.\/$
56	16, 18, 25, 55	syl3anc 1276	. . . . . . . . . 10 $/\$ $/\$ $.\/$
57	21, 2	lattr 16357	. . . . . . . . . 10 $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$
58	14, 54, 56, 48, 57	syl13anc 1278	. . . . . . . . 9 $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$
59	58	adantr 471	. . . . . . . 8 $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$
60	10, 52, 59	mp2and 690	. . . . . . 7 $/\$ $/\$ $/\$ $.\/$
61		dalem23.o	. . . . . . . . . . 11
62	1, 61	dalemyeb 33260	. . . . . . . . . 10
63	62	3ad2ant1 1035	. . . . . . . . 9 $/\$ $/\$
64	21, 2, 30	latmlem1 16382	. . . . . . . . 9 $/\$ $/\$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $./\$
65	14, 54, 48, 63, 64	syl13anc 1278	. . . . . . . 8 $/\$ $/\$ $.\/$ $./\$ $.\/$ $./\$
66	65	adantr 471	. . . . . . 7 $/\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $./\$
67	60, 66	mpd 15	. . . . . 6 $/\$ $/\$ $/\$ $./\$ $.\/$ $./\$
68		dalem23.y	. . . . . . . . . 10 $.\/$ $.\/$
69		dalem23.z	. . . . . . . . . 10 $.\/$ $.\/$
70	1, 2, 3, 4, 61, 68, 69	dalem17 33291	. . . . . . . . 9 $/\$
71	70	3adant3 1034	. . . . . . . 8 $/\$ $/\$
72	21, 2, 30	latleeqm1 16380	. . . . . . . . 9 $/\$ $/\$ $./\$
73	14, 54, 63, 72	syl3anc 1276	. . . . . . . 8 $/\$ $/\$ $./\$
74	71, 73	mpbid 215	. . . . . . 7 $/\$ $/\$ $./\$
75	74	adantr 471	. . . . . 6 $/\$ $/\$ $/\$ $./\$
76	1, 2, 3, 4, 69	dalemsly 33266	. . . . . . . . 9 $/\$
77	76	3adant3 1034	. . . . . . . 8 $/\$ $/\$
78	7	dalem-ddly 33297	. . . . . . . . 9
79	78	3ad2ant3 1037	. . . . . . . 8 $/\$ $/\$
80	21, 2, 3, 30, 4	2atjm 33056	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$
81	16, 27, 25, 63, 77, 79, 80	syl132anc 1294	. . . . . . 7 $/\$ $/\$ $.\/$ $./\$
82	81	adantr 471	. . . . . 6 $/\$ $/\$ $/\$ $.\/$ $./\$
83	67, 75, 82	3brtr3d 4448	. . . . 5 $/\$ $/\$ $/\$
84		hlatl 32972	. . . . . . . . 9
85	15, 84	syl 17	. . . . . . . 8
86	1, 2, 3, 4, 61, 68	dalemcea 33271	. . . . . . . 8
87	2, 4	atcmp 32923	. . . . . . . 8 $/\$ $/\$
88	85, 86, 26, 87	syl3anc 1276	. . . . . . 7
89	88	3ad2ant1 1035	. . . . . 6 $/\$ $/\$
90	89	adantr 471	. . . . 5 $/\$ $/\$ $/\$
91	83, 90	mpbid 215	. . . 4 $/\$ $/\$ $/\$
92	91	ex 440	. . 3 $/\$ $/\$
93	92	necon3d 2657	. 2 $/\$ $/\$
94	6, 93	mpd 15	1 $/\$ $/\$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 189 $/\$ wa 375 $/\$ w3a 991

wceq 1455

wcel 1898

wne 2633 class class class wbr 4418

cfv 5605 (class class class)co 6320

cbs 15176

cple 15252

cjn 16244

cmee 16245

clat 16346

catm 32875

cal 32876

chlt 32962

clpl 33103

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1680 ax-4 1693 ax-5 1769 ax-6 1816 ax-7 1862 ax-8 1900 ax-9 1907 ax-10 1926 ax-11 1931 ax-12 1944 ax-13 2102 ax-ext 2442 ax-rep 4531 ax-sep 4541 ax-nul 4550 ax-pow 4598 ax-pr 4656 ax-un 6615

This theorem depends on definitions: df-bi 190 df-or 376 df-an 377 df-3an 993 df-tru 1458 df-ex 1675 df-nf 1679 df-sb 1809 df-eu 2314 df-mo 2315 df-clab 2449 df-cleq 2455 df-clel 2458 df-nfc 2592 df-ne 2635 df-ral 2754 df-rex 2755 df-reu 2756 df-rab 2758 df-v 3059 df-sbc 3280 df-csb 3376 df-dif 3419 df-un 3421 df-in 3423 df-ss 3430 df-nul 3744 df-if 3894 df-pw 3965 df-sn 3981 df-pr 3983 df-op 3987 df-uni 4213 df-iun 4294 df-br 4419 df-opab 4478 df-mpt 4479 df-id 4771 df-xp 4862 df-rel 4863 df-cnv 4864 df-co 4865 df-dm 4866 df-rn 4867 df-res 4868 df-ima 4869 df-iota 5569 df-fun 5607 df-fn 5608 df-f 5609 df-f1 5610 df-fo 5611 df-f1o 5612 df-fv 5613 df-riota 6282 df-ov 6323 df-oprab 6324 df-preset 16228 df-poset 16246 df-plt 16259 df-lub 16275 df-glb 16276 df-join 16277 df-meet 16278 df-p0 16340 df-lat 16347 df-clat 16409 df-oposet 32788 df-ol 32790 df-oml 32791 df-covers 32878 df-ats 32879 df-atl 32910 df-cvlat 32934 df-hlat 32963 df-llines 33109 df-lplanes 33110

This theorem is referenced by: dalem28 33311 dalem31N 33314

W3C validator