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 ⊢ 𝐶 = ( IndMet ‘ 𝑈 )
vmcn.j ⊢ 𝐽 = ( MetOpen ‘ 𝐶 )
vmcn.m ⊢ 𝑀 = ( −𝑣 ‘ 𝑈 )
Assertion vmcn ( 𝑈 ∈ NrmCVec → 𝑀 ∈ ( ( 𝐽 ×t 𝐽 ) Cn 𝐽 ) )

Proof

Step Hyp Ref Expression
1 vmcn.c ⊢ 𝐶 = ( IndMet ‘ 𝑈 )
2 vmcn.j ⊢ 𝐽 = ( MetOpen ‘ 𝐶 )
3 vmcn.m ⊢ 𝑀 = ( −𝑣 ‘ 𝑈 )
4 eqid ⊢ ( BaseSet ‘ 𝑈 ) = ( BaseSet ‘ 𝑈 )
5 eqid ⊢ ( +𝑣 ‘ 𝑈 ) = ( +𝑣 ‘ 𝑈 )
6 eqid ⊢ ( ·𝑠OLD ‘ 𝑈 ) = ( ·𝑠OLD ‘ 𝑈 )
7 4 5 6 3 nvmfval ⊢ ( 𝑈 ∈ NrmCVec → 𝑀 = ( 𝑥 ∈ ( BaseSet ‘ 𝑈 ) , 𝑦 ∈ ( BaseSet ‘ 𝑈 ) ↦ ( 𝑥 ( +𝑣 ‘ 𝑈 ) ( - 1 ( ·𝑠OLD ‘ 𝑈 ) 𝑦 ) ) ) )
8 4 1 imsxmet ⊢ ( 𝑈 ∈ NrmCVec → 𝐶 ∈ ( ∞Met ‘ ( BaseSet ‘ 𝑈 ) ) )
9 2 mopntopon ⊢ ( 𝐶 ∈ ( ∞Met ‘ ( BaseSet ‘ 𝑈 ) ) → 𝐽 ∈ ( TopOn ‘ ( BaseSet ‘ 𝑈 ) ) )
10 8 9 syl ⊢ ( 𝑈 ∈ NrmCVec → 𝐽 ∈ ( TopOn ‘ ( BaseSet ‘ 𝑈 ) ) )
11 10 10 cnmpt1st ⊢ ( 𝑈 ∈ NrmCVec → ( 𝑥 ∈ ( BaseSet ‘ 𝑈 ) , 𝑦 ∈ ( BaseSet ‘ 𝑈 ) ↦ 𝑥 ) ∈ ( ( 𝐽 ×t 𝐽 ) Cn 𝐽 ) )
12 eqid ⊢ ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld )
13 12 cnfldtopon ⊢ ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ )
14 13 a1i ⊢ ( 𝑈 ∈ NrmCVec → ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ ) )
15 neg1cn ⊢ - 1 ∈ ℂ
16 15 a1i ⊢ ( 𝑈 ∈ NrmCVec → - 1 ∈ ℂ )
17 10 10 14 16 cnmpt2c ⊢ ( 𝑈 ∈ NrmCVec → ( 𝑥 ∈ ( BaseSet ‘ 𝑈 ) , 𝑦 ∈ ( BaseSet ‘ 𝑈 ) ↦ - 1 ) ∈ ( ( 𝐽 ×t 𝐽 ) Cn ( TopOpen ‘ ℂfld ) ) )
18 10 10 cnmpt2nd ⊢ ( 𝑈 ∈ NrmCVec → ( 𝑥 ∈ ( BaseSet ‘ 𝑈 ) , 𝑦 ∈ ( BaseSet ‘ 𝑈 ) ↦ 𝑦 ) ∈ ( ( 𝐽 ×t 𝐽 ) Cn 𝐽 ) )
19 1 2 6 12 smcn ⊢ ( 𝑈 ∈ NrmCVec → ( ·𝑠OLD ‘ 𝑈 ) ∈ ( ( ( TopOpen ‘ ℂfld ) ×t 𝐽 ) Cn 𝐽 ) )
20 10 10 17 18 19 cnmpt22f ⊢ ( 𝑈 ∈ NrmCVec → ( 𝑥 ∈ ( BaseSet ‘ 𝑈 ) , 𝑦 ∈ ( BaseSet ‘ 𝑈 ) ↦ ( - 1 ( ·𝑠OLD ‘ 𝑈 ) 𝑦 ) ) ∈ ( ( 𝐽 ×t 𝐽 ) Cn 𝐽 ) )
21 1 2 5 vacn ⊢ ( 𝑈 ∈ NrmCVec → ( +𝑣 ‘ 𝑈 ) ∈ ( ( 𝐽 ×t 𝐽 ) Cn 𝐽 ) )
22 10 10 11 20 21 cnmpt22f ⊢ ( 𝑈 ∈ NrmCVec → ( 𝑥 ∈ ( BaseSet ‘ 𝑈 ) , 𝑦 ∈ ( BaseSet ‘ 𝑈 ) ↦ ( 𝑥 ( +𝑣 ‘ 𝑈 ) ( - 1 ( ·𝑠OLD ‘ 𝑈 ) 𝑦 ) ) ) ∈ ( ( 𝐽 ×t 𝐽 ) Cn 𝐽 ) )
23 7 22 eqeltrd ⊢ ( 𝑈 ∈ NrmCVec → 𝑀 ∈ ( ( 𝐽 ×t 𝐽 ) Cn 𝐽 ) )