Metamath Proof Explorer

Theorem equivbnd2

Description: If balls are totally bounded in the metric M , then balls are totally bounded in the equivalent metric N . (Contributed by Mario Carneiro, 15-Sep-2015)

Ref Expression
Hypotheses equivbnd2.1 
|- ( ph -> M e. ( Met ` X ) )
equivbnd2.2 
|- ( ph -> N e. ( Met ` X ) )
equivbnd2.3 
|- ( ph -> R e. RR+ )
equivbnd2.4 
|- ( ph -> S e. RR+ )
equivbnd2.5 
|- ( ( ph /\ ( x e. X /\ y e. X ) ) -> ( x N y ) <_ ( R x. ( x M y ) ) )
equivbnd2.6 
|- ( ( ph /\ ( x e. X /\ y e. X ) ) -> ( x M y ) <_ ( S x. ( x N y ) ) )
equivbnd2.7 
|- C = ( M |` ( Y X. Y ) )
equivbnd2.8 
|- D = ( N |` ( Y X. Y ) )
equivbnd2.9 
|- ( ph -> ( C e. ( TotBnd ` Y ) <-> C e. ( Bnd ` Y ) ) )
Assertion equivbnd2 
|- ( ph -> ( D e. ( TotBnd ` Y ) <-> D e. ( Bnd ` Y ) ) )

Proof

Step Hyp Ref Expression
1 equivbnd2.1 
 |-  ( ph -> M e. ( Met ` X ) )
2 equivbnd2.2 
 |-  ( ph -> N e. ( Met ` X ) )
3 equivbnd2.3 
 |-  ( ph -> R e. RR+ )
4 equivbnd2.4 
 |-  ( ph -> S e. RR+ )
5 equivbnd2.5 
 |-  ( ( ph /\ ( x e. X /\ y e. X ) ) -> ( x N y ) <_ ( R x. ( x M y ) ) )
6 equivbnd2.6 
 |-  ( ( ph /\ ( x e. X /\ y e. X ) ) -> ( x M y ) <_ ( S x. ( x N y ) ) )
7 equivbnd2.7 
 |-  C = ( M |` ( Y X. Y ) )
8 equivbnd2.8 
 |-  D = ( N |` ( Y X. Y ) )
9 equivbnd2.9 
 |-  ( ph -> ( C e. ( TotBnd ` Y ) <-> C e. ( Bnd ` Y ) ) )
10 totbndbnd 
 |-  ( D e. ( TotBnd ` Y ) -> D e. ( Bnd ` Y ) )
11 simpr 
 |-  ( ( ph /\ D e. ( Bnd ` Y ) ) -> D e. ( Bnd ` Y ) )
12 1 adantr 
 |-  ( ( ph /\ D e. ( Bnd ` Y ) ) -> M e. ( Met ` X ) )
13 8 bnd2lem 
 |-  ( ( N e. ( Met ` X ) /\ D e. ( Bnd ` Y ) ) -> Y C_ X )
14 2 13 sylan 
 |-  ( ( ph /\ D e. ( Bnd ` Y ) ) -> Y C_ X )
15 metres2 
 |-  ( ( M e. ( Met ` X ) /\ Y C_ X ) -> ( M |` ( Y X. Y ) ) e. ( Met ` Y ) )
16 12 14 15 syl2anc 
 |-  ( ( ph /\ D e. ( Bnd ` Y ) ) -> ( M |` ( Y X. Y ) ) e. ( Met ` Y ) )
17 7 16 eqeltrid 
 |-  ( ( ph /\ D e. ( Bnd ` Y ) ) -> C e. ( Met ` Y ) )
18 4 adantr 
 |-  ( ( ph /\ D e. ( Bnd ` Y ) ) -> S e. RR+ )
19 14 sselda 
 |-  ( ( ( ph /\ D e. ( Bnd ` Y ) ) /\ x e. Y ) -> x e. X )
20 14 sselda 
 |-  ( ( ( ph /\ D e. ( Bnd ` Y ) ) /\ y e. Y ) -> y e. X )
21 19 20 anim12dan 
 |-  ( ( ( ph /\ D e. ( Bnd ` Y ) ) /\ ( x e. Y /\ y e. Y ) ) -> ( x e. X /\ y e. X ) )
22 6 adantlr 
 |-  ( ( ( ph /\ D e. ( Bnd ` Y ) ) /\ ( x e. X /\ y e. X ) ) -> ( x M y ) <_ ( S x. ( x N y ) ) )
23 21 22 syldan 
 |-  ( ( ( ph /\ D e. ( Bnd ` Y ) ) /\ ( x e. Y /\ y e. Y ) ) -> ( x M y ) <_ ( S x. ( x N y ) ) )
24 7 oveqi 
 |-  ( x C y ) = ( x ( M |` ( Y X. Y ) ) y )
25 ovres 
 |-  ( ( x e. Y /\ y e. Y ) -> ( x ( M |` ( Y X. Y ) ) y ) = ( x M y ) )
26 24 25 syl5eq 
 |-  ( ( x e. Y /\ y e. Y ) -> ( x C y ) = ( x M y ) )
27 26 adantl 
 |-  ( ( ( ph /\ D e. ( Bnd ` Y ) ) /\ ( x e. Y /\ y e. Y ) ) -> ( x C y ) = ( x M y ) )
28 8 oveqi 
 |-  ( x D y ) = ( x ( N |` ( Y X. Y ) ) y )
29 ovres 
 |-  ( ( x e. Y /\ y e. Y ) -> ( x ( N |` ( Y X. Y ) ) y ) = ( x N y ) )
30 28 29 syl5eq 
 |-  ( ( x e. Y /\ y e. Y ) -> ( x D y ) = ( x N y ) )
31 30 adantl 
 |-  ( ( ( ph /\ D e. ( Bnd ` Y ) ) /\ ( x e. Y /\ y e. Y ) ) -> ( x D y ) = ( x N y ) )
32 31 oveq2d 
 |-  ( ( ( ph /\ D e. ( Bnd ` Y ) ) /\ ( x e. Y /\ y e. Y ) ) -> ( S x. ( x D y ) ) = ( S x. ( x N y ) ) )
33 23 27 32 3brtr4d 
 |-  ( ( ( ph /\ D e. ( Bnd ` Y ) ) /\ ( x e. Y /\ y e. Y ) ) -> ( x C y ) <_ ( S x. ( x D y ) ) )
34 11 17 18 33 equivbnd 
 |-  ( ( ph /\ D e. ( Bnd ` Y ) ) -> C e. ( Bnd ` Y ) )
35 9 biimpar 
 |-  ( ( ph /\ C e. ( Bnd ` Y ) ) -> C e. ( TotBnd ` Y ) )
36 34 35 syldan 
 |-  ( ( ph /\ D e. ( Bnd ` Y ) ) -> C e. ( TotBnd ` Y ) )
37 bndmet 
 |-  ( D e. ( Bnd ` Y ) -> D e. ( Met ` Y ) )
38 37 adantl 
 |-  ( ( ph /\ D e. ( Bnd ` Y ) ) -> D e. ( Met ` Y ) )
39 3 adantr 
 |-  ( ( ph /\ D e. ( Bnd ` Y ) ) -> R e. RR+ )
40 5 adantlr 
 |-  ( ( ( ph /\ D e. ( Bnd ` Y ) ) /\ ( x e. X /\ y e. X ) ) -> ( x N y ) <_ ( R x. ( x M y ) ) )
41 21 40 syldan 
 |-  ( ( ( ph /\ D e. ( Bnd ` Y ) ) /\ ( x e. Y /\ y e. Y ) ) -> ( x N y ) <_ ( R x. ( x M y ) ) )
42 27 oveq2d 
 |-  ( ( ( ph /\ D e. ( Bnd ` Y ) ) /\ ( x e. Y /\ y e. Y ) ) -> ( R x. ( x C y ) ) = ( R x. ( x M y ) ) )
43 41 31 42 3brtr4d 
 |-  ( ( ( ph /\ D e. ( Bnd ` Y ) ) /\ ( x e. Y /\ y e. Y ) ) -> ( x D y ) <_ ( R x. ( x C y ) ) )
44 36 38 39 43 equivtotbnd 
 |-  ( ( ph /\ D e. ( Bnd ` Y ) ) -> D e. ( TotBnd ` Y ) )
45 44 ex 
 |-  ( ph -> ( D e. ( Bnd ` Y ) -> D e. ( TotBnd ` Y ) ) )
46 10 45 impbid2 
 |-  ( ph -> ( D e. ( TotBnd ` Y ) <-> D e. ( Bnd ` Y ) ) )