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 ⊢ 𝐶 = ( IndMet ‘ 𝑈 )
smcn.j ⊢ 𝐽 = ( MetOpen ‘ 𝐶 )
smcn.s ⊢ 𝑆 = ( ·𝑠OLD ‘ 𝑈 )
smcn.k ⊢ 𝐾 = ( TopOpen ‘ ℂfld )
Assertion smcn ( 𝑈 ∈ NrmCVec → 𝑆 ∈ ( ( 𝐾 ×t 𝐽 ) Cn 𝐽 ) )

Proof

Step Hyp Ref Expression
1 smcn.c ⊢ 𝐶 = ( IndMet ‘ 𝑈 )
2 smcn.j ⊢ 𝐽 = ( MetOpen ‘ 𝐶 )
3 smcn.s ⊢ 𝑆 = ( ·𝑠OLD ‘ 𝑈 )
4 smcn.k ⊢ 𝐾 = ( TopOpen ‘ ℂfld )
5 fveq2 ⊢ ( 𝑈 = if ( 𝑈 ∈ NrmCVec , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) → ( ·𝑠OLD ‘ 𝑈 ) = ( ·𝑠OLD ‘ if ( 𝑈 ∈ NrmCVec , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) )
6 3 5 eqtrid ⊢ ( 𝑈 = if ( 𝑈 ∈ NrmCVec , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) → 𝑆 = ( ·𝑠OLD ‘ if ( 𝑈 ∈ NrmCVec , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) )
7 fveq2 ⊢ ( 𝑈 = if ( 𝑈 ∈ NrmCVec , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) → ( IndMet ‘ 𝑈 ) = ( IndMet ‘ if ( 𝑈 ∈ NrmCVec , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) )
8 1 7 eqtrid ⊢ ( 𝑈 = if ( 𝑈 ∈ NrmCVec , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) → 𝐶 = ( IndMet ‘ if ( 𝑈 ∈ NrmCVec , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) )
9 8 fveq2d ⊢ ( 𝑈 = if ( 𝑈 ∈ NrmCVec , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) → ( MetOpen ‘ 𝐶 ) = ( MetOpen ‘ ( IndMet ‘ if ( 𝑈 ∈ NrmCVec , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) ) )
10 2 9 eqtrid ⊢ ( 𝑈 = if ( 𝑈 ∈ NrmCVec , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) → 𝐽 = ( MetOpen ‘ ( IndMet ‘ if ( 𝑈 ∈ NrmCVec , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) ) )
11 10 oveq2d ⊢ ( 𝑈 = if ( 𝑈 ∈ NrmCVec , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) → ( 𝐾 ×t 𝐽 ) = ( 𝐾 ×t ( MetOpen ‘ ( IndMet ‘ if ( 𝑈 ∈ NrmCVec , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) ) ) )
12 11 10 oveq12d ⊢ ( 𝑈 = if ( 𝑈 ∈ NrmCVec , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) → ( ( 𝐾 ×t 𝐽 ) Cn 𝐽 ) = ( ( 𝐾 ×t ( MetOpen ‘ ( IndMet ‘ if ( 𝑈 ∈ NrmCVec , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) ) ) Cn ( MetOpen ‘ ( IndMet ‘ if ( 𝑈 ∈ NrmCVec , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) ) ) )
13 6 12 eleq12d ⊢ ( 𝑈 = if ( 𝑈 ∈ NrmCVec , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) → ( 𝑆 ∈ ( ( 𝐾 ×t 𝐽 ) Cn 𝐽 ) ↔ ( ·𝑠OLD ‘ if ( 𝑈 ∈ NrmCVec , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) ∈ ( ( 𝐾 ×t ( MetOpen ‘ ( IndMet ‘ if ( 𝑈 ∈ NrmCVec , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) ) ) Cn ( MetOpen ‘ ( IndMet ‘ if ( 𝑈 ∈ NrmCVec , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) ) ) ) )
14 eqid ⊢ ( IndMet ‘ if ( 𝑈 ∈ NrmCVec , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) = ( IndMet ‘ if ( 𝑈 ∈ NrmCVec , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) )
15 eqid ⊢ ( MetOpen ‘ ( IndMet ‘ if ( 𝑈 ∈ NrmCVec , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) ) = ( MetOpen ‘ ( IndMet ‘ if ( 𝑈 ∈ NrmCVec , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) )
16 eqid ⊢ ( ·𝑠OLD ‘ if ( 𝑈 ∈ NrmCVec , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) = ( ·𝑠OLD ‘ if ( 𝑈 ∈ NrmCVec , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) )
17 eqid ⊢ ( BaseSet ‘ if ( 𝑈 ∈ NrmCVec , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) = ( BaseSet ‘ if ( 𝑈 ∈ NrmCVec , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) )
18 eqid ⊢ ( normCV ‘ if ( 𝑈 ∈ NrmCVec , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) = ( normCV ‘ if ( 𝑈 ∈ NrmCVec , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) )
19 elimnvu ⊢ if ( 𝑈 ∈ NrmCVec , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ∈ NrmCVec
20 eqid ⊢ ( 1 / ( 1 + ( ( ( ( ( normCV ‘ if ( 𝑈 ∈ NrmCVec , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) ‘ 𝑦 ) + ( abs ‘ 𝑥 ) ) + 1 ) / 𝑟 ) ) ) = ( 1 / ( 1 + ( ( ( ( ( normCV ‘ if ( 𝑈 ∈ NrmCVec , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) ‘ 𝑦 ) + ( abs ‘ 𝑥 ) ) + 1 ) / 𝑟 ) ) )
21 14 15 16 4 17 18 19 20 smcnlem ⊢ ( ·𝑠OLD ‘ if ( 𝑈 ∈ NrmCVec , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) ∈ ( ( 𝐾 ×t ( MetOpen ‘ ( IndMet ‘ if ( 𝑈 ∈ NrmCVec , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) ) ) Cn ( MetOpen ‘ ( IndMet ‘ if ( 𝑈 ∈ NrmCVec , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) ) )
22 13 21 dedth ⊢ ( 𝑈 ∈ NrmCVec → 𝑆 ∈ ( ( 𝐾 ×t 𝐽 ) Cn 𝐽 ) )