Step | Hyp | Ref
| Expression |
1 | | ancom 461 |
. . 3
β’ ((π΄(πΎβπΆ)π΅ β§ Β¬ π΄ β π·) β (Β¬ π΄ β π· β§ π΄(πΎβπΆ)π΅)) |
2 | 1 | a1i 11 |
. 2
β’ (π β ((π΄(πΎβπΆ)π΅ β§ Β¬ π΄ β π·) β (Β¬ π΄ β π· β§ π΄(πΎβπΆ)π΅))) |
3 | | hpgid.p |
. . . . 5
β’ π = (BaseβπΊ) |
4 | | hpgid.i |
. . . . 5
β’ πΌ = (ItvβπΊ) |
5 | | hpgid.l |
. . . . 5
β’ πΏ = (LineGβπΊ) |
6 | | hpgid.g |
. . . . . 6
β’ (π β πΊ β TarskiG) |
7 | 6 | adantr 481 |
. . . . 5
β’ ((π β§ Β¬ π΄ β π·) β πΊ β TarskiG) |
8 | | hpgid.d |
. . . . . 6
β’ (π β π· β ran πΏ) |
9 | 8 | adantr 481 |
. . . . 5
β’ ((π β§ Β¬ π΄ β π·) β π· β ran πΏ) |
10 | | colopp.b |
. . . . . 6
β’ (π β π΅ β π) |
11 | 10 | adantr 481 |
. . . . 5
β’ ((π β§ Β¬ π΄ β π·) β π΅ β π) |
12 | | hpgid.o |
. . . . 5
β’ π = {β¨π, πβ© β£ ((π β (π β π·) β§ π β (π β π·)) β§ βπ‘ β π· π‘ β (ππΌπ))} |
13 | | eqid 2731 |
. . . . . . 7
β’
(distβπΊ) =
(distβπΊ) |
14 | | eqid 2731 |
. . . . . . 7
β’
(pInvGβπΊ) =
(pInvGβπΊ) |
15 | | colopp.p |
. . . . . . . 8
β’ (π β πΆ β π·) |
16 | 3, 5, 4, 6, 8, 15 | tglnpt 27588 |
. . . . . . 7
β’ (π β πΆ β π) |
17 | | eqid 2731 |
. . . . . . 7
β’
((pInvGβπΊ)βπΆ) = ((pInvGβπΊ)βπΆ) |
18 | | hpgid.a |
. . . . . . 7
β’ (π β π΄ β π) |
19 | 3, 13, 4, 5, 14, 6,
16, 17, 18 | mircl 27700 |
. . . . . 6
β’ (π β (((pInvGβπΊ)βπΆ)βπ΄) β π) |
20 | 19 | adantr 481 |
. . . . 5
β’ ((π β§ Β¬ π΄ β π·) β (((pInvGβπΊ)βπΆ)βπ΄) β π) |
21 | 15 | adantr 481 |
. . . . 5
β’ ((π β§ Β¬ π΄ β π·) β πΆ β π·) |
22 | 16 | adantr 481 |
. . . . . 6
β’ ((π β§ Β¬ π΄ β π·) β πΆ β π) |
23 | 18 | adantr 481 |
. . . . . . 7
β’ ((π β§ Β¬ π΄ β π·) β π΄ β π) |
24 | | nelne2 3039 |
. . . . . . . . . 10
β’ ((πΆ β π· β§ Β¬ π΄ β π·) β πΆ β π΄) |
25 | 15, 24 | sylan 580 |
. . . . . . . . 9
β’ ((π β§ Β¬ π΄ β π·) β πΆ β π΄) |
26 | 25 | necomd 2995 |
. . . . . . . 8
β’ ((π β§ Β¬ π΄ β π·) β π΄ β πΆ) |
27 | 3, 13, 4, 5, 14, 6,
16, 17, 18 | mirbtwn 27697 |
. . . . . . . . . 10
β’ (π β πΆ β ((((pInvGβπΊ)βπΆ)βπ΄)πΌπ΄)) |
28 | 3, 13, 4, 6, 19, 16, 18, 27 | tgbtwncom 27527 |
. . . . . . . . 9
β’ (π β πΆ β (π΄πΌ(((pInvGβπΊ)βπΆ)βπ΄))) |
29 | 28 | adantr 481 |
. . . . . . . 8
β’ ((π β§ Β¬ π΄ β π·) β πΆ β (π΄πΌ(((pInvGβπΊ)βπΆ)βπ΄))) |
30 | 3, 4, 5, 7, 23, 22, 20, 26, 29 | btwnlng3 27660 |
. . . . . . 7
β’ ((π β§ Β¬ π΄ β π·) β (((pInvGβπΊ)βπΆ)βπ΄) β (π΄πΏπΆ)) |
31 | | colopp.1 |
. . . . . . . . . 10
β’ (π β (πΆ β (π΄πΏπ΅) β¨ π΄ = π΅)) |
32 | 3, 5, 4, 6, 18, 10, 16, 31 | colrot1 27598 |
. . . . . . . . 9
β’ (π β (π΄ β (π΅πΏπΆ) β¨ π΅ = πΆ)) |
33 | 3, 5, 4, 6, 10, 16, 18, 32 | colcom 27597 |
. . . . . . . 8
β’ (π β (π΄ β (πΆπΏπ΅) β¨ πΆ = π΅)) |
34 | 33 | adantr 481 |
. . . . . . 7
β’ ((π β§ Β¬ π΄ β π·) β (π΄ β (πΆπΏπ΅) β¨ πΆ = π΅)) |
35 | 3, 4, 5, 7, 20, 23, 22, 11, 30, 34 | coltr 27686 |
. . . . . 6
β’ ((π β§ Β¬ π΄ β π·) β ((((pInvGβπΊ)βπΆ)βπ΄) β (πΆπΏπ΅) β¨ πΆ = π΅)) |
36 | 3, 5, 4, 7, 22, 11, 20, 35 | colrot1 27598 |
. . . . 5
β’ ((π β§ Β¬ π΄ β π·) β (πΆ β (π΅πΏ(((pInvGβπΊ)βπΆ)βπ΄)) β¨ π΅ = (((pInvGβπΊ)βπΆ)βπ΄))) |
37 | 3, 4, 5, 7, 9, 11,
12, 20, 21, 36 | colopp 27808 |
. . . 4
β’ ((π β§ Β¬ π΄ β π·) β (π΅π(((pInvGβπΊ)βπΆ)βπ΄) β (πΆ β (π΅πΌ(((pInvGβπΊ)βπΆ)βπ΄)) β§ Β¬ π΅ β π· β§ Β¬ (((pInvGβπΊ)βπΆ)βπ΄) β π·))) |
38 | | simpr 485 |
. . . . . . 7
β’ ((π β§ Β¬ π΄ β π·) β Β¬ π΄ β π·) |
39 | 3, 13, 4, 5, 14, 6,
16, 17, 18 | mirmir 27701 |
. . . . . . . . . 10
β’ (π β (((pInvGβπΊ)βπΆ)β(((pInvGβπΊ)βπΆ)βπ΄)) = π΄) |
40 | 39 | adantr 481 |
. . . . . . . . 9
β’ ((π β§ (((pInvGβπΊ)βπΆ)βπ΄) β π·) β (((pInvGβπΊ)βπΆ)β(((pInvGβπΊ)βπΆ)βπ΄)) = π΄) |
41 | 6 | adantr 481 |
. . . . . . . . . 10
β’ ((π β§ (((pInvGβπΊ)βπΆ)βπ΄) β π·) β πΊ β TarskiG) |
42 | 8 | adantr 481 |
. . . . . . . . . 10
β’ ((π β§ (((pInvGβπΊ)βπΆ)βπ΄) β π·) β π· β ran πΏ) |
43 | 15 | adantr 481 |
. . . . . . . . . 10
β’ ((π β§ (((pInvGβπΊ)βπΆ)βπ΄) β π·) β πΆ β π·) |
44 | | simpr 485 |
. . . . . . . . . 10
β’ ((π β§ (((pInvGβπΊ)βπΆ)βπ΄) β π·) β (((pInvGβπΊ)βπΆ)βπ΄) β π·) |
45 | 3, 13, 4, 5, 14, 41, 17, 42, 43, 44 | mirln 27715 |
. . . . . . . . 9
β’ ((π β§ (((pInvGβπΊ)βπΆ)βπ΄) β π·) β (((pInvGβπΊ)βπΆ)β(((pInvGβπΊ)βπΆ)βπ΄)) β π·) |
46 | 40, 45 | eqeltrrd 2833 |
. . . . . . . 8
β’ ((π β§ (((pInvGβπΊ)βπΆ)βπ΄) β π·) β π΄ β π·) |
47 | 46 | stoic1a 1774 |
. . . . . . 7
β’ ((π β§ Β¬ π΄ β π·) β Β¬ (((pInvGβπΊ)βπΆ)βπ΄) β π·) |
48 | | simpr 485 |
. . . . . . . . . 10
β’ ((π β§ π‘ = πΆ) β π‘ = πΆ) |
49 | 48 | eleq1d 2817 |
. . . . . . . . 9
β’ ((π β§ π‘ = πΆ) β (π‘ β (π΄πΌ(((pInvGβπΊ)βπΆ)βπ΄)) β πΆ β (π΄πΌ(((pInvGβπΊ)βπΆ)βπ΄)))) |
50 | 15, 49, 28 | rspcedvd 3597 |
. . . . . . . 8
β’ (π β βπ‘ β π· π‘ β (π΄πΌ(((pInvGβπΊ)βπΆ)βπ΄))) |
51 | 50 | adantr 481 |
. . . . . . 7
β’ ((π β§ Β¬ π΄ β π·) β βπ‘ β π· π‘ β (π΄πΌ(((pInvGβπΊ)βπΆ)βπ΄))) |
52 | 38, 47, 51 | jca31 515 |
. . . . . 6
β’ ((π β§ Β¬ π΄ β π·) β ((Β¬ π΄ β π· β§ Β¬ (((pInvGβπΊ)βπΆ)βπ΄) β π·) β§ βπ‘ β π· π‘ β (π΄πΌ(((pInvGβπΊ)βπΆ)βπ΄)))) |
53 | 3, 13, 4, 12, 23, 20 | islnopp 27778 |
. . . . . 6
β’ ((π β§ Β¬ π΄ β π·) β (π΄π(((pInvGβπΊ)βπΆ)βπ΄) β ((Β¬ π΄ β π· β§ Β¬ (((pInvGβπΊ)βπΆ)βπ΄) β π·) β§ βπ‘ β π· π‘ β (π΄πΌ(((pInvGβπΊ)βπΆ)βπ΄))))) |
54 | 52, 53 | mpbird 256 |
. . . . 5
β’ ((π β§ Β¬ π΄ β π·) β π΄π(((pInvGβπΊ)βπΆ)βπ΄)) |
55 | 3, 4, 5, 12, 7, 9,
23, 11, 20, 54 | lnopp2hpgb 27802 |
. . . 4
β’ ((π β§ Β¬ π΄ β π·) β (π΅π(((pInvGβπΊ)βπΆ)βπ΄) β π΄((hpGβπΊ)βπ·)π΅)) |
56 | | colhp.k |
. . . . . . 7
β’ πΎ = (hlGβπΊ) |
57 | 10 | ad2antrr 724 |
. . . . . . 7
β’ (((π β§ Β¬ π΄ β π·) β§ (πΆ β (π΅πΌ(((pInvGβπΊ)βπΆ)βπ΄)) β§ Β¬ π΅ β π·)) β π΅ β π) |
58 | 18 | ad2antrr 724 |
. . . . . . 7
β’ (((π β§ Β¬ π΄ β π·) β§ (πΆ β (π΅πΌ(((pInvGβπΊ)βπΆ)βπ΄)) β§ Β¬ π΅ β π·)) β π΄ β π) |
59 | 16 | ad2antrr 724 |
. . . . . . 7
β’ (((π β§ Β¬ π΄ β π·) β§ (πΆ β (π΅πΌ(((pInvGβπΊ)βπΆ)βπ΄)) β§ Β¬ π΅ β π·)) β πΆ β π) |
60 | 6 | ad2antrr 724 |
. . . . . . 7
β’ (((π β§ Β¬ π΄ β π·) β§ (πΆ β (π΅πΌ(((pInvGβπΊ)βπΆ)βπ΄)) β§ Β¬ π΅ β π·)) β πΊ β TarskiG) |
61 | 15 | ad2antrr 724 |
. . . . . . . . 9
β’ (((π β§ Β¬ π΄ β π·) β§ (πΆ β (π΅πΌ(((pInvGβπΊ)βπΆ)βπ΄)) β§ Β¬ π΅ β π·)) β πΆ β π·) |
62 | | simprr 771 |
. . . . . . . . 9
β’ (((π β§ Β¬ π΄ β π·) β§ (πΆ β (π΅πΌ(((pInvGβπΊ)βπΆ)βπ΄)) β§ Β¬ π΅ β π·)) β Β¬ π΅ β π·) |
63 | | nelne2 3039 |
. . . . . . . . . 10
β’ ((πΆ β π· β§ Β¬ π΅ β π·) β πΆ β π΅) |
64 | 63 | necomd 2995 |
. . . . . . . . 9
β’ ((πΆ β π· β§ Β¬ π΅ β π·) β π΅ β πΆ) |
65 | 61, 62, 64 | syl2anc 584 |
. . . . . . . 8
β’ (((π β§ Β¬ π΄ β π·) β§ (πΆ β (π΅πΌ(((pInvGβπΊ)βπΆ)βπ΄)) β§ Β¬ π΅ β π·)) β π΅ β πΆ) |
66 | 26 | adantr 481 |
. . . . . . . 8
β’ (((π β§ Β¬ π΄ β π·) β§ (πΆ β (π΅πΌ(((pInvGβπΊ)βπΆ)βπ΄)) β§ Β¬ π΅ β π·)) β π΄ β πΆ) |
67 | | simprl 769 |
. . . . . . . 8
β’ (((π β§ Β¬ π΄ β π·) β§ (πΆ β (π΅πΌ(((pInvGβπΊ)βπΆ)βπ΄)) β§ Β¬ π΅ β π·)) β πΆ β (π΅πΌ(((pInvGβπΊ)βπΆ)βπ΄))) |
68 | 3, 13, 4, 5, 14, 60, 17, 56, 59, 57, 58, 58, 65, 66, 67 | mirhl2 27720 |
. . . . . . 7
β’ (((π β§ Β¬ π΄ β π·) β§ (πΆ β (π΅πΌ(((pInvGβπΊ)βπΆ)βπ΄)) β§ Β¬ π΅ β π·)) β π΅(πΎβπΆ)π΄) |
69 | 3, 4, 56, 57, 58, 59, 60, 68 | hlcomd 27643 |
. . . . . 6
β’ (((π β§ Β¬ π΄ β π·) β§ (πΆ β (π΅πΌ(((pInvGβπΊ)βπΆ)βπ΄)) β§ Β¬ π΅ β π·)) β π΄(πΎβπΆ)π΅) |
70 | 69 | 3adantr3 1171 |
. . . . 5
β’ (((π β§ Β¬ π΄ β π·) β§ (πΆ β (π΅πΌ(((pInvGβπΊ)βπΆ)βπ΄)) β§ Β¬ π΅ β π· β§ Β¬ (((pInvGβπΊ)βπΆ)βπ΄) β π·)) β π΄(πΎβπΆ)π΅) |
71 | 18 | ad2antrr 724 |
. . . . . . 7
β’ (((π β§ Β¬ π΄ β π·) β§ π΄(πΎβπΆ)π΅) β π΄ β π) |
72 | 10 | ad2antrr 724 |
. . . . . . 7
β’ (((π β§ Β¬ π΄ β π·) β§ π΄(πΎβπΆ)π΅) β π΅ β π) |
73 | 19 | ad2antrr 724 |
. . . . . . 7
β’ (((π β§ Β¬ π΄ β π·) β§ π΄(πΎβπΆ)π΅) β (((pInvGβπΊ)βπΆ)βπ΄) β π) |
74 | 6 | ad2antrr 724 |
. . . . . . 7
β’ (((π β§ Β¬ π΄ β π·) β§ π΄(πΎβπΆ)π΅) β πΊ β TarskiG) |
75 | 16 | ad2antrr 724 |
. . . . . . 7
β’ (((π β§ Β¬ π΄ β π·) β§ π΄(πΎβπΆ)π΅) β πΆ β π) |
76 | | simpr 485 |
. . . . . . 7
β’ (((π β§ Β¬ π΄ β π·) β§ π΄(πΎβπΆ)π΅) β π΄(πΎβπΆ)π΅) |
77 | 28 | ad2antrr 724 |
. . . . . . 7
β’ (((π β§ Β¬ π΄ β π·) β§ π΄(πΎβπΆ)π΅) β πΆ β (π΄πΌ(((pInvGβπΊ)βπΆ)βπ΄))) |
78 | 3, 4, 56, 71, 72, 73, 74, 75, 76, 77 | btwnhl 27653 |
. . . . . 6
β’ (((π β§ Β¬ π΄ β π·) β§ π΄(πΎβπΆ)π΅) β πΆ β (π΅πΌ(((pInvGβπΊ)βπΆ)βπ΄))) |
79 | 3, 4, 56, 71, 72, 75, 74, 5, 76 | hlln 27646 |
. . . . . . . . 9
β’ (((π β§ Β¬ π΄ β π·) β§ π΄(πΎβπΆ)π΅) β π΄ β (π΅πΏπΆ)) |
80 | 79 | adantr 481 |
. . . . . . . 8
β’ ((((π β§ Β¬ π΄ β π·) β§ π΄(πΎβπΆ)π΅) β§ π΅ β π·) β π΄ β (π΅πΏπΆ)) |
81 | 7 | ad2antrr 724 |
. . . . . . . . 9
β’ ((((π β§ Β¬ π΄ β π·) β§ π΄(πΎβπΆ)π΅) β§ π΅ β π·) β πΊ β TarskiG) |
82 | 11 | ad2antrr 724 |
. . . . . . . . 9
β’ ((((π β§ Β¬ π΄ β π·) β§ π΄(πΎβπΆ)π΅) β§ π΅ β π·) β π΅ β π) |
83 | 75 | adantr 481 |
. . . . . . . . 9
β’ ((((π β§ Β¬ π΄ β π·) β§ π΄(πΎβπΆ)π΅) β§ π΅ β π·) β πΆ β π) |
84 | 23 | ad2antrr 724 |
. . . . . . . . . 10
β’ ((((π β§ Β¬ π΄ β π·) β§ π΄(πΎβπΆ)π΅) β§ π΅ β π·) β π΄ β π) |
85 | 76 | adantr 481 |
. . . . . . . . . 10
β’ ((((π β§ Β¬ π΄ β π·) β§ π΄(πΎβπΆ)π΅) β§ π΅ β π·) β π΄(πΎβπΆ)π΅) |
86 | 3, 4, 56, 84, 82, 83, 81, 85 | hlne2 27645 |
. . . . . . . . 9
β’ ((((π β§ Β¬ π΄ β π·) β§ π΄(πΎβπΆ)π΅) β§ π΅ β π·) β π΅ β πΆ) |
87 | 9 | ad2antrr 724 |
. . . . . . . . 9
β’ ((((π β§ Β¬ π΄ β π·) β§ π΄(πΎβπΆ)π΅) β§ π΅ β π·) β π· β ran πΏ) |
88 | | simpr 485 |
. . . . . . . . 9
β’ ((((π β§ Β¬ π΄ β π·) β§ π΄(πΎβπΆ)π΅) β§ π΅ β π·) β π΅ β π·) |
89 | 15 | ad3antrrr 728 |
. . . . . . . . 9
β’ ((((π β§ Β¬ π΄ β π·) β§ π΄(πΎβπΆ)π΅) β§ π΅ β π·) β πΆ β π·) |
90 | 3, 4, 5, 81, 82, 83, 86, 86, 87, 88, 89 | tglinethru 27675 |
. . . . . . . 8
β’ ((((π β§ Β¬ π΄ β π·) β§ π΄(πΎβπΆ)π΅) β§ π΅ β π·) β π· = (π΅πΏπΆ)) |
91 | 80, 90 | eleqtrrd 2835 |
. . . . . . 7
β’ ((((π β§ Β¬ π΄ β π·) β§ π΄(πΎβπΆ)π΅) β§ π΅ β π·) β π΄ β π·) |
92 | 38 | ad2antrr 724 |
. . . . . . 7
β’ ((((π β§ Β¬ π΄ β π·) β§ π΄(πΎβπΆ)π΅) β§ π΅ β π·) β Β¬ π΄ β π·) |
93 | 91, 92 | pm2.65da 815 |
. . . . . 6
β’ (((π β§ Β¬ π΄ β π·) β§ π΄(πΎβπΆ)π΅) β Β¬ π΅ β π·) |
94 | 47 | adantr 481 |
. . . . . 6
β’ (((π β§ Β¬ π΄ β π·) β§ π΄(πΎβπΆ)π΅) β Β¬ (((pInvGβπΊ)βπΆ)βπ΄) β π·) |
95 | 78, 93, 94 | 3jca 1128 |
. . . . 5
β’ (((π β§ Β¬ π΄ β π·) β§ π΄(πΎβπΆ)π΅) β (πΆ β (π΅πΌ(((pInvGβπΊ)βπΆ)βπ΄)) β§ Β¬ π΅ β π· β§ Β¬ (((pInvGβπΊ)βπΆ)βπ΄) β π·)) |
96 | 70, 95 | impbida 799 |
. . . 4
β’ ((π β§ Β¬ π΄ β π·) β ((πΆ β (π΅πΌ(((pInvGβπΊ)βπΆ)βπ΄)) β§ Β¬ π΅ β π· β§ Β¬ (((pInvGβπΊ)βπΆ)βπ΄) β π·) β π΄(πΎβπΆ)π΅)) |
97 | 37, 55, 96 | 3bitr3d 308 |
. . 3
β’ ((π β§ Β¬ π΄ β π·) β (π΄((hpGβπΊ)βπ·)π΅ β π΄(πΎβπΆ)π΅)) |
98 | 97 | pm5.32da 579 |
. 2
β’ (π β ((Β¬ π΄ β π· β§ π΄((hpGβπΊ)βπ·)π΅) β (Β¬ π΄ β π· β§ π΄(πΎβπΆ)π΅))) |
99 | | simprr 771 |
. . 3
β’ ((π β§ (Β¬ π΄ β π· β§ π΄((hpGβπΊ)βπ·)π΅)) β π΄((hpGβπΊ)βπ·)π΅) |
100 | 6 | adantr 481 |
. . . . 5
β’ ((π β§ π΄((hpGβπΊ)βπ·)π΅) β πΊ β TarskiG) |
101 | 8 | adantr 481 |
. . . . 5
β’ ((π β§ π΄((hpGβπΊ)βπ·)π΅) β π· β ran πΏ) |
102 | 18 | adantr 481 |
. . . . 5
β’ ((π β§ π΄((hpGβπΊ)βπ·)π΅) β π΄ β π) |
103 | 10 | adantr 481 |
. . . . 5
β’ ((π β§ π΄((hpGβπΊ)βπ·)π΅) β π΅ β π) |
104 | | simpr 485 |
. . . . 5
β’ ((π β§ π΄((hpGβπΊ)βπ·)π΅) β π΄((hpGβπΊ)βπ·)π΅) |
105 | 3, 4, 5, 12, 100, 101, 102, 103, 104 | hpgne1 27800 |
. . . 4
β’ ((π β§ π΄((hpGβπΊ)βπ·)π΅) β Β¬ π΄ β π·) |
106 | 105, 104 | jca 512 |
. . 3
β’ ((π β§ π΄((hpGβπΊ)βπ·)π΅) β (Β¬ π΄ β π· β§ π΄((hpGβπΊ)βπ·)π΅)) |
107 | 99, 106 | impbida 799 |
. 2
β’ (π β ((Β¬ π΄ β π· β§ π΄((hpGβπΊ)βπ·)π΅) β π΄((hpGβπΊ)βπ·)π΅)) |
108 | 2, 98, 107 | 3bitr2rd 307 |
1
β’ (π β (π΄((hpGβπΊ)βπ·)π΅ β (π΄(πΎβπΆ)π΅ β§ Β¬ π΄ β π·))) |