# 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}=\mathrm{IndMet}\left({U}\right)$
vacn.j ${⊢}{J}=\mathrm{MetOpen}\left({C}\right)$
vacn.g ${⊢}{G}={+}_{v}\left({U}\right)$
Assertion vacn ${⊢}{U}\in \mathrm{NrmCVec}\to {G}\in \left(\left({J}{×}_{t}{J}\right)\mathrm{Cn}{J}\right)$

### Proof

Step Hyp Ref Expression
1 vacn.c ${⊢}{C}=\mathrm{IndMet}\left({U}\right)$
2 vacn.j ${⊢}{J}=\mathrm{MetOpen}\left({C}\right)$
3 vacn.g ${⊢}{G}={+}_{v}\left({U}\right)$
4 eqid ${⊢}\mathrm{BaseSet}\left({U}\right)=\mathrm{BaseSet}\left({U}\right)$
5 4 3 nvgf ${⊢}{U}\in \mathrm{NrmCVec}\to {G}:\mathrm{BaseSet}\left({U}\right)×\mathrm{BaseSet}\left({U}\right)⟶\mathrm{BaseSet}\left({U}\right)$
6 rphalfcl ${⊢}{r}\in {ℝ}^{+}\to \frac{{r}}{2}\in {ℝ}^{+}$
7 6 adantl ${⊢}\left(\left({U}\in \mathrm{NrmCVec}\wedge \left({x}\in \mathrm{BaseSet}\left({U}\right)\wedge {y}\in \mathrm{BaseSet}\left({U}\right)\right)\right)\wedge {r}\in {ℝ}^{+}\right)\to \frac{{r}}{2}\in {ℝ}^{+}$
8 simplll ${⊢}\left(\left(\left({U}\in \mathrm{NrmCVec}\wedge \left({x}\in \mathrm{BaseSet}\left({U}\right)\wedge {y}\in \mathrm{BaseSet}\left({U}\right)\right)\right)\wedge {r}\in {ℝ}^{+}\right)\wedge \left({z}\in \mathrm{BaseSet}\left({U}\right)\wedge {w}\in \mathrm{BaseSet}\left({U}\right)\right)\right)\to {U}\in \mathrm{NrmCVec}$
9 4 1 imsmet ${⊢}{U}\in \mathrm{NrmCVec}\to {C}\in \mathrm{Met}\left(\mathrm{BaseSet}\left({U}\right)\right)$
10 8 9 syl ${⊢}\left(\left(\left({U}\in \mathrm{NrmCVec}\wedge \left({x}\in \mathrm{BaseSet}\left({U}\right)\wedge {y}\in \mathrm{BaseSet}\left({U}\right)\right)\right)\wedge {r}\in {ℝ}^{+}\right)\wedge \left({z}\in \mathrm{BaseSet}\left({U}\right)\wedge {w}\in \mathrm{BaseSet}\left({U}\right)\right)\right)\to {C}\in \mathrm{Met}\left(\mathrm{BaseSet}\left({U}\right)\right)$
11 simplrl ${⊢}\left(\left({U}\in \mathrm{NrmCVec}\wedge \left({x}\in \mathrm{BaseSet}\left({U}\right)\wedge {y}\in \mathrm{BaseSet}\left({U}\right)\right)\right)\wedge {r}\in {ℝ}^{+}\right)\to {x}\in \mathrm{BaseSet}\left({U}\right)$
12 11 adantr ${⊢}\left(\left(\left({U}\in \mathrm{NrmCVec}\wedge \left({x}\in \mathrm{BaseSet}\left({U}\right)\wedge {y}\in \mathrm{BaseSet}\left({U}\right)\right)\right)\wedge {r}\in {ℝ}^{+}\right)\wedge \left({z}\in \mathrm{BaseSet}\left({U}\right)\wedge {w}\in \mathrm{BaseSet}\left({U}\right)\right)\right)\to {x}\in \mathrm{BaseSet}\left({U}\right)$
13 simprl ${⊢}\left(\left(\left({U}\in \mathrm{NrmCVec}\wedge \left({x}\in \mathrm{BaseSet}\left({U}\right)\wedge {y}\in \mathrm{BaseSet}\left({U}\right)\right)\right)\wedge {r}\in {ℝ}^{+}\right)\wedge \left({z}\in \mathrm{BaseSet}\left({U}\right)\wedge {w}\in \mathrm{BaseSet}\left({U}\right)\right)\right)\to {z}\in \mathrm{BaseSet}\left({U}\right)$
14 metcl ${⊢}\left({C}\in \mathrm{Met}\left(\mathrm{BaseSet}\left({U}\right)\right)\wedge {x}\in \mathrm{BaseSet}\left({U}\right)\wedge {z}\in \mathrm{BaseSet}\left({U}\right)\right)\to {x}{C}{z}\in ℝ$
15 10 12 13 14 syl3anc ${⊢}\left(\left(\left({U}\in \mathrm{NrmCVec}\wedge \left({x}\in \mathrm{BaseSet}\left({U}\right)\wedge {y}\in \mathrm{BaseSet}\left({U}\right)\right)\right)\wedge {r}\in {ℝ}^{+}\right)\wedge \left({z}\in \mathrm{BaseSet}\left({U}\right)\wedge {w}\in \mathrm{BaseSet}\left({U}\right)\right)\right)\to {x}{C}{z}\in ℝ$
16 simplrr ${⊢}\left(\left({U}\in \mathrm{NrmCVec}\wedge \left({x}\in \mathrm{BaseSet}\left({U}\right)\wedge {y}\in \mathrm{BaseSet}\left({U}\right)\right)\right)\wedge {r}\in {ℝ}^{+}\right)\to {y}\in \mathrm{BaseSet}\left({U}\right)$
17 16 adantr ${⊢}\left(\left(\left({U}\in \mathrm{NrmCVec}\wedge \left({x}\in \mathrm{BaseSet}\left({U}\right)\wedge {y}\in \mathrm{BaseSet}\left({U}\right)\right)\right)\wedge {r}\in {ℝ}^{+}\right)\wedge \left({z}\in \mathrm{BaseSet}\left({U}\right)\wedge {w}\in \mathrm{BaseSet}\left({U}\right)\right)\right)\to {y}\in \mathrm{BaseSet}\left({U}\right)$
18 simprr ${⊢}\left(\left(\left({U}\in \mathrm{NrmCVec}\wedge \left({x}\in \mathrm{BaseSet}\left({U}\right)\wedge {y}\in \mathrm{BaseSet}\left({U}\right)\right)\right)\wedge {r}\in {ℝ}^{+}\right)\wedge \left({z}\in \mathrm{BaseSet}\left({U}\right)\wedge {w}\in \mathrm{BaseSet}\left({U}\right)\right)\right)\to {w}\in \mathrm{BaseSet}\left({U}\right)$
19 metcl ${⊢}\left({C}\in \mathrm{Met}\left(\mathrm{BaseSet}\left({U}\right)\right)\wedge {y}\in \mathrm{BaseSet}\left({U}\right)\wedge {w}\in \mathrm{BaseSet}\left({U}\right)\right)\to {y}{C}{w}\in ℝ$
20 10 17 18 19 syl3anc ${⊢}\left(\left(\left({U}\in \mathrm{NrmCVec}\wedge \left({x}\in \mathrm{BaseSet}\left({U}\right)\wedge {y}\in \mathrm{BaseSet}\left({U}\right)\right)\right)\wedge {r}\in {ℝ}^{+}\right)\wedge \left({z}\in \mathrm{BaseSet}\left({U}\right)\wedge {w}\in \mathrm{BaseSet}\left({U}\right)\right)\right)\to {y}{C}{w}\in ℝ$
21 rpre ${⊢}{r}\in {ℝ}^{+}\to {r}\in ℝ$
22 21 ad2antlr ${⊢}\left(\left(\left({U}\in \mathrm{NrmCVec}\wedge \left({x}\in \mathrm{BaseSet}\left({U}\right)\wedge {y}\in \mathrm{BaseSet}\left({U}\right)\right)\right)\wedge {r}\in {ℝ}^{+}\right)\wedge \left({z}\in \mathrm{BaseSet}\left({U}\right)\wedge {w}\in \mathrm{BaseSet}\left({U}\right)\right)\right)\to {r}\in ℝ$
23 lt2halves ${⊢}\left({x}{C}{z}\in ℝ\wedge {y}{C}{w}\in ℝ\wedge {r}\in ℝ\right)\to \left(\left({x}{C}{z}<\frac{{r}}{2}\wedge {y}{C}{w}<\frac{{r}}{2}\right)\to \left({x}{C}{z}\right)+\left({y}{C}{w}\right)<{r}\right)$
24 15 20 22 23 syl3anc ${⊢}\left(\left(\left({U}\in \mathrm{NrmCVec}\wedge \left({x}\in \mathrm{BaseSet}\left({U}\right)\wedge {y}\in \mathrm{BaseSet}\left({U}\right)\right)\right)\wedge {r}\in {ℝ}^{+}\right)\wedge \left({z}\in \mathrm{BaseSet}\left({U}\right)\wedge {w}\in \mathrm{BaseSet}\left({U}\right)\right)\right)\to \left(\left({x}{C}{z}<\frac{{r}}{2}\wedge {y}{C}{w}<\frac{{r}}{2}\right)\to \left({x}{C}{z}\right)+\left({y}{C}{w}\right)<{r}\right)$
25 eqid ${⊢}{-}_{v}\left({U}\right)={-}_{v}\left({U}\right)$
26 4 25 nvmcl ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {x}\in \mathrm{BaseSet}\left({U}\right)\wedge {z}\in \mathrm{BaseSet}\left({U}\right)\right)\to {x}{-}_{v}\left({U}\right){z}\in \mathrm{BaseSet}\left({U}\right)$
27 8 12 13 26 syl3anc ${⊢}\left(\left(\left({U}\in \mathrm{NrmCVec}\wedge \left({x}\in \mathrm{BaseSet}\left({U}\right)\wedge {y}\in \mathrm{BaseSet}\left({U}\right)\right)\right)\wedge {r}\in {ℝ}^{+}\right)\wedge \left({z}\in \mathrm{BaseSet}\left({U}\right)\wedge {w}\in \mathrm{BaseSet}\left({U}\right)\right)\right)\to {x}{-}_{v}\left({U}\right){z}\in \mathrm{BaseSet}\left({U}\right)$
28 4 25 nvmcl ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {y}\in \mathrm{BaseSet}\left({U}\right)\wedge {w}\in \mathrm{BaseSet}\left({U}\right)\right)\to {y}{-}_{v}\left({U}\right){w}\in \mathrm{BaseSet}\left({U}\right)$
29 8 17 18 28 syl3anc ${⊢}\left(\left(\left({U}\in \mathrm{NrmCVec}\wedge \left({x}\in \mathrm{BaseSet}\left({U}\right)\wedge {y}\in \mathrm{BaseSet}\left({U}\right)\right)\right)\wedge {r}\in {ℝ}^{+}\right)\wedge \left({z}\in \mathrm{BaseSet}\left({U}\right)\wedge {w}\in \mathrm{BaseSet}\left({U}\right)\right)\right)\to {y}{-}_{v}\left({U}\right){w}\in \mathrm{BaseSet}\left({U}\right)$
30 eqid ${⊢}{norm}_{CV}\left({U}\right)={norm}_{CV}\left({U}\right)$
31 4 3 30 nvtri ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {x}{-}_{v}\left({U}\right){z}\in \mathrm{BaseSet}\left({U}\right)\wedge {y}{-}_{v}\left({U}\right){w}\in \mathrm{BaseSet}\left({U}\right)\right)\to {norm}_{CV}\left({U}\right)\left(\left({x}{-}_{v}\left({U}\right){z}\right){G}\left({y}{-}_{v}\left({U}\right){w}\right)\right)\le {norm}_{CV}\left({U}\right)\left({x}{-}_{v}\left({U}\right){z}\right)+{norm}_{CV}\left({U}\right)\left({y}{-}_{v}\left({U}\right){w}\right)$
32 8 27 29 31 syl3anc ${⊢}\left(\left(\left({U}\in \mathrm{NrmCVec}\wedge \left({x}\in \mathrm{BaseSet}\left({U}\right)\wedge {y}\in \mathrm{BaseSet}\left({U}\right)\right)\right)\wedge {r}\in {ℝ}^{+}\right)\wedge \left({z}\in \mathrm{BaseSet}\left({U}\right)\wedge {w}\in \mathrm{BaseSet}\left({U}\right)\right)\right)\to {norm}_{CV}\left({U}\right)\left(\left({x}{-}_{v}\left({U}\right){z}\right){G}\left({y}{-}_{v}\left({U}\right){w}\right)\right)\le {norm}_{CV}\left({U}\right)\left({x}{-}_{v}\left({U}\right){z}\right)+{norm}_{CV}\left({U}\right)\left({y}{-}_{v}\left({U}\right){w}\right)$
33 4 3 nvgcl ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {x}\in \mathrm{BaseSet}\left({U}\right)\wedge {y}\in \mathrm{BaseSet}\left({U}\right)\right)\to {x}{G}{y}\in \mathrm{BaseSet}\left({U}\right)$
34 8 12 17 33 syl3anc ${⊢}\left(\left(\left({U}\in \mathrm{NrmCVec}\wedge \left({x}\in \mathrm{BaseSet}\left({U}\right)\wedge {y}\in \mathrm{BaseSet}\left({U}\right)\right)\right)\wedge {r}\in {ℝ}^{+}\right)\wedge \left({z}\in \mathrm{BaseSet}\left({U}\right)\wedge {w}\in \mathrm{BaseSet}\left({U}\right)\right)\right)\to {x}{G}{y}\in \mathrm{BaseSet}\left({U}\right)$
35 4 3 nvgcl ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {z}\in \mathrm{BaseSet}\left({U}\right)\wedge {w}\in \mathrm{BaseSet}\left({U}\right)\right)\to {z}{G}{w}\in \mathrm{BaseSet}\left({U}\right)$
36 8 13 18 35 syl3anc ${⊢}\left(\left(\left({U}\in \mathrm{NrmCVec}\wedge \left({x}\in \mathrm{BaseSet}\left({U}\right)\wedge {y}\in \mathrm{BaseSet}\left({U}\right)\right)\right)\wedge {r}\in {ℝ}^{+}\right)\wedge \left({z}\in \mathrm{BaseSet}\left({U}\right)\wedge {w}\in \mathrm{BaseSet}\left({U}\right)\right)\right)\to {z}{G}{w}\in \mathrm{BaseSet}\left({U}\right)$
37 4 25 30 1 imsdval ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {x}{G}{y}\in \mathrm{BaseSet}\left({U}\right)\wedge {z}{G}{w}\in \mathrm{BaseSet}\left({U}\right)\right)\to \left({x}{G}{y}\right){C}\left({z}{G}{w}\right)={norm}_{CV}\left({U}\right)\left(\left({x}{G}{y}\right){-}_{v}\left({U}\right)\left({z}{G}{w}\right)\right)$
38 8 34 36 37 syl3anc ${⊢}\left(\left(\left({U}\in \mathrm{NrmCVec}\wedge \left({x}\in \mathrm{BaseSet}\left({U}\right)\wedge {y}\in \mathrm{BaseSet}\left({U}\right)\right)\right)\wedge {r}\in {ℝ}^{+}\right)\wedge \left({z}\in \mathrm{BaseSet}\left({U}\right)\wedge {w}\in \mathrm{BaseSet}\left({U}\right)\right)\right)\to \left({x}{G}{y}\right){C}\left({z}{G}{w}\right)={norm}_{CV}\left({U}\right)\left(\left({x}{G}{y}\right){-}_{v}\left({U}\right)\left({z}{G}{w}\right)\right)$
39 4 3 25 nvaddsub4 ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge \left({x}\in \mathrm{BaseSet}\left({U}\right)\wedge {y}\in \mathrm{BaseSet}\left({U}\right)\right)\wedge \left({z}\in \mathrm{BaseSet}\left({U}\right)\wedge {w}\in \mathrm{BaseSet}\left({U}\right)\right)\right)\to \left({x}{G}{y}\right){-}_{v}\left({U}\right)\left({z}{G}{w}\right)=\left({x}{-}_{v}\left({U}\right){z}\right){G}\left({y}{-}_{v}\left({U}\right){w}\right)$
40 8 12 17 13 18 39 syl122anc ${⊢}\left(\left(\left({U}\in \mathrm{NrmCVec}\wedge \left({x}\in \mathrm{BaseSet}\left({U}\right)\wedge {y}\in \mathrm{BaseSet}\left({U}\right)\right)\right)\wedge {r}\in {ℝ}^{+}\right)\wedge \left({z}\in \mathrm{BaseSet}\left({U}\right)\wedge {w}\in \mathrm{BaseSet}\left({U}\right)\right)\right)\to \left({x}{G}{y}\right){-}_{v}\left({U}\right)\left({z}{G}{w}\right)=\left({x}{-}_{v}\left({U}\right){z}\right){G}\left({y}{-}_{v}\left({U}\right){w}\right)$
41 40 fveq2d ${⊢}\left(\left(\left({U}\in \mathrm{NrmCVec}\wedge \left({x}\in \mathrm{BaseSet}\left({U}\right)\wedge {y}\in \mathrm{BaseSet}\left({U}\right)\right)\right)\wedge {r}\in {ℝ}^{+}\right)\wedge \left({z}\in \mathrm{BaseSet}\left({U}\right)\wedge {w}\in \mathrm{BaseSet}\left({U}\right)\right)\right)\to {norm}_{CV}\left({U}\right)\left(\left({x}{G}{y}\right){-}_{v}\left({U}\right)\left({z}{G}{w}\right)\right)={norm}_{CV}\left({U}\right)\left(\left({x}{-}_{v}\left({U}\right){z}\right){G}\left({y}{-}_{v}\left({U}\right){w}\right)\right)$
42 38 41 eqtrd ${⊢}\left(\left(\left({U}\in \mathrm{NrmCVec}\wedge \left({x}\in \mathrm{BaseSet}\left({U}\right)\wedge {y}\in \mathrm{BaseSet}\left({U}\right)\right)\right)\wedge {r}\in {ℝ}^{+}\right)\wedge \left({z}\in \mathrm{BaseSet}\left({U}\right)\wedge {w}\in \mathrm{BaseSet}\left({U}\right)\right)\right)\to \left({x}{G}{y}\right){C}\left({z}{G}{w}\right)={norm}_{CV}\left({U}\right)\left(\left({x}{-}_{v}\left({U}\right){z}\right){G}\left({y}{-}_{v}\left({U}\right){w}\right)\right)$
43 4 25 30 1 imsdval ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {x}\in \mathrm{BaseSet}\left({U}\right)\wedge {z}\in \mathrm{BaseSet}\left({U}\right)\right)\to {x}{C}{z}={norm}_{CV}\left({U}\right)\left({x}{-}_{v}\left({U}\right){z}\right)$
44 8 12 13 43 syl3anc ${⊢}\left(\left(\left({U}\in \mathrm{NrmCVec}\wedge \left({x}\in \mathrm{BaseSet}\left({U}\right)\wedge {y}\in \mathrm{BaseSet}\left({U}\right)\right)\right)\wedge {r}\in {ℝ}^{+}\right)\wedge \left({z}\in \mathrm{BaseSet}\left({U}\right)\wedge {w}\in \mathrm{BaseSet}\left({U}\right)\right)\right)\to {x}{C}{z}={norm}_{CV}\left({U}\right)\left({x}{-}_{v}\left({U}\right){z}\right)$
45 4 25 30 1 imsdval ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {y}\in \mathrm{BaseSet}\left({U}\right)\wedge {w}\in \mathrm{BaseSet}\left({U}\right)\right)\to {y}{C}{w}={norm}_{CV}\left({U}\right)\left({y}{-}_{v}\left({U}\right){w}\right)$
46 8 17 18 45 syl3anc ${⊢}\left(\left(\left({U}\in \mathrm{NrmCVec}\wedge \left({x}\in \mathrm{BaseSet}\left({U}\right)\wedge {y}\in \mathrm{BaseSet}\left({U}\right)\right)\right)\wedge {r}\in {ℝ}^{+}\right)\wedge \left({z}\in \mathrm{BaseSet}\left({U}\right)\wedge {w}\in \mathrm{BaseSet}\left({U}\right)\right)\right)\to {y}{C}{w}={norm}_{CV}\left({U}\right)\left({y}{-}_{v}\left({U}\right){w}\right)$
47 44 46 oveq12d ${⊢}\left(\left(\left({U}\in \mathrm{NrmCVec}\wedge \left({x}\in \mathrm{BaseSet}\left({U}\right)\wedge {y}\in \mathrm{BaseSet}\left({U}\right)\right)\right)\wedge {r}\in {ℝ}^{+}\right)\wedge \left({z}\in \mathrm{BaseSet}\left({U}\right)\wedge {w}\in \mathrm{BaseSet}\left({U}\right)\right)\right)\to \left({x}{C}{z}\right)+\left({y}{C}{w}\right)={norm}_{CV}\left({U}\right)\left({x}{-}_{v}\left({U}\right){z}\right)+{norm}_{CV}\left({U}\right)\left({y}{-}_{v}\left({U}\right){w}\right)$
48 32 42 47 3brtr4d ${⊢}\left(\left(\left({U}\in \mathrm{NrmCVec}\wedge \left({x}\in \mathrm{BaseSet}\left({U}\right)\wedge {y}\in \mathrm{BaseSet}\left({U}\right)\right)\right)\wedge {r}\in {ℝ}^{+}\right)\wedge \left({z}\in \mathrm{BaseSet}\left({U}\right)\wedge {w}\in \mathrm{BaseSet}\left({U}\right)\right)\right)\to \left({x}{G}{y}\right){C}\left({z}{G}{w}\right)\le \left({x}{C}{z}\right)+\left({y}{C}{w}\right)$
49 metcl ${⊢}\left({C}\in \mathrm{Met}\left(\mathrm{BaseSet}\left({U}\right)\right)\wedge {x}{G}{y}\in \mathrm{BaseSet}\left({U}\right)\wedge {z}{G}{w}\in \mathrm{BaseSet}\left({U}\right)\right)\to \left({x}{G}{y}\right){C}\left({z}{G}{w}\right)\in ℝ$
50 10 34 36 49 syl3anc ${⊢}\left(\left(\left({U}\in \mathrm{NrmCVec}\wedge \left({x}\in \mathrm{BaseSet}\left({U}\right)\wedge {y}\in \mathrm{BaseSet}\left({U}\right)\right)\right)\wedge {r}\in {ℝ}^{+}\right)\wedge \left({z}\in \mathrm{BaseSet}\left({U}\right)\wedge {w}\in \mathrm{BaseSet}\left({U}\right)\right)\right)\to \left({x}{G}{y}\right){C}\left({z}{G}{w}\right)\in ℝ$
51 15 20 readdcld ${⊢}\left(\left(\left({U}\in \mathrm{NrmCVec}\wedge \left({x}\in \mathrm{BaseSet}\left({U}\right)\wedge {y}\in \mathrm{BaseSet}\left({U}\right)\right)\right)\wedge {r}\in {ℝ}^{+}\right)\wedge \left({z}\in \mathrm{BaseSet}\left({U}\right)\wedge {w}\in \mathrm{BaseSet}\left({U}\right)\right)\right)\to \left({x}{C}{z}\right)+\left({y}{C}{w}\right)\in ℝ$
52 lelttr ${⊢}\left(\left({x}{G}{y}\right){C}\left({z}{G}{w}\right)\in ℝ\wedge \left({x}{C}{z}\right)+\left({y}{C}{w}\right)\in ℝ\wedge {r}\in ℝ\right)\to \left(\left(\left({x}{G}{y}\right){C}\left({z}{G}{w}\right)\le \left({x}{C}{z}\right)+\left({y}{C}{w}\right)\wedge \left({x}{C}{z}\right)+\left({y}{C}{w}\right)<{r}\right)\to \left({x}{G}{y}\right){C}\left({z}{G}{w}\right)<{r}\right)$
53 50 51 22 52 syl3anc ${⊢}\left(\left(\left({U}\in \mathrm{NrmCVec}\wedge \left({x}\in \mathrm{BaseSet}\left({U}\right)\wedge {y}\in \mathrm{BaseSet}\left({U}\right)\right)\right)\wedge {r}\in {ℝ}^{+}\right)\wedge \left({z}\in \mathrm{BaseSet}\left({U}\right)\wedge {w}\in \mathrm{BaseSet}\left({U}\right)\right)\right)\to \left(\left(\left({x}{G}{y}\right){C}\left({z}{G}{w}\right)\le \left({x}{C}{z}\right)+\left({y}{C}{w}\right)\wedge \left({x}{C}{z}\right)+\left({y}{C}{w}\right)<{r}\right)\to \left({x}{G}{y}\right){C}\left({z}{G}{w}\right)<{r}\right)$
54 48 53 mpand ${⊢}\left(\left(\left({U}\in \mathrm{NrmCVec}\wedge \left({x}\in \mathrm{BaseSet}\left({U}\right)\wedge {y}\in \mathrm{BaseSet}\left({U}\right)\right)\right)\wedge {r}\in {ℝ}^{+}\right)\wedge \left({z}\in \mathrm{BaseSet}\left({U}\right)\wedge {w}\in \mathrm{BaseSet}\left({U}\right)\right)\right)\to \left(\left({x}{C}{z}\right)+\left({y}{C}{w}\right)<{r}\to \left({x}{G}{y}\right){C}\left({z}{G}{w}\right)<{r}\right)$
55 24 54 syld ${⊢}\left(\left(\left({U}\in \mathrm{NrmCVec}\wedge \left({x}\in \mathrm{BaseSet}\left({U}\right)\wedge {y}\in \mathrm{BaseSet}\left({U}\right)\right)\right)\wedge {r}\in {ℝ}^{+}\right)\wedge \left({z}\in \mathrm{BaseSet}\left({U}\right)\wedge {w}\in \mathrm{BaseSet}\left({U}\right)\right)\right)\to \left(\left({x}{C}{z}<\frac{{r}}{2}\wedge {y}{C}{w}<\frac{{r}}{2}\right)\to \left({x}{G}{y}\right){C}\left({z}{G}{w}\right)<{r}\right)$
56 55 ralrimivva ${⊢}\left(\left({U}\in \mathrm{NrmCVec}\wedge \left({x}\in \mathrm{BaseSet}\left({U}\right)\wedge {y}\in \mathrm{BaseSet}\left({U}\right)\right)\right)\wedge {r}\in {ℝ}^{+}\right)\to \forall {z}\in \mathrm{BaseSet}\left({U}\right)\phantom{\rule{.4em}{0ex}}\forall {w}\in \mathrm{BaseSet}\left({U}\right)\phantom{\rule{.4em}{0ex}}\left(\left({x}{C}{z}<\frac{{r}}{2}\wedge {y}{C}{w}<\frac{{r}}{2}\right)\to \left({x}{G}{y}\right){C}\left({z}{G}{w}\right)<{r}\right)$
57 breq2 ${⊢}{s}=\frac{{r}}{2}\to \left({x}{C}{z}<{s}↔{x}{C}{z}<\frac{{r}}{2}\right)$
58 breq2 ${⊢}{s}=\frac{{r}}{2}\to \left({y}{C}{w}<{s}↔{y}{C}{w}<\frac{{r}}{2}\right)$
59 57 58 anbi12d ${⊢}{s}=\frac{{r}}{2}\to \left(\left({x}{C}{z}<{s}\wedge {y}{C}{w}<{s}\right)↔\left({x}{C}{z}<\frac{{r}}{2}\wedge {y}{C}{w}<\frac{{r}}{2}\right)\right)$
60 59 imbi1d ${⊢}{s}=\frac{{r}}{2}\to \left(\left(\left({x}{C}{z}<{s}\wedge {y}{C}{w}<{s}\right)\to \left({x}{G}{y}\right){C}\left({z}{G}{w}\right)<{r}\right)↔\left(\left({x}{C}{z}<\frac{{r}}{2}\wedge {y}{C}{w}<\frac{{r}}{2}\right)\to \left({x}{G}{y}\right){C}\left({z}{G}{w}\right)<{r}\right)\right)$
61 60 2ralbidv ${⊢}{s}=\frac{{r}}{2}\to \left(\forall {z}\in \mathrm{BaseSet}\left({U}\right)\phantom{\rule{.4em}{0ex}}\forall {w}\in \mathrm{BaseSet}\left({U}\right)\phantom{\rule{.4em}{0ex}}\left(\left({x}{C}{z}<{s}\wedge {y}{C}{w}<{s}\right)\to \left({x}{G}{y}\right){C}\left({z}{G}{w}\right)<{r}\right)↔\forall {z}\in \mathrm{BaseSet}\left({U}\right)\phantom{\rule{.4em}{0ex}}\forall {w}\in \mathrm{BaseSet}\left({U}\right)\phantom{\rule{.4em}{0ex}}\left(\left({x}{C}{z}<\frac{{r}}{2}\wedge {y}{C}{w}<\frac{{r}}{2}\right)\to \left({x}{G}{y}\right){C}\left({z}{G}{w}\right)<{r}\right)\right)$
62 61 rspcev ${⊢}\left(\frac{{r}}{2}\in {ℝ}^{+}\wedge \forall {z}\in \mathrm{BaseSet}\left({U}\right)\phantom{\rule{.4em}{0ex}}\forall {w}\in \mathrm{BaseSet}\left({U}\right)\phantom{\rule{.4em}{0ex}}\left(\left({x}{C}{z}<\frac{{r}}{2}\wedge {y}{C}{w}<\frac{{r}}{2}\right)\to \left({x}{G}{y}\right){C}\left({z}{G}{w}\right)<{r}\right)\right)\to \exists {s}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {z}\in \mathrm{BaseSet}\left({U}\right)\phantom{\rule{.4em}{0ex}}\forall {w}\in \mathrm{BaseSet}\left({U}\right)\phantom{\rule{.4em}{0ex}}\left(\left({x}{C}{z}<{s}\wedge {y}{C}{w}<{s}\right)\to \left({x}{G}{y}\right){C}\left({z}{G}{w}\right)<{r}\right)$
63 7 56 62 syl2anc ${⊢}\left(\left({U}\in \mathrm{NrmCVec}\wedge \left({x}\in \mathrm{BaseSet}\left({U}\right)\wedge {y}\in \mathrm{BaseSet}\left({U}\right)\right)\right)\wedge {r}\in {ℝ}^{+}\right)\to \exists {s}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {z}\in \mathrm{BaseSet}\left({U}\right)\phantom{\rule{.4em}{0ex}}\forall {w}\in \mathrm{BaseSet}\left({U}\right)\phantom{\rule{.4em}{0ex}}\left(\left({x}{C}{z}<{s}\wedge {y}{C}{w}<{s}\right)\to \left({x}{G}{y}\right){C}\left({z}{G}{w}\right)<{r}\right)$
64 63 ralrimiva ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge \left({x}\in \mathrm{BaseSet}\left({U}\right)\wedge {y}\in \mathrm{BaseSet}\left({U}\right)\right)\right)\to \forall {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {s}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {z}\in \mathrm{BaseSet}\left({U}\right)\phantom{\rule{.4em}{0ex}}\forall {w}\in \mathrm{BaseSet}\left({U}\right)\phantom{\rule{.4em}{0ex}}\left(\left({x}{C}{z}<{s}\wedge {y}{C}{w}<{s}\right)\to \left({x}{G}{y}\right){C}\left({z}{G}{w}\right)<{r}\right)$
65 64 ralrimivva ${⊢}{U}\in \mathrm{NrmCVec}\to \forall {x}\in \mathrm{BaseSet}\left({U}\right)\phantom{\rule{.4em}{0ex}}\forall {y}\in \mathrm{BaseSet}\left({U}\right)\phantom{\rule{.4em}{0ex}}\forall {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {s}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {z}\in \mathrm{BaseSet}\left({U}\right)\phantom{\rule{.4em}{0ex}}\forall {w}\in \mathrm{BaseSet}\left({U}\right)\phantom{\rule{.4em}{0ex}}\left(\left({x}{C}{z}<{s}\wedge {y}{C}{w}<{s}\right)\to \left({x}{G}{y}\right){C}\left({z}{G}{w}\right)<{r}\right)$
66 4 1 imsxmet ${⊢}{U}\in \mathrm{NrmCVec}\to {C}\in \mathrm{\infty Met}\left(\mathrm{BaseSet}\left({U}\right)\right)$
67 2 2 2 txmetcn ${⊢}\left({C}\in \mathrm{\infty Met}\left(\mathrm{BaseSet}\left({U}\right)\right)\wedge {C}\in \mathrm{\infty Met}\left(\mathrm{BaseSet}\left({U}\right)\right)\wedge {C}\in \mathrm{\infty Met}\left(\mathrm{BaseSet}\left({U}\right)\right)\right)\to \left({G}\in \left(\left({J}{×}_{t}{J}\right)\mathrm{Cn}{J}\right)↔\left({G}:\mathrm{BaseSet}\left({U}\right)×\mathrm{BaseSet}\left({U}\right)⟶\mathrm{BaseSet}\left({U}\right)\wedge \forall {x}\in \mathrm{BaseSet}\left({U}\right)\phantom{\rule{.4em}{0ex}}\forall {y}\in \mathrm{BaseSet}\left({U}\right)\phantom{\rule{.4em}{0ex}}\forall {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {s}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {z}\in \mathrm{BaseSet}\left({U}\right)\phantom{\rule{.4em}{0ex}}\forall {w}\in \mathrm{BaseSet}\left({U}\right)\phantom{\rule{.4em}{0ex}}\left(\left({x}{C}{z}<{s}\wedge {y}{C}{w}<{s}\right)\to \left({x}{G}{y}\right){C}\left({z}{G}{w}\right)<{r}\right)\right)\right)$
68 66 66 66 67 syl3anc ${⊢}{U}\in \mathrm{NrmCVec}\to \left({G}\in \left(\left({J}{×}_{t}{J}\right)\mathrm{Cn}{J}\right)↔\left({G}:\mathrm{BaseSet}\left({U}\right)×\mathrm{BaseSet}\left({U}\right)⟶\mathrm{BaseSet}\left({U}\right)\wedge \forall {x}\in \mathrm{BaseSet}\left({U}\right)\phantom{\rule{.4em}{0ex}}\forall {y}\in \mathrm{BaseSet}\left({U}\right)\phantom{\rule{.4em}{0ex}}\forall {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {s}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {z}\in \mathrm{BaseSet}\left({U}\right)\phantom{\rule{.4em}{0ex}}\forall {w}\in \mathrm{BaseSet}\left({U}\right)\phantom{\rule{.4em}{0ex}}\left(\left({x}{C}{z}<{s}\wedge {y}{C}{w}<{s}\right)\to \left({x}{G}{y}\right){C}\left({z}{G}{w}\right)<{r}\right)\right)\right)$
69 5 65 68 mpbir2and ${⊢}{U}\in \mathrm{NrmCVec}\to {G}\in \left(\left({J}{×}_{t}{J}\right)\mathrm{Cn}{J}\right)$