Metamath Proof Explorer


Theorem prdstotbnd

Description: The product metric over finite index set is totally bounded if all the factors are totally bounded. (Contributed by Mario Carneiro, 20-Sep-2015)

Ref Expression
Hypotheses prdsbnd.y Y = S 𝑠 R
prdsbnd.b B = Base Y
prdsbnd.v V = Base R x
prdsbnd.e E = dist R x V × V
prdsbnd.d D = dist Y
prdsbnd.s φ S W
prdsbnd.i φ I Fin
prdsbnd.r φ R Fn I
prdstotbnd.m φ x I E TotBnd V
Assertion prdstotbnd φ D TotBnd B

Proof

Step Hyp Ref Expression
1 prdsbnd.y Y = S 𝑠 R
2 prdsbnd.b B = Base Y
3 prdsbnd.v V = Base R x
4 prdsbnd.e E = dist R x V × V
5 prdsbnd.d D = dist Y
6 prdsbnd.s φ S W
7 prdsbnd.i φ I Fin
8 prdsbnd.r φ R Fn I
9 prdstotbnd.m φ x I E TotBnd V
10 eqid S 𝑠 x I R x = S 𝑠 x I R x
11 eqid Base S 𝑠 x I R x = Base S 𝑠 x I R x
12 eqid dist S 𝑠 x I R x = dist S 𝑠 x I R x
13 fvexd φ x I R x V
14 totbndmet E TotBnd V E Met V
15 9 14 syl φ x I E Met V
16 10 11 3 4 12 6 7 13 15 prdsmet φ dist S 𝑠 x I R x Met Base S 𝑠 x I R x
17 dffn5 R Fn I R = x I R x
18 8 17 sylib φ R = x I R x
19 18 oveq2d φ S 𝑠 R = S 𝑠 x I R x
20 1 19 syl5eq φ Y = S 𝑠 x I R x
21 20 fveq2d φ dist Y = dist S 𝑠 x I R x
22 5 21 syl5eq φ D = dist S 𝑠 x I R x
23 20 fveq2d φ Base Y = Base S 𝑠 x I R x
24 2 23 syl5eq φ B = Base S 𝑠 x I R x
25 24 fveq2d φ Met B = Met Base S 𝑠 x I R x
26 16 22 25 3eltr4d φ D Met B
27 7 adantr φ r + I Fin
28 istotbnd3 E TotBnd V E Met V r + w 𝒫 V Fin z w z ball E r = V
29 28 simprbi E TotBnd V r + w 𝒫 V Fin z w z ball E r = V
30 9 29 syl φ x I r + w 𝒫 V Fin z w z ball E r = V
31 30 r19.21bi φ x I r + w 𝒫 V Fin z w z ball E r = V
32 df-rex w 𝒫 V Fin z w z ball E r = V w w 𝒫 V Fin z w z ball E r = V
33 rexv w V w 𝒫 V Fin z w z ball E r = V w w 𝒫 V Fin z w z ball E r = V
34 32 33 bitr4i w 𝒫 V Fin z w z ball E r = V w V w 𝒫 V Fin z w z ball E r = V
35 31 34 sylib φ x I r + w V w 𝒫 V Fin z w z ball E r = V
36 35 an32s φ r + x I w V w 𝒫 V Fin z w z ball E r = V
37 36 ralrimiva φ r + x I w V w 𝒫 V Fin z w z ball E r = V
38 eleq1 w = f x w 𝒫 V Fin f x 𝒫 V Fin
39 iuneq1 w = f x z w z ball E r = z f x z ball E r
40 39 eqeq1d w = f x z w z ball E r = V z f x z ball E r = V
41 38 40 anbi12d w = f x w 𝒫 V Fin z w z ball E r = V f x 𝒫 V Fin z f x z ball E r = V
42 41 ac6sfi I Fin x I w V w 𝒫 V Fin z w z ball E r = V f f : I V x I f x 𝒫 V Fin z f x z ball E r = V
43 27 37 42 syl2anc φ r + f f : I V x I f x 𝒫 V Fin z f x z ball E r = V
44 elfpw f x 𝒫 V Fin f x V f x Fin
45 44 simplbi f x 𝒫 V Fin f x V
46 45 adantr f x 𝒫 V Fin z f x z ball E r = V f x V
47 46 ralimi x I f x 𝒫 V Fin z f x z ball E r = V x I f x V
48 47 ad2antll φ r + f : I V x I f x 𝒫 V Fin z f x z ball E r = V x I f x V
49 ss2ixp x I f x V x I f x x I V
50 48 49 syl φ r + f : I V x I f x 𝒫 V Fin z f x z ball E r = V x I f x x I V
51 fnfi R Fn I I Fin R Fin
52 8 7 51 syl2anc φ R Fin
53 fndm R Fn I dom R = I
54 8 53 syl φ dom R = I
55 1 6 52 2 54 prdsbas φ B = x I Base R x
56 3 rgenw x I V = Base R x
57 ixpeq2 x I V = Base R x x I V = x I Base R x
58 56 57 ax-mp x I V = x I Base R x
59 55 58 syl6eqr φ B = x I V
60 59 ad2antrr φ r + f : I V x I f x 𝒫 V Fin z f x z ball E r = V B = x I V
61 50 60 sseqtrrd φ r + f : I V x I f x 𝒫 V Fin z f x z ball E r = V x I f x B
62 27 adantr φ r + f : I V x I f x 𝒫 V Fin z f x z ball E r = V I Fin
63 44 simprbi f x 𝒫 V Fin f x Fin
64 63 adantr f x 𝒫 V Fin z f x z ball E r = V f x Fin
65 64 ralimi x I f x 𝒫 V Fin z f x z ball E r = V x I f x Fin
66 65 ad2antll φ r + f : I V x I f x 𝒫 V Fin z f x z ball E r = V x I f x Fin
67 ixpfi I Fin x I f x Fin x I f x Fin
68 62 66 67 syl2anc φ r + f : I V x I f x 𝒫 V Fin z f x z ball E r = V x I f x Fin
69 elfpw x I f x 𝒫 B Fin x I f x B x I f x Fin
70 61 68 69 sylanbrc φ r + f : I V x I f x 𝒫 V Fin z f x z ball E r = V x I f x 𝒫 B Fin
71 metxmet D Met B D ∞Met B
72 26 71 syl φ D ∞Met B
73 rpxr r + r *
74 blssm D ∞Met B y B r * y ball D r B
75 74 3expa D ∞Met B y B r * y ball D r B
76 75 an32s D ∞Met B r * y B y ball D r B
77 76 ralrimiva D ∞Met B r * y B y ball D r B
78 72 73 77 syl2an φ r + y B y ball D r B
79 78 adantr φ r + f : I V x I f x 𝒫 V Fin z f x z ball E r = V y B y ball D r B
80 ssralv x I f x B y B y ball D r B y x I f x y ball D r B
81 61 79 80 sylc φ r + f : I V x I f x 𝒫 V Fin z f x z ball E r = V y x I f x y ball D r B
82 iunss y x I f x y ball D r B y x I f x y ball D r B
83 81 82 sylibr φ r + f : I V x I f x 𝒫 V Fin z f x z ball E r = V y x I f x y ball D r B
84 62 adantr φ r + f : I V x I f x 𝒫 V Fin z f x z ball E r = V g B I Fin
85 60 eleq2d φ r + f : I V x I f x 𝒫 V Fin z f x z ball E r = V g B g x I V
86 vex g V
87 86 elixp g x I V g Fn I x I g x V
88 87 simprbi g x I V x I g x V
89 df-rex z f x g x z ball E r z z f x g x z ball E r
90 eliun g x z f x z ball E r z f x g x z ball E r
91 rexv z V z f x g x z ball E r z z f x g x z ball E r
92 89 90 91 3bitr4i g x z f x z ball E r z V z f x g x z ball E r
93 eleq2 z f x z ball E r = V g x z f x z ball E r g x V
94 92 93 syl5bbr z f x z ball E r = V z V z f x g x z ball E r g x V
95 94 biimprd z f x z ball E r = V g x V z V z f x g x z ball E r
96 95 adantl f x 𝒫 V Fin z f x z ball E r = V g x V z V z f x g x z ball E r
97 96 ral2imi x I f x 𝒫 V Fin z f x z ball E r = V x I g x V x I z V z f x g x z ball E r
98 97 ad2antll φ r + f : I V x I f x 𝒫 V Fin z f x z ball E r = V x I g x V x I z V z f x g x z ball E r
99 88 98 syl5 φ r + f : I V x I f x 𝒫 V Fin z f x z ball E r = V g x I V x I z V z f x g x z ball E r
100 85 99 sylbid φ r + f : I V x I f x 𝒫 V Fin z f x z ball E r = V g B x I z V z f x g x z ball E r
101 100 imp φ r + f : I V x I f x 𝒫 V Fin z f x z ball E r = V g B x I z V z f x g x z ball E r
102 eleq1 z = y x z f x y x f x
103 oveq1 z = y x z ball E r = y x ball E r
104 103 eleq2d z = y x g x z ball E r g x y x ball E r
105 102 104 anbi12d z = y x z f x g x z ball E r y x f x g x y x ball E r
106 105 ac6sfi I Fin x I z V z f x g x z ball E r y y : I V x I y x f x g x y x ball E r
107 84 101 106 syl2anc φ r + f : I V x I f x 𝒫 V Fin z f x z ball E r = V g B y y : I V x I y x f x g x y x ball E r
108 ffn y : I V y Fn I
109 simpl y x f x g x y x ball E r y x f x
110 109 ralimi x I y x f x g x y x ball E r x I y x f x
111 108 110 anim12i y : I V x I y x f x g x y x ball E r y Fn I x I y x f x
112 vex y V
113 112 elixp y x I f x y Fn I x I y x f x
114 111 113 sylibr y : I V x I y x f x g x y x ball E r y x I f x
115 114 adantl φ r + f : I V x I f x 𝒫 V Fin z f x z ball E r = V g B y : I V x I y x f x g x y x ball E r y x I f x
116 85 biimpa φ r + f : I V x I f x 𝒫 V Fin z f x z ball E r = V g B g x I V
117 ixpfn g x I V g Fn I
118 116 117 syl φ r + f : I V x I f x 𝒫 V Fin z f x z ball E r = V g B g Fn I
119 118 adantr φ r + f : I V x I f x 𝒫 V Fin z f x z ball E r = V g B y : I V x I y x f x g x y x ball E r g Fn I
120 simpr y x f x g x y x ball E r g x y x ball E r
121 120 ralimi x I y x f x g x y x ball E r x I g x y x ball E r
122 121 ad2antll φ r + f : I V x I f x 𝒫 V Fin z f x z ball E r = V g B y : I V x I y x f x g x y x ball E r x I g x y x ball E r
123 86 elixp g x I y x ball E r g Fn I x I g x y x ball E r
124 119 122 123 sylanbrc φ r + f : I V x I f x 𝒫 V Fin z f x z ball E r = V g B y : I V x I y x f x g x y x ball E r g x I y x ball E r
125 simp-4l φ r + f : I V x I f x 𝒫 V Fin z f x z ball E r = V g B y : I V x I y x f x g x y x ball E r φ
126 50 ad2antrr φ r + f : I V x I f x 𝒫 V Fin z f x z ball E r = V g B y : I V x I y x f x g x y x ball E r x I f x x I V
127 126 115 sseldd φ r + f : I V x I f x 𝒫 V Fin z f x z ball E r = V g B y : I V x I y x f x g x y x ball E r y x I V
128 125 59 syl φ r + f : I V x I f x 𝒫 V Fin z f x z ball E r = V g B y : I V x I y x f x g x y x ball E r B = x I V
129 127 128 eleqtrrd φ r + f : I V x I f x 𝒫 V Fin z f x z ball E r = V g B y : I V x I y x f x g x y x ball E r y B
130 simp-4r φ r + f : I V x I f x 𝒫 V Fin z f x z ball E r = V g B y : I V x I y x f x g x y x ball E r r +
131 fveq2 y = x R y = R x
132 131 cbvmptv y I R y = x I R x
133 132 oveq2i S 𝑠 y I R y = S 𝑠 x I R x
134 20 133 syl6eqr φ Y = S 𝑠 y I R y
135 134 fveq2d φ dist Y = dist S 𝑠 y I R y
136 5 135 syl5eq φ D = dist S 𝑠 y I R y
137 136 fveq2d φ ball D = ball dist S 𝑠 y I R y
138 137 oveqdr φ y B r + y ball D r = y ball dist S 𝑠 y I R y r
139 eqid Base S 𝑠 y I R y = Base S 𝑠 y I R y
140 eqid dist S 𝑠 y I R y = dist S 𝑠 y I R y
141 6 adantr φ y B r + S W
142 7 adantr φ y B r + I Fin
143 fvexd φ y B r + x I R x V
144 metxmet E Met V E ∞Met V
145 15 144 syl φ x I E ∞Met V
146 145 adantlr φ y B r + x I E ∞Met V
147 simprl φ y B r + y B
148 134 fveq2d φ Base Y = Base S 𝑠 y I R y
149 2 148 syl5eq φ B = Base S 𝑠 y I R y
150 149 adantr φ y B r + B = Base S 𝑠 y I R y
151 147 150 eleqtrd φ y B r + y Base S 𝑠 y I R y
152 73 ad2antll φ y B r + r *
153 rpgt0 r + 0 < r
154 153 ad2antll φ y B r + 0 < r
155 133 139 3 4 140 141 142 143 146 151 152 154 prdsbl φ y B r + y ball dist S 𝑠 y I R y r = x I y x ball E r
156 138 155 eqtrd φ y B r + y ball D r = x I y x ball E r
157 125 129 130 156 syl12anc φ r + f : I V x I f x 𝒫 V Fin z f x z ball E r = V g B y : I V x I y x f x g x y x ball E r y ball D r = x I y x ball E r
158 124 157 eleqtrrd φ r + f : I V x I f x 𝒫 V Fin z f x z ball E r = V g B y : I V x I y x f x g x y x ball E r g y ball D r
159 115 158 jca φ r + f : I V x I f x 𝒫 V Fin z f x z ball E r = V g B y : I V x I y x f x g x y x ball E r y x I f x g y ball D r
160 159 ex φ r + f : I V x I f x 𝒫 V Fin z f x z ball E r = V g B y : I V x I y x f x g x y x ball E r y x I f x g y ball D r
161 160 eximdv φ r + f : I V x I f x 𝒫 V Fin z f x z ball E r = V g B y y : I V x I y x f x g x y x ball E r y y x I f x g y ball D r
162 df-rex y x I f x g y ball D r y y x I f x g y ball D r
163 161 162 syl6ibr φ r + f : I V x I f x 𝒫 V Fin z f x z ball E r = V g B y y : I V x I y x f x g x y x ball E r y x I f x g y ball D r
164 107 163 mpd φ r + f : I V x I f x 𝒫 V Fin z f x z ball E r = V g B y x I f x g y ball D r
165 164 ex φ r + f : I V x I f x 𝒫 V Fin z f x z ball E r = V g B y x I f x g y ball D r
166 eliun g y x I f x y ball D r y x I f x g y ball D r
167 165 166 syl6ibr φ r + f : I V x I f x 𝒫 V Fin z f x z ball E r = V g B g y x I f x y ball D r
168 167 ssrdv φ r + f : I V x I f x 𝒫 V Fin z f x z ball E r = V B y x I f x y ball D r
169 83 168 eqssd φ r + f : I V x I f x 𝒫 V Fin z f x z ball E r = V y x I f x y ball D r = B
170 iuneq1 v = x I f x y v y ball D r = y x I f x y ball D r
171 170 eqeq1d v = x I f x y v y ball D r = B y x I f x y ball D r = B
172 171 rspcev x I f x 𝒫 B Fin y x I f x y ball D r = B v 𝒫 B Fin y v y ball D r = B
173 70 169 172 syl2anc φ r + f : I V x I f x 𝒫 V Fin z f x z ball E r = V v 𝒫 B Fin y v y ball D r = B
174 43 173 exlimddv φ r + v 𝒫 B Fin y v y ball D r = B
175 174 ralrimiva φ r + v 𝒫 B Fin y v y ball D r = B
176 istotbnd3 D TotBnd B D Met B r + v 𝒫 B Fin y v y ball D r = B
177 26 175 176 sylanbrc φ D TotBnd B