Metamath Proof Explorer

Theorem vmcn

Description: Vector subtraction is jointly continuous in both arguments. (Contributed by Mario Carneiro, 6-May-2014) (New usage is discouraged.)

Ref Expression
Hypotheses vmcn.c ⊢ C = IndMet ⁡ U
vmcn.j ⊢ J = MetOpen ⁡ C
vmcn.m ⊢ M = - v ⁡ U
Assertion vmcn ⊢ U ∈ NrmCVec → M ∈ J × t J Cn J

Proof

Step Hyp Ref Expression
1 vmcn.c ⊢ C = IndMet ⁡ U
2 vmcn.j ⊢ J = MetOpen ⁡ C
3 vmcn.m ⊢ M = - v ⁡ U
4 eqid ⊢ BaseSet ⁡ U = BaseSet ⁡ U
5 eqid ⊢ + v ⁡ U = + v ⁡ U
6 eqid ⊢ ⋅ 𝑠OLD ⁡ U = ⋅ 𝑠OLD ⁡ U
7 4 5 6 3 nvmfval ⊢ U ∈ NrmCVec → M = x ∈ BaseSet ⁡ U , y ∈ BaseSet ⁡ U ⟼ x + v ⁡ U -1 ⋅ 𝑠OLD ⁡ U y
8 4 1 imsxmet ⊢ U ∈ NrmCVec → C ∈ ∞Met ⁡ BaseSet ⁡ U
9 2 mopntopon ⊢ C ∈ ∞Met ⁡ BaseSet ⁡ U → J ∈ TopOn ⁡ BaseSet ⁡ U
10 8 9 syl ⊢ U ∈ NrmCVec → J ∈ TopOn ⁡ BaseSet ⁡ U
11 10 10 cnmpt1st ⊢ U ∈ NrmCVec → x ∈ BaseSet ⁡ U , y ∈ BaseSet ⁡ U ⟼ x ∈ J × t J Cn J
12 eqid ⊢ TopOpen ⁡ ℂ fld = TopOpen ⁡ ℂ fld
13 12 cnfldtopon ⊢ TopOpen ⁡ ℂ fld ∈ TopOn ⁡ ℂ
14 13 a1i ⊢ U ∈ NrmCVec → TopOpen ⁡ ℂ fld ∈ TopOn ⁡ ℂ
15 neg1cn ⊢ − 1 ∈ ℂ
16 15 a1i ⊢ U ∈ NrmCVec → − 1 ∈ ℂ
17 10 10 14 16 cnmpt2c ⊢ U ∈ NrmCVec → x ∈ BaseSet ⁡ U , y ∈ BaseSet ⁡ U ⟼ − 1 ∈ J × t J Cn TopOpen ⁡ ℂ fld
18 10 10 cnmpt2nd ⊢ U ∈ NrmCVec → x ∈ BaseSet ⁡ U , y ∈ BaseSet ⁡ U ⟼ y ∈ J × t J Cn J
19 1 2 6 12 smcn ⊢ U ∈ NrmCVec → ⋅ 𝑠OLD ⁡ U ∈ TopOpen ⁡ ℂ fld × t J Cn J
20 10 10 17 18 19 cnmpt22f ⊢ U ∈ NrmCVec → x ∈ BaseSet ⁡ U , y ∈ BaseSet ⁡ U ⟼ -1 ⋅ 𝑠OLD ⁡ U y ∈ J × t J Cn J
21 1 2 5 vacn ⊢ U ∈ NrmCVec → + v ⁡ U ∈ J × t J Cn J
22 10 10 11 20 21 cnmpt22f ⊢ U ∈ NrmCVec → x ∈ BaseSet ⁡ U , y ∈ BaseSet ⁡ U ⟼ x + v ⁡ U -1 ⋅ 𝑠OLD ⁡ U y ∈ J × t J Cn J
23 7 22 eqeltrd ⊢ U ∈ NrmCVec → M ∈ J × t J Cn J