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 e. NrmCVec -> M e. ( ( J tX 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 
 |-  ( .sOLD ` U ) = ( .sOLD ` U )
7 4 5 6 3 nvmfval 
 |-  ( U e. NrmCVec -> M = ( x e. ( BaseSet ` U ) , y e. ( BaseSet ` U ) |-> ( x ( +v ` U ) ( -u 1 ( .sOLD ` U ) y ) ) ) )
8 4 1 imsxmet 
 |-  ( U e. NrmCVec -> C e. ( *Met ` ( BaseSet ` U ) ) )
9 2 mopntopon 
 |-  ( C e. ( *Met ` ( BaseSet ` U ) ) -> J e. ( TopOn ` ( BaseSet ` U ) ) )
10 8 9 syl 
 |-  ( U e. NrmCVec -> J e. ( TopOn ` ( BaseSet ` U ) ) )
11 10 10 cnmpt1st 
 |-  ( U e. NrmCVec -> ( x e. ( BaseSet ` U ) , y e. ( BaseSet ` U ) |-> x ) e. ( ( J tX J ) Cn J ) )
12 eqid 
 |-  ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
13 12 cnfldtopon 
 |-  ( TopOpen ` CCfld ) e. ( TopOn ` CC )
14 13 a1i 
 |-  ( U e. NrmCVec -> ( TopOpen ` CCfld ) e. ( TopOn ` CC ) )
15 neg1cn 
 |-  -u 1 e. CC
16 15 a1i 
 |-  ( U e. NrmCVec -> -u 1 e. CC )
17 10 10 14 16 cnmpt2c 
 |-  ( U e. NrmCVec -> ( x e. ( BaseSet ` U ) , y e. ( BaseSet ` U ) |-> -u 1 ) e. ( ( J tX J ) Cn ( TopOpen ` CCfld ) ) )
18 10 10 cnmpt2nd 
 |-  ( U e. NrmCVec -> ( x e. ( BaseSet ` U ) , y e. ( BaseSet ` U ) |-> y ) e. ( ( J tX J ) Cn J ) )
19 1 2 6 12 smcn 
 |-  ( U e. NrmCVec -> ( .sOLD ` U ) e. ( ( ( TopOpen ` CCfld ) tX J ) Cn J ) )
20 10 10 17 18 19 cnmpt22f 
 |-  ( U e. NrmCVec -> ( x e. ( BaseSet ` U ) , y e. ( BaseSet ` U ) |-> ( -u 1 ( .sOLD ` U ) y ) ) e. ( ( J tX J ) Cn J ) )
21 1 2 5 vacn 
 |-  ( U e. NrmCVec -> ( +v ` U ) e. ( ( J tX J ) Cn J ) )
22 10 10 11 20 21 cnmpt22f 
 |-  ( U e. NrmCVec -> ( x e. ( BaseSet ` U ) , y e. ( BaseSet ` U ) |-> ( x ( +v ` U ) ( -u 1 ( .sOLD ` U ) y ) ) ) e. ( ( J tX J ) Cn J ) )
23 7 22 eqeltrd 
 |-  ( U e. NrmCVec -> M e. ( ( J tX J ) Cn J ) )