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