# 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+ )`
` |-  ( ( ( 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 ) )`
` |-  ( ( ( ( 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 ) )`
` |-  ( ( ( ( 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 )`
` |-  ( ( ( ( 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 ) ) ) )`
` |-  ( ( 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 )`
` |-  ( ( ( ( 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 ) )`