metss2

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 ) ), then D generates a finer topology. (Using this theorem twice in each direction states that if two metrics are strongly equivalent, then they generate the same topology.) (Contributed by Mario Carneiro, 14-Sep-2015)

	Ref	Expression
Hypotheses	metequiv.3	$⊢ J = MetOpen (C)$
	metequiv.4	$⊢ K = MetOpen (D)$
	metss2.1	$⊢ φ \to C \in Met (X)$
	metss2.2	$⊢ φ \to D \in Met (X)$
	metss2.3	$⊢ φ \to R \in ℝ^{+}$
	metss2.4	$⊢ (φ \land (x \in X \land y \in X)) \to x C y \leq R (x D y)$
Assertion	metss2	$⊢ φ \to J \subseteq K$

Proof

Step	Hyp	Ref	Expression
1		metequiv.3	$⊢ J = MetOpen (C)$
2		metequiv.4	$⊢ K = MetOpen (D)$
3		metss2.1	$⊢ φ \to C \in Met (X)$
4		metss2.2	$⊢ φ \to D \in Met (X)$
5		metss2.3	$⊢ φ \to R \in ℝ^{+}$
6		metss2.4	$⊢ (φ \land (x \in X \land y \in X)) \to x C y \leq R (x D y)$
7		simpr	$⊢ (x \in X \land r \in ℝ^{+}) \to r \in ℝ^{+}$
8		rpdivcl	$⊢ (r \in ℝ^{+} \land R \in ℝ^{+}) \to \frac{r}{R} \in ℝ^{+}$
9	7 5 8	syl2anr	$⊢ (φ \land (x \in X \land r \in ℝ^{+})) \to \frac{r}{R} \in ℝ^{+}$
10	1 2 3 4 5 6	metss2lem	$⊢ (φ \land (x \in X \land r \in ℝ^{+})) \to x ball (D) (\frac{r}{R}) \subseteq x ball (C) r$
11		oveq2	$⊢ s = \frac{r}{R} \to x ball (D) s = x ball (D) (\frac{r}{R})$
12	11	sseq1d	$⊢ s = \frac{r}{R} \to (x ball (D) s \subseteq x ball (C) r \leftrightarrow x ball (D) (\frac{r}{R}) \subseteq x ball (C) r)$
13	12	rspcev	$⊢ (\frac{r}{R} \in ℝ^{+} \land x ball (D) (\frac{r}{R}) \subseteq x ball (C) r) \to \exists s \in ℝ^{+} x ball (D) s \subseteq x ball (C) r$
14	9 10 13	syl2anc	$⊢ (φ \land (x \in X \land r \in ℝ^{+})) \to \exists s \in ℝ^{+} x ball (D) s \subseteq x ball (C) r$
15	14	ralrimivva	$⊢ φ \to \forall x \in X \forall r \in ℝ^{+} \exists s \in ℝ^{+} x ball (D) s \subseteq x ball (C) r$
16		metxmet	$⊢ C \in Met (X) \to C \in ∞Met (X)$
17	3 16	syl	$⊢ φ \to C \in ∞Met (X)$
18		metxmet	$⊢ D \in Met (X) \to D \in ∞Met (X)$
19	4 18	syl	$⊢ φ \to D \in ∞Met (X)$
20	1 2	metss	$⊢ (C \in ∞Met (X) \land D \in ∞Met (X)) \to (J \subseteq K \leftrightarrow \forall x \in X \forall r \in ℝ^{+} \exists s \in ℝ^{+} x ball (D) s \subseteq x ball (C) r)$
21	17 19 20	syl2anc	$⊢ φ \to (J \subseteq K \leftrightarrow \forall x \in X \forall r \in ℝ^{+} \exists s \in ℝ^{+} x ball (D) s \subseteq x ball (C) r)$
22	15 21	mpbird	$⊢ φ \to J \subseteq K$

Metamath Proof Explorer

Theorem metss2

Proof