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=⋅𝑠OLD⁡U
smcn.k ⊢K=TopOpen⁡ℂfld
Assertion smcn ⊢U∈NrmCVec→S∈K×tJCnJ

Proof

Step Hyp Ref Expression
1 smcn.c ⊢C=IndMet⁡U
2 smcn.j ⊢J=MetOpen⁡C
3 smcn.s ⊢S=⋅𝑠OLD⁡U
4 smcn.k ⊢K=TopOpen⁡ℂfld
5 fveq2 ⊢U=ifU∈NrmCVecU+×abs→⋅𝑠OLD⁡U=⋅𝑠OLD⁡ifU∈NrmCVecU+×abs
6 3 5 eqtrid ⊢U=ifU∈NrmCVecU+×abs→S=⋅𝑠OLD⁡ifU∈NrmCVecU+×abs
7 fveq2 ⊢U=ifU∈NrmCVecU+×abs→IndMet⁡U=IndMet⁡ifU∈NrmCVecU+×abs
8 1 7 eqtrid ⊢U=ifU∈NrmCVecU+×abs→C=IndMet⁡ifU∈NrmCVecU+×abs
9 8 fveq2d ⊢U=ifU∈NrmCVecU+×abs→MetOpen⁡C=MetOpen⁡IndMet⁡ifU∈NrmCVecU+×abs
10 2 9 eqtrid ⊢U=ifU∈NrmCVecU+×abs→J=MetOpen⁡IndMet⁡ifU∈NrmCVecU+×abs
11 10 oveq2d ⊢U=ifU∈NrmCVecU+×abs→K×tJ=K×tMetOpen⁡IndMet⁡ifU∈NrmCVecU+×abs
12 11 10 oveq12d ⊢U=ifU∈NrmCVecU+×abs→K×tJCnJ=K×tMetOpen⁡IndMet⁡ifU∈NrmCVecU+×absCnMetOpen⁡IndMet⁡ifU∈NrmCVecU+×abs
13 6 12 eleq12d ⊢U=ifU∈NrmCVecU+×abs→S∈K×tJCnJ↔⋅𝑠OLD⁡ifU∈NrmCVecU+×abs∈K×tMetOpen⁡IndMet⁡ifU∈NrmCVecU+×absCnMetOpen⁡IndMet⁡ifU∈NrmCVecU+×abs
14 eqid ⊢IndMet⁡ifU∈NrmCVecU+×abs=IndMet⁡ifU∈NrmCVecU+×abs
15 eqid ⊢MetOpen⁡IndMet⁡ifU∈NrmCVecU+×abs=MetOpen⁡IndMet⁡ifU∈NrmCVecU+×abs
16 eqid ⊢⋅𝑠OLD⁡ifU∈NrmCVecU+×abs=⋅𝑠OLD⁡ifU∈NrmCVecU+×abs
17 eqid ⊢BaseSet⁡ifU∈NrmCVecU+×abs=BaseSet⁡ifU∈NrmCVecU+×abs
18 eqid ⊢normCV⁡ifU∈NrmCVecU+×abs=normCV⁡ifU∈NrmCVecU+×abs
19 elimnvu ⊢ifU∈NrmCVecU+×abs∈NrmCVec
20 eqid ⊢11+normCV⁡ifU∈NrmCVecU+×abs⁡y+x+1r=11+normCV⁡ifU∈NrmCVecU+×abs⁡y+x+1r
21 14 15 16 4 17 18 19 20 smcnlem ⊢⋅𝑠OLD⁡ifU∈NrmCVecU+×abs∈K×tMetOpen⁡IndMet⁡ifU∈NrmCVecU+×absCnMetOpen⁡IndMet⁡ifU∈NrmCVecU+×abs
22 13 21 dedth ⊢U∈NrmCVec→S∈K×tJCnJ