# 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 ${⊢}{\phi }\to {M}\in \mathrm{Bnd}\left({X}\right)$
equivbnd.2 ${⊢}{\phi }\to {N}\in \mathrm{Met}\left({X}\right)$
equivbnd.3 ${⊢}{\phi }\to {R}\in {ℝ}^{+}$
equivbnd.4 ${⊢}\left({\phi }\wedge \left({x}\in {X}\wedge {y}\in {X}\right)\right)\to {x}{N}{y}\le {R}\left({x}{M}{y}\right)$
Assertion equivbnd ${⊢}{\phi }\to {N}\in \mathrm{Bnd}\left({X}\right)$

### Proof

Step Hyp Ref Expression
1 equivbnd.1 ${⊢}{\phi }\to {M}\in \mathrm{Bnd}\left({X}\right)$
2 equivbnd.2 ${⊢}{\phi }\to {N}\in \mathrm{Met}\left({X}\right)$
3 equivbnd.3 ${⊢}{\phi }\to {R}\in {ℝ}^{+}$
4 equivbnd.4 ${⊢}\left({\phi }\wedge \left({x}\in {X}\wedge {y}\in {X}\right)\right)\to {x}{N}{y}\le {R}\left({x}{M}{y}\right)$
5 isbnd3b ${⊢}{M}\in \mathrm{Bnd}\left({X}\right)↔\left({M}\in \mathrm{Met}\left({X}\right)\wedge \exists {r}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}{x}{M}{y}\le {r}\right)$
6 5 simprbi ${⊢}{M}\in \mathrm{Bnd}\left({X}\right)\to \exists {r}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}{x}{M}{y}\le {r}$
7 1 6 syl ${⊢}{\phi }\to \exists {r}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}{x}{M}{y}\le {r}$
8 3 rpred ${⊢}{\phi }\to {R}\in ℝ$
9 remulcl ${⊢}\left({R}\in ℝ\wedge {r}\in ℝ\right)\to {R}{r}\in ℝ$
10 8 9 sylan ${⊢}\left({\phi }\wedge {r}\in ℝ\right)\to {R}{r}\in ℝ$
11 bndmet ${⊢}{M}\in \mathrm{Bnd}\left({X}\right)\to {M}\in \mathrm{Met}\left({X}\right)$
12 1 11 syl ${⊢}{\phi }\to {M}\in \mathrm{Met}\left({X}\right)$
13 12 adantr ${⊢}\left({\phi }\wedge {r}\in ℝ\right)\to {M}\in \mathrm{Met}\left({X}\right)$
14 metcl ${⊢}\left({M}\in \mathrm{Met}\left({X}\right)\wedge {x}\in {X}\wedge {y}\in {X}\right)\to {x}{M}{y}\in ℝ$
15 14 3expb ${⊢}\left({M}\in \mathrm{Met}\left({X}\right)\wedge \left({x}\in {X}\wedge {y}\in {X}\right)\right)\to {x}{M}{y}\in ℝ$
16 13 15 sylan ${⊢}\left(\left({\phi }\wedge {r}\in ℝ\right)\wedge \left({x}\in {X}\wedge {y}\in {X}\right)\right)\to {x}{M}{y}\in ℝ$
17 simplr ${⊢}\left(\left({\phi }\wedge {r}\in ℝ\right)\wedge \left({x}\in {X}\wedge {y}\in {X}\right)\right)\to {r}\in ℝ$
18 3 ad2antrr ${⊢}\left(\left({\phi }\wedge {r}\in ℝ\right)\wedge \left({x}\in {X}\wedge {y}\in {X}\right)\right)\to {R}\in {ℝ}^{+}$
19 16 17 18 lemul2d ${⊢}\left(\left({\phi }\wedge {r}\in ℝ\right)\wedge \left({x}\in {X}\wedge {y}\in {X}\right)\right)\to \left({x}{M}{y}\le {r}↔{R}\left({x}{M}{y}\right)\le {R}{r}\right)$
20 4 adantlr ${⊢}\left(\left({\phi }\wedge {r}\in ℝ\right)\wedge \left({x}\in {X}\wedge {y}\in {X}\right)\right)\to {x}{N}{y}\le {R}\left({x}{M}{y}\right)$
21 2 adantr ${⊢}\left({\phi }\wedge {r}\in ℝ\right)\to {N}\in \mathrm{Met}\left({X}\right)$
22 metcl ${⊢}\left({N}\in \mathrm{Met}\left({X}\right)\wedge {x}\in {X}\wedge {y}\in {X}\right)\to {x}{N}{y}\in ℝ$
23 22 3expb ${⊢}\left({N}\in \mathrm{Met}\left({X}\right)\wedge \left({x}\in {X}\wedge {y}\in {X}\right)\right)\to {x}{N}{y}\in ℝ$
24 21 23 sylan ${⊢}\left(\left({\phi }\wedge {r}\in ℝ\right)\wedge \left({x}\in {X}\wedge {y}\in {X}\right)\right)\to {x}{N}{y}\in ℝ$
25 8 ad2antrr ${⊢}\left(\left({\phi }\wedge {r}\in ℝ\right)\wedge \left({x}\in {X}\wedge {y}\in {X}\right)\right)\to {R}\in ℝ$
26 25 16 remulcld ${⊢}\left(\left({\phi }\wedge {r}\in ℝ\right)\wedge \left({x}\in {X}\wedge {y}\in {X}\right)\right)\to {R}\left({x}{M}{y}\right)\in ℝ$
27 10 adantr ${⊢}\left(\left({\phi }\wedge {r}\in ℝ\right)\wedge \left({x}\in {X}\wedge {y}\in {X}\right)\right)\to {R}{r}\in ℝ$
28 letr ${⊢}\left({x}{N}{y}\in ℝ\wedge {R}\left({x}{M}{y}\right)\in ℝ\wedge {R}{r}\in ℝ\right)\to \left(\left({x}{N}{y}\le {R}\left({x}{M}{y}\right)\wedge {R}\left({x}{M}{y}\right)\le {R}{r}\right)\to {x}{N}{y}\le {R}{r}\right)$
29 24 26 27 28 syl3anc ${⊢}\left(\left({\phi }\wedge {r}\in ℝ\right)\wedge \left({x}\in {X}\wedge {y}\in {X}\right)\right)\to \left(\left({x}{N}{y}\le {R}\left({x}{M}{y}\right)\wedge {R}\left({x}{M}{y}\right)\le {R}{r}\right)\to {x}{N}{y}\le {R}{r}\right)$
30 20 29 mpand ${⊢}\left(\left({\phi }\wedge {r}\in ℝ\right)\wedge \left({x}\in {X}\wedge {y}\in {X}\right)\right)\to \left({R}\left({x}{M}{y}\right)\le {R}{r}\to {x}{N}{y}\le {R}{r}\right)$
31 19 30 sylbid ${⊢}\left(\left({\phi }\wedge {r}\in ℝ\right)\wedge \left({x}\in {X}\wedge {y}\in {X}\right)\right)\to \left({x}{M}{y}\le {r}\to {x}{N}{y}\le {R}{r}\right)$
32 31 ralimdvva ${⊢}\left({\phi }\wedge {r}\in ℝ\right)\to \left(\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}{x}{M}{y}\le {r}\to \forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}{x}{N}{y}\le {R}{r}\right)$
33 breq2 ${⊢}{s}={R}{r}\to \left({x}{N}{y}\le {s}↔{x}{N}{y}\le {R}{r}\right)$
34 33 2ralbidv ${⊢}{s}={R}{r}\to \left(\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}{x}{N}{y}\le {s}↔\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}{x}{N}{y}\le {R}{r}\right)$
35 34 rspcev ${⊢}\left({R}{r}\in ℝ\wedge \forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}{x}{N}{y}\le {R}{r}\right)\to \exists {s}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}{x}{N}{y}\le {s}$
36 10 32 35 syl6an ${⊢}\left({\phi }\wedge {r}\in ℝ\right)\to \left(\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}{x}{M}{y}\le {r}\to \exists {s}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}{x}{N}{y}\le {s}\right)$
37 36 rexlimdva ${⊢}{\phi }\to \left(\exists {r}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}{x}{M}{y}\le {r}\to \exists {s}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}{x}{N}{y}\le {s}\right)$
38 7 37 mpd ${⊢}{\phi }\to \exists {s}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}{x}{N}{y}\le {s}$
39 isbnd3b ${⊢}{N}\in \mathrm{Bnd}\left({X}\right)↔\left({N}\in \mathrm{Met}\left({X}\right)\wedge \exists {s}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}{x}{N}{y}\le {s}\right)$
40 2 38 39 sylanbrc ${⊢}{\phi }\to {N}\in \mathrm{Bnd}\left({X}\right)$