dalaw - Mathbox for Norm Megill

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

Theorem dalaw 33535

Description: Desargues' law, derived from Desargues' theorem dath 33385 and with no conditions on the atoms. If triples

and

are centrally perspective, i.e.

$.\/$

$./\$

$.\/$

, then they are axially perspective. Theorem 13.3 of [Crawley] p. 110. (Contributed by NM, 7-Oct-2012.)

**Hypotheses**
Ref	Expression
dalaw.l
dalaw.j	$.\/$
dalaw.m	$./\$
dalaw.a

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

**Proof of Theorem dalaw**
Step	Hyp	Ref	Expression
1		dalaw.l	. . . . . . . . 9
2		dalaw.j	. . . . . . . . 9 $.\/$
3		dalaw.m	. . . . . . . . 9 $./\$
4		dalaw.a	. . . . . . . . 9
5		eqid 2443	. . . . . . . . 9
6	1, 2, 3, 4, 5	dalawlem14 33533	. . . . . . . 8 $/\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$
7	6	3expib 1190	. . . . . . 7 $/\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$
8	7	3exp 1186	. . . . . 6 $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$
9	1, 2, 3, 4, 5	dalawlem15 33534	. . . . . . . 8 $/\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$
10	9	3expib 1190	. . . . . . 7 $/\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$
11	10	3exp 1186	. . . . . 6 $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$
12		simp11 1018	. . . . . . . . 9 $/\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
13		simp2 989	. . . . . . . . 9 $/\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
14		simp3 990	. . . . . . . . 9 $/\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
15		simp2ll 1055	. . . . . . . . . 10 $/\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $.\/$ $.\/$
16	15	3ad2ant1 1009	. . . . . . . . 9 $/\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
17		simp2rl 1057	. . . . . . . . . 10 $/\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $.\/$ $.\/$
18	17	3ad2ant1 1009	. . . . . . . . 9 $/\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
19		simp2lr 1056	. . . . . . . . . 10 $/\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$
20	19	3ad2ant1 1009	. . . . . . . . 9 $/\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$
21		simp2rr 1058	. . . . . . . . . 10 $/\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$
22	21	3ad2ant1 1009	. . . . . . . . 9 $/\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$
23		simp13 1020	. . . . . . . . 9 $/\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $.\/$
24	1, 2, 3, 4, 5	dalawlem1 33520	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$
25	12, 13, 14, 16, 18, 20, 22, 23, 24	syl323anc 1248	. . . . . . . 8 $/\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$
26	25	3expib 1190	. . . . . . 7 $/\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$
27	26	3exp 1186	. . . . . 6 $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$
28	8, 11, 27	ecased 935	. . . . 5 $.\/$ $./\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$
29	28	exp4a 606	. . . 4 $.\/$ $./\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$
30	29	com34 83	. . 3 $.\/$ $./\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$
31	30	com24 87	. 2 $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$
32	31	3imp 1181	1 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4 $/\$ wa 369 $/\$ w3a 965

wceq 1369

wcel 1756 class class class wbr 4297

cfv 5423 (class class class)co 6096

cple 14250

cjn 15119

cmee 15120

catm 32913

chlt 33000

clpl 33141

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1591 ax-4 1602 ax-5 1670 ax-6 1708 ax-7 1728 ax-8 1758 ax-9 1760 ax-10 1775 ax-11 1780 ax-12 1792 ax-13 1943 ax-ext 2423 ax-rep 4408 ax-sep 4418 ax-nul 4426 ax-pow 4475 ax-pr 4536 ax-un 6377

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 966 df-3an 967 df-tru 1372 df-ex 1587 df-nf 1590 df-sb 1701 df-eu 2257 df-mo 2258 df-clab 2430 df-cleq 2436 df-clel 2439 df-nfc 2573 df-ne 2613 df-ral 2725 df-rex 2726 df-reu 2727 df-rab 2729 df-v 2979 df-sbc 3192 df-csb 3294 df-dif 3336 df-un 3338 df-in 3340 df-ss 3347 df-nul 3643 df-if 3797 df-pw 3867 df-sn 3883 df-pr 3885 df-op 3889 df-uni 4097 df-iun 4178 df-iin 4179 df-br 4298 df-opab 4356 df-mpt 4357 df-id 4641 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 5386 df-fun 5425 df-fn 5426 df-f 5427 df-f1 5428 df-fo 5429 df-f1o 5430 df-fv 5431 df-riota 6057 df-ov 6099 df-oprab 6100 df-mpt2 6101 df-1st 6582 df-2nd 6583 df-poset 15121 df-plt 15133 df-lub 15149 df-glb 15150 df-join 15151 df-meet 15152 df-p0 15214 df-p1 15215 df-lat 15221 df-clat 15283 df-oposet 32826 df-ol 32828 df-oml 32829 df-covers 32916 df-ats 32917 df-atl 32948 df-cvlat 32972 df-hlat 33001 df-llines 33147 df-lplanes 33148 df-lvols 33149 df-psubsp 33152 df-pmap 33153 df-padd 33445

This theorem is referenced by: cdleme14 33922 cdleme20f 33963 cdlemg9 34283 cdlemg12c 34294 cdlemk6 34486 cdlemk6u 34511

W3C validator