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=ℂfld↾𝑠A↑𝑠I
cnpwstotbnd.d ⊢D=dist⁡Y↾X×X
Assertion cnpwstotbnd ⊢A⊆ℂ∧I∈Fin→D∈TotBnd⁡X↔D∈Bnd⁡X

Proof

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