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	$⊢ φ \to M \in Bnd (X)$
	equivbnd.2	$⊢ φ \to N \in Met (X)$
	equivbnd.3	$⊢ φ \to R \in ℝ^{+}$
	equivbnd.4	$⊢ (φ \land (x \in X \land y \in X)) \to x N y \leq R (x M y)$
Assertion	equivbnd	$⊢ φ \to N \in Bnd (X)$

Proof

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

Metamath Proof Explorer

Theorem equivbnd

Proof