Proof of Theorem colhp
Step | Hyp | Ref
| Expression |
1 | | ancom 466 |
. . 3
|
2 | 1 | a1i 11 |
. 2
|
3 | | hpgid.p |
. . . . 5
|
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
|
9 | 8 | adantr 481 |
. . . . 5
|
10 | | colopp.b |
. . . . . 6
|
11 | 10 | adantr 481 |
. . . . 5
|
12 | | hpgid.o |
. . . . 5
|
13 | | eqid 2622 |
. . . . . . 7
|
14 | | eqid 2622 |
. . . . . . 7
pInvG pInvG |
15 | | colopp.p |
. . . . . . . 8
|
16 | 3, 5, 4, 6, 8, 15 | tglnpt 25444 |
. . . . . . 7
|
17 | | eqid 2622 |
. . . . . . 7
pInvG pInvG |
18 | | hpgid.a |
. . . . . . 7
|
19 | 3, 13, 4, 5, 14, 6,
16, 17, 18 | mircl 25556 |
. . . . . 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 2891 |
. . . . . . . . . . 11
|
25 | 15, 24 | sylan 488 |
. . . . . . . . . 10
|
26 | 25 | necomd 2849 |
. . . . . . . . 9
|
27 | 26 | neneqd 2799 |
. . . . . . . 8
|
28 | | simpr 477 |
. . . . . . . . . . . . . . . . 17
|
29 | 3, 13, 4, 5, 14, 6,
16, 17, 18 | mirmir 25557 |
. . . . . . . . . . . . . . . . . . . 20
pInvGpInvG |
30 | 29 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
pInvG pInvGpInvG |
31 | 6 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
pInvG TarskiG |
32 | 8 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
pInvG |
33 | 15 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
pInvG |
34 | | simpr 477 |
. . . . . . . . . . . . . . . . . . . 20
pInvG pInvG |
35 | 3, 13, 4, 5, 14, 31, 17, 32, 33, 34 | mirln 25571 |
. . . . . . . . . . . . . . . . . . 19
pInvG pInvGpInvG |
36 | 30, 35 | eqeltrrd 2702 |
. . . . . . . . . . . . . . . . . 18
pInvG |
37 | 36 | stoic1a 1697 |
. . . . . . . . . . . . . . . . 17
pInvG |
38 | | simpr 477 |
. . . . . . . . . . . . . . . . . . . 20
|
39 | | eqidd 2623 |
. . . . . . . . . . . . . . . . . . . 20
pInvG pInvG |
40 | 38, 39 | eleq12d 2695 |
. . . . . . . . . . . . . . . . . . 19
pInvG
pInvG |
41 | 3, 13, 4, 5, 14, 6,
16, 17, 18 | mirbtwn 25553 |
. . . . . . . . . . . . . . . . . . . 20
pInvG |
42 | 3, 13, 4, 6, 19, 16, 18, 41 | tgbtwncom 25383 |
. . . . . . . . . . . . . . . . . . 19
pInvG |
43 | 15, 40, 42 | rspcedvd 3317 |
. . . . . . . . . . . . . . . . . 18
pInvG |
44 | 43 | adantr 481 |
. . . . . . . . . . . . . . . . 17
pInvG |
45 | 28, 37, 44 | jca31 557 |
. . . . . . . . . . . . . . . 16
pInvG
pInvG |
46 | 3, 13, 4, 12, 23, 20 | islnopp 25631 |
. . . . . . . . . . . . . . . 16
pInvG pInvG
pInvG |
47 | 45, 46 | mpbird 247 |
. . . . . . . . . . . . . . 15
pInvG |
48 | 3, 13, 4, 12, 5, 9,
7, 23, 20, 47 | oppne3 25635 |
. . . . . . . . . . . . . 14
pInvG |
49 | 42 | adantr 481 |
. . . . . . . . . . . . . 14
pInvG |
50 | 3, 4, 5, 7, 23, 20, 22, 48, 49 | btwnlng1 25514 |
. . . . . . . . . . . . 13
pInvG |
51 | 50 | orcd 407 |
. . . . . . . . . . . 12
pInvG pInvG |
52 | 3, 5, 4, 7, 23, 20, 22, 51 | colcom 25453 |
. . . . . . . . . . 11
pInvG pInvG |
53 | 3, 5, 4, 7, 20, 23, 22, 52 | colrot1 25454 |
. . . . . . . . . 10
pInvG |
54 | 53 | orcomd 403 |
. . . . . . . . 9
pInvG |
55 | 54 | ord 392 |
. . . . . . . 8
pInvG |
56 | 27, 55 | mpd 15 |
. . . . . . 7
pInvG |
57 | | colopp.1 |
. . . . . . . . . 10
|
58 | 3, 5, 4, 6, 18, 10, 16, 57 | colrot1 25454 |
. . . . . . . . 9
|
59 | 3, 5, 4, 6, 10, 16, 18, 58 | colcom 25453 |
. . . . . . . 8
|
60 | 59 | adantr 481 |
. . . . . . 7
|
61 | 3, 4, 5, 7, 20, 23, 22, 11, 56, 60 | coltr 25542 |
. . . . . 6
pInvG |
62 | 3, 5, 4, 7, 22, 11, 20, 61 | colrot1 25454 |
. . . . 5
pInvG pInvG |
63 | 3, 4, 5, 7, 9, 11,
12, 20, 21, 62 | colopp 25661 |
. . . 4
pInvG pInvG
pInvG |
64 | 3, 4, 5, 12, 7, 9,
23, 11, 20, 47 | lnopp2hpgb 25655 |
. . . 4
pInvG hpG |
65 | | colhp.k |
. . . . . . . . 9
hlG |
66 | | simpll 790 |
. . . . . . . . . 10
pInvG
|
67 | 66, 10 | syl 17 |
. . . . . . . . 9
pInvG
|
68 | 66, 18 | syl 17 |
. . . . . . . . 9
pInvG
|
69 | 66, 16 | syl 17 |
. . . . . . . . 9
pInvG
|
70 | 66, 6 | syl 17 |
. . . . . . . . 9
pInvG
TarskiG |
71 | 66, 15 | syl 17 |
. . . . . . . . . . 11
pInvG
|
72 | | simprr 796 |
. . . . . . . . . . 11
pInvG
|
73 | | nelne2 2891 |
. . . . . . . . . . . 12
|
74 | 73 | necomd 2849 |
. . . . . . . . . . 11
|
75 | 71, 72, 74 | syl2anc 693 |
. . . . . . . . . 10
pInvG
|
76 | 26 | adantr 481 |
. . . . . . . . . 10
pInvG
|
77 | | simprl 794 |
. . . . . . . . . 10
pInvG
pInvG |
78 | 3, 13, 4, 5, 14, 70, 17, 65, 69, 67, 68, 68, 75, 76, 77 | mirhl2 25576 |
. . . . . . . . 9
pInvG
|
79 | 3, 4, 65, 67, 68, 69, 70, 78 | hlcomd 25499 |
. . . . . . . 8
pInvG
|
80 | 28 | adantr 481 |
. . . . . . . 8
pInvG
|
81 | 79, 80 | jca 554 |
. . . . . . 7
pInvG
|
82 | 81 | 3adantr3 1222 |
. . . . . 6
pInvG
pInvG |
83 | 82 | simpld 475 |
. . . . 5
pInvG
pInvG |
84 | 23 | adantr 481 |
. . . . . . 7
|
85 | 11 | adantr 481 |
. . . . . . 7
|
86 | 20 | adantr 481 |
. . . . . . 7
pInvG |
87 | 7 | adantr 481 |
. . . . . . 7
TarskiG |
88 | 16 | ad2antrr 762 |
. . . . . . 7
|
89 | | simpr 477 |
. . . . . . 7
|
90 | 42 | ad2antrr 762 |
. . . . . . 7
pInvG |
91 | 3, 4, 65, 84, 85, 86, 87, 88, 89, 90 | btwnhl 25509 |
. . . . . 6
pInvG |
92 | 3, 4, 65, 84, 85, 88, 87, 5, 89 | hlln 25502 |
. . . . . . . . 9
|
93 | 92 | adantr 481 |
. . . . . . . 8
|
94 | 87 | adantr 481 |
. . . . . . . . 9
TarskiG |
95 | 85 | adantr 481 |
. . . . . . . . 9
|
96 | 88 | adantr 481 |
. . . . . . . . 9
|
97 | 84 | adantr 481 |
. . . . . . . . . 10
|
98 | 89 | adantr 481 |
. . . . . . . . . 10
|
99 | 3, 4, 65, 97, 95, 96, 94, 98 | hlne2 25501 |
. . . . . . . . 9
|
100 | 9 | ad2antrr 762 |
. . . . . . . . 9
|
101 | | simpr 477 |
. . . . . . . . 9
|
102 | 15 | ad3antrrr 766 |
. . . . . . . . 9
|
103 | 3, 4, 5, 94, 95, 96, 99, 99, 100, 101, 102 | tglinethru 25531 |
. . . . . . . 8
|
104 | 93, 103 | eleqtrrd 2704 |
. . . . . . 7
|
105 | 28 | ad2antrr 762 |
. . . . . . 7
|
106 | 104, 105 | pm2.65da 600 |
. . . . . 6
|
107 | 37 | adantr 481 |
. . . . . 6
pInvG |
108 | 91, 106, 107 | 3jca 1242 |
. . . . 5
pInvG
pInvG |
109 | 83, 108 | impbida 877 |
. . . 4
pInvG
pInvG
|
110 | 63, 64, 109 | 3bitr3d 298 |
. . 3
hpG
|
111 | 110 | pm5.32da 673 |
. 2
hpG |
112 | | simpr 477 |
. . . 4
hpG hpG |
113 | 112 | adantrl 752 |
. . 3
hpG hpG |
114 | 6 | adantr 481 |
. . . . 5
hpG TarskiG |
115 | 8 | adantr 481 |
. . . . 5
hpG |
116 | 18 | adantr 481 |
. . . . 5
hpG |
117 | 10 | adantr 481 |
. . . . 5
hpG |
118 | 3, 4, 5, 12, 114, 115, 116, 117, 112 | hpgne1 25653 |
. . . 4
hpG
|
119 | 118, 112 | jca 554 |
. . 3
hpG
hpG |
120 | 113, 119 | impbida 877 |
. 2
hpG hpG |
121 | 2, 111, 120 | 3bitr2rd 297 |
1
hpG
|