Proof of Theorem hypcgrlem2
Step | Hyp | Ref
| Expression |
1 | | hypcgr.p |
. . . 4
|
2 | | hypcgr.m |
. . . 4
|
3 | | hypcgr.i |
. . . 4
Itv |
4 | | hypcgr.g |
. . . . 5
TarskiG |
5 | 4 | adantr 481 |
. . . 4
midG
TarskiG |
6 | | hypcgr.h |
. . . . 5
DimTarskiG≥ |
7 | 6 | adantr 481 |
. . . 4
midG
DimTarskiG≥ |
8 | | hypcgr.a |
. . . . 5
|
9 | 8 | adantr 481 |
. . . 4
midG
|
10 | | hypcgr.b |
. . . . 5
|
11 | 10 | adantr 481 |
. . . 4
midG
|
12 | | hypcgr.c |
. . . . 5
|
13 | 12 | adantr 481 |
. . . 4
midG
|
14 | | eqid 2622 |
. . . . 5
LineG LineG |
15 | | eqid 2622 |
. . . . 5
pInvG pInvG |
16 | | eqid 2622 |
. . . . 5
pInvG pInvG |
17 | | hypcgr.d |
. . . . . 6
|
18 | 17 | adantr 481 |
. . . . 5
midG
|
19 | 1, 2, 3, 14, 15, 5, 11, 16, 18 | mircl 25556 |
. . . 4
midG
pInvG |
20 | | hypcgr.e |
. . . . 5
|
21 | 20 | adantr 481 |
. . . 4
midG
|
22 | | hypcgr.1 |
. . . . 5
∟G |
23 | 22 | adantr 481 |
. . . 4
midG
∟G |
24 | | eqidd 2623 |
. . . . . 6
midG
pInvG pInvG |
25 | | hypcgrlem2.b |
. . . . . . . . 9
|
26 | 25 | adantr 481 |
. . . . . . . 8
midG
|
27 | 1, 2, 3, 14, 15, 5, 11, 16, 21 | mirinv 25561 |
. . . . . . . 8
midG
pInvG |
28 | 26, 27 | mpbird 247 |
. . . . . . 7
midG
pInvG |
29 | 28 | eqcomd 2628 |
. . . . . 6
midG
pInvG |
30 | | hypcgr.f |
. . . . . . . . . 10
|
31 | 30 | adantr 481 |
. . . . . . . . 9
midG
|
32 | 1, 2, 3, 5, 7, 13,
31 | midcom 25674 |
. . . . . . . 8
midG
midG midG |
33 | | simpr 477 |
. . . . . . . 8
midG
midG |
34 | 32, 33 | eqtr3d 2658 |
. . . . . . 7
midG
midG |
35 | 1, 2, 3, 5, 7, 31,
13, 15, 11 | ismidb 25670 |
. . . . . . 7
midG
pInvG midG |
36 | 34, 35 | mpbird 247 |
. . . . . 6
midG
pInvG |
37 | 24, 29, 36 | s3eqd 13609 |
. . . . 5
midG
pInvG pInvGpInvGpInvG |
38 | | hypcgr.2 |
. . . . . . 7
∟G |
39 | 38 | adantr 481 |
. . . . . 6
midG
∟G |
40 | 1, 2, 3, 14, 15, 5, 18, 21, 31, 39, 16, 11 | mirrag 25596 |
. . . . 5
midG
pInvGpInvGpInvG ∟G |
41 | 37, 40 | eqeltrd 2701 |
. . . 4
midG
pInvG ∟G |
42 | | hypcgr.3 |
. . . . . 6
|
43 | 42 | adantr 481 |
. . . . 5
midG
|
44 | 1, 2, 3, 14, 15, 5, 11, 16, 18, 21 | miriso 25565 |
. . . . 5
midG
pInvG pInvG |
45 | 28 | oveq2d 6666 |
. . . . 5
midG
pInvG pInvG pInvG |
46 | 43, 44, 45 | 3eqtr2d 2662 |
. . . 4
midG
pInvG |
47 | 26 | oveq1d 6665 |
. . . 4
midG
|
48 | | eqid 2622 |
. . . 4
lInvGmidGpInvGLineG lInvGmidGpInvGLineG |
49 | | eqidd 2623 |
. . . 4
midG
|
50 | 1, 2, 3, 5, 7, 9, 11, 13, 19, 21, 13, 23, 41, 46, 47, 26, 48, 49 | hypcgrlem1 25691 |
. . 3
midG
pInvG |
51 | 36 | oveq2d 6666 |
. . 3
midG
pInvG pInvG pInvG |
52 | 1, 2, 3, 14, 15, 5, 11, 16, 18, 31 | miriso 25565 |
. . 3
midG
pInvG pInvG |
53 | 50, 51, 52 | 3eqtrd 2660 |
. 2
midG
|
54 | 4 | ad2antrr 762 |
. . . 4
midG
TarskiG |
55 | 6 | ad2antrr 762 |
. . . 4
midG
DimTarskiG≥ |
56 | 8 | ad2antrr 762 |
. . . 4
midG
|
57 | 10 | ad2antrr 762 |
. . . 4
midG
|
58 | 12 | ad2antrr 762 |
. . . 4
midG
|
59 | 17 | ad2antrr 762 |
. . . 4
midG
|
60 | 20 | ad2antrr 762 |
. . . 4
midG
|
61 | 30 | ad2antrr 762 |
. . . 4
midG
|
62 | 22 | ad2antrr 762 |
. . . 4
midG
∟G |
63 | 38 | ad2antrr 762 |
. . . 4
midG
∟G |
64 | 42 | ad2antrr 762 |
. . . 4
midG
|
65 | | hypcgr.4 |
. . . . 5
|
66 | 65 | ad2antrr 762 |
. . . 4
midG
|
67 | 25 | ad2antrr 762 |
. . . 4
midG
|
68 | | eqid 2622 |
. . . 4
lInvGmidGLineG lInvGmidGLineG |
69 | | simpr 477 |
. . . 4
midG
|
70 | 1, 2, 3, 54, 55, 56, 57, 58, 59, 60, 61, 62, 63, 64, 66, 67, 68, 69 | hypcgrlem1 25691 |
. . 3
midG
|
71 | 4 | ad2antrr 762 |
. . . . 5
midG
TarskiG |
72 | 6 | ad2antrr 762 |
. . . . 5
midG
DimTarskiG≥ |
73 | 8 | ad2antrr 762 |
. . . . 5
midG
|
74 | 10 | ad2antrr 762 |
. . . . 5
midG
|
75 | 12 | ad2antrr 762 |
. . . . 5
midG
|
76 | | hypcgrlem2.s |
. . . . . 6
lInvGmidGLineG |
77 | 30 | ad2antrr 762 |
. . . . . . . 8
midG
|
78 | 1, 2, 3, 71, 72, 75, 77 | midcl 25669 |
. . . . . . 7
midG
midG |
79 | | simplr 792 |
. . . . . . 7
midG
midG |
80 | 1, 3, 14, 71, 78, 74, 79 | tgelrnln 25525 |
. . . . . 6
midG
midGLineG LineG |
81 | 17 | ad2antrr 762 |
. . . . . 6
midG
|
82 | 1, 2, 3, 71, 72, 76, 14, 80, 81 | lmicl 25678 |
. . . . 5
midG
|
83 | 20 | ad2antrr 762 |
. . . . . 6
midG
|
84 | 1, 2, 3, 71, 72, 76, 14, 80, 83 | lmicl 25678 |
. . . . 5
midG
|
85 | 1, 2, 3, 71, 72, 76, 14, 80, 77 | lmicl 25678 |
. . . . 5
midG
|
86 | 22 | ad2antrr 762 |
. . . . 5
midG
∟G |
87 | 1, 2, 3, 71, 72, 76, 14, 80 | lmimot 25690 |
. . . . . 6
midG
Ismt |
88 | 38 | ad2antrr 762 |
. . . . . 6
midG
∟G |
89 | 1, 2, 3, 14, 15, 71, 81, 83, 77, 87, 88 | motrag 25603 |
. . . . 5
midG
∟G |
90 | 42 | ad2antrr 762 |
. . . . . 6
midG
|
91 | 1, 2, 3, 71, 72, 76, 14, 80, 81, 83 | lmiiso 25689 |
. . . . . 6
midG
|
92 | 90, 91 | eqtr4d 2659 |
. . . . 5
midG
|
93 | 65 | ad2antrr 762 |
. . . . . 6
midG
|
94 | 1, 2, 3, 71, 72, 76, 14, 80, 83, 77 | lmiiso 25689 |
. . . . . 6
midG
|
95 | 93, 94 | eqtr4d 2659 |
. . . . 5
midG
|
96 | 1, 3, 14, 71, 78, 74, 79 | tglinerflx2 25529 |
. . . . . . 7
midG
midGLineG |
97 | 1, 2, 3, 71, 72, 76, 14, 80, 74 | lmiinv 25684 |
. . . . . . 7
midG
midGLineG |
98 | 96, 97 | mpbird 247 |
. . . . . 6
midG
|
99 | 25 | ad2antrr 762 |
. . . . . . 7
midG
|
100 | 99 | fveq2d 6195 |
. . . . . 6
midG
|
101 | 98, 100 | eqtr3d 2658 |
. . . . 5
midG
|
102 | | eqid 2622 |
. . . . 5
lInvGmidGLineG lInvGmidGLineG |
103 | 1, 2, 3, 71, 72, 75, 77 | midcom 25674 |
. . . . . . 7
midG
midG midG |
104 | 1, 3, 14, 71, 78, 74, 79 | tglinerflx1 25528 |
. . . . . . 7
midG
midG midGLineG |
105 | 103, 104 | eqeltrrd 2702 |
. . . . . 6
midG
midG midGLineG |
106 | | simpr 477 |
. . . . . . . . . 10
midG
|
107 | 106 | necomd 2849 |
. . . . . . . . 9
midG
|
108 | 1, 3, 14, 71, 77, 75, 107 | tgelrnln 25525 |
. . . . . . . 8
midG
LineG LineG |
109 | 1, 2, 3, 71, 72, 75, 77 | midbtwn 25671 |
. . . . . . . . . . 11
midG
midG |
110 | 1, 2, 3, 71, 75, 78, 77, 109 | tgbtwncom 25383 |
. . . . . . . . . 10
midG
midG |
111 | 1, 3, 14, 71, 77, 75, 78, 107, 110 | btwnlng1 25514 |
. . . . . . . . 9
midG
midG LineG |
112 | 104, 111 | elind 3798 |
. . . . . . . 8
midG
midG midGLineG LineG |
113 | 1, 3, 14, 71, 77, 75, 107 | tglinerflx2 25529 |
. . . . . . . 8
midG
LineG |
114 | 79 | necomd 2849 |
. . . . . . . 8
midG
midG |
115 | 4 | ad2antrr 762 |
. . . . . . . . . . . 12
midG
midG TarskiG |
116 | 12 | ad2antrr 762 |
. . . . . . . . . . . 12
midG
midG |
117 | 30 | ad2antrr 762 |
. . . . . . . . . . . 12
midG
midG |
118 | 6 | ad2antrr 762 |
. . . . . . . . . . . . . 14
midG
midG DimTarskiG≥ |
119 | | simpr 477 |
. . . . . . . . . . . . . . 15
midG
midG midG |
120 | 119 | eqcomd 2628 |
. . . . . . . . . . . . . 14
midG
midG midG |
121 | 1, 2, 3, 115, 118, 116, 117, 120 | midcgr 25672 |
. . . . . . . . . . . . 13
midG
midG |
122 | 121 | eqcomd 2628 |
. . . . . . . . . . . 12
midG
midG |
123 | 1, 2, 3, 115, 116, 117, 116, 122 | axtgcgrid 25362 |
. . . . . . . . . . 11
midG
midG |
124 | 123 | ex 450 |
. . . . . . . . . 10
midG
midG |
125 | 124 | necon3d 2815 |
. . . . . . . . 9
midG
midG |
126 | 125 | imp 445 |
. . . . . . . 8
midG
midG |
127 | 99 | eqcomd 2628 |
. . . . . . . . . . 11
midG
|
128 | | eqidd 2623 |
. . . . . . . . . . . 12
midG
midG midG |
129 | 1, 2, 3, 71, 72, 75, 77, 15, 78 | ismidb 25670 |
. . . . . . . . . . . 12
midG
pInvGmidG
midG midG |
130 | 128, 129 | mpbird 247 |
. . . . . . . . . . 11
midG
pInvGmidG |
131 | 127, 130 | oveq12d 6668 |
. . . . . . . . . 10
midG
pInvGmidG |
132 | 93, 131 | eqtrd 2656 |
. . . . . . . . 9
midG
pInvGmidG |
133 | 1, 2, 3, 14, 15, 71, 74, 78, 75 | israg 25592 |
. . . . . . . . 9
midG
midG ∟G
pInvGmidG |
134 | 132, 133 | mpbird 247 |
. . . . . . . 8
midG
midG ∟G |
135 | 1, 2, 3, 14, 71, 80, 108, 112, 96, 113, 114, 126, 134 | ragperp 25612 |
. . . . . . 7
midG
midGLineG⟂GLineG |
136 | 135 | orcd 407 |
. . . . . 6
midG
midGLineG⟂GLineG |
137 | 1, 2, 3, 71, 72, 76, 14, 80, 77, 75 | islmib 25679 |
. . . . . 6
midG
midG midGLineG midGLineG⟂GLineG |
138 | 105, 136,
137 | mpbir2and 957 |
. . . . 5
midG
|
139 | 1, 2, 3, 71, 72, 73, 74, 75, 82, 84, 85, 86, 89, 92, 95, 101, 102, 138 | hypcgrlem1 25691 |
. . . 4
midG
|
140 | 1, 2, 3, 71, 72, 76, 14, 80, 81, 77 | lmiiso 25689 |
. . . 4
midG
|
141 | 139, 140 | eqtrd 2656 |
. . 3
midG
|
142 | 70, 141 | pm2.61dane 2881 |
. 2
midG
|
143 | 53, 142 | pm2.61dane 2881 |
1
|