equivcau

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 sequences 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	equivcau	$⊢ φ \to Cau (D) \subseteq Cau (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 (X ↑_{𝑝𝑚} ℂ)) \land r \in ℝ^{+}) \to r \in ℝ^{+}$
6	3	ad2antrr	$⊢ ((φ \land f \in (X ↑_{𝑝𝑚} ℂ)) \land r \in ℝ^{+}) \to R \in ℝ^{+}$
7	5 6	rpdivcld	$⊢ ((φ \land f \in (X ↑_{𝑝𝑚} ℂ)) \land r \in ℝ^{+}) \to \frac{r}{R} \in ℝ^{+}$
8		oveq2	$⊢ s = \frac{r}{R} \to f (k) ball (D) s = f (k) ball (D) (\frac{r}{R})$
9	8	feq3d	$⊢ s = \frac{r}{R} \to (({f ↾}_{ℤ_{\geq k}}) : ℤ_{\geq k} ⟶ f (k) ball (D) s \leftrightarrow ({f ↾}_{ℤ_{\geq k}}) : ℤ_{\geq k} ⟶ f (k) ball (D) (\frac{r}{R}))$
10	9	rexbidv	$⊢ s = \frac{r}{R} \to (\exists k \in ℤ ({f ↾}_{ℤ_{\geq k}}) : ℤ_{\geq k} ⟶ f (k) ball (D) s \leftrightarrow \exists k \in ℤ ({f ↾}_{ℤ_{\geq k}}) : ℤ_{\geq k} ⟶ f (k) ball (D) (\frac{r}{R}))$
11	10	rspcv	$⊢ \frac{r}{R} \in ℝ^{+} \to (\forall s \in ℝ^{+} \exists k \in ℤ ({f ↾}_{ℤ_{\geq k}}) : ℤ_{\geq k} ⟶ f (k) ball (D) s \to \exists k \in ℤ ({f ↾}_{ℤ_{\geq k}}) : ℤ_{\geq k} ⟶ f (k) ball (D) (\frac{r}{R}))$
12	7 11	syl	$⊢ ((φ \land f \in (X ↑_{𝑝𝑚} ℂ)) \land r \in ℝ^{+}) \to (\forall s \in ℝ^{+} \exists k \in ℤ ({f ↾}_{ℤ_{\geq k}}) : ℤ_{\geq k} ⟶ f (k) ball (D) s \to \exists k \in ℤ ({f ↾}_{ℤ_{\geq k}}) : ℤ_{\geq k} ⟶ f (k) ball (D) (\frac{r}{R}))$
13		simprr	$⊢ (((φ \land f \in (X ↑_{𝑝𝑚} ℂ)) \land r \in ℝ^{+}) \land (k \in ℤ \land ({f ↾}_{ℤ_{\geq k}}) : ℤ_{\geq k} ⟶ f (k) ball (D) (\frac{r}{R}))) \to ({f ↾}_{ℤ_{\geq k}}) : ℤ_{\geq k} ⟶ f (k) ball (D) (\frac{r}{R})$
14		elpmi	$⊢ f \in (X ↑_{𝑝𝑚} ℂ) \to (f : dom f ⟶ X \land dom f \subseteq ℂ)$
15	14	simpld	$⊢ f \in (X ↑_{𝑝𝑚} ℂ) \to f : dom f ⟶ X$
16	15	ad3antlr	$⊢ (((φ \land f \in (X ↑_{𝑝𝑚} ℂ)) \land r \in ℝ^{+}) \land (k \in ℤ \land ({f ↾}_{ℤ_{\geq k}}) : ℤ_{\geq k} ⟶ f (k) ball (D) (\frac{r}{R}))) \to f : dom f ⟶ X$
17		resss	$⊢ {f ↾}_{ℤ_{\geq k}} \subseteq f$
18		dmss	$⊢ {f ↾}_{ℤ_{\geq k}} \subseteq f \to dom ({f ↾}_{ℤ_{\geq k}}) \subseteq dom f$
19	17 18	ax-mp	$⊢ dom ({f ↾}_{ℤ_{\geq k}}) \subseteq dom f$
20		uzid	$⊢ k \in ℤ \to k \in ℤ_{\geq k}$
21	20	ad2antrl	$⊢ (((φ \land f \in (X ↑_{𝑝𝑚} ℂ)) \land r \in ℝ^{+}) \land (k \in ℤ \land ({f ↾}_{ℤ_{\geq k}}) : ℤ_{\geq k} ⟶ f (k) ball (D) (\frac{r}{R}))) \to k \in ℤ_{\geq k}$
22		fdm	$⊢ ({f ↾}_{ℤ_{\geq k}}) : ℤ_{\geq k} ⟶ f (k) ball (D) (\frac{r}{R}) \to dom ({f ↾}_{ℤ_{\geq k}}) = ℤ_{\geq k}$
23	22	ad2antll	$⊢ (((φ \land f \in (X ↑_{𝑝𝑚} ℂ)) \land r \in ℝ^{+}) \land (k \in ℤ \land ({f ↾}_{ℤ_{\geq k}}) : ℤ_{\geq k} ⟶ f (k) ball (D) (\frac{r}{R}))) \to dom ({f ↾}_{ℤ_{\geq k}}) = ℤ_{\geq k}$
24	21 23	eleqtrrd	$⊢ (((φ \land f \in (X ↑_{𝑝𝑚} ℂ)) \land r \in ℝ^{+}) \land (k \in ℤ \land ({f ↾}_{ℤ_{\geq k}}) : ℤ_{\geq k} ⟶ f (k) ball (D) (\frac{r}{R}))) \to k \in dom ({f ↾}_{ℤ_{\geq k}})$
25	19 24	sseldi	$⊢ (((φ \land f \in (X ↑_{𝑝𝑚} ℂ)) \land r \in ℝ^{+}) \land (k \in ℤ \land ({f ↾}_{ℤ_{\geq k}}) : ℤ_{\geq k} ⟶ f (k) ball (D) (\frac{r}{R}))) \to k \in dom f$
26	16 25	ffvelrnd	$⊢ (((φ \land f \in (X ↑_{𝑝𝑚} ℂ)) \land r \in ℝ^{+}) \land (k \in ℤ \land ({f ↾}_{ℤ_{\geq k}}) : ℤ_{\geq k} ⟶ f (k) ball (D) (\frac{r}{R}))) \to f (k) \in X$
27		eqid	$⊢ MetOpen (C) = MetOpen (C)$
28		eqid	$⊢ MetOpen (D) = MetOpen (D)$
29	27 28 1 2 3 4	metss2lem	$⊢ (φ \land (x \in X \land r \in ℝ^{+})) \to x ball (D) (\frac{r}{R}) \subseteq x ball (C) r$
30	29	expr	$⊢ (φ \land x \in X) \to (r \in ℝ^{+} \to x ball (D) (\frac{r}{R}) \subseteq x ball (C) r)$
31	30	ralrimiva	$⊢ φ \to \forall x \in X (r \in ℝ^{+} \to x ball (D) (\frac{r}{R}) \subseteq x ball (C) r)$
32	31	ad3antrrr	$⊢ (((φ \land f \in (X ↑_{𝑝𝑚} ℂ)) \land r \in ℝ^{+}) \land (k \in ℤ \land ({f ↾}_{ℤ_{\geq k}}) : ℤ_{\geq k} ⟶ f (k) ball (D) (\frac{r}{R}))) \to \forall x \in X (r \in ℝ^{+} \to x ball (D) (\frac{r}{R}) \subseteq x ball (C) r)$
33		simplr	$⊢ (((φ \land f \in (X ↑_{𝑝𝑚} ℂ)) \land r \in ℝ^{+}) \land (k \in ℤ \land ({f ↾}_{ℤ_{\geq k}}) : ℤ_{\geq k} ⟶ f (k) ball (D) (\frac{r}{R}))) \to r \in ℝ^{+}$
34		oveq1	$⊢ x = f (k) \to x ball (D) (\frac{r}{R}) = f (k) ball (D) (\frac{r}{R})$
35		oveq1	$⊢ x = f (k) \to x ball (C) r = f (k) ball (C) r$
36	34 35	sseq12d	$⊢ x = f (k) \to (x ball (D) (\frac{r}{R}) \subseteq x ball (C) r \leftrightarrow f (k) ball (D) (\frac{r}{R}) \subseteq f (k) ball (C) r)$
37	36	imbi2d	$⊢ x = f (k) \to ((r \in ℝ^{+} \to x ball (D) (\frac{r}{R}) \subseteq x ball (C) r) \leftrightarrow (r \in ℝ^{+} \to f (k) ball (D) (\frac{r}{R}) \subseteq f (k) ball (C) r))$
38	37	rspcv	$⊢ f (k) \in X \to (\forall x \in X (r \in ℝ^{+} \to x ball (D) (\frac{r}{R}) \subseteq x ball (C) r) \to (r \in ℝ^{+} \to f (k) ball (D) (\frac{r}{R}) \subseteq f (k) ball (C) r))$
39	26 32 33 38	syl3c	$⊢ (((φ \land f \in (X ↑_{𝑝𝑚} ℂ)) \land r \in ℝ^{+}) \land (k \in ℤ \land ({f ↾}_{ℤ_{\geq k}}) : ℤ_{\geq k} ⟶ f (k) ball (D) (\frac{r}{R}))) \to f (k) ball (D) (\frac{r}{R}) \subseteq f (k) ball (C) r$
40	13 39	fssd	$⊢ (((φ \land f \in (X ↑_{𝑝𝑚} ℂ)) \land r \in ℝ^{+}) \land (k \in ℤ \land ({f ↾}_{ℤ_{\geq k}}) : ℤ_{\geq k} ⟶ f (k) ball (D) (\frac{r}{R}))) \to ({f ↾}_{ℤ_{\geq k}}) : ℤ_{\geq k} ⟶ f (k) ball (C) r$
41	40	expr	$⊢ (((φ \land f \in (X ↑_{𝑝𝑚} ℂ)) \land r \in ℝ^{+}) \land k \in ℤ) \to (({f ↾}_{ℤ_{\geq k}}) : ℤ_{\geq k} ⟶ f (k) ball (D) (\frac{r}{R}) \to ({f ↾}_{ℤ_{\geq k}}) : ℤ_{\geq k} ⟶ f (k) ball (C) r)$
42	41	reximdva	$⊢ ((φ \land f \in (X ↑_{𝑝𝑚} ℂ)) \land r \in ℝ^{+}) \to (\exists k \in ℤ ({f ↾}_{ℤ_{\geq k}}) : ℤ_{\geq k} ⟶ f (k) ball (D) (\frac{r}{R}) \to \exists k \in ℤ ({f ↾}_{ℤ_{\geq k}}) : ℤ_{\geq k} ⟶ f (k) ball (C) r)$
43	12 42	syld	$⊢ ((φ \land f \in (X ↑_{𝑝𝑚} ℂ)) \land r \in ℝ^{+}) \to (\forall s \in ℝ^{+} \exists k \in ℤ ({f ↾}_{ℤ_{\geq k}}) : ℤ_{\geq k} ⟶ f (k) ball (D) s \to \exists k \in ℤ ({f ↾}_{ℤ_{\geq k}}) : ℤ_{\geq k} ⟶ f (k) ball (C) r)$
44	43	ralrimdva	$⊢ (φ \land f \in (X ↑_{𝑝𝑚} ℂ)) \to (\forall s \in ℝ^{+} \exists k \in ℤ ({f ↾}_{ℤ_{\geq k}}) : ℤ_{\geq k} ⟶ f (k) ball (D) s \to \forall r \in ℝ^{+} \exists k \in ℤ ({f ↾}_{ℤ_{\geq k}}) : ℤ_{\geq k} ⟶ f (k) ball (C) r)$
45	44	ss2rabdv	$⊢ φ \to \{f \in (X ↑_{𝑝𝑚} ℂ) \| \forall s \in ℝ^{+} \exists k \in ℤ ({f ↾}_{ℤ_{\geq k}}) : ℤ_{\geq k} ⟶ f (k) ball (D) s\} \subseteq \{f \in (X ↑_{𝑝𝑚} ℂ) \| \forall r \in ℝ^{+} \exists k \in ℤ ({f ↾}_{ℤ_{\geq k}}) : ℤ_{\geq k} ⟶ f (k) ball (C) r\}$
46		metxmet	$⊢ D \in Met (X) \to D \in ∞Met (X)$
47		caufval	$⊢ D \in ∞Met (X) \to Cau (D) = \{f \in (X ↑_{𝑝𝑚} ℂ) \| \forall s \in ℝ^{+} \exists k \in ℤ ({f ↾}_{ℤ_{\geq k}}) : ℤ_{\geq k} ⟶ f (k) ball (D) s\}$
48	2 46 47	3syl	$⊢ φ \to Cau (D) = \{f \in (X ↑_{𝑝𝑚} ℂ) \| \forall s \in ℝ^{+} \exists k \in ℤ ({f ↾}_{ℤ_{\geq k}}) : ℤ_{\geq k} ⟶ f (k) ball (D) s\}$
49		metxmet	$⊢ C \in Met (X) \to C \in ∞Met (X)$
50		caufval	$⊢ C \in ∞Met (X) \to Cau (C) = \{f \in (X ↑_{𝑝𝑚} ℂ) \| \forall r \in ℝ^{+} \exists k \in ℤ ({f ↾}_{ℤ_{\geq k}}) : ℤ_{\geq k} ⟶ f (k) ball (C) r\}$
51	1 49 50	3syl	$⊢ φ \to Cau (C) = \{f \in (X ↑_{𝑝𝑚} ℂ) \| \forall r \in ℝ^{+} \exists k \in ℤ ({f ↾}_{ℤ_{\geq k}}) : ℤ_{\geq k} ⟶ f (k) ball (C) r\}$
52	45 48 51	3sstr4d	$⊢ φ \to Cau (D) \subseteq Cau (C)$

Metamath Proof Explorer

Theorem equivcau

Proof