Metamath Proof Explorer

Theorem smcn

Description: Scalar multiplication is jointly continuous in both arguments. (Contributed by NM, 16-Jun-2009) (Revised by Mario Carneiro, 5-May-2014) (New usage is discouraged.)

Ref Expression
Hypotheses smcn.c 
|- C = ( IndMet ` U )
smcn.j 
|- J = ( MetOpen ` C )
smcn.s 
|- S = ( .sOLD ` U )
smcn.k 
|- K = ( TopOpen ` CCfld )
Assertion smcn 
|- ( U e. NrmCVec -> S e. ( ( K tX J ) Cn J ) )

Proof

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 eqtrid 
 |-  ( 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 eqtrid 
 |-  ( 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 eqtrid 
 |-  ( 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 ) )