equivtotbnd

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 total boundedness of M implies total boundedness of N . (Using this theorem twice in each direction states that if two metrics are strongly equivalent, then one is totally bounded iff the other is.) (Contributed by Mario Carneiro, 14-Sep-2015)

	Ref	Expression
Hypotheses	equivtotbnd.1	$⊢ φ \to M \in TotBnd (X)$
	equivtotbnd.2	$⊢ φ \to N \in Met (X)$
	equivtotbnd.3	$⊢ φ \to R \in ℝ^{+}$
	equivtotbnd.4	$⊢ (φ \land (x \in X \land y \in X)) \to x N y \leq R (x M y)$
Assertion	equivtotbnd	$⊢ φ \to N \in TotBnd (X)$

Proof

Step	Hyp	Ref	Expression
1		equivtotbnd.1	$⊢ φ \to M \in TotBnd (X)$
2		equivtotbnd.2	$⊢ φ \to N \in Met (X)$
3		equivtotbnd.3	$⊢ φ \to R \in ℝ^{+}$
4		equivtotbnd.4	$⊢ (φ \land (x \in X \land y \in X)) \to x N y \leq R (x M y)$
5		simpr	$⊢ (φ \land r \in ℝ^{+}) \to r \in ℝ^{+}$
6	3	adantr	$⊢ (φ \land r \in ℝ^{+}) \to R \in ℝ^{+}$
7	5 6	rpdivcld	$⊢ (φ \land r \in ℝ^{+}) \to \frac{r}{R} \in ℝ^{+}$
8	1	adantr	$⊢ (φ \land r \in ℝ^{+}) \to M \in TotBnd (X)$
9		istotbnd3	$⊢ M \in TotBnd (X) \leftrightarrow (M \in Met (X) \land \forall s \in ℝ^{+} \exists v \in (𝒫 X \cap Fin) ⋃_{x \in v} (x ball (M) s) = X)$
10	9	simprbi	$⊢ M \in TotBnd (X) \to \forall s \in ℝ^{+} \exists v \in (𝒫 X \cap Fin) ⋃_{x \in v} (x ball (M) s) = X$
11	8 10	syl	$⊢ (φ \land r \in ℝ^{+}) \to \forall s \in ℝ^{+} \exists v \in (𝒫 X \cap Fin) ⋃_{x \in v} (x ball (M) s) = X$
12		oveq2	$⊢ s = \frac{r}{R} \to x ball (M) s = x ball (M) (\frac{r}{R})$
13	12	iuneq2d	$⊢ s = \frac{r}{R} \to ⋃_{x \in v} (x ball (M) s) = ⋃_{x \in v} (x ball (M) (\frac{r}{R}))$
14	13	eqeq1d	$⊢ s = \frac{r}{R} \to (⋃_{x \in v} (x ball (M) s) = X \leftrightarrow ⋃_{x \in v} (x ball (M) (\frac{r}{R})) = X)$
15	14	rexbidv	$⊢ s = \frac{r}{R} \to (\exists v \in (𝒫 X \cap Fin) ⋃_{x \in v} (x ball (M) s) = X \leftrightarrow \exists v \in (𝒫 X \cap Fin) ⋃_{x \in v} (x ball (M) (\frac{r}{R})) = X)$
16	15	rspcv	$⊢ \frac{r}{R} \in ℝ^{+} \to (\forall s \in ℝ^{+} \exists v \in (𝒫 X \cap Fin) ⋃_{x \in v} (x ball (M) s) = X \to \exists v \in (𝒫 X \cap Fin) ⋃_{x \in v} (x ball (M) (\frac{r}{R})) = X)$
17	7 11 16	sylc	$⊢ (φ \land r \in ℝ^{+}) \to \exists v \in (𝒫 X \cap Fin) ⋃_{x \in v} (x ball (M) (\frac{r}{R})) = X$
18		elfpw	$⊢ v \in (𝒫 X \cap Fin) \leftrightarrow (v \subseteq X \land v \in Fin)$
19	18	simplbi	$⊢ v \in (𝒫 X \cap Fin) \to v \subseteq X$
20	19	adantl	$⊢ ((φ \land r \in ℝ^{+}) \land v \in (𝒫 X \cap Fin)) \to v \subseteq X$
21	20	sselda	$⊢ (((φ \land r \in ℝ^{+}) \land v \in (𝒫 X \cap Fin)) \land x \in v) \to x \in X$
22		eqid	$⊢ MetOpen (N) = MetOpen (N)$
23		eqid	$⊢ MetOpen (M) = MetOpen (M)$
24	9	simplbi	$⊢ M \in TotBnd (X) \to M \in Met (X)$
25	1 24	syl	$⊢ φ \to M \in Met (X)$
26	22 23 2 25 3 4	metss2lem	$⊢ (φ \land (x \in X \land r \in ℝ^{+})) \to x ball (M) (\frac{r}{R}) \subseteq x ball (N) r$
27	26	anass1rs	$⊢ ((φ \land r \in ℝ^{+}) \land x \in X) \to x ball (M) (\frac{r}{R}) \subseteq x ball (N) r$
28	27	adantlr	$⊢ (((φ \land r \in ℝ^{+}) \land v \in (𝒫 X \cap Fin)) \land x \in X) \to x ball (M) (\frac{r}{R}) \subseteq x ball (N) r$
29	21 28	syldan	$⊢ (((φ \land r \in ℝ^{+}) \land v \in (𝒫 X \cap Fin)) \land x \in v) \to x ball (M) (\frac{r}{R}) \subseteq x ball (N) r$
30	29	ralrimiva	$⊢ ((φ \land r \in ℝ^{+}) \land v \in (𝒫 X \cap Fin)) \to \forall x \in v x ball (M) (\frac{r}{R}) \subseteq x ball (N) r$
31		ss2iun	$⊢ \forall x \in v x ball (M) (\frac{r}{R}) \subseteq x ball (N) r \to ⋃_{x \in v} (x ball (M) (\frac{r}{R})) \subseteq ⋃_{x \in v} (x ball (N) r)$
32	30 31	syl	$⊢ ((φ \land r \in ℝ^{+}) \land v \in (𝒫 X \cap Fin)) \to ⋃_{x \in v} (x ball (M) (\frac{r}{R})) \subseteq ⋃_{x \in v} (x ball (N) r)$
33		sseq1	$⊢ ⋃_{x \in v} (x ball (M) (\frac{r}{R})) = X \to (⋃_{x \in v} (x ball (M) (\frac{r}{R})) \subseteq ⋃_{x \in v} (x ball (N) r) \leftrightarrow X \subseteq ⋃_{x \in v} (x ball (N) r))$
34	32 33	syl5ibcom	$⊢ ((φ \land r \in ℝ^{+}) \land v \in (𝒫 X \cap Fin)) \to (⋃_{x \in v} (x ball (M) (\frac{r}{R})) = X \to X \subseteq ⋃_{x \in v} (x ball (N) r))$
35	2	ad3antrrr	$⊢ (((φ \land r \in ℝ^{+}) \land v \in (𝒫 X \cap Fin)) \land x \in v) \to N \in Met (X)$
36		metxmet	$⊢ N \in Met (X) \to N \in ∞Met (X)$
37	35 36	syl	$⊢ (((φ \land r \in ℝ^{+}) \land v \in (𝒫 X \cap Fin)) \land x \in v) \to N \in ∞Met (X)$
38		simpllr	$⊢ (((φ \land r \in ℝ^{+}) \land v \in (𝒫 X \cap Fin)) \land x \in v) \to r \in ℝ^{+}$
39	38	rpxrd	$⊢ (((φ \land r \in ℝ^{+}) \land v \in (𝒫 X \cap Fin)) \land x \in v) \to r \in ℝ^{*}$
40		blssm	$⊢ (N \in ∞Met (X) \land x \in X \land r \in ℝ^{*}) \to x ball (N) r \subseteq X$
41	37 21 39 40	syl3anc	$⊢ (((φ \land r \in ℝ^{+}) \land v \in (𝒫 X \cap Fin)) \land x \in v) \to x ball (N) r \subseteq X$
42	41	ralrimiva	$⊢ ((φ \land r \in ℝ^{+}) \land v \in (𝒫 X \cap Fin)) \to \forall x \in v x ball (N) r \subseteq X$
43		iunss	$⊢ ⋃_{x \in v} (x ball (N) r) \subseteq X \leftrightarrow \forall x \in v x ball (N) r \subseteq X$
44	42 43	sylibr	$⊢ ((φ \land r \in ℝ^{+}) \land v \in (𝒫 X \cap Fin)) \to ⋃_{x \in v} (x ball (N) r) \subseteq X$
45	34 44	jctild	$⊢ ((φ \land r \in ℝ^{+}) \land v \in (𝒫 X \cap Fin)) \to (⋃_{x \in v} (x ball (M) (\frac{r}{R})) = X \to (⋃_{x \in v} (x ball (N) r) \subseteq X \land X \subseteq ⋃_{x \in v} (x ball (N) r)))$
46		eqss	$⊢ ⋃_{x \in v} (x ball (N) r) = X \leftrightarrow (⋃_{x \in v} (x ball (N) r) \subseteq X \land X \subseteq ⋃_{x \in v} (x ball (N) r))$
47	45 46	syl6ibr	$⊢ ((φ \land r \in ℝ^{+}) \land v \in (𝒫 X \cap Fin)) \to (⋃_{x \in v} (x ball (M) (\frac{r}{R})) = X \to ⋃_{x \in v} (x ball (N) r) = X)$
48	47	reximdva	$⊢ (φ \land r \in ℝ^{+}) \to (\exists v \in (𝒫 X \cap Fin) ⋃_{x \in v} (x ball (M) (\frac{r}{R})) = X \to \exists v \in (𝒫 X \cap Fin) ⋃_{x \in v} (x ball (N) r) = X)$
49	17 48	mpd	$⊢ (φ \land r \in ℝ^{+}) \to \exists v \in (𝒫 X \cap Fin) ⋃_{x \in v} (x ball (N) r) = X$
50	49	ralrimiva	$⊢ φ \to \forall r \in ℝ^{+} \exists v \in (𝒫 X \cap Fin) ⋃_{x \in v} (x ball (N) r) = X$
51		istotbnd3	$⊢ N \in TotBnd (X) \leftrightarrow (N \in Met (X) \land \forall r \in ℝ^{+} \exists v \in (𝒫 X \cap Fin) ⋃_{x \in v} (x ball (N) r) = X)$
52	2 50 51	sylanbrc	$⊢ φ \to N \in TotBnd (X)$

Metamath Proof Explorer

Theorem equivtotbnd

Proof