Proof of Theorem opphllem1
Step | Hyp | Ref
| Expression |
1 | | simpr 477 |
. . . . . 6
|
2 | | simplr 792 |
. . . . . 6
|
3 | 1, 2 | eqeltrd 2701 |
. . . . 5
|
4 | | hpg.p |
. . . . . . 7
|
5 | | hpg.i |
. . . . . . 7
Itv |
6 | | opphl.l |
. . . . . . 7
LineG |
7 | | opphl.g |
. . . . . . . 8
TarskiG |
8 | 7 | ad2antrr 762 |
. . . . . . 7
TarskiG |
9 | | opphllem1.b |
. . . . . . . 8
|
10 | 9 | ad2antrr 762 |
. . . . . . 7
|
11 | | opphl.d |
. . . . . . . . 9
|
12 | | opphllem1.r |
. . . . . . . . 9
|
13 | 4, 6, 5, 7, 11, 12 | tglnpt 25444 |
. . . . . . . 8
|
14 | 13 | ad2antrr 762 |
. . . . . . 7
|
15 | | opphllem1.a |
. . . . . . . 8
|
16 | 15 | ad2antrr 762 |
. . . . . . 7
|
17 | | opphllem1.y |
. . . . . . . 8
|
18 | 17 | ad2antrr 762 |
. . . . . . 7
|
19 | 18 | necomd 2849 |
. . . . . . . 8
|
20 | | opphllem1.z |
. . . . . . . . 9
|
21 | 20 | ad2antrr 762 |
. . . . . . . 8
|
22 | 4, 5, 6, 8, 14, 10, 16, 19, 21 | btwnlng3 25516 |
. . . . . . 7
|
23 | 4, 5, 6, 8, 10, 14, 16, 18, 22 | lncom 25517 |
. . . . . 6
|
24 | 11 | ad2antrr 762 |
. . . . . . 7
|
25 | | simplr 792 |
. . . . . . 7
|
26 | 12 | ad2antrr 762 |
. . . . . . 7
|
27 | 4, 5, 6, 8, 10, 14, 18, 18, 24, 25, 26 | tglinethru 25531 |
. . . . . 6
|
28 | 23, 27 | eleqtrrd 2704 |
. . . . 5
|
29 | 3, 28 | pm2.61dane 2881 |
. . . 4
|
30 | | hpg.d |
. . . . . 6
|
31 | | hpg.o |
. . . . . 6
|
32 | | opphllem1.c |
. . . . . 6
|
33 | | opphllem1.o |
. . . . . 6
|
34 | 4, 30, 5, 31, 6, 11, 7, 15, 32, 33 | oppne1 25633 |
. . . . 5
|
35 | 34 | adantr 481 |
. . . 4
|
36 | 29, 35 | pm2.65da 600 |
. . 3
|
37 | 4, 30, 5, 31, 6, 11, 7, 15, 32, 33 | oppne2 25634 |
. . 3
|
38 | | opphllem1.m |
. . . . . 6
|
39 | 4, 6, 5, 7, 11, 38 | tglnpt 25444 |
. . . . 5
|
40 | | eqid 2622 |
. . . . . . 7
pInvG pInvG |
41 | | opphllem1.s |
. . . . . . 7
pInvG |
42 | 4, 30, 5, 6, 40, 7,
39, 41, 15 | mirbtwn 25553 |
. . . . . 6
|
43 | | opphllem1.n |
. . . . . . . . 9
|
44 | 43 | eqcomd 2628 |
. . . . . . . 8
|
45 | 4, 30, 5, 6, 40, 7,
39, 41, 32, 44 | mircom 25558 |
. . . . . . 7
|
46 | 45 | oveq1d 6665 |
. . . . . 6
|
47 | 42, 46 | eleqtrd 2703 |
. . . . 5
|
48 | 4, 30, 5, 7, 13, 32, 15, 9, 39, 20, 47 | axtgpasch 25366 |
. . . 4
|
49 | 7 | ad2antrr 762 |
. . . . . . . . . 10
TarskiG |
50 | 13 | ad2antrr 762 |
. . . . . . . . . 10
|
51 | | simplrl 800 |
. . . . . . . . . 10
|
52 | | simplrr 801 |
. . . . . . . . . . . 12
|
53 | 52 | simprd 479 |
. . . . . . . . . . 11
|
54 | | simpr 477 |
. . . . . . . . . . . 12
|
55 | 54 | oveq1d 6665 |
. . . . . . . . . . 11
|
56 | 53, 55 | eleqtrd 2703 |
. . . . . . . . . 10
|
57 | 4, 30, 5, 49, 50, 51, 56 | axtgbtwnid 25365 |
. . . . . . . . 9
|
58 | 12 | ad2antrr 762 |
. . . . . . . . 9
|
59 | 57, 58 | eqeltrrd 2702 |
. . . . . . . 8
|
60 | 7 | adantr 481 |
. . . . . . . . . . 11
TarskiG |
61 | 60 | adantlr 751 |
. . . . . . . . . 10
TarskiG |
62 | 39 | adantr 481 |
. . . . . . . . . . 11
|
63 | 62 | adantlr 751 |
. . . . . . . . . 10
|
64 | 13 | adantr 481 |
. . . . . . . . . . 11
|
65 | 64 | adantlr 751 |
. . . . . . . . . 10
|
66 | | simplrl 800 |
. . . . . . . . . 10
|
67 | | simpr 477 |
. . . . . . . . . 10
|
68 | | simplrr 801 |
. . . . . . . . . . 11
|
69 | 68 | simprd 479 |
. . . . . . . . . 10
|
70 | 4, 5, 6, 61, 63, 65, 66, 67, 69 | btwnlng1 25514 |
. . . . . . . . 9
|
71 | | simpr 477 |
. . . . . . . . . . 11
|
72 | 11 | adantr 481 |
. . . . . . . . . . 11
|
73 | 38 | adantr 481 |
. . . . . . . . . . 11
|
74 | 12 | adantr 481 |
. . . . . . . . . . 11
|
75 | 4, 5, 6, 60, 62, 64, 71, 71, 72, 73, 74 | tglinethru 25531 |
. . . . . . . . . 10
|
76 | 75 | adantlr 751 |
. . . . . . . . 9
|
77 | 70, 76 | eleqtrrd 2704 |
. . . . . . . 8
|
78 | 59, 77 | pm2.61dane 2881 |
. . . . . . 7
|
79 | | simprrl 804 |
. . . . . . 7
|
80 | 78, 79 | jca 554 |
. . . . . 6
|
81 | 80 | ex 450 |
. . . . 5
|
82 | 81 | reximdv2 3014 |
. . . 4
|
83 | 48, 82 | mpd 15 |
. . 3
|
84 | 36, 37, 83 | jca31 557 |
. 2
|
85 | 4, 30, 5, 31, 9, 32 | islnopp 25631 |
. 2
|
86 | 84, 85 | mpbird 247 |
1
|