Step |
Hyp |
Ref |
Expression |
1 |
|
smcn.c |
|- C = ( IndMet ` U ) |
2 |
|
smcn.j |
|- J = ( MetOpen ` C ) |
3 |
|
smcn.s |
|- S = ( .sOLD ` U ) |
4 |
|
smcn.k |
|- K = ( TopOpen ` CCfld ) |
5 |
|
fveq2 |
|- ( U = if ( U e. NrmCVec , U , <. <. + , x. >. , abs >. ) -> ( .sOLD ` U ) = ( .sOLD ` if ( U e. NrmCVec , U , <. <. + , x. >. , abs >. ) ) ) |
6 |
3 5
|
syl5eq |
|- ( U = if ( U e. NrmCVec , U , <. <. + , x. >. , abs >. ) -> S = ( .sOLD ` if ( U e. NrmCVec , U , <. <. + , x. >. , abs >. ) ) ) |
7 |
|
fveq2 |
|- ( U = if ( U e. NrmCVec , U , <. <. + , x. >. , abs >. ) -> ( IndMet ` U ) = ( IndMet ` if ( U e. NrmCVec , U , <. <. + , x. >. , abs >. ) ) ) |
8 |
1 7
|
syl5eq |
|- ( U = if ( U e. NrmCVec , U , <. <. + , x. >. , abs >. ) -> C = ( IndMet ` if ( U e. NrmCVec , U , <. <. + , x. >. , abs >. ) ) ) |
9 |
8
|
fveq2d |
|- ( U = if ( U e. NrmCVec , U , <. <. + , x. >. , abs >. ) -> ( MetOpen ` C ) = ( MetOpen ` ( IndMet ` if ( U e. NrmCVec , U , <. <. + , x. >. , abs >. ) ) ) ) |
10 |
2 9
|
syl5eq |
|- ( U = if ( U e. NrmCVec , U , <. <. + , x. >. , abs >. ) -> J = ( MetOpen ` ( IndMet ` if ( U e. NrmCVec , U , <. <. + , x. >. , abs >. ) ) ) ) |
11 |
10
|
oveq2d |
|- ( U = if ( U e. NrmCVec , U , <. <. + , x. >. , abs >. ) -> ( K tX J ) = ( K tX ( MetOpen ` ( IndMet ` if ( U e. NrmCVec , U , <. <. + , x. >. , abs >. ) ) ) ) ) |
12 |
11 10
|
oveq12d |
|- ( U = if ( U e. NrmCVec , U , <. <. + , x. >. , abs >. ) -> ( ( K tX J ) Cn J ) = ( ( K tX ( MetOpen ` ( IndMet ` if ( U e. NrmCVec , U , <. <. + , x. >. , abs >. ) ) ) ) Cn ( MetOpen ` ( IndMet ` if ( U e. NrmCVec , U , <. <. + , x. >. , abs >. ) ) ) ) ) |
13 |
6 12
|
eleq12d |
|- ( U = if ( U e. NrmCVec , U , <. <. + , x. >. , abs >. ) -> ( S e. ( ( K tX J ) Cn J ) <-> ( .sOLD ` if ( U e. NrmCVec , U , <. <. + , x. >. , abs >. ) ) e. ( ( K tX ( MetOpen ` ( IndMet ` if ( U e. NrmCVec , U , <. <. + , x. >. , abs >. ) ) ) ) Cn ( MetOpen ` ( IndMet ` if ( U e. NrmCVec , U , <. <. + , x. >. , abs >. ) ) ) ) ) ) |
14 |
|
eqid |
|- ( IndMet ` if ( U e. NrmCVec , U , <. <. + , x. >. , abs >. ) ) = ( IndMet ` if ( U e. NrmCVec , U , <. <. + , x. >. , abs >. ) ) |
15 |
|
eqid |
|- ( MetOpen ` ( IndMet ` if ( U e. NrmCVec , U , <. <. + , x. >. , abs >. ) ) ) = ( MetOpen ` ( IndMet ` if ( U e. NrmCVec , U , <. <. + , x. >. , abs >. ) ) ) |
16 |
|
eqid |
|- ( .sOLD ` if ( U e. NrmCVec , U , <. <. + , x. >. , abs >. ) ) = ( .sOLD ` if ( U e. NrmCVec , U , <. <. + , x. >. , abs >. ) ) |
17 |
|
eqid |
|- ( BaseSet ` if ( U e. NrmCVec , U , <. <. + , x. >. , abs >. ) ) = ( BaseSet ` if ( U e. NrmCVec , U , <. <. + , x. >. , abs >. ) ) |
18 |
|
eqid |
|- ( normCV ` if ( U e. NrmCVec , U , <. <. + , x. >. , abs >. ) ) = ( normCV ` if ( U e. NrmCVec , U , <. <. + , x. >. , abs >. ) ) |
19 |
|
elimnvu |
|- if ( U e. NrmCVec , U , <. <. + , x. >. , abs >. ) e. NrmCVec |
20 |
|
eqid |
|- ( 1 / ( 1 + ( ( ( ( ( normCV ` if ( U e. NrmCVec , U , <. <. + , x. >. , abs >. ) ) ` y ) + ( abs ` x ) ) + 1 ) / r ) ) ) = ( 1 / ( 1 + ( ( ( ( ( normCV ` if ( U e. NrmCVec , U , <. <. + , x. >. , abs >. ) ) ` y ) + ( abs ` x ) ) + 1 ) / r ) ) ) |
21 |
14 15 16 4 17 18 19 20
|
smcnlem |
|- ( .sOLD ` if ( U e. NrmCVec , U , <. <. + , x. >. , abs >. ) ) e. ( ( K tX ( MetOpen ` ( IndMet ` if ( U e. NrmCVec , U , <. <. + , x. >. , abs >. ) ) ) ) Cn ( MetOpen ` ( IndMet ` if ( U e. NrmCVec , U , <. <. + , x. >. , abs >. ) ) ) ) |
22 |
13 21
|
dedth |
|- ( U e. NrmCVec -> S e. ( ( K tX J ) Cn J ) ) |