Step | Hyp | Ref
| Expression |
1 | | krippen.1 |
. . . 4
       |
2 | 1 | adantr 472 |
. . 3
 
       |
3 | | mirval.p |
. . . . . . 7
     |
4 | | mirval.d |
. . . . . . 7
     |
5 | | mirval.i |
. . . . . . 7
Itv   |
6 | | mirval.g |
. . . . . . . 8

TarskiG |
7 | 6 | adantr 472 |
. . . . . . 7
 
 TarskiG |
8 | | krippen.c |
. . . . . . . 8
   |
9 | 8 | adantr 472 |
. . . . . . 7
 
   |
10 | | krippen.a |
. . . . . . . 8
   |
11 | 10 | adantr 472 |
. . . . . . 7
 
   |
12 | | krippen.b |
. . . . . . . 8
   |
13 | 12 | adantr 472 |
. . . . . . 7
 
   |
14 | | krippen.3 |
. . . . . . . 8
       |
15 | 14 | adantr 472 |
. . . . . . 7
 
       |
16 | | krippen.l |
. . . . . . . 8
≤G   |
17 | | krippen.7 |
. . . . . . . . . 10
       |
18 | 17 | adantr 472 |
. . . . . . . . 9
 
   
   |
19 | | simpr 468 |
. . . . . . . . . 10
 
   |
20 | 19 | oveq2d 6324 |
. . . . . . . . 9
 
       |
21 | 18, 20 | breqtrd 4420 |
. . . . . . . 8
 
   
   |
22 | 3, 4, 5, 16, 7, 9,
11, 9, 13, 21 | legeq 24717 |
. . . . . . 7
 
   |
23 | 3, 4, 5, 7, 9, 11,
9, 13, 15, 22 | tgcgreq 24605 |
. . . . . 6
 
   |
24 | | krippen.5 |
. . . . . . 7
       |
25 | 24 | adantr 472 |
. . . . . 6
 
       |
26 | 23, 22, 25 | 3eqtr3rd 2514 |
. . . . 5
 
       |
27 | | mirval.l |
. . . . . 6
LineG   |
28 | | mirval.s |
. . . . . 6
pInvG   |
29 | | krippen.x |
. . . . . . 7
   |
30 | 29 | adantr 472 |
. . . . . 6
 
   |
31 | | krippen.m |
. . . . . 6
     |
32 | 3, 4, 5, 27, 28, 7, 30, 31, 11 | mirinv 24790 |
. . . . 5
 
     
   |
33 | 26, 32 | mpbid 215 |
. . . 4
 
   |
34 | | krippen.f |
. . . . . . . 8
   |
35 | 34 | adantr 472 |
. . . . . . 7
 
   |
36 | | krippen.4 |
. . . . . . . . 9
       |
37 | 36 | adantr 472 |
. . . . . . . 8
 
       |
38 | 37, 20 | eqtr3d 2507 |
. . . . . . 7
 
       |
39 | 3, 4, 5, 7, 9, 35,
9, 38 | axtgcgrid 24590 |
. . . . . 6
 
   |
40 | | krippen.6 |
. . . . . . 7
       |
41 | 40 | adantr 472 |
. . . . . 6
 
       |
42 | 19, 39, 41 | 3eqtrrd 2510 |
. . . . 5
 
       |
43 | | krippen.y |
. . . . . . 7
   |
44 | 43 | adantr 472 |
. . . . . 6
 
   |
45 | | krippen.n |
. . . . . 6
     |
46 | | krippen.e |
. . . . . . 7
   |
47 | 46 | adantr 472 |
. . . . . 6
 
   |
48 | 3, 4, 5, 27, 28, 7, 44, 45, 47 | mirinv 24790 |
. . . . 5
 
     
   |
49 | 42, 48 | mpbid 215 |
. . . 4
 
   |
50 | 33, 49 | oveq12d 6326 |
. . 3
 
           |
51 | 2, 50 | eleqtrrd 2552 |
. 2
 
       |
52 | 6 | adantr 472 |
. . . . . 6
 

TarskiG |
53 | 52 | ad2antrr 740 |
. . . . 5
    
                    TarskiG |
54 | 8 | adantr 472 |
. . . . . . . 8
 

  |
55 | | eqid 2471 |
. . . . . . . 8
         |
56 | 3, 4, 5, 27, 28, 52, 54, 55 | mirf 24784 |
. . . . . . 7
 

          |
57 | 43 | adantr 472 |
. . . . . . 7
 

  |
58 | 56, 57 | ffvelrnd 6038 |
. . . . . 6
 

          |
59 | 58 | ad2antrr 740 |
. . . . 5
    
                              |
60 | | simplr 770 |
. . . . 5
    
                      |
61 | 54 | ad2antrr 740 |
. . . . 5
    
                      |
62 | 57 | ad2antrr 740 |
. . . . 5
    
                      |
63 | | simprl 772 |
. . . . 5
    
                                  |
64 | 3, 4, 5, 27, 28, 6, 8, 55, 43 | mirbtwn 24782 |
. . . . . 6
               |
65 | 64 | ad3antrrr 744 |
. . . . 5
    
                                  |
66 | 3, 4, 5, 53, 59, 60, 61, 62, 63, 65 | tgbtwnexch3 24617 |
. . . 4
    
                          |
67 | 29 | ad3antrrr 744 |
. . . . . 6
    
                      |
68 | 10 | adantr 472 |
. . . . . . 7
 

  |
69 | 68 | ad2antrr 740 |
. . . . . 6
    
                      |
70 | 12 | adantr 472 |
. . . . . . 7
 

  |
71 | 70 | ad2antrr 740 |
. . . . . 6
    
                      |
72 | | eqid 2471 |
. . . . . . . 8
         |
73 | 46 | adantr 472 |
. . . . . . . . . . . . . . 15
 

  |
74 | 56, 73 | ffvelrnd 6038 |
. . . . . . . . . . . . . 14
 

          |
75 | 34 | adantr 472 |
. . . . . . . . . . . . . . 15
 

  |
76 | 56, 75 | ffvelrnd 6038 |
. . . . . . . . . . . . . 14
 

          |
77 | 6 | ad2antrr 740 |
. . . . . . . . . . . . . . . . . 18
     TarskiG |
78 | 10 | ad2antrr 740 |
. . . . . . . . . . . . . . . . . 18
       |
79 | 74 | adantr 472 |
. . . . . . . . . . . . . . . . . 18
               |
80 | 3, 4, 5, 77, 78, 79 | tgbtwntriv1 24614 |
. . . . . . . . . . . . . . . . 17
                   |
81 | | simpr 468 |
. . . . . . . . . . . . . . . . . 18
       |
82 | 81 | oveq1d 6323 |
. . . . . . . . . . . . . . . . 17
                               |
83 | 80, 82 | eleqtrd 2551 |
. . . . . . . . . . . . . . . 16
                   |
84 | 6 | ad2antrr 740 |
. . . . . . . . . . . . . . . . 17
     TarskiG |
85 | 10 | ad2antrr 740 |
. . . . . . . . . . . . . . . . 17
       |
86 | 74 | adantr 472 |
. . . . . . . . . . . . . . . . 17
               |
87 | 8 | ad2antrr 740 |
. . . . . . . . . . . . . . . . 17
       |
88 | 46 | ad2antrr 740 |
. . . . . . . . . . . . . . . . . 18
       |
89 | | simplr 770 |
. . . . . . . . . . . . . . . . . 18
       |
90 | 3, 4, 5, 6, 10, 8,
46, 1 | tgbtwncom 24611 |
. . . . . . . . . . . . . . . . . . 19
       |
91 | 90 | ad2antrr 740 |
. . . . . . . . . . . . . . . . . 18
           |
92 | 3, 4, 5, 27, 28, 84, 87, 55, 88 | mirbtwn 24782 |
. . . . . . . . . . . . . . . . . . 19
                   |
93 | 3, 4, 5, 84, 86, 87, 88, 92 | tgbtwncom 24611 |
. . . . . . . . . . . . . . . . . 18
                   |
94 | 3, 5, 84, 88, 87, 85, 86, 89, 91, 93 | tgbtwnconn2 24700 |
. . . . . . . . . . . . . . . . 17
     
                           |
95 | 17 | adantr 472 |
. . . . . . . . . . . . . . . . . . 19
 

      |
96 | 3, 4, 5, 27, 28, 52, 54, 55, 73 | mircgr 24781 |
. . . . . . . . . . . . . . . . . . 19
 

              |
97 | 95, 96 | breqtrrd 4422 |
. . . . . . . . . . . . . . . . . 18
 

              |
98 | 97 | adantr 472 |
. . . . . . . . . . . . . . . . 17
       
           |
99 | 3, 4, 5, 16, 84, 85, 86, 87, 85, 94, 98 | legbtwn 24718 |
. . . . . . . . . . . . . . . 16
                   |
100 | 83, 99 | pm2.61dane 2730 |
. . . . . . . . . . . . . . 15
 

              |
101 | 3, 4, 5, 52, 54, 68, 74, 100 | tgbtwncom 24611 |
. . . . . . . . . . . . . 14
 

              |
102 | 6 | ad2antrr 740 |
. . . . . . . . . . . . . . . . . 18
     TarskiG |
103 | 12 | ad2antrr 740 |
. . . . . . . . . . . . . . . . . 18
       |
104 | 76 | adantr 472 |
. . . . . . . . . . . . . . . . . 18
               |
105 | 3, 4, 5, 102, 103, 104 | tgbtwntriv1 24614 |
. . . . . . . . . . . . . . . . 17
                   |
106 | | simpr 468 |
. . . . . . . . . . . . . . . . . 18
       |
107 | 106 | oveq1d 6323 |
. . . . . . . . . . . . . . . . 17
                               |
108 | 105, 107 | eleqtrd 2551 |
. . . . . . . . . . . . . . . 16
                   |
109 | 6 | ad2antrr 740 |
. . . . . . . . . . . . . . . . 17
     TarskiG |
110 | 12 | ad2antrr 740 |
. . . . . . . . . . . . . . . . 17
       |
111 | 76 | adantr 472 |
. . . . . . . . . . . . . . . . 17
               |
112 | 8 | ad2antrr 740 |
. . . . . . . . . . . . . . . . 17
       |
113 | 34 | ad2antrr 740 |
. . . . . . . . . . . . . . . . . 18
       |
114 | 6 | adantr 472 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 
 TarskiG |
115 | 8 | adantr 472 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 
   |
116 | 46 | adantr 472 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 
   |
117 | 36 | adantr 472 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
 
       |
118 | | simpr 468 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
 
   |
119 | 118 | oveq2d 6324 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
 
       |
120 | 117, 119 | eqtrd 2505 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 
       |
121 | 3, 4, 5, 114, 115, 116, 115, 120 | axtgcgrid 24590 |
. . . . . . . . . . . . . . . . . . . . . . 23
 
   |
122 | 121 | eqcomd 2477 |
. . . . . . . . . . . . . . . . . . . . . 22
 
   |
123 | 122 | adantlr 729 |
. . . . . . . . . . . . . . . . . . . . 21
       |
124 | | simplr 770 |
. . . . . . . . . . . . . . . . . . . . . 22
       |
125 | 124 | neneqd 2648 |
. . . . . . . . . . . . . . . . . . . . 21
    
  |
126 | 123, 125 | pm2.65da 586 |
. . . . . . . . . . . . . . . . . . . 20
 

  |
127 | 126 | neqned 2650 |
. . . . . . . . . . . . . . . . . . 19
 

  |
128 | 127 | adantr 472 |
. . . . . . . . . . . . . . . . . 18
       |
129 | | krippen.2 |
. . . . . . . . . . . . . . . . . . . 20
       |
130 | 3, 4, 5, 6, 12, 8,
34, 129 | tgbtwncom 24611 |
. . . . . . . . . . . . . . . . . . 19
       |
131 | 130 | ad2antrr 740 |
. . . . . . . . . . . . . . . . . 18
           |
132 | 3, 4, 5, 27, 28, 109, 112, 55, 113 | mirbtwn 24782 |
. . . . . . . . . . . . . . . . . . 19
                   |
133 | 3, 4, 5, 109, 111, 112, 113, 132 | tgbtwncom 24611 |
. . . . . . . . . . . . . . . . . 18
                   |
134 | 3, 5, 109, 113, 112, 110, 111, 128, 131, 133 | tgbtwnconn2 24700 |
. . . . . . . . . . . . . . . . 17
     
                           |
135 | 17, 14, 36 | 3brtr3d 4425 |
. . . . . . . . . . . . . . . . . . . 20
       |
136 | 135 | adantr 472 |
. . . . . . . . . . . . . . . . . . 19
 

      |
137 | 3, 4, 5, 27, 28, 52, 54, 55, 75 | mircgr 24781 |
. . . . . . . . . . . . . . . . . . 19
 

              |
138 | 136, 137 | breqtrrd 4422 |
. . . . . . . . . . . . . . . . . 18
 

              |
139 | 138 | adantr 472 |
. . . . . . . . . . . . . . . . 17
       
           |
140 | 3, 4, 5, 16, 109, 110, 111, 112, 110, 134, 139 | legbtwn 24718 |
. . . . . . . . . . . . . . . 16
                   |
141 | 108, 140 | pm2.61dane 2730 |
. . . . . . . . . . . . . . 15
 

              |
142 | 3, 4, 5, 52, 54, 70, 76, 141 | tgbtwncom 24611 |
. . . . . . . . . . . . . 14
 

              |
143 | 36 | adantr 472 |
. . . . . . . . . . . . . . . 16
 

      |
144 | 143, 96, 137 | 3eqtr4d 2515 |
. . . . . . . . . . . . . . 15
 

                      |
145 | 3, 4, 5, 52, 54, 74, 54, 76, 144 | tgcgrcomlr 24603 |
. . . . . . . . . . . . . 14
 

                  
   |
146 | 14 | adantr 472 |
. . . . . . . . . . . . . . 15
 

      |
147 | 3, 4, 5, 52, 54, 68, 54, 70, 146 | tgcgrcomlr 24603 |
. . . . . . . . . . . . . 14
 

      |
148 | | eqid 2471 |
. . . . . . . . . . . . . . . . 17
                         |
149 | 3, 4, 5, 27, 28, 52, 58, 148, 74 | mircgr 24781 |
. . . . . . . . . . . . . . . 16
 

                                          
           |
150 | | eqid 2471 |
. . . . . . . . . . . . . . . . . 18
                 |
151 | | eqid 2471 |
. . . . . . . . . . . . . . . . . 18
                 |
152 | | eqid 2471 |
. . . . . . . . . . . . . . . . . 18
                 |
153 | 40 | adantr 472 |
. . . . . . . . . . . . . . . . . . 19
 

      |
154 | 45 | fveq1i 5880 |
. . . . . . . . . . . . . . . . . . 19
             |
155 | 153, 154 | syl6req 2522 |
. . . . . . . . . . . . . . . . . 18
 

          |
156 | 3, 4, 5, 27, 28, 52, 55, 150, 151, 152, 54, 57, 73, 75, 155 | mirauto 24808 |
. . . . . . . . . . . . . . . . 17
 

                                  |
157 | 156 | oveq2d 6324 |
. . . . . . . . . . . . . . . 16
 

                                          
           |
158 | 149, 157 | eqtr3d 2507 |
. . . . . . . . . . . . . . 15
 

                          
           |
159 | 3, 4, 5, 52, 58, 74, 58, 76, 158 | tgcgrcomlr 24603 |
. . . . . . . . . . . . . 14
 

                          
           |
160 | | eqidd 2472 |
. . . . . . . . . . . . . 14
 

                      |
161 | 3, 4, 5, 52, 74, 68, 54, 58, 76, 70, 54, 58, 101, 142, 145, 147, 159, 160 | tgifscgr 24632 |
. . . . . . . . . . . . 13
 

                      |
162 | 3, 4, 5, 52, 68, 58, 70, 58, 161 | tgcgrcomlr 24603 |
. . . . . . . . . . . 12
 

                  
   |
163 | 162 | ad3antrrr 744 |
. . . . . . . . . . 11
      
                                              
   |
164 | 53 | adantr 472 |
. . . . . . . . . . . . 13
      
                            TarskiG |
165 | 59 | adantr 472 |
. . . . . . . . . . . . 13
      
                                      |
166 | 60 | adantr 472 |
. . . . . . . . . . . . 13
      
                              |
167 | 63 | adantr 472 |
. . . . . . . . . . . . . 14
      
                                          |
168 | | simpr 468 |
. . . . . . . . . . . . . . 15
      
                                      |
169 | 168 | oveq2d 6324 |
. . . . . . . . . . . . . 14
      
                                                              |
170 | 167, 169 | eleqtrrd 2552 |
. . . . . . . . . . . . 13
      
                                                  |
171 | 3, 4, 5, 164, 165, 166, 170 | axtgbtwnid 24593 |
. . . . . . . . . . . 12
      
                                      |
172 | 171 | oveq1d 6323 |
. . . . . . . . . . 11
      
                                          |
173 | 171 | oveq1d 6323 |
. . . . . . . . . . 11
      
                                          |
174 | 163, 172,
173 | 3eqtr3d 2513 |
. . . . . . . . . 10
      
                                  |
175 | 52 | ad3antrrr 744 |
. . . . . . . . . . 11
      
                            TarskiG |
176 | 58 | ad3antrrr 744 |
. . . . . . . . . . 11
      
                                      |
177 | 54 | ad3antrrr 744 |
. . . . . . . . . . 11
      
                              |
178 | 60 | adantr 472 |
. . . . . . . . . . 11
      
                              |
179 | | eqid 2471 |
. . . . . . . . . . 11
cgrG  cgrG   |
180 | 68 | ad3antrrr 744 |
. . . . . . . . . . 11
      
                              |
181 | 70 | ad3antrrr 744 |
. . . . . . . . . . 11
      
                              |
182 | | simpr 468 |
. . . . . . . . . . 11
      
                                      |
183 | 59 | adantr 472 |
. . . . . . . . . . . 12
      
                                      |
184 | 63 | adantr 472 |
. . . . . . . . . . . 12
      
                                          |
185 | 3, 27, 5, 175, 183, 178, 177, 184 | btwncolg3 24681 |
. . . . . . . . . . 11
      
                                                    |
186 | 162 | ad3antrrr 744 |
. . . . . . . . . . 11
      
                                              
   |
187 | 146 | ad3antrrr 744 |
. . . . . . . . . . 11
      
                                  |
188 | 3, 27, 5, 175, 176, 177, 178, 179, 180, 181, 4, 182, 185, 186, 187 | lncgr 24693 |
. . . . . . . . . 10
      
                                  |
189 | 174, 188 | pm2.61dane 2730 |
. . . . . . . . 9
    
                    
     |
190 | 189 | eqcomd 2477 |
. . . . . . . 8
    
                    
     |
191 | | simprr 774 |
. . . . . . . . 9
    
                          |
192 | 3, 4, 5, 53, 69, 60, 71, 191 | tgbtwncom 24611 |
. . . . . . . 8
    
                          |
193 | 3, 4, 5, 27, 28, 53, 60, 72, 69, 71, 190, 192 | ismir 24783 |
. . . . . . 7
    
                              |
194 | 193 | eqcomd 2477 |
. . . . . 6
    
                              |
195 | 24 | ad3antrrr 744 |
. . . . . . 7
    
                          |
196 | 31 | fveq1i 5880 |
. . . . . . 7
             |
197 | 195, 196 | syl6req 2522 |
. . . . . 6
    
                              |
198 | 3, 4, 5, 27, 28, 53, 60, 67, 69, 71, 194, 197 | miduniq 24809 |
. . . . 5
    
                      |
199 | 198 | oveq1d 6323 |
. . . 4
    
                              |
200 | 66, 199 | eleqtrd 2551 |
. . 3
    
                          |
201 | 3, 4, 5, 27, 28, 52, 57, 45, 73 | mirbtwn 24782 |
. . . . . . 7
 

          |
202 | 153 | oveq1d 6323 |
. . . . . . 7
 

              |
203 | 201, 202 | eleqtrrd 2552 |
. . . . . 6
 

      |
204 | 3, 4, 5, 52, 75, 57, 73, 203 | tgbtwncom 24611 |
. . . . 5
 

      |
205 | 3, 4, 5, 27, 28, 52, 54, 55, 73, 57, 75, 204 | mirbtwni 24795 |
. . . 4
 

                              |
206 | 3, 4, 5, 52, 74, 68, 54, 76, 70, 58, 101, 142, 205 | tgtrisegint 24622 |
. . 3
 


                    |
207 | 200, 206 | r19.29a 2918 |
. 2
 

      |
208 | 51, 207 | pm2.61dane 2730 |
1
       |