# Metamath Proof Explorer

## Theorem cnpwstotbnd

Description: A subset of A ^ I , where A C_ CC , is totally bounded iff it is bounded. (Contributed by Mario Carneiro, 14-Sep-2015)

Ref Expression
Hypotheses cnpwstotbnd.y ${⊢}{Y}=\left({ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}\right){↑}_{𝑠}{I}$
cnpwstotbnd.d ${⊢}{D}={\mathrm{dist}\left({Y}\right)↾}_{\left({X}×{X}\right)}$
Assertion cnpwstotbnd ${⊢}\left({A}\subseteq ℂ\wedge {I}\in \mathrm{Fin}\right)\to \left({D}\in \mathrm{TotBnd}\left({X}\right)↔{D}\in \mathrm{Bnd}\left({X}\right)\right)$

### Proof

Step Hyp Ref Expression
1 cnpwstotbnd.y ${⊢}{Y}=\left({ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}\right){↑}_{𝑠}{I}$
2 cnpwstotbnd.d ${⊢}{D}={\mathrm{dist}\left({Y}\right)↾}_{\left({X}×{X}\right)}$
3 eqid ${⊢}\mathrm{Scalar}\left({ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}\right){⨉}_{𝑠}\left({I}×\left\{{ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}\right\}\right)=\mathrm{Scalar}\left({ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}\right){⨉}_{𝑠}\left({I}×\left\{{ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}\right\}\right)$
4 eqid ${⊢}{\mathrm{Base}}_{\left(\mathrm{Scalar}\left({ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}\right){⨉}_{𝑠}\left({I}×\left\{{ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}\right\}\right)\right)}={\mathrm{Base}}_{\left(\mathrm{Scalar}\left({ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}\right){⨉}_{𝑠}\left({I}×\left\{{ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}\right\}\right)\right)}$
5 eqid ${⊢}{\mathrm{Base}}_{\left({I}×\left\{{ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}\right\}\right)\left({x}\right)}={\mathrm{Base}}_{\left({I}×\left\{{ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}\right\}\right)\left({x}\right)}$
6 eqid ${⊢}{\mathrm{dist}\left(\left({I}×\left\{{ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}\right\}\right)\left({x}\right)\right)↾}_{\left({\mathrm{Base}}_{\left({I}×\left\{{ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}\right\}\right)\left({x}\right)}×{\mathrm{Base}}_{\left({I}×\left\{{ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}\right\}\right)\left({x}\right)}\right)}={\mathrm{dist}\left(\left({I}×\left\{{ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}\right\}\right)\left({x}\right)\right)↾}_{\left({\mathrm{Base}}_{\left({I}×\left\{{ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}\right\}\right)\left({x}\right)}×{\mathrm{Base}}_{\left({I}×\left\{{ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}\right\}\right)\left({x}\right)}\right)}$
7 eqid ${⊢}\mathrm{dist}\left(\mathrm{Scalar}\left({ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}\right){⨉}_{𝑠}\left({I}×\left\{{ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}\right\}\right)\right)=\mathrm{dist}\left(\mathrm{Scalar}\left({ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}\right){⨉}_{𝑠}\left({I}×\left\{{ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}\right\}\right)\right)$
8 fvexd ${⊢}\left({A}\subseteq ℂ\wedge {I}\in \mathrm{Fin}\right)\to \mathrm{Scalar}\left({ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}\right)\in \mathrm{V}$
9 simpr ${⊢}\left({A}\subseteq ℂ\wedge {I}\in \mathrm{Fin}\right)\to {I}\in \mathrm{Fin}$
10 ovex ${⊢}{ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}\in \mathrm{V}$
11 fnconstg ${⊢}{ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}\in \mathrm{V}\to \left({I}×\left\{{ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}\right\}\right)Fn{I}$
12 10 11 mp1i ${⊢}\left({A}\subseteq ℂ\wedge {I}\in \mathrm{Fin}\right)\to \left({I}×\left\{{ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}\right\}\right)Fn{I}$
13 eqid ${⊢}{\mathrm{dist}\left(\mathrm{Scalar}\left({ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}\right){⨉}_{𝑠}\left({I}×\left\{{ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}\right\}\right)\right)↾}_{\left({X}×{X}\right)}={\mathrm{dist}\left(\mathrm{Scalar}\left({ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}\right){⨉}_{𝑠}\left({I}×\left\{{ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}\right\}\right)\right)↾}_{\left({X}×{X}\right)}$
14 cnfldms ${⊢}{ℂ}_{\mathrm{fld}}\in \mathrm{MetSp}$
15 cnex ${⊢}ℂ\in \mathrm{V}$
16 15 ssex ${⊢}{A}\subseteq ℂ\to {A}\in \mathrm{V}$
17 16 ad2antrr ${⊢}\left(\left({A}\subseteq ℂ\wedge {I}\in \mathrm{Fin}\right)\wedge {x}\in {I}\right)\to {A}\in \mathrm{V}$
18 ressms ${⊢}\left({ℂ}_{\mathrm{fld}}\in \mathrm{MetSp}\wedge {A}\in \mathrm{V}\right)\to {ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}\in \mathrm{MetSp}$
19 14 17 18 sylancr ${⊢}\left(\left({A}\subseteq ℂ\wedge {I}\in \mathrm{Fin}\right)\wedge {x}\in {I}\right)\to {ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}\in \mathrm{MetSp}$
20 eqid ${⊢}{\mathrm{Base}}_{\left({ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}\right)}={\mathrm{Base}}_{\left({ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}\right)}$
21 eqid ${⊢}{\mathrm{dist}\left({ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}\right)↾}_{\left({\mathrm{Base}}_{\left({ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}\right)}×{\mathrm{Base}}_{\left({ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}\right)}\right)}={\mathrm{dist}\left({ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}\right)↾}_{\left({\mathrm{Base}}_{\left({ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}\right)}×{\mathrm{Base}}_{\left({ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}\right)}\right)}$
22 20 21 msmet ${⊢}{ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}\in \mathrm{MetSp}\to {\mathrm{dist}\left({ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}\right)↾}_{\left({\mathrm{Base}}_{\left({ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}\right)}×{\mathrm{Base}}_{\left({ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}\right)}\right)}\in \mathrm{Met}\left({\mathrm{Base}}_{\left({ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}\right)}\right)$
23 19 22 syl ${⊢}\left(\left({A}\subseteq ℂ\wedge {I}\in \mathrm{Fin}\right)\wedge {x}\in {I}\right)\to {\mathrm{dist}\left({ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}\right)↾}_{\left({\mathrm{Base}}_{\left({ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}\right)}×{\mathrm{Base}}_{\left({ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}\right)}\right)}\in \mathrm{Met}\left({\mathrm{Base}}_{\left({ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}\right)}\right)$
24 10 fvconst2 ${⊢}{x}\in {I}\to \left({I}×\left\{{ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}\right\}\right)\left({x}\right)={ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}$
25 24 adantl ${⊢}\left(\left({A}\subseteq ℂ\wedge {I}\in \mathrm{Fin}\right)\wedge {x}\in {I}\right)\to \left({I}×\left\{{ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}\right\}\right)\left({x}\right)={ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}$
26 25 fveq2d ${⊢}\left(\left({A}\subseteq ℂ\wedge {I}\in \mathrm{Fin}\right)\wedge {x}\in {I}\right)\to \mathrm{dist}\left(\left({I}×\left\{{ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}\right\}\right)\left({x}\right)\right)=\mathrm{dist}\left({ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}\right)$
27 25 fveq2d ${⊢}\left(\left({A}\subseteq ℂ\wedge {I}\in \mathrm{Fin}\right)\wedge {x}\in {I}\right)\to {\mathrm{Base}}_{\left({I}×\left\{{ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}\right\}\right)\left({x}\right)}={\mathrm{Base}}_{\left({ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}\right)}$
28 27 sqxpeqd ${⊢}\left(\left({A}\subseteq ℂ\wedge {I}\in \mathrm{Fin}\right)\wedge {x}\in {I}\right)\to {\mathrm{Base}}_{\left({I}×\left\{{ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}\right\}\right)\left({x}\right)}×{\mathrm{Base}}_{\left({I}×\left\{{ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}\right\}\right)\left({x}\right)}={\mathrm{Base}}_{\left({ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}\right)}×{\mathrm{Base}}_{\left({ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}\right)}$
29 26 28 reseq12d ${⊢}\left(\left({A}\subseteq ℂ\wedge {I}\in \mathrm{Fin}\right)\wedge {x}\in {I}\right)\to {\mathrm{dist}\left(\left({I}×\left\{{ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}\right\}\right)\left({x}\right)\right)↾}_{\left({\mathrm{Base}}_{\left({I}×\left\{{ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}\right\}\right)\left({x}\right)}×{\mathrm{Base}}_{\left({I}×\left\{{ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}\right\}\right)\left({x}\right)}\right)}={\mathrm{dist}\left({ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}\right)↾}_{\left({\mathrm{Base}}_{\left({ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}\right)}×{\mathrm{Base}}_{\left({ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}\right)}\right)}$
30 27 fveq2d ${⊢}\left(\left({A}\subseteq ℂ\wedge {I}\in \mathrm{Fin}\right)\wedge {x}\in {I}\right)\to \mathrm{Met}\left({\mathrm{Base}}_{\left({I}×\left\{{ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}\right\}\right)\left({x}\right)}\right)=\mathrm{Met}\left({\mathrm{Base}}_{\left({ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}\right)}\right)$
31 23 29 30 3eltr4d ${⊢}\left(\left({A}\subseteq ℂ\wedge {I}\in \mathrm{Fin}\right)\wedge {x}\in {I}\right)\to {\mathrm{dist}\left(\left({I}×\left\{{ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}\right\}\right)\left({x}\right)\right)↾}_{\left({\mathrm{Base}}_{\left({I}×\left\{{ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}\right\}\right)\left({x}\right)}×{\mathrm{Base}}_{\left({I}×\left\{{ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}\right\}\right)\left({x}\right)}\right)}\in \mathrm{Met}\left({\mathrm{Base}}_{\left({I}×\left\{{ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}\right\}\right)\left({x}\right)}\right)$
32 totbndbnd ${⊢}{\left({\mathrm{dist}\left({ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}\right)↾}_{\left({\mathrm{Base}}_{\left({ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}\right)}×{\mathrm{Base}}_{\left({ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}\right)}\right)}\right)↾}_{\left({y}×{y}\right)}\in \mathrm{TotBnd}\left({y}\right)\to {\left({\mathrm{dist}\left({ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}\right)↾}_{\left({\mathrm{Base}}_{\left({ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}\right)}×{\mathrm{Base}}_{\left({ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}\right)}\right)}\right)↾}_{\left({y}×{y}\right)}\in \mathrm{Bnd}\left({y}\right)$
33 eqid ${⊢}{ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}={ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}$
34 cnfldbas ${⊢}ℂ={\mathrm{Base}}_{{ℂ}_{\mathrm{fld}}}$
35 33 34 ressbas2 ${⊢}{A}\subseteq ℂ\to {A}={\mathrm{Base}}_{\left({ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}\right)}$
36 35 ad2antrr ${⊢}\left(\left({A}\subseteq ℂ\wedge {I}\in \mathrm{Fin}\right)\wedge {x}\in {I}\right)\to {A}={\mathrm{Base}}_{\left({ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}\right)}$
37 36 fveq2d ${⊢}\left(\left({A}\subseteq ℂ\wedge {I}\in \mathrm{Fin}\right)\wedge {x}\in {I}\right)\to \mathrm{Met}\left({A}\right)=\mathrm{Met}\left({\mathrm{Base}}_{\left({ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}\right)}\right)$
38 23 37 eleqtrrd ${⊢}\left(\left({A}\subseteq ℂ\wedge {I}\in \mathrm{Fin}\right)\wedge {x}\in {I}\right)\to {\mathrm{dist}\left({ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}\right)↾}_{\left({\mathrm{Base}}_{\left({ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}\right)}×{\mathrm{Base}}_{\left({ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}\right)}\right)}\in \mathrm{Met}\left({A}\right)$
39 eqid ${⊢}{\left({\mathrm{dist}\left({ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}\right)↾}_{\left({\mathrm{Base}}_{\left({ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}\right)}×{\mathrm{Base}}_{\left({ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}\right)}\right)}\right)↾}_{\left({y}×{y}\right)}={\left({\mathrm{dist}\left({ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}\right)↾}_{\left({\mathrm{Base}}_{\left({ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}\right)}×{\mathrm{Base}}_{\left({ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}\right)}\right)}\right)↾}_{\left({y}×{y}\right)}$
40 39 bnd2lem ${⊢}\left({\mathrm{dist}\left({ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}\right)↾}_{\left({\mathrm{Base}}_{\left({ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}\right)}×{\mathrm{Base}}_{\left({ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}\right)}\right)}\in \mathrm{Met}\left({A}\right)\wedge {\left({\mathrm{dist}\left({ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}\right)↾}_{\left({\mathrm{Base}}_{\left({ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}\right)}×{\mathrm{Base}}_{\left({ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}\right)}\right)}\right)↾}_{\left({y}×{y}\right)}\in \mathrm{Bnd}\left({y}\right)\right)\to {y}\subseteq {A}$
41 40 ex ${⊢}{\mathrm{dist}\left({ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}\right)↾}_{\left({\mathrm{Base}}_{\left({ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}\right)}×{\mathrm{Base}}_{\left({ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}\right)}\right)}\in \mathrm{Met}\left({A}\right)\to \left({\left({\mathrm{dist}\left({ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}\right)↾}_{\left({\mathrm{Base}}_{\left({ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}\right)}×{\mathrm{Base}}_{\left({ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}\right)}\right)}\right)↾}_{\left({y}×{y}\right)}\in \mathrm{Bnd}\left({y}\right)\to {y}\subseteq {A}\right)$
42 38 41 syl ${⊢}\left(\left({A}\subseteq ℂ\wedge {I}\in \mathrm{Fin}\right)\wedge {x}\in {I}\right)\to \left({\left({\mathrm{dist}\left({ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}\right)↾}_{\left({\mathrm{Base}}_{\left({ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}\right)}×{\mathrm{Base}}_{\left({ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}\right)}\right)}\right)↾}_{\left({y}×{y}\right)}\in \mathrm{Bnd}\left({y}\right)\to {y}\subseteq {A}\right)$
43 32 42 syl5 ${⊢}\left(\left({A}\subseteq ℂ\wedge {I}\in \mathrm{Fin}\right)\wedge {x}\in {I}\right)\to \left({\left({\mathrm{dist}\left({ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}\right)↾}_{\left({\mathrm{Base}}_{\left({ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}\right)}×{\mathrm{Base}}_{\left({ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}\right)}\right)}\right)↾}_{\left({y}×{y}\right)}\in \mathrm{TotBnd}\left({y}\right)\to {y}\subseteq {A}\right)$
44 eqid ${⊢}{\left(\mathrm{abs}\circ -\right)↾}_{\left({y}×{y}\right)}={\left(\mathrm{abs}\circ -\right)↾}_{\left({y}×{y}\right)}$
45 44 cntotbnd ${⊢}{\left(\mathrm{abs}\circ -\right)↾}_{\left({y}×{y}\right)}\in \mathrm{TotBnd}\left({y}\right)↔{\left(\mathrm{abs}\circ -\right)↾}_{\left({y}×{y}\right)}\in \mathrm{Bnd}\left({y}\right)$
46 45 a1i ${⊢}\left(\left(\left({A}\subseteq ℂ\wedge {I}\in \mathrm{Fin}\right)\wedge {x}\in {I}\right)\wedge {y}\subseteq {A}\right)\to \left({\left(\mathrm{abs}\circ -\right)↾}_{\left({y}×{y}\right)}\in \mathrm{TotBnd}\left({y}\right)↔{\left(\mathrm{abs}\circ -\right)↾}_{\left({y}×{y}\right)}\in \mathrm{Bnd}\left({y}\right)\right)$
47 36 sseq2d ${⊢}\left(\left({A}\subseteq ℂ\wedge {I}\in \mathrm{Fin}\right)\wedge {x}\in {I}\right)\to \left({y}\subseteq {A}↔{y}\subseteq {\mathrm{Base}}_{\left({ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}\right)}\right)$
48 47 biimpa ${⊢}\left(\left(\left({A}\subseteq ℂ\wedge {I}\in \mathrm{Fin}\right)\wedge {x}\in {I}\right)\wedge {y}\subseteq {A}\right)\to {y}\subseteq {\mathrm{Base}}_{\left({ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}\right)}$
49 xpss12 ${⊢}\left({y}\subseteq {\mathrm{Base}}_{\left({ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}\right)}\wedge {y}\subseteq {\mathrm{Base}}_{\left({ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}\right)}\right)\to {y}×{y}\subseteq {\mathrm{Base}}_{\left({ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}\right)}×{\mathrm{Base}}_{\left({ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}\right)}$
50 48 48 49 syl2anc ${⊢}\left(\left(\left({A}\subseteq ℂ\wedge {I}\in \mathrm{Fin}\right)\wedge {x}\in {I}\right)\wedge {y}\subseteq {A}\right)\to {y}×{y}\subseteq {\mathrm{Base}}_{\left({ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}\right)}×{\mathrm{Base}}_{\left({ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}\right)}$
51 50 resabs1d ${⊢}\left(\left(\left({A}\subseteq ℂ\wedge {I}\in \mathrm{Fin}\right)\wedge {x}\in {I}\right)\wedge {y}\subseteq {A}\right)\to {\left({\mathrm{dist}\left({ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}\right)↾}_{\left({\mathrm{Base}}_{\left({ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}\right)}×{\mathrm{Base}}_{\left({ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}\right)}\right)}\right)↾}_{\left({y}×{y}\right)}={\mathrm{dist}\left({ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}\right)↾}_{\left({y}×{y}\right)}$
52 17 adantr ${⊢}\left(\left(\left({A}\subseteq ℂ\wedge {I}\in \mathrm{Fin}\right)\wedge {x}\in {I}\right)\wedge {y}\subseteq {A}\right)\to {A}\in \mathrm{V}$
53 cnfldds ${⊢}\mathrm{abs}\circ -=\mathrm{dist}\left({ℂ}_{\mathrm{fld}}\right)$
54 33 53 ressds ${⊢}{A}\in \mathrm{V}\to \mathrm{abs}\circ -=\mathrm{dist}\left({ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}\right)$
55 52 54 syl ${⊢}\left(\left(\left({A}\subseteq ℂ\wedge {I}\in \mathrm{Fin}\right)\wedge {x}\in {I}\right)\wedge {y}\subseteq {A}\right)\to \mathrm{abs}\circ -=\mathrm{dist}\left({ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}\right)$
56 55 reseq1d ${⊢}\left(\left(\left({A}\subseteq ℂ\wedge {I}\in \mathrm{Fin}\right)\wedge {x}\in {I}\right)\wedge {y}\subseteq {A}\right)\to {\left(\mathrm{abs}\circ -\right)↾}_{\left({y}×{y}\right)}={\mathrm{dist}\left({ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}\right)↾}_{\left({y}×{y}\right)}$
57 51 56 eqtr4d ${⊢}\left(\left(\left({A}\subseteq ℂ\wedge {I}\in \mathrm{Fin}\right)\wedge {x}\in {I}\right)\wedge {y}\subseteq {A}\right)\to {\left({\mathrm{dist}\left({ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}\right)↾}_{\left({\mathrm{Base}}_{\left({ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}\right)}×{\mathrm{Base}}_{\left({ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}\right)}\right)}\right)↾}_{\left({y}×{y}\right)}={\left(\mathrm{abs}\circ -\right)↾}_{\left({y}×{y}\right)}$
58 57 eleq1d ${⊢}\left(\left(\left({A}\subseteq ℂ\wedge {I}\in \mathrm{Fin}\right)\wedge {x}\in {I}\right)\wedge {y}\subseteq {A}\right)\to \left({\left({\mathrm{dist}\left({ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}\right)↾}_{\left({\mathrm{Base}}_{\left({ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}\right)}×{\mathrm{Base}}_{\left({ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}\right)}\right)}\right)↾}_{\left({y}×{y}\right)}\in \mathrm{TotBnd}\left({y}\right)↔{\left(\mathrm{abs}\circ -\right)↾}_{\left({y}×{y}\right)}\in \mathrm{TotBnd}\left({y}\right)\right)$
59 57 eleq1d ${⊢}\left(\left(\left({A}\subseteq ℂ\wedge {I}\in \mathrm{Fin}\right)\wedge {x}\in {I}\right)\wedge {y}\subseteq {A}\right)\to \left({\left({\mathrm{dist}\left({ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}\right)↾}_{\left({\mathrm{Base}}_{\left({ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}\right)}×{\mathrm{Base}}_{\left({ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}\right)}\right)}\right)↾}_{\left({y}×{y}\right)}\in \mathrm{Bnd}\left({y}\right)↔{\left(\mathrm{abs}\circ -\right)↾}_{\left({y}×{y}\right)}\in \mathrm{Bnd}\left({y}\right)\right)$
60 46 58 59 3bitr4d ${⊢}\left(\left(\left({A}\subseteq ℂ\wedge {I}\in \mathrm{Fin}\right)\wedge {x}\in {I}\right)\wedge {y}\subseteq {A}\right)\to \left({\left({\mathrm{dist}\left({ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}\right)↾}_{\left({\mathrm{Base}}_{\left({ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}\right)}×{\mathrm{Base}}_{\left({ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}\right)}\right)}\right)↾}_{\left({y}×{y}\right)}\in \mathrm{TotBnd}\left({y}\right)↔{\left({\mathrm{dist}\left({ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}\right)↾}_{\left({\mathrm{Base}}_{\left({ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}\right)}×{\mathrm{Base}}_{\left({ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}\right)}\right)}\right)↾}_{\left({y}×{y}\right)}\in \mathrm{Bnd}\left({y}\right)\right)$
61 60 ex ${⊢}\left(\left({A}\subseteq ℂ\wedge {I}\in \mathrm{Fin}\right)\wedge {x}\in {I}\right)\to \left({y}\subseteq {A}\to \left({\left({\mathrm{dist}\left({ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}\right)↾}_{\left({\mathrm{Base}}_{\left({ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}\right)}×{\mathrm{Base}}_{\left({ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}\right)}\right)}\right)↾}_{\left({y}×{y}\right)}\in \mathrm{TotBnd}\left({y}\right)↔{\left({\mathrm{dist}\left({ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}\right)↾}_{\left({\mathrm{Base}}_{\left({ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}\right)}×{\mathrm{Base}}_{\left({ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}\right)}\right)}\right)↾}_{\left({y}×{y}\right)}\in \mathrm{Bnd}\left({y}\right)\right)\right)$
62 43 42 61 pm5.21ndd ${⊢}\left(\left({A}\subseteq ℂ\wedge {I}\in \mathrm{Fin}\right)\wedge {x}\in {I}\right)\to \left({\left({\mathrm{dist}\left({ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}\right)↾}_{\left({\mathrm{Base}}_{\left({ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}\right)}×{\mathrm{Base}}_{\left({ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}\right)}\right)}\right)↾}_{\left({y}×{y}\right)}\in \mathrm{TotBnd}\left({y}\right)↔{\left({\mathrm{dist}\left({ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}\right)↾}_{\left({\mathrm{Base}}_{\left({ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}\right)}×{\mathrm{Base}}_{\left({ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}\right)}\right)}\right)↾}_{\left({y}×{y}\right)}\in \mathrm{Bnd}\left({y}\right)\right)$
63 29 reseq1d ${⊢}\left(\left({A}\subseteq ℂ\wedge {I}\in \mathrm{Fin}\right)\wedge {x}\in {I}\right)\to {\left({\mathrm{dist}\left(\left({I}×\left\{{ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}\right\}\right)\left({x}\right)\right)↾}_{\left({\mathrm{Base}}_{\left({I}×\left\{{ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}\right\}\right)\left({x}\right)}×{\mathrm{Base}}_{\left({I}×\left\{{ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}\right\}\right)\left({x}\right)}\right)}\right)↾}_{\left({y}×{y}\right)}={\left({\mathrm{dist}\left({ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}\right)↾}_{\left({\mathrm{Base}}_{\left({ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}\right)}×{\mathrm{Base}}_{\left({ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}\right)}\right)}\right)↾}_{\left({y}×{y}\right)}$
64 63 eleq1d ${⊢}\left(\left({A}\subseteq ℂ\wedge {I}\in \mathrm{Fin}\right)\wedge {x}\in {I}\right)\to \left({\left({\mathrm{dist}\left(\left({I}×\left\{{ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}\right\}\right)\left({x}\right)\right)↾}_{\left({\mathrm{Base}}_{\left({I}×\left\{{ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}\right\}\right)\left({x}\right)}×{\mathrm{Base}}_{\left({I}×\left\{{ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}\right\}\right)\left({x}\right)}\right)}\right)↾}_{\left({y}×{y}\right)}\in \mathrm{TotBnd}\left({y}\right)↔{\left({\mathrm{dist}\left({ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}\right)↾}_{\left({\mathrm{Base}}_{\left({ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}\right)}×{\mathrm{Base}}_{\left({ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}\right)}\right)}\right)↾}_{\left({y}×{y}\right)}\in \mathrm{TotBnd}\left({y}\right)\right)$
65 63 eleq1d ${⊢}\left(\left({A}\subseteq ℂ\wedge {I}\in \mathrm{Fin}\right)\wedge {x}\in {I}\right)\to \left({\left({\mathrm{dist}\left(\left({I}×\left\{{ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}\right\}\right)\left({x}\right)\right)↾}_{\left({\mathrm{Base}}_{\left({I}×\left\{{ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}\right\}\right)\left({x}\right)}×{\mathrm{Base}}_{\left({I}×\left\{{ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}\right\}\right)\left({x}\right)}\right)}\right)↾}_{\left({y}×{y}\right)}\in \mathrm{Bnd}\left({y}\right)↔{\left({\mathrm{dist}\left({ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}\right)↾}_{\left({\mathrm{Base}}_{\left({ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}\right)}×{\mathrm{Base}}_{\left({ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}\right)}\right)}\right)↾}_{\left({y}×{y}\right)}\in \mathrm{Bnd}\left({y}\right)\right)$
66 62 64 65 3bitr4d ${⊢}\left(\left({A}\subseteq ℂ\wedge {I}\in \mathrm{Fin}\right)\wedge {x}\in {I}\right)\to \left({\left({\mathrm{dist}\left(\left({I}×\left\{{ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}\right\}\right)\left({x}\right)\right)↾}_{\left({\mathrm{Base}}_{\left({I}×\left\{{ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}\right\}\right)\left({x}\right)}×{\mathrm{Base}}_{\left({I}×\left\{{ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}\right\}\right)\left({x}\right)}\right)}\right)↾}_{\left({y}×{y}\right)}\in \mathrm{TotBnd}\left({y}\right)↔{\left({\mathrm{dist}\left(\left({I}×\left\{{ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}\right\}\right)\left({x}\right)\right)↾}_{\left({\mathrm{Base}}_{\left({I}×\left\{{ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}\right\}\right)\left({x}\right)}×{\mathrm{Base}}_{\left({I}×\left\{{ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}\right\}\right)\left({x}\right)}\right)}\right)↾}_{\left({y}×{y}\right)}\in \mathrm{Bnd}\left({y}\right)\right)$
67 3 4 5 6 7 8 9 12 13 31 66 prdsbnd2 ${⊢}\left({A}\subseteq ℂ\wedge {I}\in \mathrm{Fin}\right)\to \left({\mathrm{dist}\left(\mathrm{Scalar}\left({ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}\right){⨉}_{𝑠}\left({I}×\left\{{ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}\right\}\right)\right)↾}_{\left({X}×{X}\right)}\in \mathrm{TotBnd}\left({X}\right)↔{\mathrm{dist}\left(\mathrm{Scalar}\left({ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}\right){⨉}_{𝑠}\left({I}×\left\{{ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}\right\}\right)\right)↾}_{\left({X}×{X}\right)}\in \mathrm{Bnd}\left({X}\right)\right)$
68 eqid ${⊢}\mathrm{Scalar}\left({ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}\right)=\mathrm{Scalar}\left({ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}\right)$
69 1 68 pwsval ${⊢}\left({ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}\in \mathrm{V}\wedge {I}\in \mathrm{Fin}\right)\to {Y}=\mathrm{Scalar}\left({ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}\right){⨉}_{𝑠}\left({I}×\left\{{ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}\right\}\right)$
70 10 9 69 sylancr ${⊢}\left({A}\subseteq ℂ\wedge {I}\in \mathrm{Fin}\right)\to {Y}=\mathrm{Scalar}\left({ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}\right){⨉}_{𝑠}\left({I}×\left\{{ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}\right\}\right)$
71 70 fveq2d ${⊢}\left({A}\subseteq ℂ\wedge {I}\in \mathrm{Fin}\right)\to \mathrm{dist}\left({Y}\right)=\mathrm{dist}\left(\mathrm{Scalar}\left({ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}\right){⨉}_{𝑠}\left({I}×\left\{{ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}\right\}\right)\right)$
72 71 reseq1d ${⊢}\left({A}\subseteq ℂ\wedge {I}\in \mathrm{Fin}\right)\to {\mathrm{dist}\left({Y}\right)↾}_{\left({X}×{X}\right)}={\mathrm{dist}\left(\mathrm{Scalar}\left({ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}\right){⨉}_{𝑠}\left({I}×\left\{{ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}\right\}\right)\right)↾}_{\left({X}×{X}\right)}$
73 2 72 syl5eq ${⊢}\left({A}\subseteq ℂ\wedge {I}\in \mathrm{Fin}\right)\to {D}={\mathrm{dist}\left(\mathrm{Scalar}\left({ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}\right){⨉}_{𝑠}\left({I}×\left\{{ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}\right\}\right)\right)↾}_{\left({X}×{X}\right)}$
74 73 eleq1d ${⊢}\left({A}\subseteq ℂ\wedge {I}\in \mathrm{Fin}\right)\to \left({D}\in \mathrm{TotBnd}\left({X}\right)↔{\mathrm{dist}\left(\mathrm{Scalar}\left({ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}\right){⨉}_{𝑠}\left({I}×\left\{{ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}\right\}\right)\right)↾}_{\left({X}×{X}\right)}\in \mathrm{TotBnd}\left({X}\right)\right)$
75 73 eleq1d ${⊢}\left({A}\subseteq ℂ\wedge {I}\in \mathrm{Fin}\right)\to \left({D}\in \mathrm{Bnd}\left({X}\right)↔{\mathrm{dist}\left(\mathrm{Scalar}\left({ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}\right){⨉}_{𝑠}\left({I}×\left\{{ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}\right\}\right)\right)↾}_{\left({X}×{X}\right)}\in \mathrm{Bnd}\left({X}\right)\right)$
76 67 74 75 3bitr4d ${⊢}\left({A}\subseteq ℂ\wedge {I}\in \mathrm{Fin}\right)\to \left({D}\in \mathrm{TotBnd}\left({X}\right)↔{D}\in \mathrm{Bnd}\left({X}\right)\right)$