Proof of Theorem lmiisolem
Step | Hyp | Ref
| Expression |
1 | | ismid.p |
. . . . . . . 8
     |
2 | | ismid.d |
. . . . . . . 8
     |
3 | | ismid.i |
. . . . . . . 8
Itv   |
4 | | ismid.g |
. . . . . . . . 9

TarskiG |
5 | 4 | adantr 467 |
. . . . . . . 8
 
    
TarskiG |
6 | | lmiisolem.z |
. . . . . . . . . 10
   midG         midG     midG          |
7 | | ismid.1 |
. . . . . . . . . . 11
 DimTarskiG≥  |
8 | | lmiiso.1 |
. . . . . . . . . . . 12
   |
9 | | lmif.m |
. . . . . . . . . . . . 13
 lInvG      |
10 | | lmif.l |
. . . . . . . . . . . . 13
LineG   |
11 | | lmif.d |
. . . . . . . . . . . . 13
   |
12 | 1, 2, 3, 4, 7, 9, 10, 11, 8 | lmicl 24828 |
. . . . . . . . . . . 12
       |
13 | 1, 2, 3, 4, 7, 8, 12 | midcl 24819 |
. . . . . . . . . . 11
   midG          |
14 | | lmiiso.2 |
. . . . . . . . . . . 12
   |
15 | 1, 2, 3, 4, 7, 9, 10, 11, 14 | lmicl 24828 |
. . . . . . . . . . . 12
       |
16 | 1, 2, 3, 4, 7, 14,
15 | midcl 24819 |
. . . . . . . . . . 11
   midG          |
17 | 1, 2, 3, 4, 7, 13,
16 | midcl 24819 |
. . . . . . . . . 10
    midG         midG     midG           |
18 | 6, 17 | syl5eqel 2533 |
. . . . . . . . 9
   |
19 | 18 | adantr 467 |
. . . . . . . 8
 
    
  |
20 | | eqid 2451 |
. . . . . . . . . 10
pInvG  pInvG   |
21 | | lmiisolem.s |
. . . . . . . . . 10
 pInvG      |
22 | 1, 2, 3, 10, 20, 4, 18, 21, 8 | mircl 24706 |
. . . . . . . . 9
       |
23 | 22 | adantr 467 |
. . . . . . . 8
 
    
      |
24 | 8 | adantr 467 |
. . . . . . . 8
 
    
  |
25 | 1, 2, 3, 10, 20, 5, 19, 21, 24 | mircgr 24702 |
. . . . . . . 8
 
    
          |
26 | | simpr 463 |
. . . . . . . . 9
 
    
      |
27 | 26 | eqcomd 2457 |
. . . . . . . 8
 
    
      |
28 | 1, 2, 3, 5, 19, 23, 19, 24, 25, 27 | tgcgreq 24526 |
. . . . . . 7
 
    
  |
29 | | simpr 463 |
. . . . . . . . . . . . 13
 
  midG          midG           midG          midG          |
30 | 29 | oveq2d 6306 |
. . . . . . . . . . . 12
 
  midG          midG            midG         midG     midG            midG         midG     midG           |
31 | 30, 6 | syl6reqr 2504 |
. . . . . . . . . . 11
 
  midG          midG            midG         midG     midG           |
32 | 4 | adantr 467 |
. . . . . . . . . . . 12
 
  midG          midG         TarskiG |
33 | 7 | adantr 467 |
. . . . . . . . . . . 12
 
  midG          midG         DimTarskiG≥  |
34 | 13 | adantr 467 |
. . . . . . . . . . . 12
 
  midG          midG           midG          |
35 | 1, 2, 3, 32, 33, 34, 34 | midid 24823 |
. . . . . . . . . . 11
 
  midG          midG            midG         midG     midG           midG          |
36 | 31, 35 | eqtrd 2485 |
. . . . . . . . . 10
 
  midG          midG           midG          |
37 | | eqidd 2452 |
. . . . . . . . . . . . 13
           |
38 | 1, 2, 3, 4, 7, 9, 10, 11, 8, 12 | islmib 24829 |
. . . . . . . . . . . . 13
             midG          ⟂G                    |
39 | 37, 38 | mpbid 214 |
. . . . . . . . . . . 12
    midG          ⟂G                   |
40 | 39 | simpld 461 |
. . . . . . . . . . 11
   midG          |
41 | 40 | adantr 467 |
. . . . . . . . . 10
 
  midG          midG           midG          |
42 | 36, 41 | eqeltrd 2529 |
. . . . . . . . 9
 
  midG          midG           |
43 | 4 | adantr 467 |
. . . . . . . . . . 11
 
  midG          midG        
TarskiG |
44 | 13 | adantr 467 |
. . . . . . . . . . 11
 
  midG          midG           midG          |
45 | 16 | adantr 467 |
. . . . . . . . . . 11
 
  midG          midG           midG          |
46 | 18 | adantr 467 |
. . . . . . . . . . 11
 
  midG          midG        
  |
47 | | simpr 463 |
. . . . . . . . . . 11
 
  midG          midG           midG          midG          |
48 | 1, 2, 3, 4, 7, 13,
16 | midbtwn 24821 |
. . . . . . . . . . . . 13
    midG         midG     midG            midG            midG           |
49 | 6, 48 | syl5eqel 2533 |
. . . . . . . . . . . 12
    midG            midG           |
50 | 49 | adantr 467 |
. . . . . . . . . . 11
 
  midG          midG        
   midG            midG           |
51 | 1, 3, 10, 43, 44, 45, 46, 47, 50 | btwnlng1 24664 |
. . . . . . . . . 10
 
  midG          midG        
   midG            midG           |
52 | 11 | adantr 467 |
. . . . . . . . . . 11
 
  midG          midG        
  |
53 | 40 | adantr 467 |
. . . . . . . . . . 11
 
  midG          midG           midG          |
54 | | eqidd 2452 |
. . . . . . . . . . . . . 14
           |
55 | 1, 2, 3, 4, 7, 9, 10, 11, 14, 15 | islmib 24829 |
. . . . . . . . . . . . . 14
             midG          ⟂G                    |
56 | 54, 55 | mpbid 214 |
. . . . . . . . . . . . 13
    midG          ⟂G                   |
57 | 56 | simpld 461 |
. . . . . . . . . . . 12
   midG          |
58 | 57 | adantr 467 |
. . . . . . . . . . 11
 
  midG          midG           midG          |
59 | 1, 3, 10, 43, 44, 45, 47, 47, 52, 53, 58 | tglinethru 24681 |
. . . . . . . . . 10
 
  midG          midG        
   midG            midG           |
60 | 51, 59 | eleqtrrd 2532 |
. . . . . . . . 9
 
  midG          midG        
  |
61 | 42, 60 | pm2.61dane 2711 |
. . . . . . . 8
   |
62 | 61 | adantr 467 |
. . . . . . 7
 
    
  |
63 | 28, 62 | eqeltrrd 2530 |
. . . . . 6
 
    
  |
64 | 1, 2, 3, 4, 7, 9, 10, 11, 8 | lmiinv 24834 |
. . . . . . 7
         |
65 | 64 | biimpar 488 |
. . . . . 6
 
       |
66 | 63, 65 | syldan 473 |
. . . . 5
 
    
      |
67 | 66, 28 | eqtr4d 2488 |
. . . 4
 
    
      |
68 | 67 | oveq1d 6305 |
. . 3
 
    
                  |
69 | | eqidd 2452 |
. . . . . . . . 9
 
    
  |
70 | 4 | adantr 467 |
. . . . . . . . . 10
 
    
TarskiG |
71 | 14 | adantr 467 |
. . . . . . . . . 10
 
    
  |
72 | 16 | adantr 467 |
. . . . . . . . . 10
 
    
  midG          |
73 | 1, 2, 3, 4, 7, 14,
15 | midbtwn 24821 |
. . . . . . . . . . . 12
   midG                  |
74 | 73 | adantr 467 |
. . . . . . . . . . 11
 
    
  midG                  |
75 | | simpr 463 |
. . . . . . . . . . . 12
 
    
      |
76 | 75 | oveq2d 6306 |
. . . . . . . . . . 11
 
    
              |
77 | 74, 76 | eleqtrrd 2532 |
. . . . . . . . . 10
 
    
  midG              |
78 | 1, 2, 3, 70, 71, 72, 77 | axtgbtwnid 24514 |
. . . . . . . . 9
 
    
  midG          |
79 | | eqidd 2452 |
. . . . . . . . 9
 
    
  |
80 | 69, 78, 79 | s3eqd 12959 |
. . . . . . . 8
 
    
           midG             |
81 | 1, 2, 3, 10, 20, 4, 18, 14, 14 | ragtrivb 24747 |
. . . . . . . . 9
       ∟G    |
82 | 81 | adantr 467 |
. . . . . . . 8
 
    
      ∟G    |
83 | 80, 82 | eqeltrrd 2530 |
. . . . . . 7
 
    
     midG           ∟G    |
84 | 4 | adantr 467 |
. . . . . . . 8
 
    
TarskiG |
85 | 61 | adantr 467 |
. . . . . . . 8
 
    
  |
86 | 57 | adantr 467 |
. . . . . . . 8
 
    
  midG          |
87 | 14 | adantr 467 |
. . . . . . . 8
 
    
  |
88 | | df-ne 2624 |
. . . . . . . . . 10
    
      |
89 | 56 | simprd 465 |
. . . . . . . . . . . 12
   ⟂G                  |
90 | 89 | orcomd 390 |
. . . . . . . . . . 11
       ⟂G              |
91 | 90 | orcanai 924 |
. . . . . . . . . 10
 
      ⟂G             |
92 | 88, 91 | sylan2b 478 |
. . . . . . . . 9
 
    
 ⟂G             |
93 | 15 | adantr 467 |
. . . . . . . . . . 11
 
    
      |
94 | | simpr 463 |
. . . . . . . . . . 11
 
    
      |
95 | 16 | adantr 467 |
. . . . . . . . . . 11
 
    
  midG          |
96 | 4 | adantr 467 |
. . . . . . . . . . . . . . 15
 
  midG        
TarskiG |
97 | 14 | adantr 467 |
. . . . . . . . . . . . . . 15
 
  midG        
  |
98 | 15 | adantr 467 |
. . . . . . . . . . . . . . 15
 
  midG        
      |
99 | 7 | adantr 467 |
. . . . . . . . . . . . . . . . 17
 
  midG        
DimTarskiG≥  |
100 | | simpr 463 |
. . . . . . . . . . . . . . . . 17
 
  midG        
  midG          |
101 | 1, 2, 3, 96, 99, 97, 98, 100 | midcgr 24822 |
. . . . . . . . . . . . . . . 16
 
  midG        
          |
102 | 101 | eqcomd 2457 |
. . . . . . . . . . . . . . 15
 
  midG        
          |
103 | 1, 2, 3, 96, 97, 98, 97, 102 | axtgcgrid 24511 |
. . . . . . . . . . . . . 14
 
  midG        
      |
104 | 103 | ex 436 |
. . . . . . . . . . . . 13
    midG               |
105 | 104 | necon3d 2645 |
. . . . . . . . . . . 12
        midG           |
106 | 105 | imp 431 |
. . . . . . . . . . 11
 
    
  midG          |
107 | 73 | adantr 467 |
. . . . . . . . . . . 12
 
    
  midG                  |
108 | 1, 3, 10, 84, 87, 93, 95, 94, 107 | btwnlng1 24664 |
. . . . . . . . . . 11
 
    
  midG                  |
109 | 1, 3, 10, 84, 87, 93, 94, 95, 106, 108 | tglineelsb2 24677 |
. . . . . . . . . 10
 
    
             midG           |
110 | 1, 3, 10, 84, 95, 87, 106 | tglinecom 24680 |
. . . . . . . . . 10
 
    
   midG                midG           |
111 | 109, 110 | eqtr4d 2488 |
. . . . . . . . 9
 
    
           midG             |
112 | 92, 111 | breqtrd 4427 |
. . . . . . . 8
 
    
 ⟂G      midG             |
113 | 1, 2, 3, 10, 84, 85, 86, 87, 112 | perpdrag 24770 |
. . . . . . 7
 
    
     midG           ∟G    |
114 | 83, 113 | pm2.61dane 2711 |
. . . . . 6
      midG           ∟G    |
115 | 1, 2, 3, 10, 20, 4, 18, 16, 14 | israg 24742 |
. . . . . 6
       midG           ∟G 
     pInvG      midG                |
116 | 114, 115 | mpbid 214 |
. . . . 5
      pInvG      midG               |
117 | | eqidd 2452 |
. . . . . . 7
   midG          midG          |
118 | 1, 2, 3, 4, 7, 14,
15, 20, 16 | ismidb 24820 |
. . . . . . 7
        pInvG      midG           
  midG          midG           |
119 | 117, 118 | mpbird 236 |
. . . . . 6
       pInvG      midG              |
120 | 119 | oveq2d 6306 |
. . . . 5
          pInvG      midG               |
121 | 116, 120 | eqtr4d 2488 |
. . . 4
           |
122 | 121 | adantr 467 |
. . 3
 
    
          |
123 | 28 | oveq1d 6305 |
. . 3
 
    
      |
124 | 68, 122, 123 | 3eqtr2d 2491 |
. 2
 
    
              |
125 | 4 | adantr 467 |
. . . 4
 
    
TarskiG |
126 | 22 | adantr 467 |
. . . 4
 
    
      |
127 | 18 | adantr 467 |
. . . 4
 
    
  |
128 | 8 | adantr 467 |
. . . 4
 
    
  |
129 | 1, 2, 3, 10, 20, 4, 18, 21, 12 | mircl 24706 |
. . . . 5
           |
130 | 129 | adantr 467 |
. . . 4
 
    
          |
131 | 12 | adantr 467 |
. . . 4
 
    
      |
132 | 14 | adantr 467 |
. . . 4
 
    
  |
133 | 15 | adantr 467 |
. . . 4
 
    
      |
134 | | simpr 463 |
. . . 4
 
    
      |
135 | 1, 2, 3, 10, 20, 125, 127, 21, 128 | mirbtwn 24703 |
. . . 4
 
    
          |
136 | 1, 2, 3, 10, 20, 125, 127, 21, 131 | mirbtwn 24703 |
. . . 4
 
    
                  |
137 | | eqidd 2452 |
. . . . . . . . . . . 12
 
    
  |
138 | 4 | adantr 467 |
. . . . . . . . . . . . 13
 
    
TarskiG |
139 | 8 | adantr 467 |
. . . . . . . . . . . . 13
 
    
  |
140 | 13 | adantr 467 |
. . . . . . . . . . . . 13
 
    
  midG          |
141 | 1, 2, 3, 4, 7, 8, 12 | midbtwn 24821 |
. . . . . . . . . . . . . . 15
   midG                  |
142 | 141 | adantr 467 |
. . . . . . . . . . . . . 14
 
    
  midG                  |
143 | | simpr 463 |
. . . . . . . . . . . . . . 15
 
    
      |
144 | 143 | oveq2d 6306 |
. . . . . . . . . . . . . 14
 
    
              |
145 | 142, 144 | eleqtrrd 2532 |
. . . . . . . . . . . . 13
 
    
  midG              |
146 | 1, 2, 3, 138, 139, 140, 145 | axtgbtwnid 24514 |
. . . . . . . . . . . 12
 
    
  midG          |
147 | | eqidd 2452 |
. . . . . . . . . . . 12
 
    
  |
148 | 137, 146,
147 | s3eqd 12959 |
. . . . . . . . . . 11
 
    
           midG             |
149 | 1, 2, 3, 10, 20, 4, 18, 8, 8 | ragtrivb 24747 |
. . . . . . . . . . . 12
       ∟G    |
150 | 149 | adantr 467 |
. . . . . . . . . . 11
 
    
      ∟G    |
151 | 148, 150 | eqeltrrd 2530 |
. . . . . . . . . 10
 
    
     midG           ∟G    |
152 | 4 | adantr 467 |
. . . . . . . . . . 11
 
    
TarskiG |
153 | 61 | adantr 467 |
. . . . . . . . . . 11
 
    
  |
154 | 40 | adantr 467 |
. . . . . . . . . . 11
 
    
  midG          |
155 | 8 | adantr 467 |
. . . . . . . . . . 11
 
    
  |
156 | | df-ne 2624 |
. . . . . . . . . . . . 13
    
      |
157 | 39 | simprd 465 |
. . . . . . . . . . . . . . 15
   ⟂G                  |
158 | 157 | orcomd 390 |
. . . . . . . . . . . . . 14
       ⟂G              |
159 | 158 | orcanai 924 |
. . . . . . . . . . . . 13
 
      ⟂G             |
160 | 156, 159 | sylan2b 478 |
. . . . . . . . . . . 12
 
    
 ⟂G             |
161 | 12 | adantr 467 |
. . . . . . . . . . . . . 14
 
    
      |
162 | | simpr 463 |
. . . . . . . . . . . . . 14
 
    
      |
163 | 13 | adantr 467 |
. . . . . . . . . . . . . 14
 
    
  midG          |
164 | 4 | adantr 467 |
. . . . . . . . . . . . . . . . . 18
 
  midG        
TarskiG |
165 | 8 | adantr 467 |
. . . . . . . . . . . . . . . . . 18
 
  midG        
  |
166 | 12 | adantr 467 |
. . . . . . . . . . . . . . . . . 18
 
  midG        
      |
167 | 7 | adantr 467 |
. . . . . . . . . . . . . . . . . . . 20
 
  midG        
DimTarskiG≥  |
168 | | simpr 463 |
. . . . . . . . . . . . . . . . . . . 20
 
  midG        
  midG          |
169 | 1, 2, 3, 164, 167, 165, 166, 168 | midcgr 24822 |
. . . . . . . . . . . . . . . . . . 19
 
  midG        
          |
170 | 169 | eqcomd 2457 |
. . . . . . . . . . . . . . . . . 18
 
  midG        
          |
171 | 1, 2, 3, 164, 165, 166, 165, 170 | axtgcgrid 24511 |
. . . . . . . . . . . . . . . . 17
 
  midG        
      |
172 | 171 | ex 436 |
. . . . . . . . . . . . . . . 16
    midG               |
173 | 172 | necon3d 2645 |
. . . . . . . . . . . . . . 15
        midG           |
174 | 173 | imp 431 |
. . . . . . . . . . . . . 14
 
    
  midG          |
175 | 141 | adantr 467 |
. . . . . . . . . . . . . . 15
 
    
  midG                  |
176 | 1, 3, 10, 152, 155, 161, 163, 162, 175 | btwnlng1 24664 |
. . . . . . . . . . . . . 14
 
    
  midG                  |
177 | 1, 3, 10, 152, 155, 161, 162, 163, 174, 176 | tglineelsb2 24677 |
. . . . . . . . . . . . 13
 
    
             midG           |
178 | 1, 3, 10, 152, 163, 155, 174 | tglinecom 24680 |
. . . . . . . . . . . . 13
 
    
   midG                midG           |
179 | 177, 178 | eqtr4d 2488 |
. . . . . . . . . . . 12
 
    
           midG             |
180 | 160, 179 | breqtrd 4427 |
. . . . . . . . . . 11
 
    
 ⟂G      midG             |
181 | 1, 2, 3, 10, 152, 153, 154, 155, 180 | perpdrag 24770 |
. . . . . . . . . 10
 
    
     midG           ∟G    |
182 | 151, 181 | pm2.61dane 2711 |
. . . . . . . . 9
      midG           ∟G    |
183 | 1, 2, 3, 10, 20, 4, 18, 13, 8 | israg 24742 |
. . . . . . . . 9
       midG           ∟G 
     pInvG      midG                |
184 | 182, 183 | mpbid 214 |
. . . . . . . 8
      pInvG      midG               |
185 | | eqidd 2452 |
. . . . . . . . . 10
   midG          midG          |
186 | 1, 2, 3, 4, 7, 8, 12, 20, 13 | ismidb 24820 |
. . . . . . . . . 10
        pInvG      midG           
  midG          midG           |
187 | 185, 186 | mpbird 236 |
. . . . . . . . 9
       pInvG      midG              |
188 | 187 | oveq2d 6306 |
. . . . . . . 8
          pInvG      midG               |
189 | 184, 188 | eqtr4d 2488 |
. . . . . . 7
           |
190 | 1, 2, 3, 10, 20, 4, 18, 21, 8 | mircgr 24702 |
. . . . . . 7
           |
191 | 1, 2, 3, 10, 20, 4, 18, 21, 12 | mircgr 24702 |
. . . . . . 7
                   |
192 | 189, 190,
191 | 3eqtr4d 2495 |
. . . . . 6
                   |
193 | 192 | adantr 467 |
. . . . 5
 
    
                  |
194 | 1, 2, 3, 125, 127, 126, 127, 130, 193 | tgcgrcomlr 24524 |
. . . 4
 
    
              
   |
195 | 189 | adantr 467 |
. . . 4
 
    
          |
196 | 21 | fveq1i 5866 |
. . . . . . . . . 10
     midG           pInvG         midG          |
197 | 1, 2, 3, 4, 7, 8, 12, 21, 18 | mirmid 24825 |
. . . . . . . . . 10
       midG                 midG           |
198 | 6 | eqcomi 2460 |
. . . . . . . . . . 11
   midG         midG     midG          |
199 | 1, 2, 3, 4, 7, 13,
16, 20, 18 | ismidb 24820 |
. . . . . . . . . . 11
    midG          pInvG         midG        
   midG         midG     midG            |
200 | 198, 199 | mpbiri 237 |
. . . . . . . . . 10
   midG          pInvG         midG           |
201 | 196, 197,
200 | 3eqtr4a 2511 |
. . . . . . . . 9
       midG              midG          |
202 | 1, 2, 3, 4, 7, 22,
129, 20, 16 | ismidb 24820 |
. . . . . . . . 9
            pInvG      midG                      midG              midG           |
203 | 201, 202 | mpbird 236 |
. . . . . . . 8
           pInvG      midG                  |
204 | 119, 203 | oveq12d 6308 |
. . . . . . 7
                  pInvG      midG              pInvG      midG                   |
205 | | eqid 2451 |
. . . . . . . 8
 pInvG      midG          pInvG      midG          |
206 | 1, 2, 3, 10, 20, 4, 16, 205, 14, 22 | miriso 24715 |
. . . . . . 7
    pInvG      midG              pInvG      midG                         |
207 | 204, 206 | eqtr2d 2486 |
. . . . . 6
                       |
208 | 207 | adantr 467 |
. . . . 5
 
    
          
           |
209 | 1, 2, 3, 125, 132, 126, 133, 130, 208 | tgcgrcomlr 24524 |
. . . 4
 
    
              
       |
210 | 121 | adantr 467 |
. . . 4
 
    
          |
211 | 1, 2, 3, 125, 126, 127, 128, 130, 127, 131, 132, 133, 134, 135, 136, 194, 195, 209, 210 | axtg5seg 24513 |
. . 3
 
    
      
       |
212 | 211 | eqcomd 2457 |
. 2
 
    
              |
213 | 124, 212 | pm2.61dane 2711 |
1
               |