equivbnd2

Description: If balls are totally bounded in the metric M , then balls are totally bounded in the equivalent metric N . (Contributed by Mario Carneiro, 15-Sep-2015)

	Ref	Expression
Hypotheses	equivbnd2.1	$⊢ φ \to M \in Met (X)$
	equivbnd2.2	$⊢ φ \to N \in Met (X)$
	equivbnd2.3	$⊢ φ \to R \in ℝ^{+}$
	equivbnd2.4	$⊢ φ \to S \in ℝ^{+}$
	equivbnd2.5	$⊢ (φ \land (x \in X \land y \in X)) \to x N y \leq R (x M y)$
	equivbnd2.6	$⊢ (φ \land (x \in X \land y \in X)) \to x M y \leq S (x N y)$
	equivbnd2.7	$⊢ C = {M ↾}_{(Y \times Y)}$
	equivbnd2.8	$⊢ D = {N ↾}_{(Y \times Y)}$
	equivbnd2.9	$⊢ φ \to (C \in TotBnd (Y) \leftrightarrow C \in Bnd (Y))$
Assertion	equivbnd2	$⊢ φ \to (D \in TotBnd (Y) \leftrightarrow D \in Bnd (Y))$

Proof

Step	Hyp	Ref	Expression
1		equivbnd2.1	$⊢ φ \to M \in Met (X)$
2		equivbnd2.2	$⊢ φ \to N \in Met (X)$
3		equivbnd2.3	$⊢ φ \to R \in ℝ^{+}$
4		equivbnd2.4	$⊢ φ \to S \in ℝ^{+}$
5		equivbnd2.5	$⊢ (φ \land (x \in X \land y \in X)) \to x N y \leq R (x M y)$
6		equivbnd2.6	$⊢ (φ \land (x \in X \land y \in X)) \to x M y \leq S (x N y)$
7		equivbnd2.7	$⊢ C = {M ↾}_{(Y \times Y)}$
8		equivbnd2.8	$⊢ D = {N ↾}_{(Y \times Y)}$
9		equivbnd2.9	$⊢ φ \to (C \in TotBnd (Y) \leftrightarrow C \in Bnd (Y))$
10		totbndbnd	$⊢ D \in TotBnd (Y) \to D \in Bnd (Y)$
11		simpr	$⊢ (φ \land D \in Bnd (Y)) \to D \in Bnd (Y)$
12	1	adantr	$⊢ (φ \land D \in Bnd (Y)) \to M \in Met (X)$
13	8	bnd2lem	$⊢ (N \in Met (X) \land D \in Bnd (Y)) \to Y \subseteq X$
14	2 13	sylan	$⊢ (φ \land D \in Bnd (Y)) \to Y \subseteq X$
15		metres2	$⊢ (M \in Met (X) \land Y \subseteq X) \to {M ↾}_{(Y \times Y)} \in Met (Y)$
16	12 14 15	syl2anc	$⊢ (φ \land D \in Bnd (Y)) \to {M ↾}_{(Y \times Y)} \in Met (Y)$
17	7 16	eqeltrid	$⊢ (φ \land D \in Bnd (Y)) \to C \in Met (Y)$
18	4	adantr	$⊢ (φ \land D \in Bnd (Y)) \to S \in ℝ^{+}$
19	14	sselda	$⊢ ((φ \land D \in Bnd (Y)) \land x \in Y) \to x \in X$
20	14	sselda	$⊢ ((φ \land D \in Bnd (Y)) \land y \in Y) \to y \in X$
21	19 20	anim12dan	$⊢ ((φ \land D \in Bnd (Y)) \land (x \in Y \land y \in Y)) \to (x \in X \land y \in X)$
22	6	adantlr	$⊢ ((φ \land D \in Bnd (Y)) \land (x \in X \land y \in X)) \to x M y \leq S (x N y)$
23	21 22	syldan	$⊢ ((φ \land D \in Bnd (Y)) \land (x \in Y \land y \in Y)) \to x M y \leq S (x N y)$
24	7	oveqi	$⊢ x C y = x ({M ↾}_{(Y \times Y)}) y$
25		ovres	$⊢ (x \in Y \land y \in Y) \to x ({M ↾}_{(Y \times Y)}) y = x M y$
26	24 25	syl5eq	$⊢ (x \in Y \land y \in Y) \to x C y = x M y$
27	26	adantl	$⊢ ((φ \land D \in Bnd (Y)) \land (x \in Y \land y \in Y)) \to x C y = x M y$
28	8	oveqi	$⊢ x D y = x ({N ↾}_{(Y \times Y)}) y$
29		ovres	$⊢ (x \in Y \land y \in Y) \to x ({N ↾}_{(Y \times Y)}) y = x N y$
30	28 29	syl5eq	$⊢ (x \in Y \land y \in Y) \to x D y = x N y$
31	30	adantl	$⊢ ((φ \land D \in Bnd (Y)) \land (x \in Y \land y \in Y)) \to x D y = x N y$
32	31	oveq2d	$⊢ ((φ \land D \in Bnd (Y)) \land (x \in Y \land y \in Y)) \to S (x D y) = S (x N y)$
33	23 27 32	3brtr4d	$⊢ ((φ \land D \in Bnd (Y)) \land (x \in Y \land y \in Y)) \to x C y \leq S (x D y)$
34	11 17 18 33	equivbnd	$⊢ (φ \land D \in Bnd (Y)) \to C \in Bnd (Y)$
35	9	biimpar	$⊢ (φ \land C \in Bnd (Y)) \to C \in TotBnd (Y)$
36	34 35	syldan	$⊢ (φ \land D \in Bnd (Y)) \to C \in TotBnd (Y)$
37		bndmet	$⊢ D \in Bnd (Y) \to D \in Met (Y)$
38	37	adantl	$⊢ (φ \land D \in Bnd (Y)) \to D \in Met (Y)$
39	3	adantr	$⊢ (φ \land D \in Bnd (Y)) \to R \in ℝ^{+}$
40	5	adantlr	$⊢ ((φ \land D \in Bnd (Y)) \land (x \in X \land y \in X)) \to x N y \leq R (x M y)$
41	21 40	syldan	$⊢ ((φ \land D \in Bnd (Y)) \land (x \in Y \land y \in Y)) \to x N y \leq R (x M y)$
42	27	oveq2d	$⊢ ((φ \land D \in Bnd (Y)) \land (x \in Y \land y \in Y)) \to R (x C y) = R (x M y)$
43	41 31 42	3brtr4d	$⊢ ((φ \land D \in Bnd (Y)) \land (x \in Y \land y \in Y)) \to x D y \leq R (x C y)$
44	36 38 39 43	equivtotbnd	$⊢ (φ \land D \in Bnd (Y)) \to D \in TotBnd (Y)$
45	44	ex	$⊢ φ \to (D \in Bnd (Y) \to D \in TotBnd (Y))$
46	10 45	impbid2	$⊢ φ \to (D \in TotBnd (Y) \leftrightarrow D \in Bnd (Y))$

Metamath Proof Explorer

Theorem equivbnd2

Proof