Step | Hyp | Ref
| Expression |
1 | | poimir.0 |
. . 3
   |
2 | | poimir.i |
. . 3
   ![[,] [,]](_icc.gif)        |
3 | | poimir.r |
. . 3
                 |
4 | | elmapfn 7499 |
. . . . . . . 8
    ![[,] [,]](_icc.gif)             |
5 | 4, 2 | eleq2s 2549 |
. . . . . . 7
       |
6 | 5 | adantl 468 |
. . . . . 6
 
       |
7 | | broucube.1 |
. . . . . . . . 9
   ↾t   ↾t     |
8 | | ovex 6323 |
. . . . . . . . . . . . 13
     |
9 | | retopon 21796 |
. . . . . . . . . . . . 13
    TopOn   |
10 | 3 | pttoponconst 20624 |
. . . . . . . . . . . . 13
          TopOn  
TopOn          |
11 | 8, 9, 10 | mp2an 679 |
. . . . . . . . . . . 12
TopOn         |
12 | | reex 9635 |
. . . . . . . . . . . . . 14
 |
13 | | unitssre 11786 |
. . . . . . . . . . . . . 14
  ![[,] [,]](_icc.gif)   |
14 | | mapss 7519 |
. . . . . . . . . . . . . 14
    ![[,] [,]](_icc.gif) 
    ![[,] [,]](_icc.gif)               |
15 | 12, 13, 14 | mp2an 679 |
. . . . . . . . . . . . 13
   ![[,] [,]](_icc.gif)       
      |
16 | 2, 15 | eqsstri 3464 |
. . . . . . . . . . . 12

      |
17 | | resttopon 20189 |
. . . . . . . . . . . 12
  TopOn 
      
     
 ↾t  TopOn    |
18 | 11, 16, 17 | mp2an 679 |
. . . . . . . . . . 11
 ↾t  TopOn   |
19 | 18 | toponunii 19959 |
. . . . . . . . . 10
  ↾t   |
20 | 19, 19 | cnf 20274 |
. . . . . . . . 9
   ↾t   ↾t         |
21 | 7, 20 | syl 17 |
. . . . . . . 8
       |
22 | 21 | ffvelrnda 6027 |
. . . . . . 7
 
       |
23 | | elmapfn 7499 |
. . . . . . . 8
        ![[,] [,]](_icc.gif)                 |
24 | 23, 2 | eleq2s 2549 |
. . . . . . 7
               |
25 | 22, 24 | syl 17 |
. . . . . 6
 
           |
26 | 8 | a1i 11 |
. . . . . 6
 
       |
27 | | inidm 3643 |
. . . . . 6
               |
28 | | eqidd 2454 |
. . . . . 6
                   |
29 | | eqidd 2454 |
. . . . . 6
                           |
30 | 6, 25, 26, 26, 27, 28, 29 | offval 6543 |
. . . . 5
 
                              |
31 | 30 | mpteq2dva 4492 |
. . . 4
                                  |
32 | 18 | a1i 11 |
. . . . 5
 
↾t  TopOn    |
33 | 8 | a1i 11 |
. . . . 5
       |
34 | | retop 21794 |
. . . . . . 7
     |
35 | 34 | fconst6 5778 |
. . . . . 6
                     |
36 | 35 | a1i 11 |
. . . . 5
                       |
37 | 18 | a1i 11 |
. . . . . . . 8
 
      ↾t  TopOn    |
38 | | eqid 2453 |
. . . . . . . . . . . 12
  ℂfld   ℂfld |
39 | 38 | cnfldtop 21816 |
. . . . . . . . . . 11
  ℂfld  |
40 | | cnrest2r 20315 |
. . . . . . . . . . 11
   ℂfld  
↾t     ℂfld
↾t     ↾t    ℂfld   |
41 | 39, 40 | ax-mp 5 |
. . . . . . . . . 10
  ↾t     ℂfld
↾t     ↾t    ℂfld  |
42 | | resmpt 5157 |
. . . . . . . . . . . . 13
                             |
43 | 16, 42 | ax-mp 5 |
. . . . . . . . . . . 12
            
        |
44 | 11 | toponunii 19959 |
. . . . . . . . . . . . . . 15
        |
45 | 44, 3 | ptpjcn 20638 |
. . . . . . . . . . . . . 14
                                                               |
46 | 8, 35, 45 | mp3an12 1356 |
. . . . . . . . . . . . 13
                                     |
47 | 44 | cnrest 20313 |
. . . . . . . . . . . . 13
                                      
            
   ↾t                     |
48 | 46, 16, 47 | sylancl 669 |
. . . . . . . . . . . 12
                     ↾t                     |
49 | 43, 48 | syl5eqelr 2536 |
. . . . . . . . . . 11
             ↾t                     |
50 | | fvex 5880 |
. . . . . . . . . . . . . 14
     |
51 | 50 | fvconst2 6125 |
. . . . . . . . . . . . 13
                           |
52 | 38 | tgioo2 21833 |
. . . . . . . . . . . . 13
       ℂfld
↾t   |
53 | 51, 52 | syl6eq 2503 |
. . . . . . . . . . . 12
                        ℂfld ↾t    |
54 | 53 | oveq2d 6311 |
. . . . . . . . . . 11
      
↾t                    
↾t     ℂfld
↾t     |
55 | 49, 54 | eleqtrd 2533 |
. . . . . . . . . 10
             ↾t     ℂfld
↾t     |
56 | 41, 55 | sseldi 3432 |
. . . . . . . . 9
             ↾t    ℂfld   |
57 | 56 | adantl 468 |
. . . . . . . 8
 
             ↾t    ℂfld   |
58 | 21 | feqmptd 5923 |
. . . . . . . . . . 11
         |
59 | 58, 7 | eqeltrrd 2532 |
. . . . . . . . . 10
        
↾t   ↾t     |
60 | 59 | adantr 467 |
. . . . . . . . 9
 
             ↾t   ↾t     |
61 | | fveq1 5869 |
. . . . . . . . . . 11
           |
62 | 61 | cbvmptv 4498 |
. . . . . . . . . 10
             |
63 | 62, 57 | syl5eqelr 2536 |
. . . . . . . . 9
 
             ↾t    ℂfld   |
64 | | fveq1 5869 |
. . . . . . . . 9
                   |
65 | 37, 60, 37, 63, 64 | cnmpt11 20690 |
. . . . . . . 8
 
                 ↾t    ℂfld   |
66 | 38 | subcn 21910 |
. . . . . . . . 9
    ℂfld   ℂfld   ℂfld  |
67 | 66 | a1i 11 |
. . . . . . . 8
 
         ℂfld   ℂfld   ℂfld   |
68 | 37, 57, 65, 67 | cnmpt12f 20693 |
. . . . . . 7
 
                       ↾t    ℂfld   |
69 | | elmapi 7498 |
. . . . . . . . . . . . . . 15
    ![[,] [,]](_icc.gif)                 ![[,] [,]](_icc.gif)    |
70 | 69, 2 | eleq2s 2549 |
. . . . . . . . . . . . . 14
           ![[,] [,]](_icc.gif)    |
71 | 70 | ffvelrnda 6027 |
. . . . . . . . . . . . 13
 
           ![[,] [,]](_icc.gif)    |
72 | 13, 71 | sseldi 3432 |
. . . . . . . . . . . 12
 
           |
73 | 72 | adantll 721 |
. . . . . . . . . . 11
               |
74 | | elmapi 7498 |
. . . . . . . . . . . . . . 15
        ![[,] [,]](_icc.gif)                     ![[,] [,]](_icc.gif)    |
75 | 74, 2 | eleq2s 2549 |
. . . . . . . . . . . . . 14
                   ![[,] [,]](_icc.gif)    |
76 | 22, 75 | syl 17 |
. . . . . . . . . . . . 13
 
               ![[,] [,]](_icc.gif)    |
77 | 76 | ffvelrnda 6027 |
. . . . . . . . . . . 12
                   ![[,] [,]](_icc.gif)    |
78 | 13, 77 | sseldi 3432 |
. . . . . . . . . . 11
                   |
79 | 73, 78 | resubcld 10054 |
. . . . . . . . . 10
                         |
80 | 79 | an32s 814 |
. . . . . . . . 9
                         |
81 | | eqid 2453 |
. . . . . . . . 9
                                 |
82 | 80, 81 | fmptd 6051 |
. . . . . . . 8
 
                           |
83 | | frn 5740 |
. . . . . . . 8
                                       |
84 | 38 | cnfldtopon 21815 |
. . . . . . . . 9
  ℂfld TopOn   |
85 | | ax-resscn 9601 |
. . . . . . . . 9
 |
86 | | cnrest2 20314 |
. . . . . . . . 9
    ℂfld
TopOn  
              
                    ↾t    ℂfld

                 ↾t     ℂfld ↾t      |
87 | 84, 85, 86 | mp3an13 1357 |
. . . . . . . 8
                                    ↾t    ℂfld

                 ↾t     ℂfld ↾t      |
88 | 82, 83, 87 | 3syl 18 |
. . . . . . 7
 
                       
↾t    ℂfld

                 ↾t     ℂfld ↾t      |
89 | 68, 88 | mpbid 214 |
. . . . . 6
 
                       ↾t     ℂfld
↾t     |
90 | 54 | adantl 468 |
. . . . . 6
 
      
↾t                    
↾t     ℂfld
↾t     |
91 | 89, 90 | eleqtrrd 2534 |
. . . . 5
 
                       ↾t                     |
92 | 3, 32, 33, 36, 91 | ptcn 20654 |
. . . 4
                         ↾t     |
93 | 31, 92 | eqeltrd 2531 |
. . 3
            ↾t     |
94 | | simpr2 1016 |
. . . . . 6
 
    
        |
95 | | id 22 |
. . . . . . . . 9
   |
96 | | fveq2 5870 |
. . . . . . . . 9
           |
97 | 95, 96 | oveq12d 6313 |
. . . . . . . 8
                 |
98 | | eqid 2453 |
. . . . . . . 8
                   |
99 | | ovex 6323 |
. . . . . . . 8
        |
100 | 97, 98, 99 | fvmpt 5953 |
. . . . . . 7
                       |
101 | 100 | fveq1d 5872 |
. . . . . 6
                               |
102 | 94, 101 | syl 17 |
. . . . 5
 
    
                                    |
103 | | elmapfn 7499 |
. . . . . . . . . . . 12
    ![[,] [,]](_icc.gif)             |
104 | 103, 2 | eleq2s 2549 |
. . . . . . . . . . 11
       |
105 | 104 | adantl 468 |
. . . . . . . . . 10
       
       |
106 | 21 | ffvelrnda 6027 |
. . . . . . . . . . . 12
 
       |
107 | | elmapfn 7499 |
. . . . . . . . . . . . 13
        ![[,] [,]](_icc.gif)                 |
108 | 107, 2 | eleq2s 2549 |
. . . . . . . . . . . 12
               |
109 | 106, 108 | syl 17 |
. . . . . . . . . . 11
 
           |
110 | 109 | adantlr 722 |
. . . . . . . . . 10
       
           |
111 | 8 | a1i 11 |
. . . . . . . . . 10
       
       |
112 | | simpllr 770 |
. . . . . . . . . 10
         
           |
113 | | eqidd 2454 |
. . . . . . . . . 10
         
                       |
114 | 105, 110,
111, 111, 27, 112, 113 | ofval 6545 |
. . . . . . . . 9
         
                            |
115 | | df-neg 9868 |
. . . . . . . . 9
                    |
116 | 114, 115 | syl6eqr 2505 |
. . . . . . . 8
         
                           |
117 | 116 | exp41 615 |
. . . . . . 7
      
    
                         |
118 | 117 | com24 90 |
. . . . . 6
      
                              |
119 | 118 | 3imp2 1225 |
. . . . 5
 
    
                            |
120 | 102, 119 | eqtrd 2487 |
. . . 4
 
    
                                  |
121 | | elmapi 7498 |
. . . . . . . . . . . 12
        ![[,] [,]](_icc.gif)                     ![[,] [,]](_icc.gif)    |
122 | 121, 2 | eleq2s 2549 |
. . . . . . . . . . 11
                   ![[,] [,]](_icc.gif)    |
123 | 106, 122 | syl 17 |
. . . . . . . . . 10
 
               ![[,] [,]](_icc.gif)    |
124 | 123 | ffvelrnda 6027 |
. . . . . . . . 9
                   ![[,] [,]](_icc.gif)    |
125 | | 0xr 9692 |
. . . . . . . . . 10
 |
126 | | 1re 9647 |
. . . . . . . . . . 11
 |
127 | 126 | rexri 9698 |
. . . . . . . . . 10
 |
128 | | iccgelb 11698 |
. . . . . . . . . 10
            ![[,] [,]](_icc.gif)             |
129 | 125, 127,
128 | mp3an12 1356 |
. . . . . . . . 9
           ![[,] [,]](_icc.gif) 
          |
130 | 124, 129 | syl 17 |
. . . . . . . 8
                   |
131 | 13, 124 | sseldi 3432 |
. . . . . . . . 9
                   |
132 | 131 | le0neg2d 10193 |
. . . . . . . 8
         
       
            |
133 | 130, 132 | mpbid 214 |
. . . . . . 7
                    |
134 | 133 | an32s 814 |
. . . . . 6
                    |
135 | 134 | anasss 653 |
. . . . 5
 
    
          
  |
136 | 135 | 3adantr3 1170 |
. . . 4
 
    
                 |
137 | 120, 136 | eqbrtrd 4426 |
. . 3
 
    
                         |
138 | | iccleub 11697 |
. . . . . . . . . 10
            ![[,] [,]](_icc.gif)             |
139 | 125, 127,
138 | mp3an12 1356 |
. . . . . . . . 9
           ![[,] [,]](_icc.gif) 
          |
140 | 124, 139 | syl 17 |
. . . . . . . 8
                   |
141 | | 1red 9663 |
. . . . . . . . 9
           |
142 | 141, 131 | subge0d 10210 |
. . . . . . . 8
         
         
           |
143 | 140, 142 | mpbird 236 |
. . . . . . 7
                     |
144 | 143 | an32s 814 |
. . . . . 6
                     |
145 | 144 | anasss 653 |
. . . . 5
 
    
 
            |
146 | 145 | 3adantr3 1170 |
. . . 4
 
    
                  |
147 | | simpr2 1016 |
. . . . . 6
 
    
        |
148 | 147, 101 | syl 17 |
. . . . 5
 
    
                                    |
149 | 104 | adantl 468 |
. . . . . . . . 9
       
       |
150 | 109 | adantlr 722 |
. . . . . . . . 9
       
           |
151 | 8 | a1i 11 |
. . . . . . . . 9
       
       |
152 | | simpllr 770 |
. . . . . . . . 9
         
           |
153 | | eqidd 2454 |
. . . . . . . . 9
         
                       |
154 | 149, 150,
151, 151, 27, 152, 153 | ofval 6545 |
. . . . . . . 8
         
                            |
155 | 154 | exp41 615 |
. . . . . . 7
      
    
                          |
156 | 155 | com24 90 |
. . . . . 6
      
                               |
157 | 156 | 3imp2 1225 |
. . . . 5
 
    
                             |
158 | 148, 157 | eqtrd 2487 |
. . . 4
 
    
                                   |
159 | 146, 158 | breqtrrd 4432 |
. . 3
 
    
                         |
160 | 1, 2, 3, 93, 137, 159 | poimir 31985 |
. 2
                         |
161 | | id 22 |
. . . . . . . 8
   |
162 | | fveq2 5870 |
. . . . . . . 8
           |
163 | 161, 162 | oveq12d 6313 |
. . . . . . 7
                 |
164 | | ovex 6323 |
. . . . . . 7
        |
165 | 163, 98, 164 | fvmpt 5953 |
. . . . . 6
                       |
166 | 165 | adantl 468 |
. . . . 5
 
                       |
167 | 166 | eqeq1d 2455 |
. . . 4
 
                                         |
168 | | elmapfn 7499 |
. . . . . . . . . . 11
    ![[,] [,]](_icc.gif)             |
169 | 168, 2 | eleq2s 2549 |
. . . . . . . . . 10
       |
170 | 169 | adantl 468 |
. . . . . . . . 9
 
       |
171 | 21 | ffvelrnda 6027 |
. . . . . . . . . 10
 
       |
172 | | elmapfn 7499 |
. . . . . . . . . . 11
        ![[,] [,]](_icc.gif)                 |
173 | 172, 2 | eleq2s 2549 |
. . . . . . . . . 10
               |
174 | 171, 173 | syl 17 |
. . . . . . . . 9
 
           |
175 | 8 | a1i 11 |
. . . . . . . . 9
 
       |
176 | | eqidd 2454 |
. . . . . . . . 9
                   |
177 | | eqidd 2454 |
. . . . . . . . 9
                           |
178 | 170, 174,
175, 175, 27, 176, 177 | ofval 6545 |
. . . . . . . 8
                                    |
179 | | c0ex 9642 |
. . . . . . . . . 10
 |
180 | 179 | fvconst2 6125 |
. . . . . . . . 9
                   |
181 | 180 | adantl 468 |
. . . . . . . 8
                       |
182 | 178, 181 | eqeq12d 2468 |
. . . . . . 7
                                
                 |
183 | 13, 85 | sstri 3443 |
. . . . . . . . . 10
  ![[,] [,]](_icc.gif)   |
184 | | elmapi 7498 |
. . . . . . . . . . . 12
    ![[,] [,]](_icc.gif)                 ![[,] [,]](_icc.gif)    |
185 | 184, 2 | eleq2s 2549 |
. . . . . . . . . . 11
           ![[,] [,]](_icc.gif)    |
186 | 185 | ffvelrnda 6027 |
. . . . . . . . . 10
 
           ![[,] [,]](_icc.gif)    |
187 | 183, 186 | sseldi 3432 |
. . . . . . . . 9
 
           |
188 | 187 | adantll 721 |
. . . . . . . 8
               |
189 | | elmapi 7498 |
. . . . . . . . . . . 12
        ![[,] [,]](_icc.gif)                     ![[,] [,]](_icc.gif)    |
190 | 189, 2 | eleq2s 2549 |
. . . . . . . . . . 11
                   ![[,] [,]](_icc.gif)    |
191 | 171, 190 | syl 17 |
. . . . . . . . . 10
 
               ![[,] [,]](_icc.gif)    |
192 | 191 | ffvelrnda 6027 |
. . . . . . . . 9
                   ![[,] [,]](_icc.gif)    |
193 | 183, 192 | sseldi 3432 |
. . . . . . . 8
                   |
194 | 188, 193 | subeq0ad 10001 |
. . . . . . 7
                                       |
195 | 182, 194 | bitrd 257 |
. . . . . 6
                                
               |
196 | 195 | ralbidva 2826 |
. . . . 5
 
  
                           
                     |
197 | 170, 174,
175, 175, 27 | offn 6547 |
. . . . . 6
 
              |
198 | | fnconstg 5776 |
. . . . . . 7
               |
199 | 179, 198 | ax-mp 5 |
. . . . . 6
             |
200 | | eqfnfv 5981 |
. . . . . 6
            
                             
                               |
201 | 197, 199,
200 | sylancl 669 |
. . . . 5
 
                
                                |
202 | | eqfnfv 5981 |
. . . . . 6
                    
                    |
203 | 170, 174,
202 | syl2anc 667 |
. . . . 5
 
     
                     |
204 | 196, 201,
203 | 3bitr4d 289 |
. . . 4
 
                
       |
205 | 167, 204 | bitrd 257 |
. . 3
 
                              |
206 | 205 | rexbidva 2900 |
. 2
                                |
207 | 160, 206 | mpbid 214 |
1
        |