Step | Hyp | Ref
| Expression |
1 | | hpg.p |
. . . . 5
β’ π = (BaseβπΊ) |
2 | | hpg.d |
. . . . 5
β’ β =
(distβπΊ) |
3 | | hpg.i |
. . . . 5
β’ πΌ = (ItvβπΊ) |
4 | | opphl.g |
. . . . . 6
β’ (π β πΊ β TarskiG) |
5 | 4 | ad3antrrr 729 |
. . . . 5
β’ ((((π β§ π΄ππ΄) β§ π‘ β π·) β§ π‘ β (π΄πΌπ΄)) β πΊ β TarskiG) |
6 | | oppnid.1 |
. . . . . 6
β’ (π β π΄ β π) |
7 | 6 | ad3antrrr 729 |
. . . . 5
β’ ((((π β§ π΄ππ΄) β§ π‘ β π·) β§ π‘ β (π΄πΌπ΄)) β π΄ β π) |
8 | | opphl.l |
. . . . . 6
β’ πΏ = (LineGβπΊ) |
9 | | opphl.d |
. . . . . . 7
β’ (π β π· β ran πΏ) |
10 | 9 | ad3antrrr 729 |
. . . . . 6
β’ ((((π β§ π΄ππ΄) β§ π‘ β π·) β§ π‘ β (π΄πΌπ΄)) β π· β ran πΏ) |
11 | | simplr 768 |
. . . . . 6
β’ ((((π β§ π΄ππ΄) β§ π‘ β π·) β§ π‘ β (π΄πΌπ΄)) β π‘ β π·) |
12 | 1, 8, 3, 5, 10, 11 | tglnpt 27533 |
. . . . 5
β’ ((((π β§ π΄ππ΄) β§ π‘ β π·) β§ π‘ β (π΄πΌπ΄)) β π‘ β π) |
13 | | simpr 486 |
. . . . 5
β’ ((((π β§ π΄ππ΄) β§ π‘ β π·) β§ π‘ β (π΄πΌπ΄)) β π‘ β (π΄πΌπ΄)) |
14 | 1, 2, 3, 5, 7, 12,
13 | axtgbtwnid 27450 |
. . . 4
β’ ((((π β§ π΄ππ΄) β§ π‘ β π·) β§ π‘ β (π΄πΌπ΄)) β π΄ = π‘) |
15 | 14, 11 | eqeltrd 2838 |
. . 3
β’ ((((π β§ π΄ππ΄) β§ π‘ β π·) β§ π‘ β (π΄πΌπ΄)) β π΄ β π·) |
16 | | hpg.o |
. . . . 5
β’ π = {β¨π, πβ© β£ ((π β (π β π·) β§ π β (π β π·)) β§ βπ‘ β π· π‘ β (ππΌπ))} |
17 | 1, 2, 3, 16, 6, 6 | islnopp 27723 |
. . . 4
β’ (π β (π΄ππ΄ β ((Β¬ π΄ β π· β§ Β¬ π΄ β π·) β§ βπ‘ β π· π‘ β (π΄πΌπ΄)))) |
18 | 17 | simplbda 501 |
. . 3
β’ ((π β§ π΄ππ΄) β βπ‘ β π· π‘ β (π΄πΌπ΄)) |
19 | 15, 18 | r19.29a 3160 |
. 2
β’ ((π β§ π΄ππ΄) β π΄ β π·) |
20 | 17 | simprbda 500 |
. . 3
β’ ((π β§ π΄ππ΄) β (Β¬ π΄ β π· β§ Β¬ π΄ β π·)) |
21 | 20 | simpld 496 |
. 2
β’ ((π β§ π΄ππ΄) β Β¬ π΄ β π·) |
22 | 19, 21 | pm2.65da 816 |
1
β’ (π β Β¬ π΄ππ΄) |