equivcfil

Description: If the metric D is "strongly finer" than C (meaning that there is a positive real constant R such that C ( x , y ) <_ R x. D ( x , y ) ), all the D -Cauchy filters are also C -Cauchy. (Using this theorem twice in each direction states that if two metrics are strongly equivalent, then they have the same Cauchy sequences.) (Contributed by Mario Carneiro, 14-Sep-2015)

	Ref	Expression
Hypotheses	equivcau.1	$⊢ φ \to C \in Met (X)$
	equivcau.2	$⊢ φ \to D \in Met (X)$
	equivcau.3	$⊢ φ \to R \in ℝ^{+}$
	equivcau.4	$⊢ (φ \land (x \in X \land y \in X)) \to x C y \leq R (x D y)$
Assertion	equivcfil	$⊢ φ \to CauFil (D) \subseteq CauFil (C)$

Proof

Step	Hyp	Ref	Expression
1		equivcau.1	$⊢ φ \to C \in Met (X)$
2		equivcau.2	$⊢ φ \to D \in Met (X)$
3		equivcau.3	$⊢ φ \to R \in ℝ^{+}$
4		equivcau.4	$⊢ (φ \land (x \in X \land y \in X)) \to x C y \leq R (x D y)$
5		simpr	$⊢ ((φ \land f \in Fil (X)) \land r \in ℝ^{+}) \to r \in ℝ^{+}$
6	3	ad2antrr	$⊢ ((φ \land f \in Fil (X)) \land r \in ℝ^{+}) \to R \in ℝ^{+}$
7	5 6	rpdivcld	$⊢ ((φ \land f \in Fil (X)) \land r \in ℝ^{+}) \to \frac{r}{R} \in ℝ^{+}$
8		oveq2	$⊢ s = \frac{r}{R} \to x ball (D) s = x ball (D) (\frac{r}{R})$
9	8	eleq1d	$⊢ s = \frac{r}{R} \to (x ball (D) s \in f \leftrightarrow x ball (D) (\frac{r}{R}) \in f)$
10	9	rexbidv	$⊢ s = \frac{r}{R} \to (\exists x \in X x ball (D) s \in f \leftrightarrow \exists x \in X x ball (D) (\frac{r}{R}) \in f)$
11	10	rspcv	$⊢ \frac{r}{R} \in ℝ^{+} \to (\forall s \in ℝ^{+} \exists x \in X x ball (D) s \in f \to \exists x \in X x ball (D) (\frac{r}{R}) \in f)$
12	7 11	syl	$⊢ ((φ \land f \in Fil (X)) \land r \in ℝ^{+}) \to (\forall s \in ℝ^{+} \exists x \in X x ball (D) s \in f \to \exists x \in X x ball (D) (\frac{r}{R}) \in f)$
13		simpllr	$⊢ (((φ \land f \in Fil (X)) \land r \in ℝ^{+}) \land x \in X) \to f \in Fil (X)$
14		eqid	$⊢ MetOpen (C) = MetOpen (C)$
15		eqid	$⊢ MetOpen (D) = MetOpen (D)$
16	14 15 1 2 3 4	metss2lem	$⊢ (φ \land (x \in X \land r \in ℝ^{+})) \to x ball (D) (\frac{r}{R}) \subseteq x ball (C) r$
17	16	ancom2s	$⊢ (φ \land (r \in ℝ^{+} \land x \in X)) \to x ball (D) (\frac{r}{R}) \subseteq x ball (C) r$
18	17	adantlr	$⊢ ((φ \land f \in Fil (X)) \land (r \in ℝ^{+} \land x \in X)) \to x ball (D) (\frac{r}{R}) \subseteq x ball (C) r$
19	18	anassrs	$⊢ (((φ \land f \in Fil (X)) \land r \in ℝ^{+}) \land x \in X) \to x ball (D) (\frac{r}{R}) \subseteq x ball (C) r$
20	1	ad3antrrr	$⊢ (((φ \land f \in Fil (X)) \land r \in ℝ^{+}) \land x \in X) \to C \in Met (X)$
21		metxmet	$⊢ C \in Met (X) \to C \in ∞Met (X)$
22	20 21	syl	$⊢ (((φ \land f \in Fil (X)) \land r \in ℝ^{+}) \land x \in X) \to C \in ∞Met (X)$
23		simpr	$⊢ (((φ \land f \in Fil (X)) \land r \in ℝ^{+}) \land x \in X) \to x \in X$
24		rpxr	$⊢ r \in ℝ^{+} \to r \in ℝ^{*}$
25	24	ad2antlr	$⊢ (((φ \land f \in Fil (X)) \land r \in ℝ^{+}) \land x \in X) \to r \in ℝ^{*}$
26		blssm	$⊢ (C \in ∞Met (X) \land x \in X \land r \in ℝ^{*}) \to x ball (C) r \subseteq X$
27	22 23 25 26	syl3anc	$⊢ (((φ \land f \in Fil (X)) \land r \in ℝ^{+}) \land x \in X) \to x ball (C) r \subseteq X$
28		filss	$⊢ (f \in Fil (X) \land (x ball (D) (\frac{r}{R}) \in f \land x ball (C) r \subseteq X \land x ball (D) (\frac{r}{R}) \subseteq x ball (C) r)) \to x ball (C) r \in f$
29	28	3exp2	$⊢ f \in Fil (X) \to (x ball (D) (\frac{r}{R}) \in f \to (x ball (C) r \subseteq X \to (x ball (D) (\frac{r}{R}) \subseteq x ball (C) r \to x ball (C) r \in f)))$
30	29	com24	$⊢ f \in Fil (X) \to (x ball (D) (\frac{r}{R}) \subseteq x ball (C) r \to (x ball (C) r \subseteq X \to (x ball (D) (\frac{r}{R}) \in f \to x ball (C) r \in f)))$
31	13 19 27 30	syl3c	$⊢ (((φ \land f \in Fil (X)) \land r \in ℝ^{+}) \land x \in X) \to (x ball (D) (\frac{r}{R}) \in f \to x ball (C) r \in f)$
32	31	reximdva	$⊢ ((φ \land f \in Fil (X)) \land r \in ℝ^{+}) \to (\exists x \in X x ball (D) (\frac{r}{R}) \in f \to \exists x \in X x ball (C) r \in f)$
33	12 32	syld	$⊢ ((φ \land f \in Fil (X)) \land r \in ℝ^{+}) \to (\forall s \in ℝ^{+} \exists x \in X x ball (D) s \in f \to \exists x \in X x ball (C) r \in f)$
34	33	ralrimdva	$⊢ (φ \land f \in Fil (X)) \to (\forall s \in ℝ^{+} \exists x \in X x ball (D) s \in f \to \forall r \in ℝ^{+} \exists x \in X x ball (C) r \in f)$
35	34	imdistanda	$⊢ φ \to ((f \in Fil (X) \land \forall s \in ℝ^{+} \exists x \in X x ball (D) s \in f) \to (f \in Fil (X) \land \forall r \in ℝ^{+} \exists x \in X x ball (C) r \in f))$
36		metxmet	$⊢ D \in Met (X) \to D \in ∞Met (X)$
37		iscfil3	$⊢ D \in ∞Met (X) \to (f \in CauFil (D) \leftrightarrow (f \in Fil (X) \land \forall s \in ℝ^{+} \exists x \in X x ball (D) s \in f))$
38	2 36 37	3syl	$⊢ φ \to (f \in CauFil (D) \leftrightarrow (f \in Fil (X) \land \forall s \in ℝ^{+} \exists x \in X x ball (D) s \in f))$
39		iscfil3	$⊢ C \in ∞Met (X) \to (f \in CauFil (C) \leftrightarrow (f \in Fil (X) \land \forall r \in ℝ^{+} \exists x \in X x ball (C) r \in f))$
40	1 21 39	3syl	$⊢ φ \to (f \in CauFil (C) \leftrightarrow (f \in Fil (X) \land \forall r \in ℝ^{+} \exists x \in X x ball (C) r \in f))$
41	35 38 40	3imtr4d	$⊢ φ \to (f \in CauFil (D) \to f \in CauFil (C))$
42	41	ssrdv	$⊢ φ \to CauFil (D) \subseteq CauFil (C)$

Metamath Proof Explorer

Theorem equivcfil

Proof