Step | Hyp | Ref
| Expression |
1 | | lmieu.a |
. . . 4
   |
2 | 1 | adantr 467 |
. . 3
 
   |
3 | | simpr 463 |
. . . . . . . . . . . 12
      
  midG    

  |
4 | | eqidd 2452 |
. . . . . . . . . . . . . . 15
      
  midG    
   midG      midG      |
5 | | ismid.p |
. . . . . . . . . . . . . . . 16
     |
6 | | ismid.d |
. . . . . . . . . . . . . . . 16
     |
7 | | ismid.i |
. . . . . . . . . . . . . . . 16
Itv   |
8 | | ismid.g |
. . . . . . . . . . . . . . . . 17

TarskiG |
9 | 8 | ad4antr 738 |
. . . . . . . . . . . . . . . 16
      
  midG    

TarskiG |
10 | | ismid.1 |
. . . . . . . . . . . . . . . . 17
 DimTarskiG≥  |
11 | 10 | ad4antr 738 |
. . . . . . . . . . . . . . . 16
      
  midG    
 DimTarskiG≥  |
12 | 2 | ad3antrrr 736 |
. . . . . . . . . . . . . . . 16
      
  midG    

  |
13 | | simpllr 769 |
. . . . . . . . . . . . . . . 16
      
  midG    
   |
14 | | eqid 2451 |
. . . . . . . . . . . . . . . 16
pInvG  pInvG   |
15 | 5, 6, 7, 9, 11, 12, 13 | midcl 24819 |
. . . . . . . . . . . . . . . 16
      
  midG    
   midG      |
16 | 5, 6, 7, 9, 11, 12, 13, 14, 15 | ismidb 24820 |
. . . . . . . . . . . . . . 15
      
  midG    
    pInvG      midG       
  midG      midG       |
17 | 4, 16 | mpbird 236 |
. . . . . . . . . . . . . 14
      
  midG    
   pInvG      midG          |
18 | 17 | adantr 467 |
. . . . . . . . . . . . 13
     
    midG    
        pInvG      midG          |
19 | | lmieu.l |
. . . . . . . . . . . . . . . 16
LineG   |
20 | 9 | adantr 467 |
. . . . . . . . . . . . . . . 16
     
    midG    
     
TarskiG |
21 | | lmieu.1 |
. . . . . . . . . . . . . . . . . 18
   |
22 | 21 | ad4antr 738 |
. . . . . . . . . . . . . . . . 17
      
  midG    

  |
23 | 22 | adantr 467 |
. . . . . . . . . . . . . . . 16
     
    midG    
     
  |
24 | 12 | adantr 467 |
. . . . . . . . . . . . . . . . 17
     
    midG    
     
  |
25 | 13 | adantr 467 |
. . . . . . . . . . . . . . . . 17
     
    midG    
        |
26 | 3 | neqned 2631 |
. . . . . . . . . . . . . . . . . 18
      
  midG    
   |
27 | 26 | adantr 467 |
. . . . . . . . . . . . . . . . 17
     
    midG    
        |
28 | 5, 7, 19, 20, 24, 25, 27 | tgelrnln 24675 |
. . . . . . . . . . . . . . . 16
     
    midG    
            |
29 | | simpr 463 |
. . . . . . . . . . . . . . . 16
     
    midG    
            |
30 | | simp-4r 777 |
. . . . . . . . . . . . . . . . . 18
      
  midG    

  |
31 | 30 | adantr 467 |
. . . . . . . . . . . . . . . . 17
     
    midG    
     
  |
32 | 5, 7, 19, 20, 24, 25, 27 | tglinerflx1 24678 |
. . . . . . . . . . . . . . . . 17
     
    midG    
     
      |
33 | 31, 32 | elind 3618 |
. . . . . . . . . . . . . . . 16
     
    midG    
     
        |
34 | | simpllr 769 |
. . . . . . . . . . . . . . . . 17
     
    midG    
        midG      |
35 | 5, 6, 7, 9, 11, 12, 13 | midbtwn 24821 |
. . . . . . . . . . . . . . . . . . 19
      
  midG    
   midG          |
36 | 5, 7, 19, 9, 12, 13, 15, 26, 35 | btwnlng1 24664 |
. . . . . . . . . . . . . . . . . 18
      
  midG    
   midG          |
37 | 36 | adantr 467 |
. . . . . . . . . . . . . . . . 17
     
    midG    
        midG          |
38 | 34, 37 | elind 3618 |
. . . . . . . . . . . . . . . 16
     
    midG    
        midG            |
39 | 5, 7, 19, 20, 23, 28, 29, 33, 38 | tglineineq 24688 |
. . . . . . . . . . . . . . 15
     
    midG    
     
  midG      |
40 | 39 | fveq2d 5869 |
. . . . . . . . . . . . . 14
     
    midG    
       pInvG      pInvG      midG       |
41 | 40 | fveq1d 5867 |
. . . . . . . . . . . . 13
     
    midG    
        pInvG          pInvG      midG          |
42 | | eqid 2451 |
. . . . . . . . . . . . . 14
 pInvG      pInvG      |
43 | 5, 6, 7, 19, 14, 20, 24, 42 | mircinv 24713 |
. . . . . . . . . . . . 13
     
    midG    
        pInvG          |
44 | 18, 41, 43 | 3eqtr2rd 2492 |
. . . . . . . . . . . 12
     
    midG    
     
  |
45 | 3, 44 | mtand 665 |
. . . . . . . . . . 11
      
  midG    

      |
46 | 8 | ad5antr 740 |
. . . . . . . . . . . 12
     
    midG    
  ⟂G        TarskiG |
47 | 21 | ad5antr 740 |
. . . . . . . . . . . 12
     
    midG    
  ⟂G          |
48 | | nne 2628 |
. . . . . . . . . . . . . . 15
    
      |
49 | 45, 48 | sylib 200 |
. . . . . . . . . . . . . 14
      
  midG    

      |
50 | 49 | adantr 467 |
. . . . . . . . . . . . 13
     
    midG    
  ⟂G              |
51 | 50, 47 | eqeltrrd 2530 |
. . . . . . . . . . . 12
     
    midG    
  ⟂G              |
52 | | simpr 463 |
. . . . . . . . . . . 12
     
    midG    
  ⟂G         ⟂G         |
53 | 5, 6, 7, 19, 46, 47, 51, 52 | perpneq 24759 |
. . . . . . . . . . 11
     
    midG    
  ⟂G              |
54 | 45, 53 | mtand 665 |
. . . . . . . . . 10
      
  midG    
  ⟂G         |
55 | 54 | ex 436 |
. . . . . . . . 9
   


  midG    

 ⟂G          |
56 | 55 | con4d 109 |
. . . . . . . 8
   


  midG    
  ⟂G          |
57 | | idd 25 |
. . . . . . . 8
   


  midG    

   |
58 | 56, 57 | jaod 382 |
. . . . . . 7
   


  midG    
   ⟂G           |
59 | 58 | impr 625 |
. . . . . 6
   


   midG      ⟂G         
  |
60 | 59 | eqcomd 2457 |
. . . . 5
   


   midG      ⟂G         
  |
61 | | simpr 463 |
. . . . . . . . 9
   


   |
62 | 61 | oveq2d 6306 |
. . . . . . . 8
   


   midG      midG      |
63 | 5, 6, 7, 8, 10, 1,
1 | midid 24823 |
. . . . . . . . 9
   midG      |
64 | 63 | ad3antrrr 736 |
. . . . . . . 8
   


   midG      |
65 | 62, 64 | eqtrd 2485 |
. . . . . . 7
   


   midG      |
66 | | simpllr 769 |
. . . . . . 7
   


   |
67 | 65, 66 | eqeltrd 2529 |
. . . . . 6
   


   midG      |
68 | 61 | eqcomd 2457 |
. . . . . . 7
   


   |
69 | 68 | olcd 395 |
. . . . . 6
   


   ⟂G          |
70 | 67, 69 | jca 535 |
. . . . 5
   


    midG      ⟂G           |
71 | 60, 70 | impbida 843 |
. . . 4
         midG      ⟂G        
   |
72 | 71 | ralrimiva 2802 |
. . 3
 
 
    midG      ⟂G        
   |
73 | | reu6i 3229 |
. . 3
       midG      ⟂G        
  
   midG      ⟂G           |
74 | 2, 72, 73 | syl2anc 667 |
. 2
 
 
   midG      ⟂G           |
75 | 8 | adantr 467 |
. . . . . 6
 
 TarskiG |
76 | 75 | ad2antrr 732 |
. . . . 5
   

      ⟂G    TarskiG |
77 | 21 | adantr 467 |
. . . . . . 7
 
   |
78 | 77 | ad2antrr 732 |
. . . . . 6
   

      ⟂G      |
79 | | simplr 762 |
. . . . . 6
   

      ⟂G      |
80 | 5, 19, 7, 76, 78, 79 | tglnpt 24594 |
. . . . 5
   

      ⟂G      |
81 | | eqid 2451 |
. . . . 5
 pInvG      pInvG      |
82 | 1 | adantr 467 |
. . . . . 6
 
   |
83 | 82 | ad2antrr 732 |
. . . . 5
   

      ⟂G      |
84 | 5, 6, 7, 19, 14, 76, 80, 81, 83 | mircl 24706 |
. . . 4
   

      ⟂G      pInvG          |
85 | | oveq2 6298 |
. . . . . . . . . 10
   midG             midG       |
86 | 85 | breq1d 4412 |
. . . . . . . . 9
   midG          ⟂G  
     midG      ⟂G      |
87 | | simprl 764 |
. . . . . . . . 9
     
       ⟂G    
   midG      ⟂G         
  midG      |
88 | | simpr 463 |
. . . . . . . . . . . 12
 

  |
89 | 5, 6, 7, 19, 75, 77, 82, 88 | foot 24764 |
. . . . . . . . . . 11
 
 
     ⟂G     |
90 | | reurmo 3010 |
. . . . . . . . . . 11
       ⟂G         ⟂G     |
91 | 89, 90 | syl 17 |
. . . . . . . . . 10
 
 
     ⟂G     |
92 | 91 | ad4antr 738 |
. . . . . . . . 9
     
       ⟂G    
   midG      ⟂G         

     ⟂G     |
93 | 79 | ad2antrr 732 |
. . . . . . . . 9
     
       ⟂G    
   midG      ⟂G         
  |
94 | | simpllr 769 |
. . . . . . . . 9
     
       ⟂G    
   midG      ⟂G         
     ⟂G     |
95 | 76 | ad2antrr 732 |
. . . . . . . . . . 11
     
       ⟂G    
   midG      ⟂G         
TarskiG |
96 | 83 | ad2antrr 732 |
. . . . . . . . . . 11
     
       ⟂G    
   midG      ⟂G         
  |
97 | | simplr 762 |
. . . . . . . . . . 11
     
       ⟂G    
   midG      ⟂G         
  |
98 | 10 | ad5antr 740 |
. . . . . . . . . . . . 13
     
       ⟂G    
   midG      ⟂G         
DimTarskiG≥  |
99 | 5, 6, 7, 95, 98, 96, 97 | midcl 24819 |
. . . . . . . . . . . 12
     
       ⟂G    
   midG      ⟂G         
  midG      |
100 | 5, 6, 7, 95, 98, 96, 97 | midbtwn 24821 |
. . . . . . . . . . . 12
     
       ⟂G    
   midG      ⟂G         
  midG          |
101 | 88 | ad4antr 738 |
. . . . . . . . . . . . 13
     
       ⟂G    
   midG      ⟂G         
  |
102 | | nelne2 2721 |
. . . . . . . . . . . . 13
    midG   
   midG      |
103 | 87, 101, 102 | syl2anc 667 |
. . . . . . . . . . . 12
     
       ⟂G    
   midG      ⟂G         
  midG      |
104 | 5, 6, 7, 95, 96, 99, 97, 100, 103 | tgbtwnne 24534 |
. . . . . . . . . . 11
     
       ⟂G    
   midG      ⟂G         
  |
105 | 5, 7, 19, 95, 96, 97, 99, 104, 100 | btwnlng1 24664 |
. . . . . . . . . . 11
     
       ⟂G    
   midG      ⟂G         
  midG          |
106 | 5, 7, 19, 95, 96, 97, 104, 99, 103, 105 | tglineelsb2 24677 |
. . . . . . . . . 10
     
       ⟂G    
   midG      ⟂G         
         midG       |
107 | 78 | ad2antrr 732 |
. . . . . . . . . . 11
     
       ⟂G    
   midG      ⟂G         
  |
108 | 5, 7, 19, 95, 96, 97, 104 | tgelrnln 24675 |
. . . . . . . . . . 11
     
       ⟂G    
   midG      ⟂G         
      |
109 | 104 | neneqd 2629 |
. . . . . . . . . . . 12
     
       ⟂G    
   midG      ⟂G         
  |
110 | | simprr 766 |
. . . . . . . . . . . . . 14
     
       ⟂G    
   midG      ⟂G         
  ⟂G          |
111 | 110 | orcomd 390 |
. . . . . . . . . . . . 13
     
       ⟂G    
   midG      ⟂G         

 ⟂G          |
112 | 111 | ord 379 |
. . . . . . . . . . . 12
     
       ⟂G    
   midG      ⟂G         

 ⟂G          |
113 | 109, 112 | mpd 15 |
. . . . . . . . . . 11
     
       ⟂G    
   midG      ⟂G         
 ⟂G         |
114 | 5, 6, 7, 19, 95, 107, 108, 113 | perpcom 24758 |
. . . . . . . . . 10
     
       ⟂G    
   midG      ⟂G         
     ⟂G     |
115 | 106, 114 | eqbrtrrd 4425 |
. . . . . . . . 9
     
       ⟂G    
   midG      ⟂G         
     midG      ⟂G     |
116 | 86, 87, 92, 93, 94, 115 | rmoi2 3362 |
. . . . . . . 8
     
       ⟂G    
   midG      ⟂G         
  midG      |
117 | 116 | eqcomd 2457 |
. . . . . . 7
     
       ⟂G    
   midG      ⟂G         
  midG      |
118 | 80 | ad2antrr 732 |
. . . . . . . 8
     
       ⟂G    
   midG      ⟂G         
  |
119 | 5, 6, 7, 95, 98, 96, 97, 14, 118 | ismidb 24820 |
. . . . . . 7
     
       ⟂G    
   midG      ⟂G         
   pInvG          midG       |
120 | 117, 119 | mpbird 236 |
. . . . . 6
     
       ⟂G    
   midG      ⟂G         
  pInvG          |
121 | | simpr 463 |
. . . . . . . . 9
     
       ⟂G    
  pInvG        
  pInvG          |
122 | 76 | ad2antrr 732 |
. . . . . . . . . 10
     
       ⟂G    
  pInvG        
TarskiG |
123 | 10 | ad5antr 740 |
. . . . . . . . . 10
     
       ⟂G    
  pInvG        
DimTarskiG≥  |
124 | 83 | ad2antrr 732 |
. . . . . . . . . 10
     
       ⟂G    
  pInvG        
  |
125 | | simplr 762 |
. . . . . . . . . 10
     
       ⟂G    
  pInvG        
  |
126 | 80 | ad2antrr 732 |
. . . . . . . . . 10
     
       ⟂G    
  pInvG        
  |
127 | 5, 6, 7, 122, 123, 124, 125, 14, 126 | ismidb 24820 |
. . . . . . . . 9
     
       ⟂G    
  pInvG        
   pInvG          midG       |
128 | 121, 127 | mpbid 214 |
. . . . . . . 8
     
       ⟂G    
  pInvG        
  midG      |
129 | 79 | ad2antrr 732 |
. . . . . . . 8
     
       ⟂G    
  pInvG        
  |
130 | 128, 129 | eqeltrd 2529 |
. . . . . . 7
     
       ⟂G    
  pInvG        
  midG      |
131 | 122 | adantr 467 |
. . . . . . . . . . . 12
      


     ⟂G    
  pInvG        
 TarskiG |
132 | | simp-4r 777 |
. . . . . . . . . . . . 13
      


     ⟂G    
  pInvG        
      ⟂G     |
133 | 19, 131, 132 | perpln1 24755 |
. . . . . . . . . . . 12
      


     ⟂G    
  pInvG        
       |
134 | 78 | ad3antrrr 736 |
. . . . . . . . . . . 12
      


     ⟂G    
  pInvG        
   |
135 | 5, 6, 7, 19, 131, 133, 134, 132 | perpcom 24758 |
. . . . . . . . . . 11
      


     ⟂G    
  pInvG        
  ⟂G         |
136 | 124 | adantr 467 |
. . . . . . . . . . . 12
      


     ⟂G    
  pInvG        
   |
137 | 126 | adantr 467 |
. . . . . . . . . . . 12
      


     ⟂G    
  pInvG        
   |
138 | 5, 7, 19, 131, 136, 137, 133 | tglnne 24673 |
. . . . . . . . . . . 12
      


     ⟂G    
  pInvG        
   |
139 | | simpllr 769 |
. . . . . . . . . . . 12
      


     ⟂G    
  pInvG        
   |
140 | | simpr 463 |
. . . . . . . . . . . . 13
      


     ⟂G    
  pInvG        
   |
141 | 140 | necomd 2679 |
. . . . . . . . . . . 12
      


     ⟂G    
  pInvG        
   |
142 | 5, 6, 7, 19, 14, 131, 137, 81, 136 | mirbtwn 24703 |
. . . . . . . . . . . . . . 15
      


     ⟂G    
  pInvG        
    pInvG             |
143 | | simplr 762 |
. . . . . . . . . . . . . . . 16
      


     ⟂G    
  pInvG        
   pInvG          |
144 | 143 | oveq1d 6305 |
. . . . . . . . . . . . . . 15
      


     ⟂G    
  pInvG        
        pInvG             |
145 | 142, 144 | eleqtrrd 2532 |
. . . . . . . . . . . . . 14
      


     ⟂G    
  pInvG        
       |
146 | 5, 7, 19, 131, 139, 136, 137, 141, 145 | btwnlng1 24664 |
. . . . . . . . . . . . 13
      


     ⟂G    
  pInvG        
       |
147 | 5, 7, 19, 131, 136, 137, 139, 138, 146, 141 | lnrot1 24668 |
. . . . . . . . . . . 12
      


     ⟂G    
  pInvG        
       |
148 | 5, 7, 19, 131, 136, 137, 138, 139, 141, 147 | tglineelsb2 24677 |
. . . . . . . . . . 11
      


     ⟂G    
  pInvG        
           |
149 | 135, 148 | breqtrd 4427 |
. . . . . . . . . 10
      


     ⟂G    
  pInvG        
  ⟂G         |
150 | 149 | ex 436 |
. . . . . . . . 9
     
       ⟂G    
  pInvG        

 ⟂G          |
151 | 150 | necon1bd 2642 |
. . . . . . . 8
     
       ⟂G    
  pInvG        
  ⟂G      
   |
152 | 151 | orrd 380 |
. . . . . . 7
     
       ⟂G    
  pInvG        
  ⟂G          |
153 | 130, 152 | jca 535 |
. . . . . 6
     
       ⟂G    
  pInvG        
   midG      ⟂G           |
154 | 120, 153 | impbida 843 |
. . . . 5
     
      ⟂G    
    midG      ⟂G        
  pInvG           |
155 | 154 | ralrimiva 2802 |
. . . 4
   

      ⟂G         midG      ⟂G           pInvG           |
156 | | reu6i 3229 |
. . . 4
    pInvG       

    midG      ⟂G        
  pInvG          
   midG      ⟂G           |
157 | 84, 155, 156 | syl2anc 667 |
. . 3
   

      ⟂G        midG      ⟂G           |
158 | 5, 6, 7, 19, 75, 77, 82, 88 | footex 24763 |
. . 3
 
 
     ⟂G     |
159 | 157, 158 | r19.29a 2932 |
. 2
 
 
   midG      ⟂G           |
160 | 74, 159 | pm2.61dan 800 |
1
     midG      ⟂G           |