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×tJCnJ

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⁡Uy
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×tJCnJ
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×tJCnTopOpen⁡ℂfld
18 10 10 cnmpt2nd ⊢U∈NrmCVec→x∈BaseSet⁡U,y∈BaseSet⁡U⟼y∈J×tJCnJ
19 1 2 6 12 smcn ⊢U∈NrmCVec→⋅𝑠OLD⁡U∈TopOpen⁡ℂfld×tJCnJ
20 10 10 17 18 19 cnmpt22f ⊢U∈NrmCVec→x∈BaseSet⁡U,y∈BaseSet⁡U⟼-1⋅𝑠OLD⁡Uy∈J×tJCnJ
21 1 2 5 vacn ⊢U∈NrmCVec→+v⁡U∈J×tJCnJ
22 10 10 11 20 21 cnmpt22f ⊢U∈NrmCVec→x∈BaseSet⁡U,y∈BaseSet⁡U⟼x+v⁡U-1⋅𝑠OLD⁡Uy∈J×tJCnJ
23 7 22 eqeltrd ⊢U∈NrmCVec→M∈J×tJCnJ