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 × t J Cn J

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 = if U ∈ NrmCVec U + × abs → ⋅ 𝑠OLD ⁡ U = ⋅ 𝑠OLD ⁡ if U ∈ NrmCVec U + × abs
6 3 5 eqtrid ⊢ U = if U ∈ NrmCVec U + × abs → S = ⋅ 𝑠OLD ⁡ if U ∈ NrmCVec U + × abs
7 fveq2 ⊢ U = if U ∈ NrmCVec U + × abs → IndMet ⁡ U = IndMet ⁡ if U ∈ NrmCVec U + × abs
8 1 7 eqtrid ⊢ U = if U ∈ NrmCVec U + × abs → C = IndMet ⁡ if U ∈ NrmCVec U + × abs
9 8 fveq2d ⊢ U = if U ∈ NrmCVec U + × abs → MetOpen ⁡ C = MetOpen ⁡ IndMet ⁡ if U ∈ NrmCVec U + × abs
10 2 9 eqtrid ⊢ U = if U ∈ NrmCVec U + × abs → J = MetOpen ⁡ IndMet ⁡ if U ∈ NrmCVec U + × abs
11 10 oveq2d ⊢ U = if U ∈ NrmCVec U + × abs → K × t J = K × t MetOpen ⁡ IndMet ⁡ if U ∈ NrmCVec U + × abs
12 11 10 oveq12d ⊢ U = if U ∈ NrmCVec U + × abs → K × t J Cn J = K × t MetOpen ⁡ IndMet ⁡ if U ∈ NrmCVec U + × abs Cn MetOpen ⁡ IndMet ⁡ if U ∈ NrmCVec U + × abs
13 6 12 eleq12d ⊢ U = if U ∈ NrmCVec U + × abs → S ∈ K × t J Cn J ↔ ⋅ 𝑠OLD ⁡ if U ∈ NrmCVec U + × abs ∈ K × t MetOpen ⁡ IndMet ⁡ if U ∈ NrmCVec U + × abs Cn MetOpen ⁡ IndMet ⁡ if U ∈ NrmCVec U + × abs
14 eqid ⊢ IndMet ⁡ if U ∈ NrmCVec U + × abs = IndMet ⁡ if U ∈ NrmCVec U + × abs
15 eqid ⊢ MetOpen ⁡ IndMet ⁡ if U ∈ NrmCVec U + × abs = MetOpen ⁡ IndMet ⁡ if U ∈ NrmCVec U + × abs
16 eqid ⊢ ⋅ 𝑠OLD ⁡ if U ∈ NrmCVec U + × abs = ⋅ 𝑠OLD ⁡ if U ∈ NrmCVec U + × abs
17 eqid ⊢ BaseSet ⁡ if U ∈ NrmCVec U + × abs = BaseSet ⁡ if U ∈ NrmCVec U + × abs
18 eqid ⊢ norm CV ⁡ if U ∈ NrmCVec U + × abs = norm CV ⁡ if U ∈ NrmCVec U + × abs
19 elimnvu ⊢ if U ∈ NrmCVec U + × abs ∈ NrmCVec
20 eqid ⊢ 1 1 + norm CV ⁡ if U ∈ NrmCVec U + × abs ⁡ y + x + 1 r = 1 1 + norm CV ⁡ if U ∈ NrmCVec U + × abs ⁡ y + x + 1 r
21 14 15 16 4 17 18 19 20 smcnlem ⊢ ⋅ 𝑠OLD ⁡ if U ∈ NrmCVec U + × abs ∈ K × t MetOpen ⁡ IndMet ⁡ if U ∈ NrmCVec U + × abs Cn MetOpen ⁡ IndMet ⁡ if U ∈ NrmCVec U + × abs
22 13 21 dedth ⊢ U ∈ NrmCVec → S ∈ K × t J Cn J