Step | Hyp | Ref
| Expression |
1 | | cnheibor.2 |
. . . . 5
ℂfld |
2 | 1 | cnfldtop 22587 |
. . . 4
|
3 | | cnheibor.4 |
. . . . . . . . . 10
|
4 | 3 | cnref1o 11827 |
. . . . . . . . 9
|
5 | | f1ofn 6138 |
. . . . . . . . 9
|
6 | | elpreima 6337 |
. . . . . . . . 9
|
7 | 4, 5, 6 | mp2b 10 |
. . . . . . . 8
|
8 | | 1st2nd2 7205 |
. . . . . . . . . . 11
|
9 | 8 | ad2antrl 764 |
. . . . . . . . . 10
|
10 | | xp1st 7198 |
. . . . . . . . . . . . 13
|
11 | 10 | ad2antrl 764 |
. . . . . . . . . . . 12
|
12 | 11 | recnd 10068 |
. . . . . . . . . . . . . . . 16
|
13 | 12 | abscld 14175 |
. . . . . . . . . . . . . . 15
|
14 | 1 | cnfldtopon 22586 |
. . . . . . . . . . . . . . . . . . . . 21
TopOn |
15 | 14 | toponunii 20721 |
. . . . . . . . . . . . . . . . . . . 20
|
16 | 15 | cldss 20833 |
. . . . . . . . . . . . . . . . . . 19
|
17 | 16 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
|
18 | 17 | adantr 481 |
. . . . . . . . . . . . . . . . 17
|
19 | | simprr 796 |
. . . . . . . . . . . . . . . . 17
|
20 | 18, 19 | sseldd 3604 |
. . . . . . . . . . . . . . . 16
|
21 | 20 | abscld 14175 |
. . . . . . . . . . . . . . 15
|
22 | | simplrl 800 |
. . . . . . . . . . . . . . 15
|
23 | | simprl 794 |
. . . . . . . . . . . . . . . . . . . . 21
|
24 | | f1ocnvfv1 6532 |
. . . . . . . . . . . . . . . . . . . . 21
|
25 | 4, 23, 24 | sylancr 695 |
. . . . . . . . . . . . . . . . . . . 20
|
26 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
27 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
28 | 26, 27 | opeq12d 4410 |
. . . . . . . . . . . . . . . . . . . . . 22
|
29 | 3 | cnrecnv 13905 |
. . . . . . . . . . . . . . . . . . . . . 22
|
30 | | opex 4932 |
. . . . . . . . . . . . . . . . . . . . . 22
|
31 | 28, 29, 30 | fvmpt 6282 |
. . . . . . . . . . . . . . . . . . . . 21
|
32 | 20, 31 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
|
33 | 25, 32 | eqtr3d 2658 |
. . . . . . . . . . . . . . . . . . 19
|
34 | 33 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . 18
|
35 | | fvex 6201 |
. . . . . . . . . . . . . . . . . . 19
|
36 | | fvex 6201 |
. . . . . . . . . . . . . . . . . . 19
|
37 | 35, 36 | op1st 7176 |
. . . . . . . . . . . . . . . . . 18
|
38 | 34, 37 | syl6eq 2672 |
. . . . . . . . . . . . . . . . 17
|
39 | 38 | fveq2d 6195 |
. . . . . . . . . . . . . . . 16
|
40 | | absrele 14048 |
. . . . . . . . . . . . . . . . 17
|
41 | 20, 40 | syl 17 |
. . . . . . . . . . . . . . . 16
|
42 | 39, 41 | eqbrtrd 4675 |
. . . . . . . . . . . . . . 15
|
43 | | simplrr 801 |
. . . . . . . . . . . . . . . 16
|
44 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . 18
|
45 | 44 | breq1d 4663 |
. . . . . . . . . . . . . . . . 17
|
46 | 45 | rspcv 3305 |
. . . . . . . . . . . . . . . 16
|
47 | 19, 43, 46 | sylc 65 |
. . . . . . . . . . . . . . 15
|
48 | 13, 21, 22, 42, 47 | letrd 10194 |
. . . . . . . . . . . . . 14
|
49 | 11, 22 | absled 14169 |
. . . . . . . . . . . . . 14
|
50 | 48, 49 | mpbid 222 |
. . . . . . . . . . . . 13
|
51 | 50 | simpld 475 |
. . . . . . . . . . . 12
|
52 | 50 | simprd 479 |
. . . . . . . . . . . 12
|
53 | | renegcl 10344 |
. . . . . . . . . . . . . 14
|
54 | 22, 53 | syl 17 |
. . . . . . . . . . . . 13
|
55 | | elicc2 12238 |
. . . . . . . . . . . . 13
|
56 | 54, 22, 55 | syl2anc 693 |
. . . . . . . . . . . 12
|
57 | 11, 51, 52, 56 | mpbir3and 1245 |
. . . . . . . . . . 11
|
58 | | xp2nd 7199 |
. . . . . . . . . . . . 13
|
59 | 58 | ad2antrl 764 |
. . . . . . . . . . . 12
|
60 | 59 | recnd 10068 |
. . . . . . . . . . . . . . . 16
|
61 | 60 | abscld 14175 |
. . . . . . . . . . . . . . 15
|
62 | 33 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . 18
|
63 | 35, 36 | op2nd 7177 |
. . . . . . . . . . . . . . . . . 18
|
64 | 62, 63 | syl6eq 2672 |
. . . . . . . . . . . . . . . . 17
|
65 | 64 | fveq2d 6195 |
. . . . . . . . . . . . . . . 16
|
66 | | absimle 14049 |
. . . . . . . . . . . . . . . . 17
|
67 | 20, 66 | syl 17 |
. . . . . . . . . . . . . . . 16
|
68 | 65, 67 | eqbrtrd 4675 |
. . . . . . . . . . . . . . 15
|
69 | 61, 21, 22, 68, 47 | letrd 10194 |
. . . . . . . . . . . . . 14
|
70 | 59, 22 | absled 14169 |
. . . . . . . . . . . . . 14
|
71 | 69, 70 | mpbid 222 |
. . . . . . . . . . . . 13
|
72 | 71 | simpld 475 |
. . . . . . . . . . . 12
|
73 | 71 | simprd 479 |
. . . . . . . . . . . 12
|
74 | | elicc2 12238 |
. . . . . . . . . . . . 13
|
75 | 54, 22, 74 | syl2anc 693 |
. . . . . . . . . . . 12
|
76 | 59, 72, 73, 75 | mpbir3and 1245 |
. . . . . . . . . . 11
|
77 | 57, 76 | opelxpd 5149 |
. . . . . . . . . 10
|
78 | 9, 77 | eqeltrd 2701 |
. . . . . . . . 9
|
79 | 78 | ex 450 |
. . . . . . . 8
|
80 | 7, 79 | syl5bi 232 |
. . . . . . 7
|
81 | 80 | ssrdv 3609 |
. . . . . 6
|
82 | | f1ofun 6139 |
. . . . . . . 8
|
83 | 4, 82 | ax-mp 5 |
. . . . . . 7
|
84 | | f1ofo 6144 |
. . . . . . . . 9
|
85 | | forn 6118 |
. . . . . . . . 9
|
86 | 4, 84, 85 | mp2b 10 |
. . . . . . . 8
|
87 | 17, 86 | syl6sseqr 3652 |
. . . . . . 7
|
88 | | funimass1 5971 |
. . . . . . 7
|
89 | 83, 87, 88 | sylancr 695 |
. . . . . 6
|
90 | 81, 89 | mpd 15 |
. . . . 5
|
91 | | cnheibor.5 |
. . . . 5
|
92 | 90, 91 | syl6sseqr 3652 |
. . . 4
|
93 | | eqid 2622 |
. . . . . . . 8
|
94 | 3, 93, 1 | cnrehmeo 22752 |
. . . . . . 7
|
95 | | imaexg 7103 |
. . . . . . 7
|
96 | 94, 95 | ax-mp 5 |
. . . . . 6
|
97 | 91, 96 | eqeltri 2697 |
. . . . 5
|
98 | 97 | a1i 11 |
. . . 4
|
99 | | restabs 20969 |
. . . 4
↾t
↾t ↾t |
100 | 2, 92, 98, 99 | mp3an2i 1429 |
. . 3
↾t ↾t ↾t |
101 | | cnheibor.3 |
. . 3
↾t |
102 | 100, 101 | syl6eqr 2674 |
. 2
↾t ↾t |
103 | 91 | oveq2i 6661 |
. . . . 5
↾t ↾t |
104 | | ishmeo 21562 |
. . . . . . . 8
|
105 | 94, 104 | mpbi 220 |
. . . . . . 7
|
106 | 105 | simpli 474 |
. . . . . 6
|
107 | | iccssre 12255 |
. . . . . . . . . . 11
|
108 | 53, 107 | mpancom 703 |
. . . . . . . . . 10
|
109 | 1, 93 | rerest 22607 |
. . . . . . . . . 10
↾t ↾t |
110 | 108, 109 | syl 17 |
. . . . . . . . 9
↾t ↾t |
111 | 110, 110 | oveq12d 6668 |
. . . . . . . 8
↾t
↾t ↾t ↾t |
112 | | retop 22565 |
. . . . . . . . 9
|
113 | | ovex 6678 |
. . . . . . . . 9
|
114 | | txrest 21434 |
. . . . . . . . 9
↾t ↾t ↾t |
115 | 112, 112,
113, 113, 114 | mp4an 709 |
. . . . . . . 8
↾t ↾t ↾t |
116 | 111, 115 | syl6eqr 2674 |
. . . . . . 7
↾t
↾t ↾t |
117 | | eqid 2622 |
. . . . . . . . . . 11
↾t ↾t |
118 | 93, 117 | icccmp 22628 |
. . . . . . . . . 10
↾t |
119 | 53, 118 | mpancom 703 |
. . . . . . . . 9
↾t |
120 | 110, 119 | eqeltrd 2701 |
. . . . . . . 8
↾t |
121 | | txcmp 21446 |
. . . . . . . 8
↾t ↾t
↾t
↾t |
122 | 120, 120,
121 | syl2anc 693 |
. . . . . . 7
↾t
↾t |
123 | 116, 122 | eqeltrrd 2702 |
. . . . . 6
↾t |
124 | | imacmp 21200 |
. . . . . 6
↾t ↾t |
125 | 106, 123,
124 | sylancr 695 |
. . . . 5
↾t |
126 | 103, 125 | syl5eqel 2705 |
. . . 4
↾t |
127 | 126 | ad2antrl 764 |
. . 3
↾t |
128 | | imassrn 5477 |
. . . . . 6
|
129 | 91, 128 | eqsstri 3635 |
. . . . 5
|
130 | | f1of 6137 |
. . . . . 6
|
131 | | frn 6053 |
. . . . . 6
|
132 | 4, 130, 131 | mp2b 10 |
. . . . 5
|
133 | 129, 132 | sstri 3612 |
. . . 4
|
134 | | simpl 473 |
. . . 4
|
135 | 15 | restcldi 20977 |
. . . 4
↾t |
136 | 133, 134,
92, 135 | mp3an2i 1429 |
. . 3
↾t |
137 | | cmpcld 21205 |
. . 3
↾t
↾t ↾t ↾t |
138 | 127, 136,
137 | syl2anc 693 |
. 2
↾t ↾t |
139 | 102, 138 | eqeltrrd 2702 |
1
|