Description: Lemma for dath . Construct the condition ph with c , G H I , and Y in place of C , Y , and Z respectively. This lets us reuse the special case of Desargues's theorem where Y =/= Z , to eventually prove the case where Y = Z . (Contributed by NM, 16-Aug-2012)
Ref | Expression | ||
---|---|---|---|
Hypotheses | dalem.ph | |
|
dalem.l | |
||
dalem.j | |
||
dalem.a | |
||
dalem.ps | |
||
dalem44.m | |
||
dalem44.o | |
||
dalem44.y | |
||
dalem44.z | |
||
dalem44.g | |
||
dalem44.h | |
||
dalem44.i | |
||
Assertion | dalem51 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dalem.ph | |
|
2 | dalem.l | |
|
3 | dalem.j | |
|
4 | dalem.a | |
|
5 | dalem.ps | |
|
6 | dalem44.m | |
|
7 | dalem44.o | |
|
8 | dalem44.y | |
|
9 | dalem44.z | |
|
10 | dalem44.g | |
|
11 | dalem44.h | |
|
12 | dalem44.i | |
|
13 | 1 | dalemkehl | |
14 | 13 | 3ad2ant1 | |
15 | 5 | dalemccea | |
16 | 15 | 3ad2ant3 | |
17 | 14 16 | jca | |
18 | 1 2 3 4 5 6 7 8 9 10 | dalem23 | |
19 | 1 2 3 4 5 6 7 8 9 11 | dalem29 | |
20 | 1 2 3 4 5 6 7 8 9 12 | dalem34 | |
21 | 18 19 20 | 3jca | |
22 | 1 | dalempea | |
23 | 1 | dalemqea | |
24 | 1 | dalemrea | |
25 | 22 23 24 | 3jca | |
26 | 25 | 3ad2ant1 | |
27 | 17 21 26 | 3jca | |
28 | 1 2 3 4 5 6 7 8 9 10 11 12 | dalem42 | |
29 | 1 | dalemyeo | |
30 | 29 | 3ad2ant1 | |
31 | 28 30 | jca | |
32 | 1 2 3 4 5 6 7 8 9 10 11 12 | dalem45 | |
33 | 1 2 3 4 5 6 7 8 9 10 11 12 | dalem46 | |
34 | 1 2 3 4 5 6 7 8 9 10 11 12 | dalem47 | |
35 | 32 33 34 | 3jca | |
36 | 1 2 3 4 5 6 7 8 9 10 11 12 | dalem48 | |
37 | 1 2 3 4 5 6 7 8 9 10 11 12 | dalem49 | |
38 | 1 2 3 4 5 6 7 8 9 10 11 12 | dalem50 | |
39 | 36 37 38 | 3jca | |
40 | 39 | 3adant2 | |
41 | 1 2 3 4 5 6 7 8 9 10 | dalem27 | |
42 | 1 2 3 4 5 6 7 8 9 11 | dalem32 | |
43 | 1 2 3 4 5 6 7 8 9 12 | dalem36 | |
44 | 41 42 43 | 3jca | |
45 | 35 40 44 | 3jca | |
46 | 27 31 45 | 3jca | |
47 | 1 2 3 4 5 6 7 8 9 10 11 12 | dalem43 | |
48 | 46 47 | jca | |