Step |
Hyp |
Ref |
Expression |
1 |
|
dvlog2.s |
|- S = ( 1 ( ball ` ( abs o. - ) ) 1 ) |
2 |
|
ssid |
|- CC C_ CC |
3 |
|
logf1o |
|- log : ( CC \ { 0 } ) -1-1-onto-> ran log |
4 |
|
f1of |
|- ( log : ( CC \ { 0 } ) -1-1-onto-> ran log -> log : ( CC \ { 0 } ) --> ran log ) |
5 |
3 4
|
ax-mp |
|- log : ( CC \ { 0 } ) --> ran log |
6 |
|
logrncn |
|- ( x e. ran log -> x e. CC ) |
7 |
6
|
ssriv |
|- ran log C_ CC |
8 |
|
fss |
|- ( ( log : ( CC \ { 0 } ) --> ran log /\ ran log C_ CC ) -> log : ( CC \ { 0 } ) --> CC ) |
9 |
5 7 8
|
mp2an |
|- log : ( CC \ { 0 } ) --> CC |
10 |
|
eqid |
|- ( CC \ ( -oo (,] 0 ) ) = ( CC \ ( -oo (,] 0 ) ) |
11 |
10
|
logdmss |
|- ( CC \ ( -oo (,] 0 ) ) C_ ( CC \ { 0 } ) |
12 |
|
fssres |
|- ( ( log : ( CC \ { 0 } ) --> CC /\ ( CC \ ( -oo (,] 0 ) ) C_ ( CC \ { 0 } ) ) -> ( log |` ( CC \ ( -oo (,] 0 ) ) ) : ( CC \ ( -oo (,] 0 ) ) --> CC ) |
13 |
9 11 12
|
mp2an |
|- ( log |` ( CC \ ( -oo (,] 0 ) ) ) : ( CC \ ( -oo (,] 0 ) ) --> CC |
14 |
|
difss |
|- ( CC \ ( -oo (,] 0 ) ) C_ CC |
15 |
|
cnxmet |
|- ( abs o. - ) e. ( *Met ` CC ) |
16 |
|
ax-1cn |
|- 1 e. CC |
17 |
|
1xr |
|- 1 e. RR* |
18 |
|
blssm |
|- ( ( ( abs o. - ) e. ( *Met ` CC ) /\ 1 e. CC /\ 1 e. RR* ) -> ( 1 ( ball ` ( abs o. - ) ) 1 ) C_ CC ) |
19 |
15 16 17 18
|
mp3an |
|- ( 1 ( ball ` ( abs o. - ) ) 1 ) C_ CC |
20 |
1 19
|
eqsstri |
|- S C_ CC |
21 |
|
eqid |
|- ( TopOpen ` CCfld ) = ( TopOpen ` CCfld ) |
22 |
21
|
cnfldtopon |
|- ( TopOpen ` CCfld ) e. ( TopOn ` CC ) |
23 |
22
|
toponrestid |
|- ( TopOpen ` CCfld ) = ( ( TopOpen ` CCfld ) |`t CC ) |
24 |
21 23
|
dvres |
|- ( ( ( CC C_ CC /\ ( log |` ( CC \ ( -oo (,] 0 ) ) ) : ( CC \ ( -oo (,] 0 ) ) --> CC ) /\ ( ( CC \ ( -oo (,] 0 ) ) C_ CC /\ S C_ CC ) ) -> ( CC _D ( ( log |` ( CC \ ( -oo (,] 0 ) ) ) |` S ) ) = ( ( CC _D ( log |` ( CC \ ( -oo (,] 0 ) ) ) ) |` ( ( int ` ( TopOpen ` CCfld ) ) ` S ) ) ) |
25 |
2 13 14 20 24
|
mp4an |
|- ( CC _D ( ( log |` ( CC \ ( -oo (,] 0 ) ) ) |` S ) ) = ( ( CC _D ( log |` ( CC \ ( -oo (,] 0 ) ) ) ) |` ( ( int ` ( TopOpen ` CCfld ) ) ` S ) ) |
26 |
1
|
dvlog2lem |
|- S C_ ( CC \ ( -oo (,] 0 ) ) |
27 |
|
resabs1 |
|- ( S C_ ( CC \ ( -oo (,] 0 ) ) -> ( ( log |` ( CC \ ( -oo (,] 0 ) ) ) |` S ) = ( log |` S ) ) |
28 |
26 27
|
ax-mp |
|- ( ( log |` ( CC \ ( -oo (,] 0 ) ) ) |` S ) = ( log |` S ) |
29 |
28
|
oveq2i |
|- ( CC _D ( ( log |` ( CC \ ( -oo (,] 0 ) ) ) |` S ) ) = ( CC _D ( log |` S ) ) |
30 |
10
|
dvlog |
|- ( CC _D ( log |` ( CC \ ( -oo (,] 0 ) ) ) ) = ( x e. ( CC \ ( -oo (,] 0 ) ) |-> ( 1 / x ) ) |
31 |
21
|
cnfldtop |
|- ( TopOpen ` CCfld ) e. Top |
32 |
21
|
cnfldtopn |
|- ( TopOpen ` CCfld ) = ( MetOpen ` ( abs o. - ) ) |
33 |
32
|
blopn |
|- ( ( ( abs o. - ) e. ( *Met ` CC ) /\ 1 e. CC /\ 1 e. RR* ) -> ( 1 ( ball ` ( abs o. - ) ) 1 ) e. ( TopOpen ` CCfld ) ) |
34 |
15 16 17 33
|
mp3an |
|- ( 1 ( ball ` ( abs o. - ) ) 1 ) e. ( TopOpen ` CCfld ) |
35 |
1 34
|
eqeltri |
|- S e. ( TopOpen ` CCfld ) |
36 |
|
isopn3i |
|- ( ( ( TopOpen ` CCfld ) e. Top /\ S e. ( TopOpen ` CCfld ) ) -> ( ( int ` ( TopOpen ` CCfld ) ) ` S ) = S ) |
37 |
31 35 36
|
mp2an |
|- ( ( int ` ( TopOpen ` CCfld ) ) ` S ) = S |
38 |
30 37
|
reseq12i |
|- ( ( CC _D ( log |` ( CC \ ( -oo (,] 0 ) ) ) ) |` ( ( int ` ( TopOpen ` CCfld ) ) ` S ) ) = ( ( x e. ( CC \ ( -oo (,] 0 ) ) |-> ( 1 / x ) ) |` S ) |
39 |
25 29 38
|
3eqtr3i |
|- ( CC _D ( log |` S ) ) = ( ( x e. ( CC \ ( -oo (,] 0 ) ) |-> ( 1 / x ) ) |` S ) |
40 |
|
resmpt |
|- ( S C_ ( CC \ ( -oo (,] 0 ) ) -> ( ( x e. ( CC \ ( -oo (,] 0 ) ) |-> ( 1 / x ) ) |` S ) = ( x e. S |-> ( 1 / x ) ) ) |
41 |
26 40
|
ax-mp |
|- ( ( x e. ( CC \ ( -oo (,] 0 ) ) |-> ( 1 / x ) ) |` S ) = ( x e. S |-> ( 1 / x ) ) |
42 |
39 41
|
eqtri |
|- ( CC _D ( log |` S ) ) = ( x e. S |-> ( 1 / x ) ) |