Metamath Proof Explorer


Theorem prdsbnd2

Description: If balls are totally bounded in each factor, then balls are bounded in a metric product. (Contributed by Mario Carneiro, 16-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
prdsbnd2.c C = D A × A
prdsbnd2.e φ x I E Met V
prdsbnd2.m φ x I E y × y TotBnd y E y × y Bnd y
Assertion prdsbnd2 φ C TotBnd A C Bnd A

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 prdsbnd2.c C = D A × A
10 prdsbnd2.e φ x I E Met V
11 prdsbnd2.m φ x I E y × y TotBnd y E y × y Bnd y
12 totbndbnd C TotBnd A C Bnd A
13 bndmet C Bnd A C Met A
14 0totbnd A = C TotBnd A C Met A
15 13 14 syl5ibr A = C Bnd A C TotBnd A
16 15 a1i φ A = C Bnd A C TotBnd A
17 n0 A a a A
18 simprr φ a A C Bnd A C Bnd A
19 eqid S 𝑠 x I R x = S 𝑠 x I R x
20 eqid Base S 𝑠 x I R x = Base S 𝑠 x I R x
21 eqid dist S 𝑠 x I R x = dist S 𝑠 x I R x
22 fvexd φ x I R x V
23 19 20 3 4 21 6 7 22 10 prdsmet φ dist S 𝑠 x I R x Met Base S 𝑠 x I R x
24 dffn5 R Fn I R = x I R x
25 8 24 sylib φ R = x I R x
26 25 oveq2d φ S 𝑠 R = S 𝑠 x I R x
27 1 26 syl5eq φ Y = S 𝑠 x I R x
28 27 fveq2d φ dist Y = dist S 𝑠 x I R x
29 5 28 syl5eq φ D = dist S 𝑠 x I R x
30 27 fveq2d φ Base Y = Base S 𝑠 x I R x
31 2 30 syl5eq φ B = Base S 𝑠 x I R x
32 31 fveq2d φ Met B = Met Base S 𝑠 x I R x
33 23 29 32 3eltr4d φ D Met B
34 33 adantr φ a A C Bnd A D Met B
35 simpr a A C Bnd A C Bnd A
36 9 bnd2lem D Met B C Bnd A A B
37 33 35 36 syl2an φ a A C Bnd A A B
38 simprl φ a A C Bnd A a A
39 37 38 sseldd φ a A C Bnd A a B
40 9 ssbnd D Met B a B C Bnd A r A a ball D r
41 34 39 40 syl2anc φ a A C Bnd A C Bnd A r A a ball D r
42 18 41 mpbid φ a A C Bnd A r A a ball D r
43 simprr φ a A C Bnd A r A a ball D r A a ball D r
44 xpss12 A a ball D r A a ball D r A × A a ball D r × a ball D r
45 43 43 44 syl2anc φ a A C Bnd A r A a ball D r A × A a ball D r × a ball D r
46 45 resabs1d φ a A C Bnd A r A a ball D r D a ball D r × a ball D r A × A = D A × A
47 46 9 syl6eqr φ a A C Bnd A r A a ball D r D a ball D r × a ball D r A × A = C
48 simpll φ a A C Bnd A r A a ball D r φ
49 39 adantr φ a A C Bnd A r A a ball D r a B
50 simprl φ a A C Bnd A r A a ball D r r
51 38 adantr φ a A C Bnd A r A a ball D r a A
52 43 51 sseldd φ a A C Bnd A r A a ball D r a a ball D r
53 52 ne0d φ a A C Bnd A r A a ball D r a ball D r
54 33 ad2antrr φ a A C Bnd A r A a ball D r D Met B
55 metxmet D Met B D ∞Met B
56 54 55 syl φ a A C Bnd A r A a ball D r D ∞Met B
57 50 rexrd φ a A C Bnd A r A a ball D r r *
58 xbln0 D ∞Met B a B r * a ball D r 0 < r
59 56 49 57 58 syl3anc φ a A C Bnd A r A a ball D r a ball D r 0 < r
60 53 59 mpbid φ a A C Bnd A r A a ball D r 0 < r
61 50 60 elrpd φ a A C Bnd A r A a ball D r r +
62 eqid S 𝑠 y I R y 𝑠 a y ball dist R y Base R y × Base R y r = S 𝑠 y I R y 𝑠 a y ball dist R y Base R y × Base R y r
63 eqid Base S 𝑠 y I R y 𝑠 a y ball dist R y Base R y × Base R y r = Base S 𝑠 y I R y 𝑠 a y ball dist R y Base R y × Base R y r
64 eqid Base y I R y 𝑠 a y ball dist R y Base R y × Base R y r x = Base y I R y 𝑠 a y ball dist R y Base R y × Base R y r x
65 eqid dist y I R y 𝑠 a y ball dist R y Base R y × Base R y r x Base y I R y 𝑠 a y ball dist R y Base R y × Base R y r x × Base y I R y 𝑠 a y ball dist R y Base R y × Base R y r x = dist y I R y 𝑠 a y ball dist R y Base R y × Base R y r x Base y I R y 𝑠 a y ball dist R y Base R y × Base R y r x × Base y I R y 𝑠 a y ball dist R y Base R y × Base R y r x
66 eqid dist S 𝑠 y I R y 𝑠 a y ball dist R y Base R y × Base R y r = dist S 𝑠 y I R y 𝑠 a y ball dist R y Base R y × Base R y r
67 6 adantr φ a B r + S W
68 7 adantr φ a B r + I Fin
69 ovex R x 𝑠 a x ball E r V
70 fveq2 y = x R y = R x
71 2fveq3 y = x dist R y = dist R x
72 2fveq3 y = x Base R y = Base R x
73 72 3 syl6eqr y = x Base R y = V
74 73 sqxpeqd y = x Base R y × Base R y = V × V
75 71 74 reseq12d y = x dist R y Base R y × Base R y = dist R x V × V
76 75 4 syl6eqr y = x dist R y Base R y × Base R y = E
77 76 fveq2d y = x ball dist R y Base R y × Base R y = ball E
78 fveq2 y = x a y = a x
79 eqidd y = x r = r
80 77 78 79 oveq123d y = x a y ball dist R y Base R y × Base R y r = a x ball E r
81 70 80 oveq12d y = x R y 𝑠 a y ball dist R y Base R y × Base R y r = R x 𝑠 a x ball E r
82 81 cbvmptv y I R y 𝑠 a y ball dist R y Base R y × Base R y r = x I R x 𝑠 a x ball E r
83 69 82 fnmpti y I R y 𝑠 a y ball dist R y Base R y × Base R y r Fn I
84 83 a1i φ a B r + y I R y 𝑠 a y ball dist R y Base R y × Base R y r Fn I
85 10 adantlr φ a B r + x I E Met V
86 metxmet E Met V E ∞Met V
87 85 86 syl φ a B r + x I E ∞Met V
88 22 ralrimiva φ x I R x V
89 88 adantr φ a B r + x I R x V
90 simprl φ a B r + a B
91 31 adantr φ a B r + B = Base S 𝑠 x I R x
92 90 91 eleqtrd φ a B r + a Base S 𝑠 x I R x
93 19 20 67 68 89 3 92 prdsbascl φ a B r + x I a x V
94 93 r19.21bi φ a B r + x I a x V
95 simplrr φ a B r + x I r +
96 95 rpred φ a B r + x I r
97 blbnd E ∞Met V a x V r E a x ball E r × a x ball E r Bnd a x ball E r
98 87 94 96 97 syl3anc φ a B r + x I E a x ball E r × a x ball E r Bnd a x ball E r
99 ovex a x ball E r V
100 xpeq12 y = a x ball E r y = a x ball E r y × y = a x ball E r × a x ball E r
101 100 anidms y = a x ball E r y × y = a x ball E r × a x ball E r
102 101 reseq2d y = a x ball E r E y × y = E a x ball E r × a x ball E r
103 fveq2 y = a x ball E r TotBnd y = TotBnd a x ball E r
104 102 103 eleq12d y = a x ball E r E y × y TotBnd y E a x ball E r × a x ball E r TotBnd a x ball E r
105 fveq2 y = a x ball E r Bnd y = Bnd a x ball E r
106 102 105 eleq12d y = a x ball E r E y × y Bnd y E a x ball E r × a x ball E r Bnd a x ball E r
107 104 106 bibi12d y = a x ball E r E y × y TotBnd y E y × y Bnd y E a x ball E r × a x ball E r TotBnd a x ball E r E a x ball E r × a x ball E r Bnd a x ball E r
108 107 imbi2d y = a x ball E r φ x I E y × y TotBnd y E y × y Bnd y φ x I E a x ball E r × a x ball E r TotBnd a x ball E r E a x ball E r × a x ball E r Bnd a x ball E r
109 99 108 11 vtocl φ x I E a x ball E r × a x ball E r TotBnd a x ball E r E a x ball E r × a x ball E r Bnd a x ball E r
110 109 adantlr φ a B r + x I E a x ball E r × a x ball E r TotBnd a x ball E r E a x ball E r × a x ball E r Bnd a x ball E r
111 98 110 mpbird φ a B r + x I E a x ball E r × a x ball E r TotBnd a x ball E r
112 eqid y I R y 𝑠 a y ball dist R y Base R y × Base R y r = y I R y 𝑠 a y ball dist R y Base R y × Base R y r
113 81 112 69 fvmpt x I y I R y 𝑠 a y ball dist R y Base R y × Base R y r x = R x 𝑠 a x ball E r
114 113 adantl φ a B r + x I y I R y 𝑠 a y ball dist R y Base R y × Base R y r x = R x 𝑠 a x ball E r
115 114 fveq2d φ a B r + x I dist y I R y 𝑠 a y ball dist R y Base R y × Base R y r x = dist R x 𝑠 a x ball E r
116 eqid R x 𝑠 a x ball E r = R x 𝑠 a x ball E r
117 eqid dist R x = dist R x
118 116 117 ressds a x ball E r V dist R x = dist R x 𝑠 a x ball E r
119 99 118 ax-mp dist R x = dist R x 𝑠 a x ball E r
120 115 119 syl6eqr φ a B r + x I dist y I R y 𝑠 a y ball dist R y Base R y × Base R y r x = dist R x
121 114 fveq2d φ a B r + x I Base y I R y 𝑠 a y ball dist R y Base R y × Base R y r x = Base R x 𝑠 a x ball E r
122 rpxr r + r *
123 122 ad2antll φ a B r + r *
124 123 adantr φ a B r + x I r *
125 blssm E ∞Met V a x V r * a x ball E r V
126 87 94 124 125 syl3anc φ a B r + x I a x ball E r V
127 116 3 ressbas2 a x ball E r V a x ball E r = Base R x 𝑠 a x ball E r
128 126 127 syl φ a B r + x I a x ball E r = Base R x 𝑠 a x ball E r
129 121 128 eqtr4d φ a B r + x I Base y I R y 𝑠 a y ball dist R y Base R y × Base R y r x = a x ball E r
130 129 sqxpeqd φ a B r + x I Base y I R y 𝑠 a y ball dist R y Base R y × Base R y r x × Base y I R y 𝑠 a y ball dist R y Base R y × Base R y r x = a x ball E r × a x ball E r
131 120 130 reseq12d φ a B r + x I dist y I R y 𝑠 a y ball dist R y Base R y × Base R y r x Base y I R y 𝑠 a y ball dist R y Base R y × Base R y r x × Base y I R y 𝑠 a y ball dist R y Base R y × Base R y r x = dist R x a x ball E r × a x ball E r
132 4 reseq1i E a x ball E r × a x ball E r = dist R x V × V a x ball E r × a x ball E r
133 xpss12 a x ball E r V a x ball E r V a x ball E r × a x ball E r V × V
134 126 126 133 syl2anc φ a B r + x I a x ball E r × a x ball E r V × V
135 134 resabs1d φ a B r + x I dist R x V × V a x ball E r × a x ball E r = dist R x a x ball E r × a x ball E r
136 132 135 syl5eq φ a B r + x I E a x ball E r × a x ball E r = dist R x a x ball E r × a x ball E r
137 131 136 eqtr4d φ a B r + x I dist y I R y 𝑠 a y ball dist R y Base R y × Base R y r x Base y I R y 𝑠 a y ball dist R y Base R y × Base R y r x × Base y I R y 𝑠 a y ball dist R y Base R y × Base R y r x = E a x ball E r × a x ball E r
138 129 fveq2d φ a B r + x I TotBnd Base y I R y 𝑠 a y ball dist R y Base R y × Base R y r x = TotBnd a x ball E r
139 111 137 138 3eltr4d φ a B r + x I dist y I R y 𝑠 a y ball dist R y Base R y × Base R y r x Base y I R y 𝑠 a y ball dist R y Base R y × Base R y r x × Base y I R y 𝑠 a y ball dist R y Base R y × Base R y r x TotBnd Base y I R y 𝑠 a y ball dist R y Base R y × Base R y r x
140 62 63 64 65 66 67 68 84 139 prdstotbnd φ a B r + dist S 𝑠 y I R y 𝑠 a y ball dist R y Base R y × Base R y r TotBnd Base S 𝑠 y I R y 𝑠 a y ball dist R y Base R y × Base R y r
141 27 adantr φ a B r + Y = S 𝑠 x I R x
142 eqidd φ a B r + S 𝑠 x I R x 𝑠 a x ball E r = S 𝑠 x I R x 𝑠 a x ball E r
143 eqid Base S 𝑠 x I R x 𝑠 a x ball E r = Base S 𝑠 x I R x 𝑠 a x ball E r
144 82 oveq2i S 𝑠 y I R y 𝑠 a y ball dist R y Base R y × Base R y r = S 𝑠 x I R x 𝑠 a x ball E r
145 144 fveq2i dist S 𝑠 y I R y 𝑠 a y ball dist R y Base R y × Base R y r = dist S 𝑠 x I R x 𝑠 a x ball E r
146 fvexd φ a B r + x I R x V
147 99 a1i φ a B r + x I a x ball E r V
148 141 142 143 5 145 67 67 68 146 147 ressprdsds φ a B r + dist S 𝑠 y I R y 𝑠 a y ball dist R y Base R y × Base R y r = D Base S 𝑠 x I R x 𝑠 a x ball E r × Base S 𝑠 x I R x 𝑠 a x ball E r
149 128 ixpeq2dva φ a B r + x I a x ball E r = x I Base R x 𝑠 a x ball E r
150 70 cbvmptv y I R y = x I R x
151 150 oveq2i S 𝑠 y I R y = S 𝑠 x I R x
152 27 151 syl6eqr φ Y = S 𝑠 y I R y
153 152 fveq2d φ dist Y = dist S 𝑠 y I R y
154 5 153 syl5eq φ D = dist S 𝑠 y I R y
155 154 fveq2d φ ball D = ball dist S 𝑠 y I R y
156 155 oveqdr φ a B r + a ball D r = a ball dist S 𝑠 y I R y r
157 eqid Base S 𝑠 y I R y = Base S 𝑠 y I R y
158 eqid dist S 𝑠 y I R y = dist S 𝑠 y I R y
159 152 fveq2d φ Base Y = Base S 𝑠 y I R y
160 2 159 syl5eq φ B = Base S 𝑠 y I R y
161 160 adantr φ a B r + B = Base S 𝑠 y I R y
162 90 161 eleqtrd φ a B r + a Base S 𝑠 y I R y
163 rpgt0 r + 0 < r
164 163 ad2antll φ a B r + 0 < r
165 151 157 3 4 158 67 68 146 87 162 123 164 prdsbl φ a B r + a ball dist S 𝑠 y I R y r = x I a x ball E r
166 156 165 eqtrd φ a B r + a ball D r = x I a x ball E r
167 eqid S 𝑠 x I R x 𝑠 a x ball E r = S 𝑠 x I R x 𝑠 a x ball E r
168 69 a1i φ a B r + x I R x 𝑠 a x ball E r V
169 168 ralrimiva φ a B r + x I R x 𝑠 a x ball E r V
170 eqid Base R x 𝑠 a x ball E r = Base R x 𝑠 a x ball E r
171 167 143 67 68 169 170 prdsbas3 φ a B r + Base S 𝑠 x I R x 𝑠 a x ball E r = x I Base R x 𝑠 a x ball E r
172 149 166 171 3eqtr4rd φ a B r + Base S 𝑠 x I R x 𝑠 a x ball E r = a ball D r
173 172 sqxpeqd φ a B r + Base S 𝑠 x I R x 𝑠 a x ball E r × Base S 𝑠 x I R x 𝑠 a x ball E r = a ball D r × a ball D r
174 173 reseq2d φ a B r + D Base S 𝑠 x I R x 𝑠 a x ball E r × Base S 𝑠 x I R x 𝑠 a x ball E r = D a ball D r × a ball D r
175 148 174 eqtrd φ a B r + dist S 𝑠 y I R y 𝑠 a y ball dist R y Base R y × Base R y r = D a ball D r × a ball D r
176 144 fveq2i Base S 𝑠 y I R y 𝑠 a y ball dist R y Base R y × Base R y r = Base S 𝑠 x I R x 𝑠 a x ball E r
177 176 172 syl5eq φ a B r + Base S 𝑠 y I R y 𝑠 a y ball dist R y Base R y × Base R y r = a ball D r
178 177 fveq2d φ a B r + TotBnd Base S 𝑠 y I R y 𝑠 a y ball dist R y Base R y × Base R y r = TotBnd a ball D r
179 140 175 178 3eltr3d φ a B r + D a ball D r × a ball D r TotBnd a ball D r
180 48 49 61 179 syl12anc φ a A C Bnd A r A a ball D r D a ball D r × a ball D r TotBnd a ball D r
181 totbndss D a ball D r × a ball D r TotBnd a ball D r A a ball D r D a ball D r × a ball D r A × A TotBnd A
182 180 43 181 syl2anc φ a A C Bnd A r A a ball D r D a ball D r × a ball D r A × A TotBnd A
183 47 182 eqeltrrd φ a A C Bnd A r A a ball D r C TotBnd A
184 42 183 rexlimddv φ a A C Bnd A C TotBnd A
185 184 exp32 φ a A C Bnd A C TotBnd A
186 185 exlimdv φ a a A C Bnd A C TotBnd A
187 17 186 syl5bi φ A C Bnd A C TotBnd A
188 16 187 pm2.61dne φ C Bnd A C TotBnd A
189 12 188 impbid2 φ C TotBnd A C Bnd A