Step | Hyp | Ref
| Expression |
1 | | oppcom.o |
. . . . . 6
β’ (π β π΄ππ΅) |
2 | | hpg.p |
. . . . . . 7
β’ π = (BaseβπΊ) |
3 | | hpg.d |
. . . . . . 7
β’ β =
(distβπΊ) |
4 | | hpg.i |
. . . . . . 7
β’ πΌ = (ItvβπΊ) |
5 | | hpg.o |
. . . . . . 7
β’ π = {β¨π, πβ© β£ ((π β (π β π·) β§ π β (π β π·)) β§ βπ‘ β π· π‘ β (ππΌπ))} |
6 | | oppcom.a |
. . . . . . 7
β’ (π β π΄ β π) |
7 | | oppcom.b |
. . . . . . 7
β’ (π β π΅ β π) |
8 | 2, 3, 4, 5, 6, 7 | islnopp 27990 |
. . . . . 6
β’ (π β (π΄ππ΅ β ((Β¬ π΄ β π· β§ Β¬ π΅ β π·) β§ βπ‘ β π· π‘ β (π΄πΌπ΅)))) |
9 | 1, 8 | mpbid 231 |
. . . . 5
β’ (π β ((Β¬ π΄ β π· β§ Β¬ π΅ β π·) β§ βπ‘ β π· π‘ β (π΄πΌπ΅))) |
10 | 9 | simpld 496 |
. . . 4
β’ (π β (Β¬ π΄ β π· β§ Β¬ π΅ β π·)) |
11 | 10 | simprd 497 |
. . 3
β’ (π β Β¬ π΅ β π·) |
12 | 10 | simpld 496 |
. . 3
β’ (π β Β¬ π΄ β π·) |
13 | 9 | simprd 497 |
. . . 4
β’ (π β βπ‘ β π· π‘ β (π΄πΌπ΅)) |
14 | | opphl.g |
. . . . . . . 8
β’ (π β πΊ β TarskiG) |
15 | 14 | ad2antrr 725 |
. . . . . . 7
β’ (((π β§ π‘ β π·) β§ π‘ β (π΄πΌπ΅)) β πΊ β TarskiG) |
16 | 6 | ad2antrr 725 |
. . . . . . 7
β’ (((π β§ π‘ β π·) β§ π‘ β (π΄πΌπ΅)) β π΄ β π) |
17 | | opphl.l |
. . . . . . . . 9
β’ πΏ = (LineGβπΊ) |
18 | 14 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π‘ β π·) β πΊ β TarskiG) |
19 | | opphl.d |
. . . . . . . . . 10
β’ (π β π· β ran πΏ) |
20 | 19 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π‘ β π·) β π· β ran πΏ) |
21 | | simpr 486 |
. . . . . . . . 9
β’ ((π β§ π‘ β π·) β π‘ β π·) |
22 | 2, 17, 4, 18, 20, 21 | tglnpt 27800 |
. . . . . . . 8
β’ ((π β§ π‘ β π·) β π‘ β π) |
23 | 22 | adantr 482 |
. . . . . . 7
β’ (((π β§ π‘ β π·) β§ π‘ β (π΄πΌπ΅)) β π‘ β π) |
24 | 7 | ad2antrr 725 |
. . . . . . 7
β’ (((π β§ π‘ β π·) β§ π‘ β (π΄πΌπ΅)) β π΅ β π) |
25 | | simpr 486 |
. . . . . . 7
β’ (((π β§ π‘ β π·) β§ π‘ β (π΄πΌπ΅)) β π‘ β (π΄πΌπ΅)) |
26 | 2, 3, 4, 15, 16, 23, 24, 25 | tgbtwncom 27739 |
. . . . . 6
β’ (((π β§ π‘ β π·) β§ π‘ β (π΄πΌπ΅)) β π‘ β (π΅πΌπ΄)) |
27 | 14 | ad2antrr 725 |
. . . . . . 7
β’ (((π β§ π‘ β π·) β§ π‘ β (π΅πΌπ΄)) β πΊ β TarskiG) |
28 | 7 | ad2antrr 725 |
. . . . . . 7
β’ (((π β§ π‘ β π·) β§ π‘ β (π΅πΌπ΄)) β π΅ β π) |
29 | 22 | adantr 482 |
. . . . . . 7
β’ (((π β§ π‘ β π·) β§ π‘ β (π΅πΌπ΄)) β π‘ β π) |
30 | 6 | ad2antrr 725 |
. . . . . . 7
β’ (((π β§ π‘ β π·) β§ π‘ β (π΅πΌπ΄)) β π΄ β π) |
31 | | simpr 486 |
. . . . . . 7
β’ (((π β§ π‘ β π·) β§ π‘ β (π΅πΌπ΄)) β π‘ β (π΅πΌπ΄)) |
32 | 2, 3, 4, 27, 28, 29, 30, 31 | tgbtwncom 27739 |
. . . . . 6
β’ (((π β§ π‘ β π·) β§ π‘ β (π΅πΌπ΄)) β π‘ β (π΄πΌπ΅)) |
33 | 26, 32 | impbida 800 |
. . . . 5
β’ ((π β§ π‘ β π·) β (π‘ β (π΄πΌπ΅) β π‘ β (π΅πΌπ΄))) |
34 | 33 | rexbidva 3177 |
. . . 4
β’ (π β (βπ‘ β π· π‘ β (π΄πΌπ΅) β βπ‘ β π· π‘ β (π΅πΌπ΄))) |
35 | 13, 34 | mpbid 231 |
. . 3
β’ (π β βπ‘ β π· π‘ β (π΅πΌπ΄)) |
36 | 11, 12, 35 | jca31 516 |
. 2
β’ (π β ((Β¬ π΅ β π· β§ Β¬ π΄ β π·) β§ βπ‘ β π· π‘ β (π΅πΌπ΄))) |
37 | 2, 3, 4, 5, 7, 6 | islnopp 27990 |
. 2
β’ (π β (π΅ππ΄ β ((Β¬ π΅ β π· β§ Β¬ π΄ β π·) β§ βπ‘ β π· π‘ β (π΅πΌπ΄)))) |
38 | 36, 37 | mpbird 257 |
1
β’ (π β π΅ππ΄) |