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	⊢ ( 𝜑 → 𝑀 ∈ ( Bnd ‘ 𝑋 ) )
	equivbnd.2	⊢ ( 𝜑 → 𝑁 ∈ ( Met ‘ 𝑋 ) )
	equivbnd.3	⊢ ( 𝜑 → 𝑅 ∈ ℝ+ )
	equivbnd.4	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( 𝑥 𝑁 𝑦 ) ≤ ( 𝑅 · ( 𝑥 𝑀 𝑦 ) ) )
Assertion	equivbnd	⊢ ( 𝜑 → 𝑁 ∈ ( Bnd ‘ 𝑋 ) )

Proof

Step	Hyp	Ref	Expression
1		equivbnd.1	⊢ ( 𝜑 → 𝑀 ∈ ( Bnd ‘ 𝑋 ) )
2		equivbnd.2	⊢ ( 𝜑 → 𝑁 ∈ ( Met ‘ 𝑋 ) )
3		equivbnd.3	⊢ ( 𝜑 → 𝑅 ∈ ℝ+ )
4		equivbnd.4	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( 𝑥 𝑁 𝑦 ) ≤ ( 𝑅 · ( 𝑥 𝑀 𝑦 ) ) )
5		isbnd3b	⊢ ( 𝑀 ∈ ( Bnd ‘ 𝑋 ) ↔ ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ ∃ 𝑟 ∈ ℝ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑀 𝑦 ) ≤ 𝑟 ) )
6	5	simprbi	⊢ ( 𝑀 ∈ ( Bnd ‘ 𝑋 ) → ∃ 𝑟 ∈ ℝ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑀 𝑦 ) ≤ 𝑟 )
7	1 6	syl	⊢ ( 𝜑 → ∃ 𝑟 ∈ ℝ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑀 𝑦 ) ≤ 𝑟 )
8	3	rpred	⊢ ( 𝜑 → 𝑅 ∈ ℝ )
9		remulcl	⊢ ( ( 𝑅 ∈ ℝ ∧ 𝑟 ∈ ℝ ) → ( 𝑅 · 𝑟 ) ∈ ℝ )
10	8 9	sylan	⊢ ( ( 𝜑 ∧ 𝑟 ∈ ℝ ) → ( 𝑅 · 𝑟 ) ∈ ℝ )
11		bndmet	⊢ ( 𝑀 ∈ ( Bnd ‘ 𝑋 ) → 𝑀 ∈ ( Met ‘ 𝑋 ) )
12	1 11	syl	⊢ ( 𝜑 → 𝑀 ∈ ( Met ‘ 𝑋 ) )
13	12	adantr	⊢ ( ( 𝜑 ∧ 𝑟 ∈ ℝ ) → 𝑀 ∈ ( Met ‘ 𝑋 ) )
14		metcl	⊢ ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( 𝑥 𝑀 𝑦 ) ∈ ℝ )
15	14	3expb	⊢ ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( 𝑥 𝑀 𝑦 ) ∈ ℝ )
16	13 15	sylan	⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( 𝑥 𝑀 𝑦 ) ∈ ℝ )
17		simplr	⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → 𝑟 ∈ ℝ )
18	3	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → 𝑅 ∈ ℝ+ )
19	16 17 18	lemul2d	⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( ( 𝑥 𝑀 𝑦 ) ≤ 𝑟 ↔ ( 𝑅 · ( 𝑥 𝑀 𝑦 ) ) ≤ ( 𝑅 · 𝑟 ) ) )
20	4	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( 𝑥 𝑁 𝑦 ) ≤ ( 𝑅 · ( 𝑥 𝑀 𝑦 ) ) )
21	2	adantr	⊢ ( ( 𝜑 ∧ 𝑟 ∈ ℝ ) → 𝑁 ∈ ( Met ‘ 𝑋 ) )
22		metcl	⊢ ( ( 𝑁 ∈ ( Met ‘ 𝑋 ) ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( 𝑥 𝑁 𝑦 ) ∈ ℝ )
23	22	3expb	⊢ ( ( 𝑁 ∈ ( Met ‘ 𝑋 ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( 𝑥 𝑁 𝑦 ) ∈ ℝ )
24	21 23	sylan	⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( 𝑥 𝑁 𝑦 ) ∈ ℝ )
25	8	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → 𝑅 ∈ ℝ )
26	25 16	remulcld	⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( 𝑅 · ( 𝑥 𝑀 𝑦 ) ) ∈ ℝ )
27	10	adantr	⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( 𝑅 · 𝑟 ) ∈ ℝ )
28		letr	⊢ ( ( ( 𝑥 𝑁 𝑦 ) ∈ ℝ ∧ ( 𝑅 · ( 𝑥 𝑀 𝑦 ) ) ∈ ℝ ∧ ( 𝑅 · 𝑟 ) ∈ ℝ ) → ( ( ( 𝑥 𝑁 𝑦 ) ≤ ( 𝑅 · ( 𝑥 𝑀 𝑦 ) ) ∧ ( 𝑅 · ( 𝑥 𝑀 𝑦 ) ) ≤ ( 𝑅 · 𝑟 ) ) → ( 𝑥 𝑁 𝑦 ) ≤ ( 𝑅 · 𝑟 ) ) )
29	24 26 27 28	syl3anc	⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( ( ( 𝑥 𝑁 𝑦 ) ≤ ( 𝑅 · ( 𝑥 𝑀 𝑦 ) ) ∧ ( 𝑅 · ( 𝑥 𝑀 𝑦 ) ) ≤ ( 𝑅 · 𝑟 ) ) → ( 𝑥 𝑁 𝑦 ) ≤ ( 𝑅 · 𝑟 ) ) )
30	20 29	mpand	⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( ( 𝑅 · ( 𝑥 𝑀 𝑦 ) ) ≤ ( 𝑅 · 𝑟 ) → ( 𝑥 𝑁 𝑦 ) ≤ ( 𝑅 · 𝑟 ) ) )
31	19 30	sylbid	⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( ( 𝑥 𝑀 𝑦 ) ≤ 𝑟 → ( 𝑥 𝑁 𝑦 ) ≤ ( 𝑅 · 𝑟 ) ) )
32	31	ralimdvva	⊢ ( ( 𝜑 ∧ 𝑟 ∈ ℝ ) → ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑀 𝑦 ) ≤ 𝑟 → ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑁 𝑦 ) ≤ ( 𝑅 · 𝑟 ) ) )
33		breq2	⊢ ( 𝑠 = ( 𝑅 · 𝑟 ) → ( ( 𝑥 𝑁 𝑦 ) ≤ 𝑠 ↔ ( 𝑥 𝑁 𝑦 ) ≤ ( 𝑅 · 𝑟 ) ) )
34	33	2ralbidv	⊢ ( 𝑠 = ( 𝑅 · 𝑟 ) → ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑁 𝑦 ) ≤ 𝑠 ↔ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑁 𝑦 ) ≤ ( 𝑅 · 𝑟 ) ) )
35	34	rspcev	⊢ ( ( ( 𝑅 · 𝑟 ) ∈ ℝ ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑁 𝑦 ) ≤ ( 𝑅 · 𝑟 ) ) → ∃ 𝑠 ∈ ℝ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑁 𝑦 ) ≤ 𝑠 )
36	10 32 35	syl6an	⊢ ( ( 𝜑 ∧ 𝑟 ∈ ℝ ) → ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑀 𝑦 ) ≤ 𝑟 → ∃ 𝑠 ∈ ℝ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑁 𝑦 ) ≤ 𝑠 ) )
37	36	rexlimdva	⊢ ( 𝜑 → ( ∃ 𝑟 ∈ ℝ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑀 𝑦 ) ≤ 𝑟 → ∃ 𝑠 ∈ ℝ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑁 𝑦 ) ≤ 𝑠 ) )
38	7 37	mpd	⊢ ( 𝜑 → ∃ 𝑠 ∈ ℝ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑁 𝑦 ) ≤ 𝑠 )
39		isbnd3b	⊢ ( 𝑁 ∈ ( Bnd ‘ 𝑋 ) ↔ ( 𝑁 ∈ ( Met ‘ 𝑋 ) ∧ ∃ 𝑠 ∈ ℝ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑁 𝑦 ) ≤ 𝑠 ) )
40	2 38 39	sylanbrc	⊢ ( 𝜑 → 𝑁 ∈ ( Bnd ‘ 𝑋 ) )