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 32903

Description: Desargues' law, derived from Desargues' theorem dath 32753 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 2402	. . . . . . . . 9
6	1, 2, 3, 4, 5	dalawlem14 32901	. . . . . . . 8 $/\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$
7	6	3expib 1200	. . . . . . 7 $/\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$
8	7	3exp 1196	. . . . . 6 $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$
9	1, 2, 3, 4, 5	dalawlem15 32902	. . . . . . . 8 $/\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$
10	9	3expib 1200	. . . . . . 7 $/\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$
11	10	3exp 1196	. . . . . 6 $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$
12		simp11 1027	. . . . . . . . 9 $/\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
13		simp2 998	. . . . . . . . 9 $/\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
14		simp3 999	. . . . . . . . 9 $/\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
15		simp2ll 1064	. . . . . . . . . 10 $/\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $.\/$ $.\/$
16	15	3ad2ant1 1018	. . . . . . . . 9 $/\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
17		simp2rl 1066	. . . . . . . . . 10 $/\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $.\/$ $.\/$
18	17	3ad2ant1 1018	. . . . . . . . 9 $/\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
19		simp2lr 1065	. . . . . . . . . 10 $/\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$
20	19	3ad2ant1 1018	. . . . . . . . 9 $/\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$
21		simp2rr 1067	. . . . . . . . . 10 $/\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$
22	21	3ad2ant1 1018	. . . . . . . . 9 $/\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$
23		simp13 1029	. . . . . . . . 9 $/\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $.\/$
24	1, 2, 3, 4, 5	dalawlem1 32888	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$
25	12, 13, 14, 16, 18, 20, 22, 23, 24	syl323anc 1260	. . . . . . . 8 $/\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$
26	25	3expib 1200	. . . . . . 7 $/\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$
27	26	3exp 1196	. . . . . 6 $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$
28	8, 11, 27	ecased 945	. . . . 5 $.\/$ $./\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$
29	28	exp4a 604	. . . 4 $.\/$ $./\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$
30	29	com34 83	. . 3 $.\/$ $./\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$
31	30	com24 87	. 2 $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$
32	31	3imp 1191	1 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4 $/\$ wa 367 $/\$ w3a 974

wceq 1405

wcel 1842 class class class wbr 4395

cfv 5569 (class class class)co 6278

cple 14916

cjn 15897

cmee 15898

catm 32281

chlt 32368

clpl 32509

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 4507 ax-sep 4517 ax-nul 4525 ax-pow 4572 ax-pr 4630 ax-un 6574

This theorem depends on definitions: df-bi 185 df-or 368 df-an 369 df-3or 975 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 2759 df-rex 2760 df-reu 2761 df-rab 2763 df-v 3061 df-sbc 3278 df-csb 3374 df-dif 3417 df-un 3419 df-in 3421 df-ss 3428 df-nul 3739 df-if 3886 df-pw 3957 df-sn 3973 df-pr 3975 df-op 3979 df-uni 4192 df-iun 4273 df-iin 4274 df-br 4396 df-opab 4454 df-mpt 4455 df-id 4738 df-xp 4829 df-rel 4830 df-cnv 4831 df-co 4832 df-dm 4833 df-rn 4834 df-res 4835 df-ima 4836 df-iota 5533 df-fun 5571 df-fn 5572 df-f 5573 df-f1 5574 df-fo 5575 df-f1o 5576 df-fv 5577 df-riota 6240 df-ov 6281 df-oprab 6282 df-mpt2 6283 df-1st 6784 df-2nd 6785 df-preset 15881 df-poset 15899 df-plt 15912 df-lub 15928 df-glb 15929 df-join 15930 df-meet 15931 df-p0 15993 df-p1 15994 df-lat 16000 df-clat 16062 df-oposet 32194 df-ol 32196 df-oml 32197 df-covers 32284 df-ats 32285 df-atl 32316 df-cvlat 32340 df-hlat 32369 df-llines 32515 df-lplanes 32516 df-lvols 32517 df-psubsp 32520 df-pmap 32521 df-padd 32813

This theorem is referenced by: cdleme14 33291 cdleme20f 33333 cdlemg9 33653 cdlemg12c 33664 cdlemk6 33856 cdlemk6u 33881

W3C validator