Step | Hyp | Ref
| Expression |
1 | | cnheibor.2 |
. . . . . 6
  ℂfld |
2 | 1 | cnfldtop 21804 |
. . . . 5
 |
3 | 2 | a1i 11 |
. . . 4
      

     
  |
4 | | cnheibor.4 |
. . . . . . . . . 10
 


    |
5 | 4 | cnref1o 11297 |
. . . . . . . . 9
       |
6 | | f1ofn 5815 |
. . . . . . . . 9
      

   |
7 | | elpreima 6002 |
. . . . . . . . 9
  
     
           |
8 | 5, 6, 7 | mp2b 10 |
. . . . . . . 8
     
          |
9 | | 1st2nd2 6830 |
. . . . . . . . . . 11
  
             |
10 | 9 | ad2antrl 734 |
. . . . . . . . . 10
                                     |
11 | | xp1st 6823 |
. . . . . . . . . . . . 13
  
      |
12 | 11 | ad2antrl 734 |
. . . . . . . . . . . 12
                              |
13 | 12 | recnd 9669 |
. . . . . . . . . . . . . . . 16
                              |
14 | 13 | abscld 13498 |
. . . . . . . . . . . . . . 15
                                  |
15 | 1 | cnfldtopon 21803 |
. . . . . . . . . . . . . . . . . . . . 21
TopOn   |
16 | 15 | toponunii 19947 |
. . . . . . . . . . . . . . . . . . . 20
  |
17 | 16 | cldss 20044 |
. . . . . . . . . . . . . . . . . . 19
    
  |
18 | 17 | adantr 467 |
. . . . . . . . . . . . . . . . . 18
      

        |
19 | 18 | adantr 467 |
. . . . . . . . . . . . . . . . 17
                          |
20 | | simprr 766 |
. . . . . . . . . . . . . . . . 17
                              |
21 | 19, 20 | sseldd 3433 |
. . . . . . . . . . . . . . . 16
                              |
22 | 21 | abscld 13498 |
. . . . . . . . . . . . . . 15
                                  |
23 | | simplrl 770 |
. . . . . . . . . . . . . . 15
                          |
24 | | simprl 764 |
. . . . . . . . . . . . . . . . . . . . 21
                            |
25 | | f1ocnvfv1 6175 |
. . . . . . . . . . . . . . . . . . . . 21
       
              |
26 | 5, 24, 25 | sylancr 669 |
. . . . . . . . . . . . . . . . . . . 20
                                   |
27 | | fveq2 5865 |
. . . . . . . . . . . . . . . . . . . . . . 23
                   |
28 | | fveq2 5865 |
. . . . . . . . . . . . . . . . . . . . . . 23
                   |
29 | 27, 28 | opeq12d 4174 |
. . . . . . . . . . . . . . . . . . . . . 22
                                     |
30 | 4 | cnrecnv 13228 |
. . . . . . . . . . . . . . . . . . . . . 22
               |
31 | | opex 4664 |
. . . . . . . . . . . . . . . . . . . . . 22
                    |
32 | 29, 30, 31 | fvmpt 5948 |
. . . . . . . . . . . . . . . . . . . . 21
                                   |
33 | 21, 32 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
                                                      |
34 | 26, 33 | eqtr3d 2487 |
. . . . . . . . . . . . . . . . . . 19
                                             |
35 | 34 | fveq2d 5869 |
. . . . . . . . . . . . . . . . . 18
                                                     |
36 | | fvex 5875 |
. . . . . . . . . . . . . . . . . . 19
         |
37 | | fvex 5875 |
. . . . . . . . . . . . . . . . . . 19
         |
38 | 36, 37 | op1st 6801 |
. . . . . . . . . . . . . . . . . 18
                                |
39 | 35, 38 | syl6eq 2501 |
. . . . . . . . . . . . . . . . 17
                                      |
40 | 39 | fveq2d 5869 |
. . . . . . . . . . . . . . . 16
                                              |
41 | | absrele 13371 |
. . . . . . . . . . . . . . . . 17
                           |
42 | 21, 41 | syl 17 |
. . . . . . . . . . . . . . . 16
                                              |
43 | 40, 42 | eqbrtrd 4423 |
. . . . . . . . . . . . . . 15
                                          |
44 | | simplrr 771 |
. . . . . . . . . . . . . . . 16
                        
      |
45 | | fveq2 5865 |
. . . . . . . . . . . . . . . . . 18
                   |
46 | 45 | breq1d 4412 |
. . . . . . . . . . . . . . . . 17
         
           |
47 | 46 | rspcv 3146 |
. . . . . . . . . . . . . . . 16
      
               |
48 | 20, 44, 47 | sylc 62 |
. . . . . . . . . . . . . . 15
                                  |
49 | 14, 22, 23, 43, 48 | letrd 9792 |
. . . . . . . . . . . . . 14
                                  |
50 | 12, 23 | absled 13492 |
. . . . . . . . . . . . . 14
                                
     
        |
51 | 49, 50 | mpbid 214 |
. . . . . . . . . . . . 13
                         
           |
52 | 51 | simpld 461 |
. . . . . . . . . . . 12
                               |
53 | 51 | simprd 465 |
. . . . . . . . . . . 12
                              |
54 | | renegcl 9937 |
. . . . . . . . . . . . . 14
    |
55 | 23, 54 | syl 17 |
. . . . . . . . . . . . 13
                           |
56 | | elicc2 11699 |
. . . . . . . . . . . . 13
            ![[,] [,]](_icc.gif)       
            |
57 | 55, 23, 56 | syl2anc 667 |
. . . . . . . . . . . 12
                                ![[,] [,]](_icc.gif) 
         
        |
58 | 12, 52, 53, 57 | mpbir3and 1191 |
. . . . . . . . . . 11
                               ![[,] [,]](_icc.gif)    |
59 | | xp2nd 6824 |
. . . . . . . . . . . . 13
  
      |
60 | 59 | ad2antrl 734 |
. . . . . . . . . . . 12
                              |
61 | 60 | recnd 9669 |
. . . . . . . . . . . . . . . 16
                              |
62 | 61 | abscld 13498 |
. . . . . . . . . . . . . . 15
                                  |
63 | 34 | fveq2d 5869 |
. . . . . . . . . . . . . . . . . 18
                                                     |
64 | 36, 37 | op2nd 6802 |
. . . . . . . . . . . . . . . . . 18
                                |
65 | 63, 64 | syl6eq 2501 |
. . . . . . . . . . . . . . . . 17
                                      |
66 | 65 | fveq2d 5869 |
. . . . . . . . . . . . . . . 16
                                              |
67 | | absimle 13372 |
. . . . . . . . . . . . . . . . 17
                           |
68 | 21, 67 | syl 17 |
. . . . . . . . . . . . . . . 16
                                              |
69 | 66, 68 | eqbrtrd 4423 |
. . . . . . . . . . . . . . 15
                                          |
70 | 62, 22, 23, 69, 48 | letrd 9792 |
. . . . . . . . . . . . . 14
                                  |
71 | 60, 23 | absled 13492 |
. . . . . . . . . . . . . 14
                                
     
        |
72 | 70, 71 | mpbid 214 |
. . . . . . . . . . . . 13
                         
           |
73 | 72 | simpld 461 |
. . . . . . . . . . . 12
                               |
74 | 72 | simprd 465 |
. . . . . . . . . . . 12
                              |
75 | | elicc2 11699 |
. . . . . . . . . . . . 13
            ![[,] [,]](_icc.gif)       
            |
76 | 55, 23, 75 | syl2anc 667 |
. . . . . . . . . . . 12
                                ![[,] [,]](_icc.gif) 
         
        |
77 | 60, 73, 74, 76 | mpbir3and 1191 |
. . . . . . . . . . 11
                               ![[,] [,]](_icc.gif)    |
78 | | opelxpi 4866 |
. . . . . . . . . . 11
         ![[,] [,]](_icc.gif)         ![[,] [,]](_icc.gif)                  ![[,] [,]](_icc.gif)     ![[,] [,]](_icc.gif)     |
79 | 58, 77, 78 | syl2anc 667 |
. . . . . . . . . 10
                                       ![[,] [,]](_icc.gif)     ![[,] [,]](_icc.gif)     |
80 | 10, 79 | eqeltrd 2529 |
. . . . . . . . 9
                            ![[,] [,]](_icc.gif)     ![[,] [,]](_icc.gif)     |
81 | 80 | ex 436 |
. . . . . . . 8
      

              
    ![[,] [,]](_icc.gif)     ![[,] [,]](_icc.gif)      |
82 | 8, 81 | syl5bi 221 |
. . . . . . 7
      

                ![[,] [,]](_icc.gif)     ![[,] [,]](_icc.gif)      |
83 | 82 | ssrdv 3438 |
. . . . . 6
      

               ![[,] [,]](_icc.gif)     ![[,] [,]](_icc.gif)     |
84 | | f1ofun 5816 |
. . . . . . . 8
      
  |
85 | 5, 84 | ax-mp 5 |
. . . . . . 7
 |
86 | | f1ofo 5821 |
. . . . . . . . 9
      
        |
87 | | forn 5796 |
. . . . . . . . 9
      
  |
88 | 5, 86, 87 | mp2b 10 |
. . . . . . . 8
 |
89 | 18, 88 | syl6sseqr 3479 |
. . . . . . 7
      

        |
90 | | funimass1 5656 |
. . . . . . 7
             ![[,] [,]](_icc.gif)     ![[,] [,]](_icc.gif)          ![[,] [,]](_icc.gif)     ![[,] [,]](_icc.gif)       |
91 | 85, 89, 90 | sylancr 669 |
. . . . . 6
      

                ![[,] [,]](_icc.gif)     ![[,] [,]](_icc.gif)          ![[,] [,]](_icc.gif)     ![[,] [,]](_icc.gif)       |
92 | 83, 91 | mpd 15 |
. . . . 5
      

             ![[,] [,]](_icc.gif)     ![[,] [,]](_icc.gif)      |
93 | | cnheibor.5 |
. . . . 5
       ![[,] [,]](_icc.gif)     ![[,] [,]](_icc.gif)     |
94 | 92, 93 | syl6sseqr 3479 |
. . . 4
      

        |
95 | | eqid 2451 |
. . . . . . . 8
         |
96 | 4, 95, 1 | cnrehmeo 21981 |
. . . . . . 7
        
      |
97 | | imaexg 6730 |
. . . . . . 7
                      ![[,] [,]](_icc.gif)     ![[,] [,]](_icc.gif)      |
98 | 96, 97 | ax-mp 5 |
. . . . . 6
       ![[,] [,]](_icc.gif)     ![[,] [,]](_icc.gif)     |
99 | 93, 98 | eqeltri 2525 |
. . . . 5
 |
100 | 99 | a1i 11 |
. . . 4
      

     
  |
101 | | restabs 20181 |
. . . 4
    
↾t 
↾t   ↾t    |
102 | 3, 94, 100, 101 | syl3anc 1268 |
. . 3
      

        ↾t  ↾t   ↾t    |
103 | | cnheibor.3 |
. . 3

↾t   |
104 | 102, 103 | syl6eqr 2503 |
. 2
      

        ↾t  ↾t    |
105 | 93 | oveq2i 6301 |
. . . . 5
 ↾t   ↾t        ![[,] [,]](_icc.gif)     ![[,] [,]](_icc.gif)      |
106 | | ishmeo 20774 |
. . . . . . . 8
              
         
                   |
107 | 96, 106 | mpbi 212 |
. . . . . . 7
                            |
108 | 107 | simpli 460 |
. . . . . 6
        
    |
109 | | iccssre 11716 |
. . . . . . . . . . 11
       ![[,] [,]](_icc.gif)    |
110 | 54, 109 | mpancom 675 |
. . . . . . . . . 10
    ![[,] [,]](_icc.gif)    |
111 | 1, 95 | rerest 21822 |
. . . . . . . . . 10
    ![[,] [,]](_icc.gif) 
 ↾t    ![[,] [,]](_icc.gif)        ↾t    ![[,] [,]](_icc.gif)     |
112 | 110, 111 | syl 17 |
. . . . . . . . 9
  ↾t    ![[,] [,]](_icc.gif)        ↾t    ![[,] [,]](_icc.gif)     |
113 | 112, 112 | oveq12d 6308 |
. . . . . . . 8
  
↾t    ![[,] [,]](_icc.gif)   
↾t    ![[,] [,]](_icc.gif)          ↾t    ![[,] [,]](_icc.gif)        ↾t    ![[,] [,]](_icc.gif)      |
114 | | retop 21782 |
. . . . . . . . 9
     |
115 | | ovex 6318 |
. . . . . . . . 9
   ![[,] [,]](_icc.gif)   |
116 | | txrest 20646 |
. . . . . . . . 9
                ![[,] [,]](_icc.gif)     ![[,] [,]](_icc.gif)   
           ↾t     ![[,] [,]](_icc.gif)     ![[,] [,]](_icc.gif)          ↾t    ![[,] [,]](_icc.gif)        ↾t    ![[,] [,]](_icc.gif)      |
117 | 114, 114,
115, 115, 116 | mp4an 679 |
. . . . . . . 8
           ↾t     ![[,] [,]](_icc.gif)     ![[,] [,]](_icc.gif)          ↾t    ![[,] [,]](_icc.gif)        ↾t    ![[,] [,]](_icc.gif)     |
118 | 113, 117 | syl6eqr 2503 |
. . . . . . 7
  
↾t    ![[,] [,]](_icc.gif)   
↾t    ![[,] [,]](_icc.gif)               ↾t     ![[,] [,]](_icc.gif)     ![[,] [,]](_icc.gif)      |
119 | | eqid 2451 |
. . . . . . . . . . 11
     ↾t    ![[,] [,]](_icc.gif)        ↾t    ![[,] [,]](_icc.gif)    |
120 | 95, 119 | icccmp 21843 |
. . . . . . . . . 10
        
↾t    ![[,] [,]](_icc.gif)     |
121 | 54, 120 | mpancom 675 |
. . . . . . . . 9
      ↾t    ![[,] [,]](_icc.gif)     |
122 | 112, 121 | eqeltrd 2529 |
. . . . . . . 8
  ↾t    ![[,] [,]](_icc.gif)     |
123 | | txcmp 20658 |
. . . . . . . 8
  
↾t    ![[,] [,]](_icc.gif)    ↾t    ![[,] [,]](_icc.gif)     
↾t    ![[,] [,]](_icc.gif)   
↾t    ![[,] [,]](_icc.gif)      |
124 | 122, 122,
123 | syl2anc 667 |
. . . . . . 7
  
↾t    ![[,] [,]](_icc.gif)   
↾t    ![[,] [,]](_icc.gif)      |
125 | 118, 124 | eqeltrrd 2530 |
. . . . . 6
            ↾t     ![[,] [,]](_icc.gif)     ![[,] [,]](_icc.gif)      |
126 | | imacmp 20412 |
. . . . . 6
                         ↾t     ![[,] [,]](_icc.gif)     ![[,] [,]](_icc.gif)      ↾t        ![[,] [,]](_icc.gif)     ![[,] [,]](_icc.gif)       |
127 | 108, 125,
126 | sylancr 669 |
. . . . 5
  ↾t        ![[,] [,]](_icc.gif)     ![[,] [,]](_icc.gif)       |
128 | 105, 127 | syl5eqel 2533 |
. . . 4
  ↾t    |
129 | 128 | ad2antrl 734 |
. . 3
      

      
↾t    |
130 | | imassrn 5179 |
. . . . . . 7
       ![[,] [,]](_icc.gif)     ![[,] [,]](_icc.gif)   
 |
131 | 93, 130 | eqsstri 3462 |
. . . . . 6
 |
132 | | f1of 5814 |
. . . . . . 7
      
        |
133 | | frn 5735 |
. . . . . . 7
         |
134 | 5, 132, 133 | mp2b 10 |
. . . . . 6
 |
135 | 131, 134 | sstri 3441 |
. . . . 5
 |
136 | 135 | a1i 11 |
. . . 4
      

        |
137 | | simpl 459 |
. . . 4
      

     
      |
138 | 16 | restcldi 20189 |
. . . 4
 
   

    ↾t     |
139 | 136, 137,
94, 138 | syl3anc 1268 |
. . 3
      

     
   
↾t     |
140 | | cmpcld 20417 |
. . 3
  
↾t     
↾t      ↾t  ↾t    |
141 | 129, 139,
140 | syl2anc 667 |
. 2
      

        ↾t  ↾t    |
142 | 104, 141 | eqeltrrd 2530 |
1
      

     
  |