dalem17 - Mathbox for Norm Megill

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

Theorem dalem17 32953

Description: Lemma for dath 33009. When planes

and

are equal, the center of perspectivity

is in

. (Contributed by NM, 1-Aug-2012.)

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

**Assertion**
Ref	Expression
dalem17	$/\$

**Proof of Theorem dalem17**
Step	Hyp	Ref	Expression
1		dalema.ph	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$
2	1	dalemclrju 32909	. . 3 $.\/$
3	2	adantr 466	. 2 $/\$ $.\/$
4	1	dalemkelat 32897	. . . . . 6
5		dalemc.j	. . . . . . 7 $.\/$
6		dalemc.a	. . . . . . 7
7	1, 5, 6	dalempjqeb 32918	. . . . . 6 $.\/$
8	1, 6	dalemreb 32914	. . . . . 6
9		eqid 2429	. . . . . . 7
10		dalemc.l	. . . . . . 7
11	9, 10, 5	latlej2 16258	. . . . . 6 $/\$ $.\/$ $/\$ $.\/$ $.\/$
12	4, 7, 8, 11	syl3anc 1264	. . . . 5 $.\/$ $.\/$
13		dalem17.y	. . . . 5 $.\/$ $.\/$
14	12, 13	syl6breqr 4466	. . . 4
15	14	adantr 466	. . 3 $/\$
16	1, 5, 6	dalemsjteb 32919	. . . . . . 7 $.\/$
17	1, 6	dalemueb 32917	. . . . . . 7
18	9, 10, 5	latlej2 16258	. . . . . . 7 $/\$ $.\/$ $/\$ $.\/$ $.\/$
19	4, 16, 17, 18	syl3anc 1264	. . . . . 6 $.\/$ $.\/$
20		dalem17.z	. . . . . 6 $.\/$ $.\/$
21	19, 20	syl6breqr 4466	. . . . 5
22	21	adantr 466	. . . 4 $/\$
23		simpr 462	. . . 4 $/\$
24	22, 23	breqtrrd 4452	. . 3 $/\$
25		dalem17.o	. . . . . 6
26	1, 25	dalemyeb 32922	. . . . 5
27	9, 10, 5	latjle12 16259	. . . . 5 $/\$ $/\$ $/\$ $/\$ $.\/$
28	4, 8, 17, 26, 27	syl13anc 1266	. . . 4 $/\$ $.\/$
29	28	adantr 466	. . 3 $/\$ $/\$ $.\/$
30	15, 24, 29	mpbi2and 929	. 2 $/\$ $.\/$
31	1, 6	dalemceb 32911	. . . 4
32	1	dalemkehl 32896	. . . . 5
33	1	dalemrea 32901	. . . . 5
34	1	dalemuea 32904	. . . . 5
35	9, 5, 6	hlatjcl 32640	. . . . 5 $/\$ $/\$ $.\/$
36	32, 33, 34, 35	syl3anc 1264	. . . 4 $.\/$
37	9, 10	lattr 16253	. . . 4 $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$
38	4, 31, 36, 26, 37	syl13anc 1266	. . 3 $.\/$ $/\$ $.\/$
39	38	adantr 466	. 2 $/\$ $.\/$ $/\$ $.\/$
40	3, 30, 39	mp2and 683	1 $/\$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

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

wceq 1437

wcel 1870 class class class wbr 4426

cfv 5601 (class class class)co 6305

cbs 15084

cple 15159

cjn 16140

clat 16242

catm 32537

chlt 32624

clpl 32765

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 1751 ax-6 1797 ax-7 1841 ax-8 1872 ax-9 1874 ax-10 1889 ax-11 1894 ax-12 1907 ax-13 2055 ax-ext 2407 ax-rep 4538 ax-sep 4548 ax-nul 4556 ax-pow 4603 ax-pr 4661 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 1660 df-nf 1664 df-sb 1790 df-eu 2270 df-mo 2271 df-clab 2415 df-cleq 2421 df-clel 2424 df-nfc 2579 df-ne 2627 df-ral 2787 df-rex 2788 df-reu 2789 df-rab 2791 df-v 3089 df-sbc 3306 df-csb 3402 df-dif 3445 df-un 3447 df-in 3449 df-ss 3456 df-nul 3768 df-if 3916 df-pw 3987 df-sn 4003 df-pr 4005 df-op 4009 df-uni 4223 df-iun 4304 df-br 4427 df-opab 4485 df-mpt 4486 df-id 4769 df-xp 4860 df-rel 4861 df-cnv 4862 df-co 4863 df-dm 4864 df-rn 4865 df-res 4866 df-ima 4867 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-poset 16142 df-lub 16171 df-glb 16172 df-join 16173 df-meet 16174 df-lat 16243 df-ats 32541 df-atl 32572 df-cvlat 32596 df-hlat 32625 df-lplanes 32772

This theorem is referenced by: dalem19 32955 dalem25 32971

W3C validator