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 ⊢ Base Scalar ⁡ ℂ fld ↾ 𝑠 A ⨉ 𝑠 I × ℂ fld ↾ 𝑠 A = Base Scalar ⁡ ℂ fld ↾ 𝑠 A ⨉ 𝑠 I × ℂ fld ↾ 𝑠 A
5 eqid ⊢ Base I × ℂ fld ↾ 𝑠 A ⁡ x = Base I × ℂ fld ↾ 𝑠 A ⁡ x
6 eqid ⊢ dist ⁡ I × ℂ fld ↾ 𝑠 A ⁡ x ↾ Base I × ℂ fld ↾ 𝑠 A ⁡ x × Base I × ℂ fld ↾ 𝑠 A ⁡ x = dist ⁡ I × ℂ fld ↾ 𝑠 A ⁡ x ↾ Base I × ℂ fld ↾ 𝑠 A ⁡ x × Base I × ℂ 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 ↾ 𝑠 A Fn I
12 10 11 mp1i ⊢ A ⊆ ℂ ∧ I ∈ Fin → I × ℂ fld ↾ 𝑠 A Fn I
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 → Base I × ℂ fld ↾ 𝑠 A ⁡ x = Base ℂ fld ↾ 𝑠 A
28 27 sqxpeqd ⊢ A ⊆ ℂ ∧ I ∈ Fin ∧ x ∈ I → Base I × ℂ fld ↾ 𝑠 A ⁡ x × Base I × ℂ fld ↾ 𝑠 A ⁡ x = Base ℂ fld ↾ 𝑠 A × Base ℂ fld ↾ 𝑠 A
29 26 28 reseq12d ⊢ A ⊆ ℂ ∧ I ∈ Fin ∧ x ∈ I → dist ⁡ I × ℂ fld ↾ 𝑠 A ⁡ x ↾ Base I × ℂ fld ↾ 𝑠 A ⁡ x × Base I × ℂ fld ↾ 𝑠 A ⁡ x = dist ⁡ ℂ fld ↾ 𝑠 A ↾ Base ℂ fld ↾ 𝑠 A × Base ℂ fld ↾ 𝑠 A
30 27 fveq2d ⊢ A ⊆ ℂ ∧ I ∈ Fin ∧ x ∈ I → Met ⁡ Base I × ℂ fld ↾ 𝑠 A ⁡ x = Met ⁡ Base ℂ fld ↾ 𝑠 A
31 23 29 30 3eltr4d ⊢ A ⊆ ℂ ∧ I ∈ Fin ∧ x ∈ I → dist ⁡ I × ℂ fld ↾ 𝑠 A ⁡ x ↾ Base I × ℂ fld ↾ 𝑠 A ⁡ x × Base I × ℂ fld ↾ 𝑠 A ⁡ x ∈ Met ⁡ Base I × ℂ 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 ↾ Base I × ℂ fld ↾ 𝑠 A ⁡ x × Base I × ℂ 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 ↾ Base I × ℂ fld ↾ 𝑠 A ⁡ x × Base I × ℂ 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 ↾ Base I × ℂ fld ↾ 𝑠 A ⁡ x × Base I × ℂ 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 ↾ Base I × ℂ fld ↾ 𝑠 A ⁡ x × Base I × ℂ fld ↾ 𝑠 A ⁡ x ↾ y × y ∈ TotBnd ⁡ y ↔ dist ⁡ I × ℂ fld ↾ 𝑠 A ⁡ x ↾ Base I × ℂ fld ↾ 𝑠 A ⁡ x × Base I × ℂ 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 syl5eq ⊢ 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