Metamath Proof Explorer

Theorem vacn

Description: Vector addition is jointly continuous in both arguments. (Contributed by Jeff Hankins, 16-Jun-2009) (Revised by Mario Carneiro, 10-Sep-2015) (New usage is discouraged.)

Ref Expression
Hypotheses vacn.c 
|- C = ( IndMet ` U )
vacn.j 
|- J = ( MetOpen ` C )
vacn.g 
|- G = ( +v ` U )
Assertion vacn 
|- ( U e. NrmCVec -> G e. ( ( J tX J ) Cn J ) )

Proof

Step Hyp Ref Expression
1 vacn.c 
 |-  C = ( IndMet ` U )
2 vacn.j 
 |-  J = ( MetOpen ` C )
3 vacn.g 
 |-  G = ( +v ` U )
4 eqid 
 |-  ( BaseSet ` U ) = ( BaseSet ` U )
5 4 3 nvgf 
 |-  ( U e. NrmCVec -> G : ( ( BaseSet ` U ) X. ( BaseSet ` U ) ) --> ( BaseSet ` U ) )
6 rphalfcl 
 |-  ( r e. RR+ -> ( r / 2 ) e. RR+ )
7 6 adantl 
 |-  ( ( ( U e. NrmCVec /\ ( x e. ( BaseSet ` U ) /\ y e. ( BaseSet ` U ) ) ) /\ r e. RR+ ) -> ( r / 2 ) e. RR+ )
8 simplll 
 |-  ( ( ( ( U e. NrmCVec /\ ( x e. ( BaseSet ` U ) /\ y e. ( BaseSet ` U ) ) ) /\ r e. RR+ ) /\ ( z e. ( BaseSet ` U ) /\ w e. ( BaseSet ` U ) ) ) -> U e. NrmCVec )
9 4 1 imsmet 
 |-  ( U e. NrmCVec -> C e. ( Met ` ( BaseSet ` U ) ) )
10 8 9 syl 
 |-  ( ( ( ( U e. NrmCVec /\ ( x e. ( BaseSet ` U ) /\ y e. ( BaseSet ` U ) ) ) /\ r e. RR+ ) /\ ( z e. ( BaseSet ` U ) /\ w e. ( BaseSet ` U ) ) ) -> C e. ( Met ` ( BaseSet ` U ) ) )
11 simplrl 
 |-  ( ( ( U e. NrmCVec /\ ( x e. ( BaseSet ` U ) /\ y e. ( BaseSet ` U ) ) ) /\ r e. RR+ ) -> x e. ( BaseSet ` U ) )
12 11 adantr 
 |-  ( ( ( ( U e. NrmCVec /\ ( x e. ( BaseSet ` U ) /\ y e. ( BaseSet ` U ) ) ) /\ r e. RR+ ) /\ ( z e. ( BaseSet ` U ) /\ w e. ( BaseSet ` U ) ) ) -> x e. ( BaseSet ` U ) )
13 simprl 
 |-  ( ( ( ( U e. NrmCVec /\ ( x e. ( BaseSet ` U ) /\ y e. ( BaseSet ` U ) ) ) /\ r e. RR+ ) /\ ( z e. ( BaseSet ` U ) /\ w e. ( BaseSet ` U ) ) ) -> z e. ( BaseSet ` U ) )
14 metcl 
 |-  ( ( C e. ( Met ` ( BaseSet ` U ) ) /\ x e. ( BaseSet ` U ) /\ z e. ( BaseSet ` U ) ) -> ( x C z ) e. RR )
15 10 12 13 14 syl3anc 
 |-  ( ( ( ( U e. NrmCVec /\ ( x e. ( BaseSet ` U ) /\ y e. ( BaseSet ` U ) ) ) /\ r e. RR+ ) /\ ( z e. ( BaseSet ` U ) /\ w e. ( BaseSet ` U ) ) ) -> ( x C z ) e. RR )
16 simplrr 
 |-  ( ( ( U e. NrmCVec /\ ( x e. ( BaseSet ` U ) /\ y e. ( BaseSet ` U ) ) ) /\ r e. RR+ ) -> y e. ( BaseSet ` U ) )
17 16 adantr 
 |-  ( ( ( ( U e. NrmCVec /\ ( x e. ( BaseSet ` U ) /\ y e. ( BaseSet ` U ) ) ) /\ r e. RR+ ) /\ ( z e. ( BaseSet ` U ) /\ w e. ( BaseSet ` U ) ) ) -> y e. ( BaseSet ` U ) )
18 simprr 
 |-  ( ( ( ( U e. NrmCVec /\ ( x e. ( BaseSet ` U ) /\ y e. ( BaseSet ` U ) ) ) /\ r e. RR+ ) /\ ( z e. ( BaseSet ` U ) /\ w e. ( BaseSet ` U ) ) ) -> w e. ( BaseSet ` U ) )
19 metcl 
 |-  ( ( C e. ( Met ` ( BaseSet ` U ) ) /\ y e. ( BaseSet ` U ) /\ w e. ( BaseSet ` U ) ) -> ( y C w ) e. RR )
20 10 17 18 19 syl3anc 
 |-  ( ( ( ( U e. NrmCVec /\ ( x e. ( BaseSet ` U ) /\ y e. ( BaseSet ` U ) ) ) /\ r e. RR+ ) /\ ( z e. ( BaseSet ` U ) /\ w e. ( BaseSet ` U ) ) ) -> ( y C w ) e. RR )
21 rpre 
 |-  ( r e. RR+ -> r e. RR )
22 21 ad2antlr 
 |-  ( ( ( ( U e. NrmCVec /\ ( x e. ( BaseSet ` U ) /\ y e. ( BaseSet ` U ) ) ) /\ r e. RR+ ) /\ ( z e. ( BaseSet ` U ) /\ w e. ( BaseSet ` U ) ) ) -> r e. RR )
23 lt2halves 
 |-  ( ( ( x C z ) e. RR /\ ( y C w ) e. RR /\ r e. RR ) -> ( ( ( x C z ) < ( r / 2 ) /\ ( y C w ) < ( r / 2 ) ) -> ( ( x C z ) + ( y C w ) ) < r ) )
24 15 20 22 23 syl3anc 
 |-  ( ( ( ( U e. NrmCVec /\ ( x e. ( BaseSet ` U ) /\ y e. ( BaseSet ` U ) ) ) /\ r e. RR+ ) /\ ( z e. ( BaseSet ` U ) /\ w e. ( BaseSet ` U ) ) ) -> ( ( ( x C z ) < ( r / 2 ) /\ ( y C w ) < ( r / 2 ) ) -> ( ( x C z ) + ( y C w ) ) < r ) )
25 eqid 
 |-  ( -v ` U ) = ( -v ` U )
26 4 25 nvmcl 
 |-  ( ( U e. NrmCVec /\ x e. ( BaseSet ` U ) /\ z e. ( BaseSet ` U ) ) -> ( x ( -v ` U ) z ) e. ( BaseSet ` U ) )
27 8 12 13 26 syl3anc 
 |-  ( ( ( ( U e. NrmCVec /\ ( x e. ( BaseSet ` U ) /\ y e. ( BaseSet ` U ) ) ) /\ r e. RR+ ) /\ ( z e. ( BaseSet ` U ) /\ w e. ( BaseSet ` U ) ) ) -> ( x ( -v ` U ) z ) e. ( BaseSet ` U ) )
28 4 25 nvmcl 
 |-  ( ( U e. NrmCVec /\ y e. ( BaseSet ` U ) /\ w e. ( BaseSet ` U ) ) -> ( y ( -v ` U ) w ) e. ( BaseSet ` U ) )
29 8 17 18 28 syl3anc 
 |-  ( ( ( ( U e. NrmCVec /\ ( x e. ( BaseSet ` U ) /\ y e. ( BaseSet ` U ) ) ) /\ r e. RR+ ) /\ ( z e. ( BaseSet ` U ) /\ w e. ( BaseSet ` U ) ) ) -> ( y ( -v ` U ) w ) e. ( BaseSet ` U ) )
30 eqid 
 |-  ( normCV ` U ) = ( normCV ` U )
31 4 3 30 nvtri 
 |-  ( ( U e. NrmCVec /\ ( x ( -v ` U ) z ) e. ( BaseSet ` U ) /\ ( y ( -v ` U ) w ) e. ( BaseSet ` U ) ) -> ( ( normCV ` U ) ` ( ( x ( -v ` U ) z ) G ( y ( -v ` U ) w ) ) ) <_ ( ( ( normCV ` U ) ` ( x ( -v ` U ) z ) ) + ( ( normCV ` U ) ` ( y ( -v ` U ) w ) ) ) )
32 8 27 29 31 syl3anc 
 |-  ( ( ( ( U e. NrmCVec /\ ( x e. ( BaseSet ` U ) /\ y e. ( BaseSet ` U ) ) ) /\ r e. RR+ ) /\ ( z e. ( BaseSet ` U ) /\ w e. ( BaseSet ` U ) ) ) -> ( ( normCV ` U ) ` ( ( x ( -v ` U ) z ) G ( y ( -v ` U ) w ) ) ) <_ ( ( ( normCV ` U ) ` ( x ( -v ` U ) z ) ) + ( ( normCV ` U ) ` ( y ( -v ` U ) w ) ) ) )
33 4 3 nvgcl 
 |-  ( ( U e. NrmCVec /\ x e. ( BaseSet ` U ) /\ y e. ( BaseSet ` U ) ) -> ( x G y ) e. ( BaseSet ` U ) )
34 8 12 17 33 syl3anc 
 |-  ( ( ( ( U e. NrmCVec /\ ( x e. ( BaseSet ` U ) /\ y e. ( BaseSet ` U ) ) ) /\ r e. RR+ ) /\ ( z e. ( BaseSet ` U ) /\ w e. ( BaseSet ` U ) ) ) -> ( x G y ) e. ( BaseSet ` U ) )
35 4 3 nvgcl 
 |-  ( ( U e. NrmCVec /\ z e. ( BaseSet ` U ) /\ w e. ( BaseSet ` U ) ) -> ( z G w ) e. ( BaseSet ` U ) )
36 8 13 18 35 syl3anc 
 |-  ( ( ( ( U e. NrmCVec /\ ( x e. ( BaseSet ` U ) /\ y e. ( BaseSet ` U ) ) ) /\ r e. RR+ ) /\ ( z e. ( BaseSet ` U ) /\ w e. ( BaseSet ` U ) ) ) -> ( z G w ) e. ( BaseSet ` U ) )
37 4 25 30 1 imsdval 
 |-  ( ( U e. NrmCVec /\ ( x G y ) e. ( BaseSet ` U ) /\ ( z G w ) e. ( BaseSet ` U ) ) -> ( ( x G y ) C ( z G w ) ) = ( ( normCV ` U ) ` ( ( x G y ) ( -v ` U ) ( z G w ) ) ) )
38 8 34 36 37 syl3anc 
 |-  ( ( ( ( U e. NrmCVec /\ ( x e. ( BaseSet ` U ) /\ y e. ( BaseSet ` U ) ) ) /\ r e. RR+ ) /\ ( z e. ( BaseSet ` U ) /\ w e. ( BaseSet ` U ) ) ) -> ( ( x G y ) C ( z G w ) ) = ( ( normCV ` U ) ` ( ( x G y ) ( -v ` U ) ( z G w ) ) ) )
39 4 3 25 nvaddsub4 
 |-  ( ( U e. NrmCVec /\ ( x e. ( BaseSet ` U ) /\ y e. ( BaseSet ` U ) ) /\ ( z e. ( BaseSet ` U ) /\ w e. ( BaseSet ` U ) ) ) -> ( ( x G y ) ( -v ` U ) ( z G w ) ) = ( ( x ( -v ` U ) z ) G ( y ( -v ` U ) w ) ) )
40 8 12 17 13 18 39 syl122anc 
 |-  ( ( ( ( U e. NrmCVec /\ ( x e. ( BaseSet ` U ) /\ y e. ( BaseSet ` U ) ) ) /\ r e. RR+ ) /\ ( z e. ( BaseSet ` U ) /\ w e. ( BaseSet ` U ) ) ) -> ( ( x G y ) ( -v ` U ) ( z G w ) ) = ( ( x ( -v ` U ) z ) G ( y ( -v ` U ) w ) ) )
41 40 fveq2d 
 |-  ( ( ( ( U e. NrmCVec /\ ( x e. ( BaseSet ` U ) /\ y e. ( BaseSet ` U ) ) ) /\ r e. RR+ ) /\ ( z e. ( BaseSet ` U ) /\ w e. ( BaseSet ` U ) ) ) -> ( ( normCV ` U ) ` ( ( x G y ) ( -v ` U ) ( z G w ) ) ) = ( ( normCV ` U ) ` ( ( x ( -v ` U ) z ) G ( y ( -v ` U ) w ) ) ) )
42 38 41 eqtrd 
 |-  ( ( ( ( U e. NrmCVec /\ ( x e. ( BaseSet ` U ) /\ y e. ( BaseSet ` U ) ) ) /\ r e. RR+ ) /\ ( z e. ( BaseSet ` U ) /\ w e. ( BaseSet ` U ) ) ) -> ( ( x G y ) C ( z G w ) ) = ( ( normCV ` U ) ` ( ( x ( -v ` U ) z ) G ( y ( -v ` U ) w ) ) ) )
43 4 25 30 1 imsdval 
 |-  ( ( U e. NrmCVec /\ x e. ( BaseSet ` U ) /\ z e. ( BaseSet ` U ) ) -> ( x C z ) = ( ( normCV ` U ) ` ( x ( -v ` U ) z ) ) )
44 8 12 13 43 syl3anc 
 |-  ( ( ( ( U e. NrmCVec /\ ( x e. ( BaseSet ` U ) /\ y e. ( BaseSet ` U ) ) ) /\ r e. RR+ ) /\ ( z e. ( BaseSet ` U ) /\ w e. ( BaseSet ` U ) ) ) -> ( x C z ) = ( ( normCV ` U ) ` ( x ( -v ` U ) z ) ) )
45 4 25 30 1 imsdval 
 |-  ( ( U e. NrmCVec /\ y e. ( BaseSet ` U ) /\ w e. ( BaseSet ` U ) ) -> ( y C w ) = ( ( normCV ` U ) ` ( y ( -v ` U ) w ) ) )
46 8 17 18 45 syl3anc 
 |-  ( ( ( ( U e. NrmCVec /\ ( x e. ( BaseSet ` U ) /\ y e. ( BaseSet ` U ) ) ) /\ r e. RR+ ) /\ ( z e. ( BaseSet ` U ) /\ w e. ( BaseSet ` U ) ) ) -> ( y C w ) = ( ( normCV ` U ) ` ( y ( -v ` U ) w ) ) )
47 44 46 oveq12d 
 |-  ( ( ( ( U e. NrmCVec /\ ( x e. ( BaseSet ` U ) /\ y e. ( BaseSet ` U ) ) ) /\ r e. RR+ ) /\ ( z e. ( BaseSet ` U ) /\ w e. ( BaseSet ` U ) ) ) -> ( ( x C z ) + ( y C w ) ) = ( ( ( normCV ` U ) ` ( x ( -v ` U ) z ) ) + ( ( normCV ` U ) ` ( y ( -v ` U ) w ) ) ) )
48 32 42 47 3brtr4d 
 |-  ( ( ( ( U e. NrmCVec /\ ( x e. ( BaseSet ` U ) /\ y e. ( BaseSet ` U ) ) ) /\ r e. RR+ ) /\ ( z e. ( BaseSet ` U ) /\ w e. ( BaseSet ` U ) ) ) -> ( ( x G y ) C ( z G w ) ) <_ ( ( x C z ) + ( y C w ) ) )
49 metcl 
 |-  ( ( C e. ( Met ` ( BaseSet ` U ) ) /\ ( x G y ) e. ( BaseSet ` U ) /\ ( z G w ) e. ( BaseSet ` U ) ) -> ( ( x G y ) C ( z G w ) ) e. RR )
50 10 34 36 49 syl3anc 
 |-  ( ( ( ( U e. NrmCVec /\ ( x e. ( BaseSet ` U ) /\ y e. ( BaseSet ` U ) ) ) /\ r e. RR+ ) /\ ( z e. ( BaseSet ` U ) /\ w e. ( BaseSet ` U ) ) ) -> ( ( x G y ) C ( z G w ) ) e. RR )
51 15 20 readdcld 
 |-  ( ( ( ( U e. NrmCVec /\ ( x e. ( BaseSet ` U ) /\ y e. ( BaseSet ` U ) ) ) /\ r e. RR+ ) /\ ( z e. ( BaseSet ` U ) /\ w e. ( BaseSet ` U ) ) ) -> ( ( x C z ) + ( y C w ) ) e. RR )
52 lelttr 
 |-  ( ( ( ( x G y ) C ( z G w ) ) e. RR /\ ( ( x C z ) + ( y C w ) ) e. RR /\ r e. RR ) -> ( ( ( ( x G y ) C ( z G w ) ) <_ ( ( x C z ) + ( y C w ) ) /\ ( ( x C z ) + ( y C w ) ) < r ) -> ( ( x G y ) C ( z G w ) ) < r ) )
53 50 51 22 52 syl3anc 
 |-  ( ( ( ( U e. NrmCVec /\ ( x e. ( BaseSet ` U ) /\ y e. ( BaseSet ` U ) ) ) /\ r e. RR+ ) /\ ( z e. ( BaseSet ` U ) /\ w e. ( BaseSet ` U ) ) ) -> ( ( ( ( x G y ) C ( z G w ) ) <_ ( ( x C z ) + ( y C w ) ) /\ ( ( x C z ) + ( y C w ) ) < r ) -> ( ( x G y ) C ( z G w ) ) < r ) )
54 48 53 mpand 
 |-  ( ( ( ( U e. NrmCVec /\ ( x e. ( BaseSet ` U ) /\ y e. ( BaseSet ` U ) ) ) /\ r e. RR+ ) /\ ( z e. ( BaseSet ` U ) /\ w e. ( BaseSet ` U ) ) ) -> ( ( ( x C z ) + ( y C w ) ) < r -> ( ( x G y ) C ( z G w ) ) < r ) )
55 24 54 syld 
 |-  ( ( ( ( U e. NrmCVec /\ ( x e. ( BaseSet ` U ) /\ y e. ( BaseSet ` U ) ) ) /\ r e. RR+ ) /\ ( z e. ( BaseSet ` U ) /\ w e. ( BaseSet ` U ) ) ) -> ( ( ( x C z ) < ( r / 2 ) /\ ( y C w ) < ( r / 2 ) ) -> ( ( x G y ) C ( z G w ) ) < r ) )
56 55 ralrimivva 
 |-  ( ( ( U e. NrmCVec /\ ( x e. ( BaseSet ` U ) /\ y e. ( BaseSet ` U ) ) ) /\ r e. RR+ ) -> A. z e. ( BaseSet ` U ) A. w e. ( BaseSet ` U ) ( ( ( x C z ) < ( r / 2 ) /\ ( y C w ) < ( r / 2 ) ) -> ( ( x G y ) C ( z G w ) ) < r ) )
57 breq2 
 |-  ( s = ( r / 2 ) -> ( ( x C z ) < s <-> ( x C z ) < ( r / 2 ) ) )
58 breq2 
 |-  ( s = ( r / 2 ) -> ( ( y C w ) < s <-> ( y C w ) < ( r / 2 ) ) )
59 57 58 anbi12d 
 |-  ( s = ( r / 2 ) -> ( ( ( x C z ) < s /\ ( y C w ) < s ) <-> ( ( x C z ) < ( r / 2 ) /\ ( y C w ) < ( r / 2 ) ) ) )
60 59 imbi1d 
 |-  ( s = ( r / 2 ) -> ( ( ( ( x C z ) < s /\ ( y C w ) < s ) -> ( ( x G y ) C ( z G w ) ) < r ) <-> ( ( ( x C z ) < ( r / 2 ) /\ ( y C w ) < ( r / 2 ) ) -> ( ( x G y ) C ( z G w ) ) < r ) ) )
61 60 2ralbidv 
 |-  ( s = ( r / 2 ) -> ( A. z e. ( BaseSet ` U ) A. w e. ( BaseSet ` U ) ( ( ( x C z ) < s /\ ( y C w ) < s ) -> ( ( x G y ) C ( z G w ) ) < r ) <-> A. z e. ( BaseSet ` U ) A. w e. ( BaseSet ` U ) ( ( ( x C z ) < ( r / 2 ) /\ ( y C w ) < ( r / 2 ) ) -> ( ( x G y ) C ( z G w ) ) < r ) ) )
62 61 rspcev 
 |-  ( ( ( r / 2 ) e. RR+ /\ A. z e. ( BaseSet ` U ) A. w e. ( BaseSet ` U ) ( ( ( x C z ) < ( r / 2 ) /\ ( y C w ) < ( r / 2 ) ) -> ( ( x G y ) C ( z G w ) ) < r ) ) -> E. s e. RR+ A. z e. ( BaseSet ` U ) A. w e. ( BaseSet ` U ) ( ( ( x C z ) < s /\ ( y C w ) < s ) -> ( ( x G y ) C ( z G w ) ) < r ) )
63 7 56 62 syl2anc 
 |-  ( ( ( U e. NrmCVec /\ ( x e. ( BaseSet ` U ) /\ y e. ( BaseSet ` U ) ) ) /\ r e. RR+ ) -> E. s e. RR+ A. z e. ( BaseSet ` U ) A. w e. ( BaseSet ` U ) ( ( ( x C z ) < s /\ ( y C w ) < s ) -> ( ( x G y ) C ( z G w ) ) < r ) )
64 63 ralrimiva 
 |-  ( ( U e. NrmCVec /\ ( x e. ( BaseSet ` U ) /\ y e. ( BaseSet ` U ) ) ) -> A. r e. RR+ E. s e. RR+ A. z e. ( BaseSet ` U ) A. w e. ( BaseSet ` U ) ( ( ( x C z ) < s /\ ( y C w ) < s ) -> ( ( x G y ) C ( z G w ) ) < r ) )
65 64 ralrimivva 
 |-  ( U e. NrmCVec -> A. x e. ( BaseSet ` U ) A. y e. ( BaseSet ` U ) A. r e. RR+ E. s e. RR+ A. z e. ( BaseSet ` U ) A. w e. ( BaseSet ` U ) ( ( ( x C z ) < s /\ ( y C w ) < s ) -> ( ( x G y ) C ( z G w ) ) < r ) )
66 4 1 imsxmet 
 |-  ( U e. NrmCVec -> C e. ( *Met ` ( BaseSet ` U ) ) )
67 2 2 2 txmetcn 
 |-  ( ( C e. ( *Met ` ( BaseSet ` U ) ) /\ C e. ( *Met ` ( BaseSet ` U ) ) /\ C e. ( *Met ` ( BaseSet ` U ) ) ) -> ( G e. ( ( J tX J ) Cn J ) <-> ( G : ( ( BaseSet ` U ) X. ( BaseSet ` U ) ) --> ( BaseSet ` U ) /\ A. x e. ( BaseSet ` U ) A. y e. ( BaseSet ` U ) A. r e. RR+ E. s e. RR+ A. z e. ( BaseSet ` U ) A. w e. ( BaseSet ` U ) ( ( ( x C z ) < s /\ ( y C w ) < s ) -> ( ( x G y ) C ( z G w ) ) < r ) ) ) )
68 66 66 66 67 syl3anc 
 |-  ( U e. NrmCVec -> ( G e. ( ( J tX J ) Cn J ) <-> ( G : ( ( BaseSet ` U ) X. ( BaseSet ` U ) ) --> ( BaseSet ` U ) /\ A. x e. ( BaseSet ` U ) A. y e. ( BaseSet ` U ) A. r e. RR+ E. s e. RR+ A. z e. ( BaseSet ` U ) A. w e. ( BaseSet ` U ) ( ( ( x C z ) < s /\ ( y C w ) < s ) -> ( ( x G y ) C ( z G w ) ) < r ) ) ) )
69 5 65 68 mpbir2and 
 |-  ( U e. NrmCVec -> G e. ( ( J tX J ) Cn J ) )