Proof of Theorem opphllem6
Step | Hyp | Ref
| Expression |
1 | | hpg.p |
. . . 4
|
2 | | hpg.d |
. . . 4
|
3 | | hpg.i |
. . . 4
Itv |
4 | | opphl.l |
. . . 4
LineG |
5 | | eqid 2622 |
. . . 4
pInvG pInvG |
6 | | opphl.g |
. . . . 5
TarskiG |
7 | 6 | adantr 481 |
. . . 4
TarskiG |
8 | | opphllem5.n |
. . . 4
pInvG |
9 | | opphl.k |
. . . 4
hlG |
10 | | opphllem5.m |
. . . . 5
|
11 | 10 | adantr 481 |
. . . 4
|
12 | | opphllem5.a |
. . . . 5
|
13 | 12 | adantr 481 |
. . . 4
|
14 | | opphllem5.c |
. . . . 5
|
15 | 14 | adantr 481 |
. . . 4
|
16 | | opphllem5.u |
. . . . 5
|
17 | 16 | adantr 481 |
. . . 4
|
18 | | opphl.d |
. . . . . . . 8
|
19 | | opphllem5.r |
. . . . . . . 8
|
20 | 1, 4, 3, 6, 18, 19 | tglnpt 25444 |
. . . . . . 7
|
21 | | opphllem5.p |
. . . . . . . 8
⟂G |
22 | 4, 6, 21 | perpln2 25606 |
. . . . . . 7
|
23 | 1, 3, 4, 6, 12, 20, 22 | tglnne 25523 |
. . . . . 6
|
24 | 23 | adantr 481 |
. . . . 5
|
25 | | opphllem6.v |
. . . . . . . 8
|
26 | 25 | adantr 481 |
. . . . . . 7
|
27 | | simpr 477 |
. . . . . . 7
|
28 | 26, 27 | eqtr4d 2659 |
. . . . . 6
|
29 | 1, 2, 3, 4, 5, 6, 10, 8, 20 | mirinv 25561 |
. . . . . . 7
|
30 | 29 | adantr 481 |
. . . . . 6
|
31 | 28, 30 | mpbid 222 |
. . . . 5
|
32 | 24, 31 | neeqtrrd 2868 |
. . . 4
|
33 | | opphllem5.s |
. . . . . . . 8
|
34 | 1, 4, 3, 6, 18, 33 | tglnpt 25444 |
. . . . . . 7
|
35 | | opphllem5.q |
. . . . . . . 8
⟂G |
36 | 4, 6, 35 | perpln2 25606 |
. . . . . . 7
|
37 | 1, 3, 4, 6, 14, 34, 36 | tglnne 25523 |
. . . . . 6
|
38 | 37 | adantr 481 |
. . . . 5
|
39 | 31, 27 | eqtrd 2656 |
. . . . 5
|
40 | 38, 39 | neeqtrrd 2868 |
. . . 4
|
41 | | simpr 477 |
. . . . . . . 8
|
42 | 6 | ad3antrrr 766 |
. . . . . . . . . 10
TarskiG |
43 | 42 | adantr 481 |
. . . . . . . . 9
TarskiG |
44 | 14 | ad3antrrr 766 |
. . . . . . . . . 10
|
45 | 44 | adantr 481 |
. . . . . . . . 9
|
46 | 20 | ad3antrrr 766 |
. . . . . . . . . 10
|
47 | 46 | adantr 481 |
. . . . . . . . 9
|
48 | 18 | ad3antrrr 766 |
. . . . . . . . . . 11
|
49 | | simplr 792 |
. . . . . . . . . . 11
|
50 | 1, 4, 3, 42, 48, 49 | tglnpt 25444 |
. . . . . . . . . 10
|
51 | 50 | adantr 481 |
. . . . . . . . 9
|
52 | 12 | ad3antrrr 766 |
. . . . . . . . . 10
|
53 | 52 | adantr 481 |
. . . . . . . . 9
|
54 | 34 | ad3antrrr 766 |
. . . . . . . . . . 11
|
55 | 54 | adantr 481 |
. . . . . . . . . 10
|
56 | | simpllr 799 |
. . . . . . . . . . . 12
|
57 | 1, 3, 4, 6, 14, 34, 37 | tglinerflx2 25529 |
. . . . . . . . . . . . 13
|
58 | 57 | ad3antrrr 766 |
. . . . . . . . . . . 12
|
59 | 56, 58 | eqeltrd 2701 |
. . . . . . . . . . 11
|
60 | 59 | adantr 481 |
. . . . . . . . . 10
|
61 | 1, 3, 4, 6, 14, 34, 37 | tgelrnln 25525 |
. . . . . . . . . . . . 13
|
62 | 1, 2, 3, 4, 6, 18,
61, 35 | perpcom 25608 |
. . . . . . . . . . . 12
⟂G |
63 | 62 | ad4antr 768 |
. . . . . . . . . . 11
⟂G |
64 | | simpr 477 |
. . . . . . . . . . . 12
|
65 | 48 | adantr 481 |
. . . . . . . . . . . 12
|
66 | 19 | ad3antrrr 766 |
. . . . . . . . . . . . 13
|
67 | 66 | adantr 481 |
. . . . . . . . . . . 12
|
68 | 49 | adantr 481 |
. . . . . . . . . . . 12
|
69 | 1, 3, 4, 43, 47, 51, 64, 64, 65, 67, 68 | tglinethru 25531 |
. . . . . . . . . . 11
|
70 | 63, 69 | breqtrd 4679 |
. . . . . . . . . 10
⟂G |
71 | 1, 2, 3, 4, 43, 45, 55, 60, 51, 70 | perprag 25618 |
. . . . . . . . 9
∟G |
72 | 1, 3, 4, 6, 12, 20, 23 | tglinerflx2 25529 |
. . . . . . . . . . . 12
|
73 | 72 | ad3antrrr 766 |
. . . . . . . . . . 11
|
74 | 73 | adantr 481 |
. . . . . . . . . 10
|
75 | 1, 3, 4, 6, 12, 20, 23 | tgelrnln 25525 |
. . . . . . . . . . . . 13
|
76 | 1, 2, 3, 4, 6, 18,
75, 21 | perpcom 25608 |
. . . . . . . . . . . 12
⟂G |
77 | 76 | ad4antr 768 |
. . . . . . . . . . 11
⟂G |
78 | 77, 69 | breqtrd 4679 |
. . . . . . . . . 10
⟂G |
79 | 1, 2, 3, 4, 43, 53, 47, 74, 51, 78 | perprag 25618 |
. . . . . . . . 9
∟G |
80 | | simplr 792 |
. . . . . . . . . 10
|
81 | 1, 2, 3, 43, 53, 51, 45, 80 | tgbtwncom 25383 |
. . . . . . . . 9
|
82 | 1, 2, 3, 4, 5, 43,
45, 47, 51, 53, 71, 79, 81 | ragflat2 25598 |
. . . . . . . 8
|
83 | 41, 82 | pm2.61dane 2881 |
. . . . . . 7
|
84 | | simpr 477 |
. . . . . . 7
|
85 | 83, 84 | eqeltrd 2701 |
. . . . . 6
|
86 | | opphllem5.o |
. . . . . . . . 9
|
87 | | hpg.o |
. . . . . . . . . 10
|
88 | 1, 2, 3, 87, 12, 14 | islnopp 25631 |
. . . . . . . . 9
|
89 | 86, 88 | mpbid 222 |
. . . . . . . 8
|
90 | 89 | simprd 479 |
. . . . . . 7
|
91 | 90 | adantr 481 |
. . . . . 6
|
92 | 85, 91 | r19.29a 3078 |
. . . . 5
|
93 | 31, 92 | eqeltrd 2701 |
. . . 4
|
94 | 1, 2, 3, 4, 5, 7, 8, 9, 11, 13, 15, 17, 32, 40, 93 | mirbtwnhl 25575 |
. . 3
|
95 | 31 | fveq2d 6195 |
. . . 4
|
96 | 95 | breqd 4664 |
. . 3
|
97 | 39 | fveq2d 6195 |
. . . 4
|
98 | 97 | breqd 4664 |
. . 3
|
99 | 94, 96, 98 | 3bitr3d 298 |
. 2
|
100 | 18 | ad2antrr 762 |
. . . 4
≤G |
101 | 6 | ad2antrr 762 |
. . . 4
≤G TarskiG |
102 | 12 | ad2antrr 762 |
. . . 4
≤G |
103 | 14 | ad2antrr 762 |
. . . 4
≤G |
104 | 19 | ad2antrr 762 |
. . . 4
≤G |
105 | 33 | ad2antrr 762 |
. . . 4
≤G |
106 | 10 | ad2antrr 762 |
. . . 4
≤G |
107 | 86 | ad2antrr 762 |
. . . 4
≤G |
108 | 21 | ad2antrr 762 |
. . . 4
≤G ⟂G |
109 | 35 | ad2antrr 762 |
. . . 4
≤G ⟂G |
110 | | simpr 477 |
. . . . 5
|
111 | 110 | adantr 481 |
. . . 4
≤G |
112 | | simpr 477 |
. . . 4
≤G ≤G |
113 | 16 | ad2antrr 762 |
. . . 4
≤G |
114 | 25 | ad2antrr 762 |
. . . 4
≤G |
115 | 1, 2, 3, 87, 4, 100, 101, 9, 8, 102, 103, 104, 105, 106, 107, 108, 109, 111, 112, 113, 114 | opphllem3 25641 |
. . 3
≤G |
116 | 18 | ad2antrr 762 |
. . . . 5
≤G |
117 | 6 | adantr 481 |
. . . . . 6
TarskiG |
118 | 117 | adantr 481 |
. . . . 5
≤G TarskiG |
119 | 14 | ad2antrr 762 |
. . . . 5
≤G |
120 | 12 | adantr 481 |
. . . . . 6
|
121 | 120 | adantr 481 |
. . . . 5
≤G |
122 | 33 | adantr 481 |
. . . . . 6
|
123 | 122 | adantr 481 |
. . . . 5
≤G |
124 | 19 | adantr 481 |
. . . . . 6
|
125 | 124 | adantr 481 |
. . . . 5
≤G |
126 | 10 | ad2antrr 762 |
. . . . 5
≤G |
127 | 86 | ad2antrr 762 |
. . . . . 6
≤G |
128 | 1, 2, 3, 87, 4, 116, 118, 121, 119, 127 | oppcom 25636 |
. . . . 5
≤G |
129 | 35 | ad2antrr 762 |
. . . . 5
≤G ⟂G |
130 | 21 | adantr 481 |
. . . . . 6
⟂G |
131 | 130 | adantr 481 |
. . . . 5
≤G ⟂G |
132 | 110 | necomd 2849 |
. . . . . 6
|
133 | 132 | adantr 481 |
. . . . 5
≤G |
134 | | simpr 477 |
. . . . 5
≤G ≤G |
135 | 16 | ad2antrr 762 |
. . . . . 6
≤G |
136 | 1, 2, 3, 4, 5, 118, 126, 8, 135 | mircl 25556 |
. . . . 5
≤G |
137 | 20 | adantr 481 |
. . . . . . 7
|
138 | 137 | adantr 481 |
. . . . . 6
≤G |
139 | 25 | ad2antrr 762 |
. . . . . 6
≤G |
140 | 1, 2, 3, 4, 5, 118, 126, 8, 138, 139 | mircom 25558 |
. . . . 5
≤G |
141 | 1, 2, 3, 87, 4, 116, 118, 9, 8, 119, 121, 123, 125, 126, 128, 129, 131, 133, 134, 136, 140 | opphllem3 25641 |
. . . 4
≤G |
142 | 1, 2, 3, 4, 5, 118, 126, 8, 135 | mirmir 25557 |
. . . . 5
≤G |
143 | 142 | breq1d 4663 |
. . . 4
≤G |
144 | 141, 143 | bitr2d 269 |
. . 3
≤G |
145 | | eqid 2622 |
. . . . 5
≤G ≤G |
146 | 1, 2, 3, 145, 6, 34, 14, 20, 12 | legtrid 25486 |
. . . 4
≤G ≤G |
147 | 146 | adantr 481 |
. . 3
≤G ≤G |
148 | 115, 144,
147 | mpjaodan 827 |
. 2
|
149 | 99, 148 | pm2.61dane 2881 |
1
|