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 ⊢ 𝑌 = ( ( ℂfld ↾s 𝐴 ) ↑s 𝐼 )
cnpwstotbnd.d ⊢ 𝐷 = ( ( dist ‘ 𝑌 ) ↾ ( 𝑋 × 𝑋 ) )
Assertion cnpwstotbnd ( ( 𝐴 ⊆ ℂ ∧ 𝐼 ∈ Fin ) → ( 𝐷 ∈ ( TotBnd ‘ 𝑋 ) ↔ 𝐷 ∈ ( Bnd ‘ 𝑋 ) ) )

Proof

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