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 𝐽 ) )