Description: Desargues's law, derived from Desargues's theorem dath and with no conditions on the atoms. If triples <. P , Q , R >. and <. S , T , U >. are centrally perspective, i.e., ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) , then they are axially perspective. Theorem 13.3 of Crawley p. 110. (Contributed by NM, 7-Oct-2012)
Ref | Expression | ||
---|---|---|---|
Hypotheses | dalaw.l | |
|
dalaw.j | |
||
dalaw.m | |
||
dalaw.a | |
||
Assertion | dalaw | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dalaw.l | |
|
2 | dalaw.j | |
|
3 | dalaw.m | |
|
4 | dalaw.a | |
|
5 | eqid | |
|
6 | 1 2 3 4 5 | dalawlem14 | |
7 | 6 | 3expib | |
8 | 7 | 3exp | |
9 | 1 2 3 4 5 | dalawlem15 | |
10 | 9 | 3expib | |
11 | 10 | 3exp | |
12 | simp11 | |
|
13 | simp2 | |
|
14 | simp3 | |
|
15 | simp2ll | |
|
16 | 15 | 3ad2ant1 | |
17 | simp2rl | |
|
18 | 17 | 3ad2ant1 | |
19 | simp2lr | |
|
20 | 19 | 3ad2ant1 | |
21 | simp2rr | |
|
22 | 21 | 3ad2ant1 | |
23 | simp13 | |
|
24 | 1 2 3 4 5 | dalawlem1 | |
25 | 12 13 14 16 18 20 22 23 24 | syl323anc | |
26 | 25 | 3expib | |
27 | 26 | 3exp | |
28 | 8 11 27 | ecased | |
29 | 28 | exp4a | |
30 | 29 | com34 | |
31 | 30 | com24 | |
32 | 31 | 3imp | |