Step | Hyp | Ref
| Expression |
1 | | midexlem.c |
. . . . 5
   |
2 | | midexlem.m |
. . . . . . . . 9
     |
3 | | fveq2 5865 |
. . . . . . . . 9
           |
4 | 2, 3 | syl5eq 2497 |
. . . . . . . 8
       |
5 | 4 | fveq1d 5867 |
. . . . . . 7
               |
6 | 5 | eqeq2d 2461 |
. . . . . 6
 
   
           |
7 | 6 | rspcev 3150 |
. . . . 5
 
         
      |
8 | 1, 7 | sylan 474 |
. . . 4
 
         
      |
9 | 8 | adantlr 721 |
. . 3
   
     
         
      |
10 | | midexlem.a |
. . . . . 6
   |
11 | 10 | adantr 467 |
. . . . 5
 
   |
12 | | mirval.p |
. . . . . . . 8
     |
13 | | mirval.d |
. . . . . . . 8
     |
14 | | mirval.i |
. . . . . . . 8
Itv   |
15 | | mirval.l |
. . . . . . . 8
LineG   |
16 | | mirval.s |
. . . . . . . 8
pInvG   |
17 | | mirval.g |
. . . . . . . 8

TarskiG |
18 | | eqid 2451 |
. . . . . . . 8
         |
19 | 12, 13, 14, 15, 16, 17, 10, 18 | mircinv 24713 |
. . . . . . 7
           |
20 | 19 | adantr 467 |
. . . . . 6
 
           |
21 | | simpr 463 |
. . . . . 6
 
   |
22 | 20, 21 | eqtr2d 2486 |
. . . . 5
 
           |
23 | | fveq2 5865 |
. . . . . . . . 9
           |
24 | 2, 23 | syl5eq 2497 |
. . . . . . . 8
       |
25 | 24 | fveq1d 5867 |
. . . . . . 7
               |
26 | 25 | eqeq2d 2461 |
. . . . . 6
 
   
           |
27 | 26 | rspcev 3150 |
. . . . 5
 
         
      |
28 | 11, 22, 27 | syl2anc 667 |
. . . 4
 
 
      |
29 | 28 | adantlr 721 |
. . 3
   
     
 
      |
30 | 17 | adantr 467 |
. . . 4
 
      
TarskiG |
31 | | eqid 2451 |
. . . 4
         |
32 | 10 | adantr 467 |
. . . 4
 
      
  |
33 | | midexlem.b |
. . . . 5
   |
34 | 33 | adantr 467 |
. . . 4
 
      
  |
35 | 1 | adantr 467 |
. . . 4
 
      
  |
36 | | simpr 463 |
. . . 4
 
               |
37 | | midexlem.1 |
. . . . 5
       |
38 | 37 | adantr 467 |
. . . 4
 
             |
39 | 12, 13, 14, 15, 16, 30, 31, 32, 34, 35, 36, 38 | colmid 24733 |
. . 3
 
               
   |
40 | 9, 29, 39 | mpjaodan 795 |
. 2
 
       
      |
41 | 17 | adantr 467 |
. . . . . . . . . . 11
 

     
TarskiG |
42 | 41 | ad2antrr 732 |
. . . . . . . . . 10
            
      TarskiG |
43 | 42 | ad2antrr 732 |
. . . . . . . . 9
     

     
         
    
     TarskiG |
44 | 43 | ad2antrr 732 |
. . . . . . . 8
                
      
          
            TarskiG |
45 | 44 | adantr 467 |
. . . . . . 7
               
         
    
     
           
           
TarskiG |
46 | | simprl 764 |
. . . . . . 7
               
         
    
     
           
           
  |
47 | 10 | adantr 467 |
. . . . . . . . . . 11
 

     
  |
48 | 47 | ad2antrr 732 |
. . . . . . . . . 10
            
        |
49 | 48 | ad2antrr 732 |
. . . . . . . . 9
     

     
         
    
       |
50 | 49 | ad2antrr 732 |
. . . . . . . 8
                
      
          
              |
51 | 50 | adantr 467 |
. . . . . . 7
               
         
    
     
           
           
  |
52 | 33 | ad3antrrr 736 |
. . . . . . . . . 10
            
        |
53 | 52 | ad2antrr 732 |
. . . . . . . . 9
     

     
         
    
       |
54 | 53 | ad2antrr 732 |
. . . . . . . 8
                
      
          
              |
55 | 54 | adantr 467 |
. . . . . . 7
               
         
    
     
           
           
  |
56 | 45 | ad2antrr 732 |
. . . . . . . . 9
           
       
      
          
             
          
             cgrG           TarskiG |
57 | | simpllr 769 |
. . . . . . . . . 10
               
         
    
     
           
              |
58 | 57 | ad2antrr 732 |
. . . . . . . . 9
           
       
      
          
             
          
             cgrG             |
59 | 1 | adantr 467 |
. . . . . . . . . . . . . 14
 

     
  |
60 | 59 | ad2antrr 732 |
. . . . . . . . . . . . 13
            
        |
61 | 60 | ad2antrr 732 |
. . . . . . . . . . . 12
     

     
         
    
       |
62 | 61 | ad2antrr 732 |
. . . . . . . . . . 11
                
      
          
              |
63 | 62 | adantr 467 |
. . . . . . . . . 10
               
         
    
     
           
           
  |
64 | 63 | ad2antrr 732 |
. . . . . . . . 9
           
       
      
          
             
          
             cgrG             |
65 | 46 | ad2antrr 732 |
. . . . . . . . 9
           
       
      
          
             
          
             cgrG             |
66 | | eqid 2451 |
. . . . . . . . 9
cgrG  cgrG   |
67 | 55 | ad2antrr 732 |
. . . . . . . . 9
           
       
      
          
             
          
             cgrG             |
68 | 51 | ad2antrr 732 |
. . . . . . . . 9
           
       
      
          
             
          
             cgrG             |
69 | | simpr 463 |
. . . . . . . . . . 11
                    
      
          
             
          
             cgrG              |
70 | 33 | adantr 467 |
. . . . . . . . . . . . . . . 16
 

     
  |
71 | | simpr 463 |
. . . . . . . . . . . . . . . 16
 

              |
72 | 12, 14, 15, 41, 59, 47, 70, 71 | ncolne1 24670 |
. . . . . . . . . . . . . . 15
 

        |
73 | 72 | ad7antr 744 |
. . . . . . . . . . . . . 14
               
         
    
     
           
              |
74 | 73 | ad2antrr 732 |
. . . . . . . . . . . . 13
           
       
      
          
             
          
             cgrG             |
75 | 74 | adantr 467 |
. . . . . . . . . . . 12
                    
      
          
             
          
             cgrG              |
76 | 75 | necomd 2679 |
. . . . . . . . . . 11
                    
      
          
             
          
             cgrG              |
77 | 69, 76 | eqnetrd 2691 |
. . . . . . . . . 10
                    
      
          
             
          
             cgrG              |
78 | 56 | adantr 467 |
. . . . . . . . . . 11
                    
      
          
             
          
             cgrG            TarskiG |
79 | 58 | adantr 467 |
. . . . . . . . . . 11
                    
      
          
             
          
             cgrG              |
80 | 68 | adantr 467 |
. . . . . . . . . . 11
                    
      
          
             
          
             cgrG              |
81 | 64 | adantr 467 |
. . . . . . . . . . 11
                    
      
          
             
          
             cgrG              |
82 | | simplr 762 |
. . . . . . . . . . . . . . 15
     

     
         
    
       |
83 | 82 | ad3antrrr 736 |
. . . . . . . . . . . . . 14
               
         
    
     
           
              |
84 | 83 | ad2antrr 732 |
. . . . . . . . . . . . 13
           
       
      
          
             
          
             cgrG             |
85 | 84 | adantr 467 |
. . . . . . . . . . . 12
                    
      
          
             
          
             cgrG              |
86 | 71 | ad9antr 748 |
. . . . . . . . . . . . . . . 16
           
       
      
          
             
          
             cgrG           
       |
87 | 12, 15, 14, 56, 68, 67, 64, 86 | ncolrot2 24608 |
. . . . . . . . . . . . . . 15
           
       
      
          
             
          
             cgrG           
       |
88 | 17 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . 21
 
      
TarskiG |
89 | 33 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . 21
 
      
  |
90 | 10 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . 21
 
      
  |
91 | 1 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . 21
 
      
  |
92 | | simpr 463 |
. . . . . . . . . . . . . . . . . . . . 21
 
               |
93 | 12, 15, 14, 88, 89, 90, 91, 92 | colcom 24603 |
. . . . . . . . . . . . . . . . . . . 20
 
               |
94 | 93 | stoic1a 1655 |
. . . . . . . . . . . . . . . . . . 19
 

              |
95 | 94 | ad9antr 748 |
. . . . . . . . . . . . . . . . . 18
           
       
      
          
             
          
             cgrG           
       |
96 | 12, 14, 15, 56, 64, 67, 68, 95 | ncolne1 24670 |
. . . . . . . . . . . . . . . . 17
           
       
      
          
             
          
             cgrG             |
97 | 96 | necomd 2679 |
. . . . . . . . . . . . . . . 16
           
       
      
          
             
          
             cgrG             |
98 | | simprl 764 |
. . . . . . . . . . . . . . . . . . 19
     

     
         
    
           |
99 | 98 | ad3antrrr 736 |
. . . . . . . . . . . . . . . . . 18
               
         
    
     
           
           
      |
100 | 99 | ad2antrr 732 |
. . . . . . . . . . . . . . . . 17
           
       
      
          
             
          
             cgrG                 |
101 | 12, 14, 15, 56, 64, 67, 84, 96, 100 | btwnlng3 24666 |
. . . . . . . . . . . . . . . 16
           
       
      
          
             
          
             cgrG                 |
102 | 12, 14, 15, 56, 67, 64, 84, 97, 101 | lncom 24667 |
. . . . . . . . . . . . . . 15
           
       
      
          
             
          
             cgrG                 |
103 | 56 | adantr 467 |
. . . . . . . . . . . . . . . . . 18
                    
      
          
             
          
             cgrG            TarskiG |
104 | 64 | adantr 467 |
. . . . . . . . . . . . . . . . . 18
                    
      
          
             
          
             cgrG              |
105 | 67 | adantr 467 |
. . . . . . . . . . . . . . . . . 18
                    
      
          
             
          
             cgrG              |
106 | 100 | adantr 467 |
. . . . . . . . . . . . . . . . . . 19
                    
      
          
             
          
             cgrG                  |
107 | | simpr 463 |
. . . . . . . . . . . . . . . . . . . 20
                    
      
          
             
          
             cgrG              |
108 | 107 | oveq2d 6306 |
. . . . . . . . . . . . . . . . . . 19
                    
      
          
             
          
             cgrG                      |
109 | 106, 108 | eleqtrd 2531 |
. . . . . . . . . . . . . . . . . 18
                    
      
          
             
          
             cgrG                  |
110 | 12, 13, 14, 103, 104, 105, 109 | axtgbtwnid 24514 |
. . . . . . . . . . . . . . . . 17
                    
      
          
             
          
             cgrG              |
111 | 96 | adantr 467 |
. . . . . . . . . . . . . . . . . 18
                    
      
          
             
          
             cgrG              |
112 | 111 | neneqd 2629 |
. . . . . . . . . . . . . . . . 17
                    
      
          
             
          
             cgrG           
  |
113 | 110, 112 | pm2.65da 580 |
. . . . . . . . . . . . . . . 16
           
       
      
          
             
          
             cgrG          
  |
114 | 113 | neqned 2631 |
. . . . . . . . . . . . . . 15
           
       
      
          
             
          
             cgrG             |
115 | 12, 14, 15, 56, 67, 64, 68, 84, 87, 102, 114 | ncolncol 24691 |
. . . . . . . . . . . . . 14
           
       
      
          
             
          
             cgrG                   |
116 | 12, 15, 14, 56, 64, 68, 84, 115 | ncolcom 24606 |
. . . . . . . . . . . . 13
           
       
      
          
             
          
             cgrG                   |
117 | 116 | adantr 467 |
. . . . . . . . . . . 12
                    
      
          
             
          
             cgrG                    |
118 | | simp-4r 777 |
. . . . . . . . . . . . . . . . . . . 20
     

     
         
    
       |
119 | 118 | ad2antrr 732 |
. . . . . . . . . . . . . . . . . . 19
                
      
          
              |
120 | 119 | adantr 467 |
. . . . . . . . . . . . . . . . . 18
               
         
    
     
           
           
  |
121 | 120 | ad2antrr 732 |
. . . . . . . . . . . . . . . . 17
           
       
      
          
             
          
             cgrG             |
122 | | simp-4r 777 |
. . . . . . . . . . . . . . . . . . . . 21
               
         
    
     
           
                        |
123 | 122 | simprd 465 |
. . . . . . . . . . . . . . . . . . . 20
               
         
    
     
           
                  |
124 | 123 | eqcomd 2457 |
. . . . . . . . . . . . . . . . . . 19
               
         
    
     
           
                  |
125 | 124 | ad2antrr 732 |
. . . . . . . . . . . . . . . . . 18
           
       
      
          
             
          
             cgrG                 |
126 | 12, 13, 14, 56, 68, 121, 67, 84, 125 | tgcgrcomlr 24524 |
. . . . . . . . . . . . . . . . 17
           
       
      
          
             
          
             cgrG           
     |
127 | | simpllr 769 |
. . . . . . . . . . . . . . . . . . . 20
     

     
         
    
             |
128 | 127 | ad5antr 740 |
. . . . . . . . . . . . . . . . . . 19
           
       
      
          
             
          
             cgrG           
       |
129 | 128 | simprd 465 |
. . . . . . . . . . . . . . . . . 18
           
       
      
          
             
          
             cgrG             |
130 | 129 | necomd 2679 |
. . . . . . . . . . . . . . . . 17
           
       
      
          
             
          
             cgrG             |
131 | 12, 13, 14, 56, 121, 68, 84, 67, 126, 130 | tgcgrneq 24527 |
. . . . . . . . . . . . . . . 16
           
       
      
          
             
          
             cgrG             |
132 | 12, 14, 15, 56, 64, 67, 68, 84, 95, 101, 131 | ncolncol 24691 |
. . . . . . . . . . . . . . 15
           
       
      
          
             
          
             cgrG                   |
133 | 12, 14, 15, 56, 84, 67, 68, 132 | ncolne2 24671 |
. . . . . . . . . . . . . 14
           
       
      
          
             
          
             cgrG             |
134 | 133 | necomd 2679 |
. . . . . . . . . . . . . . 15
           
       
      
          
             
          
             cgrG             |
135 | | simp-4r 777 |
. . . . . . . . . . . . . . . 16
           
       
      
          
             
          
             cgrG               
       |
136 | 135 | simpld 461 |
. . . . . . . . . . . . . . 15
           
       
      
          
             
          
             cgrG                 |
137 | 12, 14, 15, 56, 68, 84, 58, 134, 136 | btwnlng1 24664 |
. . . . . . . . . . . . . 14
           
       
      
          
             
          
             cgrG                 |
138 | 12, 14, 15, 56, 84, 68, 58, 133, 137 | lncom 24667 |
. . . . . . . . . . . . 13
           
       
      
          
             
          
             cgrG                 |
139 | 138 | adantr 467 |
. . . . . . . . . . . 12
                    
      
          
             
          
             cgrG                  |
140 | | simpr 463 |
. . . . . . . . . . . 12
                    
      
          
             
          
             cgrG              |
141 | 12, 14, 15, 78, 85, 80, 81, 79, 117, 139, 140 | ncolncol 24691 |
. . . . . . . . . . 11
                    
      
          
             
          
             cgrG                    |
142 | 12, 14, 15, 78, 79, 80, 81, 141 | ncolne2 24671 |
. . . . . . . . . 10
                    
      
          
             
          
             cgrG              |
143 | 77, 142 | pm2.61dane 2711 |
. . . . . . . . 9
           
       
      
          
             
          
             cgrG             |
144 | | simpllr 769 |
. . . . . . . . . . . 12
           
       
      
          
             
          
             cgrG            
            |
145 | 144 | simprd 465 |
. . . . . . . . . . 11
           
       
      
          
             
          
             cgrG               
       |
146 | 145 | simprd 465 |
. . . . . . . . . 10
           
       
      
          
             
          
             cgrG                 |
147 | 12, 15, 14, 56, 58, 65, 64, 146 | btwncolg3 24602 |
. . . . . . . . 9
           
       
      
          
             
          
             cgrG           
       |
148 | | simplr 762 |
. . . . . . . . . . 11
           
       
      
          
             
          
             cgrG             |
149 | | simplr 762 |
. . . . . . . . . . . . 13
               
         
    
     
           
                        |
150 | 149 | simprd 465 |
. . . . . . . . . . . 12
               
         
    
     
           
                  |
151 | 150 | ad2antrr 732 |
. . . . . . . . . . 11
           
       
      
          
             
          
             cgrG                 |
152 | | simprl 764 |
. . . . . . . . . . 11
           
       
      
          
             
          
             cgrG                 |
153 | 127 | simpld 461 |
. . . . . . . . . . . . . . . 16
     

     
         
    
           |
154 | 153 | ad2antrr 732 |
. . . . . . . . . . . . . . 15
                
      
          
                  |
155 | 154 | adantr 467 |
. . . . . . . . . . . . . 14
               
         
    
     
           
           
      |
156 | 37 | ad8antr 746 |
. . . . . . . . . . . . . 14
               
         
    
     
           
                  |
157 | 156 | eqcomd 2457 |
. . . . . . . . . . . . . 14
               
         
    
     
           
                  |
158 | 12, 13, 14, 45, 51, 55 | axtgcgrrflx 24510 |
. . . . . . . . . . . . . 14
               
         
    
     
           
                  |
159 | 12, 13, 14, 45, 63, 51, 120, 63, 55, 83, 55, 51, 73, 155, 99, 156, 124, 157, 158 | axtg5seg 24513 |
. . . . . . . . . . . . 13
               
         
    
     
           
                  |
160 | 12, 13, 14, 45, 120, 55, 83, 51, 159 | tgcgrcomlr 24524 |
. . . . . . . . . . . 12
               
         
    
     
           
                  |
161 | 160 | ad2antrr 732 |
. . . . . . . . . . 11
           
       
      
          
             
          
             cgrG                 |
162 | | simprr 766 |
. . . . . . . . . . . 12
           
       
      
       |