Metamath Proof Explorer

Theorem equivbnd

Description: If the metric M is "strongly finer" than N (meaning that there is a positive real constant R such that N ( x , y ) <_ R x. M ( x , y ) ), then boundedness of M implies boundedness of N . (Using this theorem twice in each direction states that if two metrics are strongly equivalent, then one is bounded iff the other is.) (Contributed by Mario Carneiro, 14-Sep-2015)

Ref Expression
Hypotheses equivbnd.1 
|- ( ph -> M e. ( Bnd ` X ) )
equivbnd.2 
|- ( ph -> N e. ( Met ` X ) )
equivbnd.3 
|- ( ph -> R e. RR+ )
equivbnd.4 
|- ( ( ph /\ ( x e. X /\ y e. X ) ) -> ( x N y ) <_ ( R x. ( x M y ) ) )
Assertion equivbnd 
|- ( ph -> N e. ( Bnd ` X ) )

Proof

Step Hyp Ref Expression
1 equivbnd.1 
 |-  ( ph -> M e. ( Bnd ` X ) )
2 equivbnd.2 
 |-  ( ph -> N e. ( Met ` X ) )
3 equivbnd.3 
 |-  ( ph -> R e. RR+ )
4 equivbnd.4 
 |-  ( ( ph /\ ( x e. X /\ y e. X ) ) -> ( x N y ) <_ ( R x. ( x M y ) ) )
5 isbnd3b 
 |-  ( M e. ( Bnd ` X ) <-> ( M e. ( Met ` X ) /\ E. r e. RR A. x e. X A. y e. X ( x M y ) <_ r ) )
6 5 simprbi 
 |-  ( M e. ( Bnd ` X ) -> E. r e. RR A. x e. X A. y e. X ( x M y ) <_ r )
7 1 6 syl 
 |-  ( ph -> E. r e. RR A. x e. X A. y e. X ( x M y ) <_ r )
8 3 rpred 
 |-  ( ph -> R e. RR )
9 remulcl 
 |-  ( ( R e. RR /\ r e. RR ) -> ( R x. r ) e. RR )
10 8 9 sylan 
 |-  ( ( ph /\ r e. RR ) -> ( R x. r ) e. RR )
11 bndmet 
 |-  ( M e. ( Bnd ` X ) -> M e. ( Met ` X ) )
12 1 11 syl 
 |-  ( ph -> M e. ( Met ` X ) )
13 12 adantr 
 |-  ( ( ph /\ r e. RR ) -> M e. ( Met ` X ) )
14 metcl 
 |-  ( ( M e. ( Met ` X ) /\ x e. X /\ y e. X ) -> ( x M y ) e. RR )
15 14 3expb 
 |-  ( ( M e. ( Met ` X ) /\ ( x e. X /\ y e. X ) ) -> ( x M y ) e. RR )
16 13 15 sylan 
 |-  ( ( ( ph /\ r e. RR ) /\ ( x e. X /\ y e. X ) ) -> ( x M y ) e. RR )
17 simplr 
 |-  ( ( ( ph /\ r e. RR ) /\ ( x e. X /\ y e. X ) ) -> r e. RR )
18 3 ad2antrr 
 |-  ( ( ( ph /\ r e. RR ) /\ ( x e. X /\ y e. X ) ) -> R e. RR+ )
19 16 17 18 lemul2d 
 |-  ( ( ( ph /\ r e. RR ) /\ ( x e. X /\ y e. X ) ) -> ( ( x M y ) <_ r <-> ( R x. ( x M y ) ) <_ ( R x. r ) ) )
20 4 adantlr 
 |-  ( ( ( ph /\ r e. RR ) /\ ( x e. X /\ y e. X ) ) -> ( x N y ) <_ ( R x. ( x M y ) ) )
21 2 adantr 
 |-  ( ( ph /\ r e. RR ) -> N e. ( Met ` X ) )
22 metcl 
 |-  ( ( N e. ( Met ` X ) /\ x e. X /\ y e. X ) -> ( x N y ) e. RR )
23 22 3expb 
 |-  ( ( N e. ( Met ` X ) /\ ( x e. X /\ y e. X ) ) -> ( x N y ) e. RR )
24 21 23 sylan 
 |-  ( ( ( ph /\ r e. RR ) /\ ( x e. X /\ y e. X ) ) -> ( x N y ) e. RR )
25 8 ad2antrr 
 |-  ( ( ( ph /\ r e. RR ) /\ ( x e. X /\ y e. X ) ) -> R e. RR )
26 25 16 remulcld 
 |-  ( ( ( ph /\ r e. RR ) /\ ( x e. X /\ y e. X ) ) -> ( R x. ( x M y ) ) e. RR )
27 10 adantr 
 |-  ( ( ( ph /\ r e. RR ) /\ ( x e. X /\ y e. X ) ) -> ( R x. r ) e. RR )
28 letr 
 |-  ( ( ( x N y ) e. RR /\ ( R x. ( x M y ) ) e. RR /\ ( R x. r ) e. RR ) -> ( ( ( x N y ) <_ ( R x. ( x M y ) ) /\ ( R x. ( x M y ) ) <_ ( R x. r ) ) -> ( x N y ) <_ ( R x. r ) ) )
29 24 26 27 28 syl3anc 
 |-  ( ( ( ph /\ r e. RR ) /\ ( x e. X /\ y e. X ) ) -> ( ( ( x N y ) <_ ( R x. ( x M y ) ) /\ ( R x. ( x M y ) ) <_ ( R x. r ) ) -> ( x N y ) <_ ( R x. r ) ) )
30 20 29 mpand 
 |-  ( ( ( ph /\ r e. RR ) /\ ( x e. X /\ y e. X ) ) -> ( ( R x. ( x M y ) ) <_ ( R x. r ) -> ( x N y ) <_ ( R x. r ) ) )
31 19 30 sylbid 
 |-  ( ( ( ph /\ r e. RR ) /\ ( x e. X /\ y e. X ) ) -> ( ( x M y ) <_ r -> ( x N y ) <_ ( R x. r ) ) )
32 31 ralimdvva 
 |-  ( ( ph /\ r e. RR ) -> ( A. x e. X A. y e. X ( x M y ) <_ r -> A. x e. X A. y e. X ( x N y ) <_ ( R x. r ) ) )
33 breq2 
 |-  ( s = ( R x. r ) -> ( ( x N y ) <_ s <-> ( x N y ) <_ ( R x. r ) ) )
34 33 2ralbidv 
 |-  ( s = ( R x. r ) -> ( A. x e. X A. y e. X ( x N y ) <_ s <-> A. x e. X A. y e. X ( x N y ) <_ ( R x. r ) ) )
35 34 rspcev 
 |-  ( ( ( R x. r ) e. RR /\ A. x e. X A. y e. X ( x N y ) <_ ( R x. r ) ) -> E. s e. RR A. x e. X A. y e. X ( x N y ) <_ s )
36 10 32 35 syl6an 
 |-  ( ( ph /\ r e. RR ) -> ( A. x e. X A. y e. X ( x M y ) <_ r -> E. s e. RR A. x e. X A. y e. X ( x N y ) <_ s ) )
37 36 rexlimdva 
 |-  ( ph -> ( E. r e. RR A. x e. X A. y e. X ( x M y ) <_ r -> E. s e. RR A. x e. X A. y e. X ( x N y ) <_ s ) )
38 7 37 mpd 
 |-  ( ph -> E. s e. RR A. x e. X A. y e. X ( x N y ) <_ s )
39 isbnd3b 
 |-  ( N e. ( Bnd ` X ) <-> ( N e. ( Met ` X ) /\ E. s e. RR A. x e. X A. y e. X ( x N y ) <_ s ) )
40 2 38 39 sylanbrc 
 |-  ( ph -> N e. ( Bnd ` X ) )