Step | Hyp | Ref
| Expression |
1 | | ulmdv.m |
. . . . . 6
   |
2 | | uzid 11197 |
. . . . . 6
       |
3 | 1, 2 | syl 17 |
. . . . 5
       |
4 | | ulmdv.z |
. . . . 5
     |
5 | 3, 4 | syl6eleqr 2560 |
. . . 4
   |
6 | | ulmdv.s |
. . . . . . 7
      |
7 | | ulmdv.f |
. . . . . . 7
         |
8 | | ulmdv.g |
. . . . . . 7
       |
9 | | ulmdv.l |
. . . . . . 7
 
                 |
10 | | ulmdv.u |
. . . . . . 7
                  |
11 | 4, 6, 1, 7, 8, 9, 10 | ulmdvlem2 23435 |
. . . . . 6
 
 
       |
12 | | recnprss 22938 |
. . . . . . . . 9
   
  |
13 | 6, 12 | syl 17 |
. . . . . . . 8

  |
14 | 13 | adantr 472 |
. . . . . . 7
 
   |
15 | 7 | ffvelrnda 6037 |
. . . . . . . 8
 
         |
16 | | elmapi 7511 |
. . . . . . . 8
                 |
17 | 15, 16 | syl 17 |
. . . . . . 7
 
           |
18 | | dvbsss 22936 |
. . . . . . . 8
       |
19 | 11, 18 | syl6eqssr 3469 |
. . . . . . 7
 
   |
20 | | eqid 2471 |
. . . . . . 7
   ℂfld ↾t     ℂfld
↾t   |
21 | | eqid 2471 |
. . . . . . 7
  ℂfld   ℂfld |
22 | 14, 17, 19, 20, 21 | dvbssntr 22934 |
. . . . . 6
 
 
    
       ℂfld ↾t        |
23 | 11, 22 | eqsstr3d 3453 |
. . . . 5
 
        ℂfld
↾t        |
24 | 23 | ralrimiva 2809 |
. . . 4
         ℂfld
↾t        |
25 | | biidd 245 |
. . . . 5
         ℂfld
↾t     
       ℂfld
↾t         |
26 | 25 | rspcv 3132 |
. . . 4
  
       ℂfld
↾t             ℂfld
↾t         |
27 | 5, 24, 26 | sylc 61 |
. . 3

       ℂfld ↾t        |
28 | 27 | sselda 3418 |
. 2
 
        ℂfld
↾t        |
29 | | ulmcl 23415 |
. . . . 5
                      |
30 | 10, 29 | syl 17 |
. . . 4
       |
31 | 30 | ffvelrnda 6037 |
. . 3
 
       |
32 | | rphalfcl 11350 |
. . . . . . . 8

    |
33 | 32 | adantl 473 |
. . . . . . 7
         |
34 | | rphalfcl 11350 |
. . . . . . 7
  
      |
35 | 33, 34 | syl 17 |
. . . . . 6
           |
36 | | ulmrel 23412 |
. . . . . . . . . 10
      |
37 | | releldm 5073 |
. . . . . . . . . 10
                                      |
38 | 36, 10, 37 | sylancr 676 |
. . . . . . . . 9
                |
39 | | ulmscl 23413 |
. . . . . . . . . . 11
               
  |
40 | 10, 39 | syl 17 |
. . . . . . . . . 10
   |
41 | | ovex 6336 |
. . . . . . . . . . . . 13
       |
42 | 41 | rgenw 2768 |
. . . . . . . . . . . 12

       |
43 | | eqid 2471 |
. . . . . . . . . . . . 13
                 |
44 | 43 | fnmpt 5714 |
. . . . . . . . . . . 12
 
                |
45 | 42, 44 | mp1i 13 |
. . . . . . . . . . 11
           |
46 | | ulmf2 23418 |
. . . . . . . . . . 11
                                      
   |
47 | 45, 10, 46 | syl2anc 673 |
. . . . . . . . . 10
             
   |
48 | 4, 1, 40, 47 | ulmcau2 23430 |
. . . . . . . . 9
               

      
     
                                         |
49 | 38, 48 | mpbid 215 |
. . . . . . . 8
   
           
                                        |
50 | 4 | uztrn2 11200 |
. . . . . . . . . . . . . . . . . 18
 
    
  |
51 | 50 | ad2ant2lr 762 |
. . . . . . . . . . . . . . . . 17
                 |
52 | | fveq2 5879 |
. . . . . . . . . . . . . . . . . . 19
           |
53 | 52 | oveq2d 6324 |
. . . . . . . . . . . . . . . . . 18
               |
54 | | ovex 6336 |
. . . . . . . . . . . . . . . . . 18
       |
55 | 53, 43, 54 | fvmpt 5963 |
. . . . . . . . . . . . . . . . 17
                     |
56 | 51, 55 | syl 17 |
. . . . . . . . . . . . . . . 16
                                   |
57 | 56 | fveq1d 5881 |
. . . . . . . . . . . . . . 15
                                           |
58 | | simprr 774 |
. . . . . . . . . . . . . . . . . 18
                     |
59 | 4 | uztrn2 11200 |
. . . . . . . . . . . . . . . . . 18
 
    
  |
60 | 51, 58, 59 | syl2anc 673 |
. . . . . . . . . . . . . . . . 17
                 |
61 | | fveq2 5879 |
. . . . . . . . . . . . . . . . . . 19
           |
62 | 61 | oveq2d 6324 |
. . . . . . . . . . . . . . . . . 18
               |
63 | | ovex 6336 |
. . . . . . . . . . . . . . . . . 18
       |
64 | 62, 43, 63 | fvmpt 5963 |
. . . . . . . . . . . . . . . . 17
                     |
65 | 60, 64 | syl 17 |
. . . . . . . . . . . . . . . 16
                                   |
66 | 65 | fveq1d 5881 |
. . . . . . . . . . . . . . 15
                                           |
67 | 57, 66 | oveq12d 6326 |
. . . . . . . . . . . . . 14
                                                                         |
68 | 67 | fveq2d 5883 |
. . . . . . . . . . . . 13
                                                                                 |
69 | 68 | breq1d 4405 |
. . . . . . . . . . . 12
                                                                                   |
70 | 69 | ralbidv 2829 |
. . . . . . . . . . 11
                
                                     

                             |
71 | 70 | 2ralbidva 2831 |
. . . . . . . . . 10
 
  
     
     
                                     
      
     
                             |
72 | 71 | rexbidva 2889 |
. . . . . . . . 9
         
     
                                     

      
     
                             |
73 | 72 | ralbidv 2829 |
. . . . . . . 8
    
     
     
                                     
        
     
                             |
74 | 49, 73 | mpbid 215 |
. . . . . . 7
   
           
                            |
75 | 74 | ad2antrr 740 |
. . . . . 6
             
     
                            |
76 | | breq2 4399 |
. . . . . . . . 9
                               
                                 |
77 | 76 | 2ralbidv 2832 |
. . . . . . . 8
      
     
                                
                                 |
78 | 77 | rexralbidv 2898 |
. . . . . . 7
      

     
     
                           
           
                                 |
79 | 78 | rspcv 3132 |
. . . . . 6
    
 

      
     
                           
     
     
                                 |
80 | 35, 75, 79 | sylc 61 |
. . . . 5
     
      
     
                                |
81 | 1 | ad2antrr 740 |
. . . . . 6
       |
82 | 53 | fveq1d 5881 |
. . . . . . . 8
                       |
83 | | eqid 2471 |
. . . . . . . 8
                         |
84 | | fvex 5889 |
. . . . . . . 8
           |
85 | 82, 83, 84 | fvmpt 5963 |
. . . . . . 7
                             |
86 | 85 | adantl 473 |
. . . . . 6
   



                            |
87 | 47 | ad2antrr 740 |
. . . . . . 7
                     |
88 | | simplr 770 |
. . . . . . 7
       |
89 | | fvex 5889 |
. . . . . . . . . 10
     |
90 | 4, 89 | eqeltri 2545 |
. . . . . . . . 9
 |
91 | 90 | mptex 6152 |
. . . . . . . 8
             |
92 | 91 | a1i 11 |
. . . . . . 7
                   |
93 | 55 | adantl 473 |
. . . . . . . . 9
   



                    |
94 | 93 | fveq1d 5881 |
. . . . . . . 8
   



                            |
95 | 94, 86 | eqtr4d 2508 |
. . . . . . 7
   



                                  |
96 | 10 | ad2antrr 740 |
. . . . . . 7
                      |
97 | 4, 81, 87, 88, 92, 95, 96 | ulmclm 23421 |
. . . . . 6
                       |
98 | 4, 81, 33, 86, 97 | climi2 13652 |
. . . . 5
     
                              |
99 | 4 | rexanuz2 13489 |
. . . . . . 7
  
      
     
                                                    
 

           
                              

                              |
100 | 4 | r19.2uz 13491 |
. . . . . . 7
  
      
     
                                                     
       
                                                       |
101 | 99, 100 | sylbir 218 |
. . . . . 6
   
     
     
                                                            
       
                                                       |
102 | 35 | adantr 472 |
. . . . . . . . . 10
   



      |
103 | | simpllr 777 |
. . . . . . . . . . . . . . . 16
   



  |
104 | 87 | ffvelrnda 6037 |
. . . . . . . . . . . . . . . . . 18
   



                |
105 | 93, 104 | eqeltrrd 2550 |
. . . . . . . . . . . . . . . . 17
   



          |
106 | | elmapi 7511 |
. . . . . . . . . . . . . . . . 17
                     |
107 | | fdm 5745 |
. . . . . . . . . . . . . . . . 17
                   |
108 | 105, 106,
107 | 3syl 18 |
. . . . . . . . . . . . . . . 16
   



        |
109 | 103, 108 | eleqtrrd 2552 |
. . . . . . . . . . . . . . 15
   



        |
110 | 6 | ad3antrrr 744 |
. . . . . . . . . . . . . . . 16
   



     |
111 | | dvfg 22940 |
. . . . . . . . . . . . . . . 16
   
        
         |
112 | | ffun 5742 |
. . . . . . . . . . . . . . . 16
                         |
113 | | funfvbrb 6010 |
. . . . . . . . . . . . . . . 16
      
                            |
114 | 110, 111,
112, 113 | 4syl 19 |
. . . . . . . . . . . . . . 15
   



                            |
115 | 109, 114 | mpbid 215 |
. . . . . . . . . . . . . 14
   



                    |
116 | | eqid 2471 |
. . . . . . . . . . . . . . 15
                                                         |
117 | 110, 12 | syl 17 |
. . . . . . . . . . . . . . 15
   



  |
118 | 7 | ad2antrr 740 |
. . . . . . . . . . . . . . . . 17
             |
119 | 118 | ffvelrnda 6037 |
. . . . . . . . . . . . . . . 16
   



        |
120 | | elmapi 7511 |
. . . . . . . . . . . . . . . 16
                 |
121 | 119, 120 | syl 17 |
. . . . . . . . . . . . . . 15
   



          |
122 | 19 | ralrimiva 2809 |
. . . . . . . . . . . . . . . . 17
    |
123 | | biidd 245 |
. . . . . . . . . . . . . . . . . 18
 
   |
124 | 123 | rspcv 3132 |
. . . . . . . . . . . . . . . . 17
  
   |
125 | 5, 122, 124 | sylc 61 |
. . . . . . . . . . . . . . . 16

  |
126 | 125 | ad3antrrr 744 |
. . . . . . . . . . . . . . 15
   



  |
127 | 20, 21, 116, 117, 121, 126 | eldv 22932 |
. . . . . . . . . . . . . 14
   



                  
        ℂfld
↾t                                             lim      |
128 | 115, 127 | mpbid 215 |
. . . . . . . . . . . . 13
   



        ℂfld
↾t                                             lim     |
129 | 128 | simprd 470 |
. . . . . . . . . . . 12
   



                                       lim    |
130 | 125 | adantr 472 |
. . . . . . . . . . . . . . . . 17
 
   |
131 | 13 | adantr 472 |
. . . . . . . . . . . . . . . . 17
 
   |
132 | 130, 131 | sstrd 3428 |
. . . . . . . . . . . . . . . 16
 
   |
133 | 132 | ad2antrr 740 |
. . . . . . . . . . . . . . 15
   



  |
134 | 121, 133,
103 | dvlem 22930 |
. . . . . . . . . . . . . 14
       

                            |
135 | 134, 116 | fmptd 6061 |
. . . . . . . . . . . . 13
   



                                      |
136 | 133 | ssdifssd 3560 |
. . . . . . . . . . . . 13
   



      |
137 | 133, 103 | sseldd 3419 |
. . . . . . . . . . . . 13
   



  |
138 | 135, 136,
137 | ellimc3 22913 |
. . . . . . . . . . . 12
   



                                        lim                                                                                   |
139 | 129, 138 | mpbid 215 |
. . . . . . . . . . 11
   



                                                                                |
140 | 139 | simprd 470 |
. . . . . . . . . 10
   



                                                                    |
141 | | fveq2 5879 |
. . . . . . . . . . . . . . . . . . . 20
                   |
142 | 141 | oveq1d 6323 |
. . . . . . . . . . . . . . . . . . 19
                                       |
143 | | oveq1 6315 |
. . . . . . . . . . . . . . . . . . 19
       |
144 | 142, 143 | oveq12d 6326 |
. . . . . . . . . . . . . . . . . 18
                                               |
145 | | ovex 6336 |
. . . . . . . . . . . . . . . . . 18
                       |
146 | 144, 116,
145 | fvmpt 5963 |
. . . . . . . . . . . . . . . . 17
                                                             |
147 | 146 | oveq1d 6323 |
. . . . . . . . . . . . . . . 16
                                                                                     |
148 | 147 | fveq2d 5883 |
. . . . . . . . . . . . . . 15
                                                                                             |
149 | | id 22 |
. . . . . . . . . . . . . . 15
           |
150 | 148, 149 | breqan12rd 4412 |
. . . . . . . . . . . . . 14
     
    
                                                                                              |
151 | 150 | imbi2d 323 |
. . . . . . . . . . . . 13
     
    
                                                          
                                                       |
152 | 151 | ralbidva 2828 |
. . . . . . . . . . . 12
      
                                                                                                                            |
153 | 152 | rexbidv 2892 |
. . . . . . . . . . 11
      
                                                               
                                                              |
154 | 153 | rspcv 3132 |
. . . . . . . . . 10
    
 
                                                                 
                                                             |
155 | 102, 140,
154 | sylc 61 |
. . . . . . . . 9
   



                                                             |
156 | 155 | adantrr 731 |
. . . . . . . 8
   

         
                                                       
                                                            |
157 | | anass 661 |
. . . . . . . . . . . . . . . 16
     
          
                                                       

      
             
          
                                                         
      
       
    |
158 | | df-3an 1009 |
. . . . . . . . . . . . . . . . . . 19
         
                                                       

      
       
                                                                        
     
                                                         
      
       
                                                                       |
159 | | anass 661 |
. . . . . . . . . . . . . . . . . . . 20
    
 
    |
160 | 9 | ralrimiva 2809 |
. . . . . . . . . . . . . . . . . . . . . . 23
                  |
161 | | fveq2 5879 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
                   |
162 | 161 | mpteq2dv 4483 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
                       |
163 | | fveq2 5879 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
           |
164 | 162, 163 | breq12d 4408 |
. . . . . . . . . . . . . . . . . . . . . . . 24
               

                |
165 | 164 | rspccva 3135 |
. . . . . . . . . . . . . . . . . . . . . . 23
                
                 |
166 | 160, 165 | sylan 479 |
. . . . . . . . . . . . . . . . . . . . . 22
 
                 |
167 | | simprll 780 |
. . . . . . . . . . . . . . . . . . . . . 22
 
 
 
       
                                                               
       
                                                                         |
168 | | simprlr 781 |
. . . . . . . . . . . . . . . . . . . . . 22
 
 
 
       
                                                               
       
                                                                         |
169 | | simprr3 1080 |
. . . . . . . . . . . . . . . . . . . . . . 23
 
 
 
       
                                                               
       
                                                                          
       
    
 
                                                                      |
170 | | simplll 776 |
. . . . . . . . . . . . . . . . . . . . . . 23
    
       
    
 
                                                                      |
171 | 169, 170 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
 
 
 
       
                                                               
       
                                                                         |
172 | | simplr 770 |
. . . . . . . . . . . . . . . . . . . . . . 23
    
       
    
 
                                                                      |
173 | 169, 172 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
 
 
 
       
                                                               
       
                                                                         |
174 | | simpllr 777 |
. . . . . . . . . . . . . . . . . . . . . . . 24
    
       
    
 
                                                                    
       
    
   |
175 | 169, 174 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
 
 
 
       
                                                               
       
                                                                       
      
         |
176 | 175 | simpld 466 |
. . . . . . . . . . . . . . . . . . . . . 22
 
 
 
       
                                                               
       
                                                                         |
177 | 175 | simprd 470 |
. . . . . . . . . . . . . . . . . . . . . 22
 
 
 
       
                                                               
       
                                                                             
     
  |
178 | | simpr3 1038 |
. . . . . . . . . . . . . . . . . . . . . . . 24
    
       
    
 
                                                                              |
179 | 169, 178 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
 
 
 
       
                                                               
       
                                                                                 |
180 | 179 | simprd 470 |
. . . . . . . . . . . . . . . . . . . . . 22
 
 
 
       
                                                               
       
                                                                               |
181 | | simprr1 1078 |
. . . . . . . . . . . . . . . . . . . . . 22
 
 
 
       
                                                               
       
                                                                         |
182 | | simprr2 1079 |
. . . . . . . . . . . . . . . . . . . . . . 23
 
 
 
       
                                                               
       
                                                                        
     
                                                       |
183 | 182 | simpld 466 |
. . . . . . . . . . . . . . . . . . . . . 22
 
 
 
       
                                                               
       
                                                                             
                                |
184 | 182 | simprd 470 |
. . . . . . . . . . . . . . . . . . . . . 22
 
 
 
       
                                                               
       
                                                                                               |
185 | | simpr1 1036 |
. . . . . . . . . . . . . . . . . . . . . . . 24
    
       
    
 
                                                                          |
186 | 169, 185 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
 
 
 
       
                                                               
       
                                                                             |
187 | 186 | eldifad 3402 |
. . . . . . . . . . . . . . . . . . . . . 22
 
 
 
       
                                                               
       
                                                                         |
188 | 179 | simpld 466 |
. . . . . . . . . . . . . . . . . . . . . 22
 
 
 
       
                                                               
       
                                                                         |
189 | | simpr2 1037 |
. . . . . . . . . . . . . . . . . . . . . . . 24
    
       
    
 
                                                                                                                          |
190 | 169, 189 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
 
 
 
       
                                                               
       
                                                                                                                             |
191 | 188, 190 | mpand 689 |
. . . . . . . . . . . . . . . . . . . . . 22
 
 
 
       
                                                               
       
                                                                                                                           |
192 | 4, 6, 1, 7, 8, 166, 10, 167, 168, 171, 173, 176, 177, 180, 181, 183, 184, 187, 188, 191 | ulmdvlem1 23434 |
. . . . . . . . . . . . . . . . . . . . 21
 
 
 
       
                                                               
       
                                                                                                |