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 ⊢ 𝐶 = ( IndMet ‘ 𝑈 )
vacn.j ⊢ 𝐽 = ( MetOpen ‘ 𝐶 )
vacn.g ⊢ 𝐺 = ( +𝑣 ‘ 𝑈 )
Assertion vacn ( 𝑈 ∈ NrmCVec → 𝐺 ∈ ( ( 𝐽 ×t 𝐽 ) Cn 𝐽 ) )

Proof

Step Hyp Ref Expression
1 vacn.c ⊢ 𝐶 = ( IndMet ‘ 𝑈 )
2 vacn.j ⊢ 𝐽 = ( MetOpen ‘ 𝐶 )
3 vacn.g ⊢ 𝐺 = ( +𝑣 ‘ 𝑈 )
4 eqid ⊢ ( BaseSet ‘ 𝑈 ) = ( BaseSet ‘ 𝑈 )
5 4 3 nvgf ⊢ ( 𝑈 ∈ NrmCVec → 𝐺 : ( ( BaseSet ‘ 𝑈 ) × ( BaseSet ‘ 𝑈 ) ) ⟶ ( BaseSet ‘ 𝑈 ) )
6 rphalfcl ⊢ ( 𝑟 ∈ ℝ+ → ( 𝑟 / 2 ) ∈ ℝ+ )
7 6 adantl ⊢ ( ( ( 𝑈 ∈ NrmCVec ∧ ( 𝑥 ∈ ( BaseSet ‘ 𝑈 ) ∧ 𝑦 ∈ ( BaseSet ‘ 𝑈 ) ) ) ∧ 𝑟 ∈ ℝ+ ) → ( 𝑟 / 2 ) ∈ ℝ+ )
8 simplll ⊢ ( ( ( ( 𝑈 ∈ NrmCVec ∧ ( 𝑥 ∈ ( BaseSet ‘ 𝑈 ) ∧ 𝑦 ∈ ( BaseSet ‘ 𝑈 ) ) ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑧 ∈ ( BaseSet ‘ 𝑈 ) ∧ 𝑤 ∈ ( BaseSet ‘ 𝑈 ) ) ) → 𝑈 ∈ NrmCVec )
9 4 1 imsmet ⊢ ( 𝑈 ∈ NrmCVec → 𝐶 ∈ ( Met ‘ ( BaseSet ‘ 𝑈 ) ) )
10 8 9 syl ⊢ ( ( ( ( 𝑈 ∈ NrmCVec ∧ ( 𝑥 ∈ ( BaseSet ‘ 𝑈 ) ∧ 𝑦 ∈ ( BaseSet ‘ 𝑈 ) ) ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑧 ∈ ( BaseSet ‘ 𝑈 ) ∧ 𝑤 ∈ ( BaseSet ‘ 𝑈 ) ) ) → 𝐶 ∈ ( Met ‘ ( BaseSet ‘ 𝑈 ) ) )
11 simplrl ⊢ ( ( ( 𝑈 ∈ NrmCVec ∧ ( 𝑥 ∈ ( BaseSet ‘ 𝑈 ) ∧ 𝑦 ∈ ( BaseSet ‘ 𝑈 ) ) ) ∧ 𝑟 ∈ ℝ+ ) → 𝑥 ∈ ( BaseSet ‘ 𝑈 ) )
12 11 adantr ⊢ ( ( ( ( 𝑈 ∈ NrmCVec ∧ ( 𝑥 ∈ ( BaseSet ‘ 𝑈 ) ∧ 𝑦 ∈ ( BaseSet ‘ 𝑈 ) ) ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑧 ∈ ( BaseSet ‘ 𝑈 ) ∧ 𝑤 ∈ ( BaseSet ‘ 𝑈 ) ) ) → 𝑥 ∈ ( BaseSet ‘ 𝑈 ) )
13 simprl ⊢ ( ( ( ( 𝑈 ∈ NrmCVec ∧ ( 𝑥 ∈ ( BaseSet ‘ 𝑈 ) ∧ 𝑦 ∈ ( BaseSet ‘ 𝑈 ) ) ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑧 ∈ ( BaseSet ‘ 𝑈 ) ∧ 𝑤 ∈ ( BaseSet ‘ 𝑈 ) ) ) → 𝑧 ∈ ( BaseSet ‘ 𝑈 ) )
14 metcl ⊢ ( ( 𝐶 ∈ ( Met ‘ ( BaseSet ‘ 𝑈 ) ) ∧ 𝑥 ∈ ( BaseSet ‘ 𝑈 ) ∧ 𝑧 ∈ ( BaseSet ‘ 𝑈 ) ) → ( 𝑥 𝐶 𝑧 ) ∈ ℝ )
15 10 12 13 14 syl3anc ⊢ ( ( ( ( 𝑈 ∈ NrmCVec ∧ ( 𝑥 ∈ ( BaseSet ‘ 𝑈 ) ∧ 𝑦 ∈ ( BaseSet ‘ 𝑈 ) ) ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑧 ∈ ( BaseSet ‘ 𝑈 ) ∧ 𝑤 ∈ ( BaseSet ‘ 𝑈 ) ) ) → ( 𝑥 𝐶 𝑧 ) ∈ ℝ )
16 simplrr ⊢ ( ( ( 𝑈 ∈ NrmCVec ∧ ( 𝑥 ∈ ( BaseSet ‘ 𝑈 ) ∧ 𝑦 ∈ ( BaseSet ‘ 𝑈 ) ) ) ∧ 𝑟 ∈ ℝ+ ) → 𝑦 ∈ ( BaseSet ‘ 𝑈 ) )
17 16 adantr ⊢ ( ( ( ( 𝑈 ∈ NrmCVec ∧ ( 𝑥 ∈ ( BaseSet ‘ 𝑈 ) ∧ 𝑦 ∈ ( BaseSet ‘ 𝑈 ) ) ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑧 ∈ ( BaseSet ‘ 𝑈 ) ∧ 𝑤 ∈ ( BaseSet ‘ 𝑈 ) ) ) → 𝑦 ∈ ( BaseSet ‘ 𝑈 ) )
18 simprr ⊢ ( ( ( ( 𝑈 ∈ NrmCVec ∧ ( 𝑥 ∈ ( BaseSet ‘ 𝑈 ) ∧ 𝑦 ∈ ( BaseSet ‘ 𝑈 ) ) ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑧 ∈ ( BaseSet ‘ 𝑈 ) ∧ 𝑤 ∈ ( BaseSet ‘ 𝑈 ) ) ) → 𝑤 ∈ ( BaseSet ‘ 𝑈 ) )
19 metcl ⊢ ( ( 𝐶 ∈ ( Met ‘ ( BaseSet ‘ 𝑈 ) ) ∧ 𝑦 ∈ ( BaseSet ‘ 𝑈 ) ∧ 𝑤 ∈ ( BaseSet ‘ 𝑈 ) ) → ( 𝑦 𝐶 𝑤 ) ∈ ℝ )
20 10 17 18 19 syl3anc ⊢ ( ( ( ( 𝑈 ∈ NrmCVec ∧ ( 𝑥 ∈ ( BaseSet ‘ 𝑈 ) ∧ 𝑦 ∈ ( BaseSet ‘ 𝑈 ) ) ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑧 ∈ ( BaseSet ‘ 𝑈 ) ∧ 𝑤 ∈ ( BaseSet ‘ 𝑈 ) ) ) → ( 𝑦 𝐶 𝑤 ) ∈ ℝ )
21 rpre ⊢ ( 𝑟 ∈ ℝ+ → 𝑟 ∈ ℝ )
22 21 ad2antlr ⊢ ( ( ( ( 𝑈 ∈ NrmCVec ∧ ( 𝑥 ∈ ( BaseSet ‘ 𝑈 ) ∧ 𝑦 ∈ ( BaseSet ‘ 𝑈 ) ) ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑧 ∈ ( BaseSet ‘ 𝑈 ) ∧ 𝑤 ∈ ( BaseSet ‘ 𝑈 ) ) ) → 𝑟 ∈ ℝ )
23 lt2halves ⊢ ( ( ( 𝑥 𝐶 𝑧 ) ∈ ℝ ∧ ( 𝑦 𝐶 𝑤 ) ∈ ℝ ∧ 𝑟 ∈ ℝ ) → ( ( ( 𝑥 𝐶 𝑧 ) < ( 𝑟 / 2 ) ∧ ( 𝑦 𝐶 𝑤 ) < ( 𝑟 / 2 ) ) → ( ( 𝑥 𝐶 𝑧 ) + ( 𝑦 𝐶 𝑤 ) ) < 𝑟 ) )
24 15 20 22 23 syl3anc ⊢ ( ( ( ( 𝑈 ∈ NrmCVec ∧ ( 𝑥 ∈ ( BaseSet ‘ 𝑈 ) ∧ 𝑦 ∈ ( BaseSet ‘ 𝑈 ) ) ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑧 ∈ ( BaseSet ‘ 𝑈 ) ∧ 𝑤 ∈ ( BaseSet ‘ 𝑈 ) ) ) → ( ( ( 𝑥 𝐶 𝑧 ) < ( 𝑟 / 2 ) ∧ ( 𝑦 𝐶 𝑤 ) < ( 𝑟 / 2 ) ) → ( ( 𝑥 𝐶 𝑧 ) + ( 𝑦 𝐶 𝑤 ) ) < 𝑟 ) )
25 eqid ⊢ ( −𝑣 ‘ 𝑈 ) = ( −𝑣 ‘ 𝑈 )
26 4 25 nvmcl ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑥 ∈ ( BaseSet ‘ 𝑈 ) ∧ 𝑧 ∈ ( BaseSet ‘ 𝑈 ) ) → ( 𝑥 ( −𝑣 ‘ 𝑈 ) 𝑧 ) ∈ ( BaseSet ‘ 𝑈 ) )
27 8 12 13 26 syl3anc ⊢ ( ( ( ( 𝑈 ∈ NrmCVec ∧ ( 𝑥 ∈ ( BaseSet ‘ 𝑈 ) ∧ 𝑦 ∈ ( BaseSet ‘ 𝑈 ) ) ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑧 ∈ ( BaseSet ‘ 𝑈 ) ∧ 𝑤 ∈ ( BaseSet ‘ 𝑈 ) ) ) → ( 𝑥 ( −𝑣 ‘ 𝑈 ) 𝑧 ) ∈ ( BaseSet ‘ 𝑈 ) )
28 4 25 nvmcl ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑦 ∈ ( BaseSet ‘ 𝑈 ) ∧ 𝑤 ∈ ( BaseSet ‘ 𝑈 ) ) → ( 𝑦 ( −𝑣 ‘ 𝑈 ) 𝑤 ) ∈ ( BaseSet ‘ 𝑈 ) )
29 8 17 18 28 syl3anc ⊢ ( ( ( ( 𝑈 ∈ NrmCVec ∧ ( 𝑥 ∈ ( BaseSet ‘ 𝑈 ) ∧ 𝑦 ∈ ( BaseSet ‘ 𝑈 ) ) ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑧 ∈ ( BaseSet ‘ 𝑈 ) ∧ 𝑤 ∈ ( BaseSet ‘ 𝑈 ) ) ) → ( 𝑦 ( −𝑣 ‘ 𝑈 ) 𝑤 ) ∈ ( BaseSet ‘ 𝑈 ) )
30 eqid ⊢ ( normCV ‘ 𝑈 ) = ( normCV ‘ 𝑈 )
31 4 3 30 nvtri ⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( 𝑥 ( −𝑣 ‘ 𝑈 ) 𝑧 ) ∈ ( BaseSet ‘ 𝑈 ) ∧ ( 𝑦 ( −𝑣 ‘ 𝑈 ) 𝑤 ) ∈ ( BaseSet ‘ 𝑈 ) ) → ( ( normCV ‘ 𝑈 ) ‘ ( ( 𝑥 ( −𝑣 ‘ 𝑈 ) 𝑧 ) 𝐺 ( 𝑦 ( −𝑣 ‘ 𝑈 ) 𝑤 ) ) ) ≤ ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝑥 ( −𝑣 ‘ 𝑈 ) 𝑧 ) ) + ( ( normCV ‘ 𝑈 ) ‘ ( 𝑦 ( −𝑣 ‘ 𝑈 ) 𝑤 ) ) ) )
32 8 27 29 31 syl3anc ⊢ ( ( ( ( 𝑈 ∈ NrmCVec ∧ ( 𝑥 ∈ ( BaseSet ‘ 𝑈 ) ∧ 𝑦 ∈ ( BaseSet ‘ 𝑈 ) ) ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑧 ∈ ( BaseSet ‘ 𝑈 ) ∧ 𝑤 ∈ ( BaseSet ‘ 𝑈 ) ) ) → ( ( normCV ‘ 𝑈 ) ‘ ( ( 𝑥 ( −𝑣 ‘ 𝑈 ) 𝑧 ) 𝐺 ( 𝑦 ( −𝑣 ‘ 𝑈 ) 𝑤 ) ) ) ≤ ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝑥 ( −𝑣 ‘ 𝑈 ) 𝑧 ) ) + ( ( normCV ‘ 𝑈 ) ‘ ( 𝑦 ( −𝑣 ‘ 𝑈 ) 𝑤 ) ) ) )
33 4 3 nvgcl ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑥 ∈ ( BaseSet ‘ 𝑈 ) ∧ 𝑦 ∈ ( BaseSet ‘ 𝑈 ) ) → ( 𝑥 𝐺 𝑦 ) ∈ ( BaseSet ‘ 𝑈 ) )
34 8 12 17 33 syl3anc ⊢ ( ( ( ( 𝑈 ∈ NrmCVec ∧ ( 𝑥 ∈ ( BaseSet ‘ 𝑈 ) ∧ 𝑦 ∈ ( BaseSet ‘ 𝑈 ) ) ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑧 ∈ ( BaseSet ‘ 𝑈 ) ∧ 𝑤 ∈ ( BaseSet ‘ 𝑈 ) ) ) → ( 𝑥 𝐺 𝑦 ) ∈ ( BaseSet ‘ 𝑈 ) )
35 4 3 nvgcl ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑧 ∈ ( BaseSet ‘ 𝑈 ) ∧ 𝑤 ∈ ( BaseSet ‘ 𝑈 ) ) → ( 𝑧 𝐺 𝑤 ) ∈ ( BaseSet ‘ 𝑈 ) )
36 8 13 18 35 syl3anc ⊢ ( ( ( ( 𝑈 ∈ NrmCVec ∧ ( 𝑥 ∈ ( BaseSet ‘ 𝑈 ) ∧ 𝑦 ∈ ( BaseSet ‘ 𝑈 ) ) ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑧 ∈ ( BaseSet ‘ 𝑈 ) ∧ 𝑤 ∈ ( BaseSet ‘ 𝑈 ) ) ) → ( 𝑧 𝐺 𝑤 ) ∈ ( BaseSet ‘ 𝑈 ) )
37 4 25 30 1 imsdval ⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( 𝑥 𝐺 𝑦 ) ∈ ( BaseSet ‘ 𝑈 ) ∧ ( 𝑧 𝐺 𝑤 ) ∈ ( BaseSet ‘ 𝑈 ) ) → ( ( 𝑥 𝐺 𝑦 ) 𝐶 ( 𝑧 𝐺 𝑤 ) ) = ( ( normCV ‘ 𝑈 ) ‘ ( ( 𝑥 𝐺 𝑦 ) ( −𝑣 ‘ 𝑈 ) ( 𝑧 𝐺 𝑤 ) ) ) )
38 8 34 36 37 syl3anc ⊢ ( ( ( ( 𝑈 ∈ NrmCVec ∧ ( 𝑥 ∈ ( BaseSet ‘ 𝑈 ) ∧ 𝑦 ∈ ( BaseSet ‘ 𝑈 ) ) ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑧 ∈ ( BaseSet ‘ 𝑈 ) ∧ 𝑤 ∈ ( BaseSet ‘ 𝑈 ) ) ) → ( ( 𝑥 𝐺 𝑦 ) 𝐶 ( 𝑧 𝐺 𝑤 ) ) = ( ( normCV ‘ 𝑈 ) ‘ ( ( 𝑥 𝐺 𝑦 ) ( −𝑣 ‘ 𝑈 ) ( 𝑧 𝐺 𝑤 ) ) ) )
39 4 3 25 nvaddsub4 ⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( 𝑥 ∈ ( BaseSet ‘ 𝑈 ) ∧ 𝑦 ∈ ( BaseSet ‘ 𝑈 ) ) ∧ ( 𝑧 ∈ ( BaseSet ‘ 𝑈 ) ∧ 𝑤 ∈ ( BaseSet ‘ 𝑈 ) ) ) → ( ( 𝑥 𝐺 𝑦 ) ( −𝑣 ‘ 𝑈 ) ( 𝑧 𝐺 𝑤 ) ) = ( ( 𝑥 ( −𝑣 ‘ 𝑈 ) 𝑧 ) 𝐺 ( 𝑦 ( −𝑣 ‘ 𝑈 ) 𝑤 ) ) )
40 8 12 17 13 18 39 syl122anc ⊢ ( ( ( ( 𝑈 ∈ NrmCVec ∧ ( 𝑥 ∈ ( BaseSet ‘ 𝑈 ) ∧ 𝑦 ∈ ( BaseSet ‘ 𝑈 ) ) ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑧 ∈ ( BaseSet ‘ 𝑈 ) ∧ 𝑤 ∈ ( BaseSet ‘ 𝑈 ) ) ) → ( ( 𝑥 𝐺 𝑦 ) ( −𝑣 ‘ 𝑈 ) ( 𝑧 𝐺 𝑤 ) ) = ( ( 𝑥 ( −𝑣 ‘ 𝑈 ) 𝑧 ) 𝐺 ( 𝑦 ( −𝑣 ‘ 𝑈 ) 𝑤 ) ) )
41 40 fveq2d ⊢ ( ( ( ( 𝑈 ∈ NrmCVec ∧ ( 𝑥 ∈ ( BaseSet ‘ 𝑈 ) ∧ 𝑦 ∈ ( BaseSet ‘ 𝑈 ) ) ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑧 ∈ ( BaseSet ‘ 𝑈 ) ∧ 𝑤 ∈ ( BaseSet ‘ 𝑈 ) ) ) → ( ( normCV ‘ 𝑈 ) ‘ ( ( 𝑥 𝐺 𝑦 ) ( −𝑣 ‘ 𝑈 ) ( 𝑧 𝐺 𝑤 ) ) ) = ( ( normCV ‘ 𝑈 ) ‘ ( ( 𝑥 ( −𝑣 ‘ 𝑈 ) 𝑧 ) 𝐺 ( 𝑦 ( −𝑣 ‘ 𝑈 ) 𝑤 ) ) ) )
42 38 41 eqtrd ⊢ ( ( ( ( 𝑈 ∈ NrmCVec ∧ ( 𝑥 ∈ ( BaseSet ‘ 𝑈 ) ∧ 𝑦 ∈ ( BaseSet ‘ 𝑈 ) ) ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑧 ∈ ( BaseSet ‘ 𝑈 ) ∧ 𝑤 ∈ ( BaseSet ‘ 𝑈 ) ) ) → ( ( 𝑥 𝐺 𝑦 ) 𝐶 ( 𝑧 𝐺 𝑤 ) ) = ( ( normCV ‘ 𝑈 ) ‘ ( ( 𝑥 ( −𝑣 ‘ 𝑈 ) 𝑧 ) 𝐺 ( 𝑦 ( −𝑣 ‘ 𝑈 ) 𝑤 ) ) ) )
43 4 25 30 1 imsdval ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑥 ∈ ( BaseSet ‘ 𝑈 ) ∧ 𝑧 ∈ ( BaseSet ‘ 𝑈 ) ) → ( 𝑥 𝐶 𝑧 ) = ( ( normCV ‘ 𝑈 ) ‘ ( 𝑥 ( −𝑣 ‘ 𝑈 ) 𝑧 ) ) )
44 8 12 13 43 syl3anc ⊢ ( ( ( ( 𝑈 ∈ NrmCVec ∧ ( 𝑥 ∈ ( BaseSet ‘ 𝑈 ) ∧ 𝑦 ∈ ( BaseSet ‘ 𝑈 ) ) ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑧 ∈ ( BaseSet ‘ 𝑈 ) ∧ 𝑤 ∈ ( BaseSet ‘ 𝑈 ) ) ) → ( 𝑥 𝐶 𝑧 ) = ( ( normCV ‘ 𝑈 ) ‘ ( 𝑥 ( −𝑣 ‘ 𝑈 ) 𝑧 ) ) )
45 4 25 30 1 imsdval ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑦 ∈ ( BaseSet ‘ 𝑈 ) ∧ 𝑤 ∈ ( BaseSet ‘ 𝑈 ) ) → ( 𝑦 𝐶 𝑤 ) = ( ( normCV ‘ 𝑈 ) ‘ ( 𝑦 ( −𝑣 ‘ 𝑈 ) 𝑤 ) ) )
46 8 17 18 45 syl3anc ⊢ ( ( ( ( 𝑈 ∈ NrmCVec ∧ ( 𝑥 ∈ ( BaseSet ‘ 𝑈 ) ∧ 𝑦 ∈ ( BaseSet ‘ 𝑈 ) ) ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑧 ∈ ( BaseSet ‘ 𝑈 ) ∧ 𝑤 ∈ ( BaseSet ‘ 𝑈 ) ) ) → ( 𝑦 𝐶 𝑤 ) = ( ( normCV ‘ 𝑈 ) ‘ ( 𝑦 ( −𝑣 ‘ 𝑈 ) 𝑤 ) ) )
47 44 46 oveq12d ⊢ ( ( ( ( 𝑈 ∈ NrmCVec ∧ ( 𝑥 ∈ ( BaseSet ‘ 𝑈 ) ∧ 𝑦 ∈ ( BaseSet ‘ 𝑈 ) ) ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑧 ∈ ( BaseSet ‘ 𝑈 ) ∧ 𝑤 ∈ ( BaseSet ‘ 𝑈 ) ) ) → ( ( 𝑥 𝐶 𝑧 ) + ( 𝑦 𝐶 𝑤 ) ) = ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝑥 ( −𝑣 ‘ 𝑈 ) 𝑧 ) ) + ( ( normCV ‘ 𝑈 ) ‘ ( 𝑦 ( −𝑣 ‘ 𝑈 ) 𝑤 ) ) ) )
48 32 42 47 3brtr4d ⊢ ( ( ( ( 𝑈 ∈ NrmCVec ∧ ( 𝑥 ∈ ( BaseSet ‘ 𝑈 ) ∧ 𝑦 ∈ ( BaseSet ‘ 𝑈 ) ) ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑧 ∈ ( BaseSet ‘ 𝑈 ) ∧ 𝑤 ∈ ( BaseSet ‘ 𝑈 ) ) ) → ( ( 𝑥 𝐺 𝑦 ) 𝐶 ( 𝑧 𝐺 𝑤 ) ) ≤ ( ( 𝑥 𝐶 𝑧 ) + ( 𝑦 𝐶 𝑤 ) ) )
49 metcl ⊢ ( ( 𝐶 ∈ ( Met ‘ ( BaseSet ‘ 𝑈 ) ) ∧ ( 𝑥 𝐺 𝑦 ) ∈ ( BaseSet ‘ 𝑈 ) ∧ ( 𝑧 𝐺 𝑤 ) ∈ ( BaseSet ‘ 𝑈 ) ) → ( ( 𝑥 𝐺 𝑦 ) 𝐶 ( 𝑧 𝐺 𝑤 ) ) ∈ ℝ )
50 10 34 36 49 syl3anc ⊢ ( ( ( ( 𝑈 ∈ NrmCVec ∧ ( 𝑥 ∈ ( BaseSet ‘ 𝑈 ) ∧ 𝑦 ∈ ( BaseSet ‘ 𝑈 ) ) ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑧 ∈ ( BaseSet ‘ 𝑈 ) ∧ 𝑤 ∈ ( BaseSet ‘ 𝑈 ) ) ) → ( ( 𝑥 𝐺 𝑦 ) 𝐶 ( 𝑧 𝐺 𝑤 ) ) ∈ ℝ )
51 15 20 readdcld ⊢ ( ( ( ( 𝑈 ∈ NrmCVec ∧ ( 𝑥 ∈ ( BaseSet ‘ 𝑈 ) ∧ 𝑦 ∈ ( BaseSet ‘ 𝑈 ) ) ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑧 ∈ ( BaseSet ‘ 𝑈 ) ∧ 𝑤 ∈ ( BaseSet ‘ 𝑈 ) ) ) → ( ( 𝑥 𝐶 𝑧 ) + ( 𝑦 𝐶 𝑤 ) ) ∈ ℝ )
52 lelttr ⊢ ( ( ( ( 𝑥 𝐺 𝑦 ) 𝐶 ( 𝑧 𝐺 𝑤 ) ) ∈ ℝ ∧ ( ( 𝑥 𝐶 𝑧 ) + ( 𝑦 𝐶 𝑤 ) ) ∈ ℝ ∧ 𝑟 ∈ ℝ ) → ( ( ( ( 𝑥 𝐺 𝑦 ) 𝐶 ( 𝑧 𝐺 𝑤 ) ) ≤ ( ( 𝑥 𝐶 𝑧 ) + ( 𝑦 𝐶 𝑤 ) ) ∧ ( ( 𝑥 𝐶 𝑧 ) + ( 𝑦 𝐶 𝑤 ) ) < 𝑟 ) → ( ( 𝑥 𝐺 𝑦 ) 𝐶 ( 𝑧 𝐺 𝑤 ) ) < 𝑟 ) )
53 50 51 22 52 syl3anc ⊢ ( ( ( ( 𝑈 ∈ NrmCVec ∧ ( 𝑥 ∈ ( BaseSet ‘ 𝑈 ) ∧ 𝑦 ∈ ( BaseSet ‘ 𝑈 ) ) ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑧 ∈ ( BaseSet ‘ 𝑈 ) ∧ 𝑤 ∈ ( BaseSet ‘ 𝑈 ) ) ) → ( ( ( ( 𝑥 𝐺 𝑦 ) 𝐶 ( 𝑧 𝐺 𝑤 ) ) ≤ ( ( 𝑥 𝐶 𝑧 ) + ( 𝑦 𝐶 𝑤 ) ) ∧ ( ( 𝑥 𝐶 𝑧 ) + ( 𝑦 𝐶 𝑤 ) ) < 𝑟 ) → ( ( 𝑥 𝐺 𝑦 ) 𝐶 ( 𝑧 𝐺 𝑤 ) ) < 𝑟 ) )
54 48 53 mpand ⊢ ( ( ( ( 𝑈 ∈ NrmCVec ∧ ( 𝑥 ∈ ( BaseSet ‘ 𝑈 ) ∧ 𝑦 ∈ ( BaseSet ‘ 𝑈 ) ) ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑧 ∈ ( BaseSet ‘ 𝑈 ) ∧ 𝑤 ∈ ( BaseSet ‘ 𝑈 ) ) ) → ( ( ( 𝑥 𝐶 𝑧 ) + ( 𝑦 𝐶 𝑤 ) ) < 𝑟 → ( ( 𝑥 𝐺 𝑦 ) 𝐶 ( 𝑧 𝐺 𝑤 ) ) < 𝑟 ) )
55 24 54 syld ⊢ ( ( ( ( 𝑈 ∈ NrmCVec ∧ ( 𝑥 ∈ ( BaseSet ‘ 𝑈 ) ∧ 𝑦 ∈ ( BaseSet ‘ 𝑈 ) ) ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑧 ∈ ( BaseSet ‘ 𝑈 ) ∧ 𝑤 ∈ ( BaseSet ‘ 𝑈 ) ) ) → ( ( ( 𝑥 𝐶 𝑧 ) < ( 𝑟 / 2 ) ∧ ( 𝑦 𝐶 𝑤 ) < ( 𝑟 / 2 ) ) → ( ( 𝑥 𝐺 𝑦 ) 𝐶 ( 𝑧 𝐺 𝑤 ) ) < 𝑟 ) )
56 55 ralrimivva ⊢ ( ( ( 𝑈 ∈ NrmCVec ∧ ( 𝑥 ∈ ( BaseSet ‘ 𝑈 ) ∧ 𝑦 ∈ ( BaseSet ‘ 𝑈 ) ) ) ∧ 𝑟 ∈ ℝ+ ) → ∀ 𝑧 ∈ ( BaseSet ‘ 𝑈 ) ∀ 𝑤 ∈ ( BaseSet ‘ 𝑈 ) ( ( ( 𝑥 𝐶 𝑧 ) < ( 𝑟 / 2 ) ∧ ( 𝑦 𝐶 𝑤 ) < ( 𝑟 / 2 ) ) → ( ( 𝑥 𝐺 𝑦 ) 𝐶 ( 𝑧 𝐺 𝑤 ) ) < 𝑟 ) )
57 breq2 ⊢ ( 𝑠 = ( 𝑟 / 2 ) → ( ( 𝑥 𝐶 𝑧 ) < 𝑠 ↔ ( 𝑥 𝐶 𝑧 ) < ( 𝑟 / 2 ) ) )
58 breq2 ⊢ ( 𝑠 = ( 𝑟 / 2 ) → ( ( 𝑦 𝐶 𝑤 ) < 𝑠 ↔ ( 𝑦 𝐶 𝑤 ) < ( 𝑟 / 2 ) ) )
59 57 58 anbi12d ⊢ ( 𝑠 = ( 𝑟 / 2 ) → ( ( ( 𝑥 𝐶 𝑧 ) < 𝑠 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑠 ) ↔ ( ( 𝑥 𝐶 𝑧 ) < ( 𝑟 / 2 ) ∧ ( 𝑦 𝐶 𝑤 ) < ( 𝑟 / 2 ) ) ) )
60 59 imbi1d ⊢ ( 𝑠 = ( 𝑟 / 2 ) → ( ( ( ( 𝑥 𝐶 𝑧 ) < 𝑠 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑠 ) → ( ( 𝑥 𝐺 𝑦 ) 𝐶 ( 𝑧 𝐺 𝑤 ) ) < 𝑟 ) ↔ ( ( ( 𝑥 𝐶 𝑧 ) < ( 𝑟 / 2 ) ∧ ( 𝑦 𝐶 𝑤 ) < ( 𝑟 / 2 ) ) → ( ( 𝑥 𝐺 𝑦 ) 𝐶 ( 𝑧 𝐺 𝑤 ) ) < 𝑟 ) ) )
61 60 2ralbidv ⊢ ( 𝑠 = ( 𝑟 / 2 ) → ( ∀ 𝑧 ∈ ( BaseSet ‘ 𝑈 ) ∀ 𝑤 ∈ ( BaseSet ‘ 𝑈 ) ( ( ( 𝑥 𝐶 𝑧 ) < 𝑠 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑠 ) → ( ( 𝑥 𝐺 𝑦 ) 𝐶 ( 𝑧 𝐺 𝑤 ) ) < 𝑟 ) ↔ ∀ 𝑧 ∈ ( BaseSet ‘ 𝑈 ) ∀ 𝑤 ∈ ( BaseSet ‘ 𝑈 ) ( ( ( 𝑥 𝐶 𝑧 ) < ( 𝑟 / 2 ) ∧ ( 𝑦 𝐶 𝑤 ) < ( 𝑟 / 2 ) ) → ( ( 𝑥 𝐺 𝑦 ) 𝐶 ( 𝑧 𝐺 𝑤 ) ) < 𝑟 ) ) )
62 61 rspcev ⊢ ( ( ( 𝑟 / 2 ) ∈ ℝ+ ∧ ∀ 𝑧 ∈ ( BaseSet ‘ 𝑈 ) ∀ 𝑤 ∈ ( BaseSet ‘ 𝑈 ) ( ( ( 𝑥 𝐶 𝑧 ) < ( 𝑟 / 2 ) ∧ ( 𝑦 𝐶 𝑤 ) < ( 𝑟 / 2 ) ) → ( ( 𝑥 𝐺 𝑦 ) 𝐶 ( 𝑧 𝐺 𝑤 ) ) < 𝑟 ) ) → ∃ 𝑠 ∈ ℝ+ ∀ 𝑧 ∈ ( BaseSet ‘ 𝑈 ) ∀ 𝑤 ∈ ( BaseSet ‘ 𝑈 ) ( ( ( 𝑥 𝐶 𝑧 ) < 𝑠 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑠 ) → ( ( 𝑥 𝐺 𝑦 ) 𝐶 ( 𝑧 𝐺 𝑤 ) ) < 𝑟 ) )
63 7 56 62 syl2anc ⊢ ( ( ( 𝑈 ∈ NrmCVec ∧ ( 𝑥 ∈ ( BaseSet ‘ 𝑈 ) ∧ 𝑦 ∈ ( BaseSet ‘ 𝑈 ) ) ) ∧ 𝑟 ∈ ℝ+ ) → ∃ 𝑠 ∈ ℝ+ ∀ 𝑧 ∈ ( BaseSet ‘ 𝑈 ) ∀ 𝑤 ∈ ( BaseSet ‘ 𝑈 ) ( ( ( 𝑥 𝐶 𝑧 ) < 𝑠 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑠 ) → ( ( 𝑥 𝐺 𝑦 ) 𝐶 ( 𝑧 𝐺 𝑤 ) ) < 𝑟 ) )
64 63 ralrimiva ⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( 𝑥 ∈ ( BaseSet ‘ 𝑈 ) ∧ 𝑦 ∈ ( BaseSet ‘ 𝑈 ) ) ) → ∀ 𝑟 ∈ ℝ+ ∃ 𝑠 ∈ ℝ+ ∀ 𝑧 ∈ ( BaseSet ‘ 𝑈 ) ∀ 𝑤 ∈ ( BaseSet ‘ 𝑈 ) ( ( ( 𝑥 𝐶 𝑧 ) < 𝑠 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑠 ) → ( ( 𝑥 𝐺 𝑦 ) 𝐶 ( 𝑧 𝐺 𝑤 ) ) < 𝑟 ) )
65 64 ralrimivva ⊢ ( 𝑈 ∈ NrmCVec → ∀ 𝑥 ∈ ( BaseSet ‘ 𝑈 ) ∀ 𝑦 ∈ ( BaseSet ‘ 𝑈 ) ∀ 𝑟 ∈ ℝ+ ∃ 𝑠 ∈ ℝ+ ∀ 𝑧 ∈ ( BaseSet ‘ 𝑈 ) ∀ 𝑤 ∈ ( BaseSet ‘ 𝑈 ) ( ( ( 𝑥 𝐶 𝑧 ) < 𝑠 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑠 ) → ( ( 𝑥 𝐺 𝑦 ) 𝐶 ( 𝑧 𝐺 𝑤 ) ) < 𝑟 ) )
66 4 1 imsxmet ⊢ ( 𝑈 ∈ NrmCVec → 𝐶 ∈ ( ∞Met ‘ ( BaseSet ‘ 𝑈 ) ) )
67 2 2 2 txmetcn ⊢ ( ( 𝐶 ∈ ( ∞Met ‘ ( BaseSet ‘ 𝑈 ) ) ∧ 𝐶 ∈ ( ∞Met ‘ ( BaseSet ‘ 𝑈 ) ) ∧ 𝐶 ∈ ( ∞Met ‘ ( BaseSet ‘ 𝑈 ) ) ) → ( 𝐺 ∈ ( ( 𝐽 ×t 𝐽 ) Cn 𝐽 ) ↔ ( 𝐺 : ( ( BaseSet ‘ 𝑈 ) × ( BaseSet ‘ 𝑈 ) ) ⟶ ( BaseSet ‘ 𝑈 ) ∧ ∀ 𝑥 ∈ ( BaseSet ‘ 𝑈 ) ∀ 𝑦 ∈ ( BaseSet ‘ 𝑈 ) ∀ 𝑟 ∈ ℝ+ ∃ 𝑠 ∈ ℝ+ ∀ 𝑧 ∈ ( BaseSet ‘ 𝑈 ) ∀ 𝑤 ∈ ( BaseSet ‘ 𝑈 ) ( ( ( 𝑥 𝐶 𝑧 ) < 𝑠 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑠 ) → ( ( 𝑥 𝐺 𝑦 ) 𝐶 ( 𝑧 𝐺 𝑤 ) ) < 𝑟 ) ) ) )
68 66 66 66 67 syl3anc ⊢ ( 𝑈 ∈ NrmCVec → ( 𝐺 ∈ ( ( 𝐽 ×t 𝐽 ) Cn 𝐽 ) ↔ ( 𝐺 : ( ( BaseSet ‘ 𝑈 ) × ( BaseSet ‘ 𝑈 ) ) ⟶ ( BaseSet ‘ 𝑈 ) ∧ ∀ 𝑥 ∈ ( BaseSet ‘ 𝑈 ) ∀ 𝑦 ∈ ( BaseSet ‘ 𝑈 ) ∀ 𝑟 ∈ ℝ+ ∃ 𝑠 ∈ ℝ+ ∀ 𝑧 ∈ ( BaseSet ‘ 𝑈 ) ∀ 𝑤 ∈ ( BaseSet ‘ 𝑈 ) ( ( ( 𝑥 𝐶 𝑧 ) < 𝑠 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑠 ) → ( ( 𝑥 𝐺 𝑦 ) 𝐶 ( 𝑧 𝐺 𝑤 ) ) < 𝑟 ) ) ) )
69 5 65 68 mpbir2and ⊢ ( 𝑈 ∈ NrmCVec → 𝐺 ∈ ( ( 𝐽 ×t 𝐽 ) Cn 𝐽 ) )