stdbdmopn

Description: The standard bounded metric corresponding to C generates the same topology as C . (Contributed by Mario Carneiro, 26-Aug-2015)

	Ref	Expression
Hypotheses	stdbdmet.1	$⊢ D = (x \in X, y \in X ⟼ if (x C y \leq R, x C y, R))$
	stdbdmopn.2	$⊢ J = MetOpen (C)$
Assertion	stdbdmopn	$⊢ (C \in ∞Met (X) \land R \in ℝ^{*} \land 0 < R) \to J = MetOpen (D)$

Proof

Step	Hyp	Ref	Expression
1		stdbdmet.1	$⊢ D = (x \in X, y \in X ⟼ if (x C y \leq R, x C y, R))$
2		stdbdmopn.2	$⊢ J = MetOpen (C)$
3		rpxr	$⊢ r \in ℝ^{+} \to r \in ℝ^{*}$
4	3	ad2antll	$⊢ ((C \in ∞Met (X) \land R \in ℝ^{} \land 0 < R) \land (z \in X \land r \in ℝ^{+})) \to r \in ℝ^{}$
5		simpl2	$⊢ ((C \in ∞Met (X) \land R \in ℝ^{} \land 0 < R) \land (z \in X \land r \in ℝ^{+})) \to R \in ℝ^{}$
6	4 5	ifcld	$⊢ ((C \in ∞Met (X) \land R \in ℝ^{} \land 0 < R) \land (z \in X \land r \in ℝ^{+})) \to if (r \leq R, r, R) \in ℝ^{}$
7		rpre	$⊢ r \in ℝ^{+} \to r \in ℝ$
8	7	ad2antll	$⊢ ((C \in ∞Met (X) \land R \in ℝ^{*} \land 0 < R) \land (z \in X \land r \in ℝ^{+})) \to r \in ℝ$
9		rpgt0	$⊢ r \in ℝ^{+} \to 0 < r$
10	9	ad2antll	$⊢ ((C \in ∞Met (X) \land R \in ℝ^{*} \land 0 < R) \land (z \in X \land r \in ℝ^{+})) \to 0 < r$
11		simpl3	$⊢ ((C \in ∞Met (X) \land R \in ℝ^{*} \land 0 < R) \land (z \in X \land r \in ℝ^{+})) \to 0 < R$
12		breq2	$⊢ r = if (r \leq R, r, R) \to (0 < r \leftrightarrow 0 < if (r \leq R, r, R))$
13		breq2	$⊢ R = if (r \leq R, r, R) \to (0 < R \leftrightarrow 0 < if (r \leq R, r, R))$
14	12 13	ifboth	$⊢ (0 < r \land 0 < R) \to 0 < if (r \leq R, r, R)$
15	10 11 14	syl2anc	$⊢ ((C \in ∞Met (X) \land R \in ℝ^{*} \land 0 < R) \land (z \in X \land r \in ℝ^{+})) \to 0 < if (r \leq R, r, R)$
16		0xr	$⊢ 0 \in ℝ^{*}$
17		xrltle	$⊢ (0 \in ℝ^{} \land if (r \leq R, r, R) \in ℝ^{}) \to (0 < if (r \leq R, r, R) \to 0 \leq if (r \leq R, r, R))$
18	16 6 17	sylancr	$⊢ ((C \in ∞Met (X) \land R \in ℝ^{*} \land 0 < R) \land (z \in X \land r \in ℝ^{+})) \to (0 < if (r \leq R, r, R) \to 0 \leq if (r \leq R, r, R))$
19	15 18	mpd	$⊢ ((C \in ∞Met (X) \land R \in ℝ^{*} \land 0 < R) \land (z \in X \land r \in ℝ^{+})) \to 0 \leq if (r \leq R, r, R)$
20		xrmin1	$⊢ (r \in ℝ^{} \land R \in ℝ^{}) \to if (r \leq R, r, R) \leq r$
21	4 5 20	syl2anc	$⊢ ((C \in ∞Met (X) \land R \in ℝ^{*} \land 0 < R) \land (z \in X \land r \in ℝ^{+})) \to if (r \leq R, r, R) \leq r$
22		xrrege0	$⊢ ((if (r \leq R, r, R) \in ℝ^{*} \land r \in ℝ) \land (0 \leq if (r \leq R, r, R) \land if (r \leq R, r, R) \leq r)) \to if (r \leq R, r, R) \in ℝ$
23	6 8 19 21 22	syl22anc	$⊢ ((C \in ∞Met (X) \land R \in ℝ^{*} \land 0 < R) \land (z \in X \land r \in ℝ^{+})) \to if (r \leq R, r, R) \in ℝ$
24	23 15	elrpd	$⊢ ((C \in ∞Met (X) \land R \in ℝ^{*} \land 0 < R) \land (z \in X \land r \in ℝ^{+})) \to if (r \leq R, r, R) \in ℝ^{+}$
25		simprl	$⊢ ((C \in ∞Met (X) \land R \in ℝ^{*} \land 0 < R) \land (z \in X \land r \in ℝ^{+})) \to z \in X$
26		xrmin2	$⊢ (r \in ℝ^{} \land R \in ℝ^{}) \to if (r \leq R, r, R) \leq R$
27	4 5 26	syl2anc	$⊢ ((C \in ∞Met (X) \land R \in ℝ^{*} \land 0 < R) \land (z \in X \land r \in ℝ^{+})) \to if (r \leq R, r, R) \leq R$
28	25 6 27	3jca	$⊢ ((C \in ∞Met (X) \land R \in ℝ^{} \land 0 < R) \land (z \in X \land r \in ℝ^{+})) \to (z \in X \land if (r \leq R, r, R) \in ℝ^{} \land if (r \leq R, r, R) \leq R)$
29	1	stdbdbl	$⊢ ((C \in ∞Met (X) \land R \in ℝ^{} \land 0 < R) \land (z \in X \land if (r \leq R, r, R) \in ℝ^{} \land if (r \leq R, r, R) \leq R)) \to z ball (D) if (r \leq R, r, R) = z ball (C) if (r \leq R, r, R)$
30	28 29	syldan	$⊢ ((C \in ∞Met (X) \land R \in ℝ^{*} \land 0 < R) \land (z \in X \land r \in ℝ^{+})) \to z ball (D) if (r \leq R, r, R) = z ball (C) if (r \leq R, r, R)$
31	30	eqcomd	$⊢ ((C \in ∞Met (X) \land R \in ℝ^{*} \land 0 < R) \land (z \in X \land r \in ℝ^{+})) \to z ball (C) if (r \leq R, r, R) = z ball (D) if (r \leq R, r, R)$
32		breq1	$⊢ s = if (r \leq R, r, R) \to (s \leq r \leftrightarrow if (r \leq R, r, R) \leq r)$
33		oveq2	$⊢ s = if (r \leq R, r, R) \to z ball (C) s = z ball (C) if (r \leq R, r, R)$
34		oveq2	$⊢ s = if (r \leq R, r, R) \to z ball (D) s = z ball (D) if (r \leq R, r, R)$
35	33 34	eqeq12d	$⊢ s = if (r \leq R, r, R) \to (z ball (C) s = z ball (D) s \leftrightarrow z ball (C) if (r \leq R, r, R) = z ball (D) if (r \leq R, r, R))$
36	32 35	anbi12d	$⊢ s = if (r \leq R, r, R) \to ((s \leq r \land z ball (C) s = z ball (D) s) \leftrightarrow (if (r \leq R, r, R) \leq r \land z ball (C) if (r \leq R, r, R) = z ball (D) if (r \leq R, r, R)))$
37	36	rspcev	$⊢ (if (r \leq R, r, R) \in ℝ^{+} \land (if (r \leq R, r, R) \leq r \land z ball (C) if (r \leq R, r, R) = z ball (D) if (r \leq R, r, R))) \to \exists s \in ℝ^{+} (s \leq r \land z ball (C) s = z ball (D) s)$
38	24 21 31 37	syl12anc	$⊢ ((C \in ∞Met (X) \land R \in ℝ^{*} \land 0 < R) \land (z \in X \land r \in ℝ^{+})) \to \exists s \in ℝ^{+} (s \leq r \land z ball (C) s = z ball (D) s)$
39	38	ralrimivva	$⊢ (C \in ∞Met (X) \land R \in ℝ^{*} \land 0 < R) \to \forall z \in X \forall r \in ℝ^{+} \exists s \in ℝ^{+} (s \leq r \land z ball (C) s = z ball (D) s)$
40		simp1	$⊢ (C \in ∞Met (X) \land R \in ℝ^{*} \land 0 < R) \to C \in ∞Met (X)$
41	1	stdbdxmet	$⊢ (C \in ∞Met (X) \land R \in ℝ^{*} \land 0 < R) \to D \in ∞Met (X)$
42		eqid	$⊢ MetOpen (D) = MetOpen (D)$
43	2 42	metequiv2	$⊢ (C \in ∞Met (X) \land D \in ∞Met (X)) \to (\forall z \in X \forall r \in ℝ^{+} \exists s \in ℝ^{+} (s \leq r \land z ball (C) s = z ball (D) s) \to J = MetOpen (D))$
44	40 41 43	syl2anc	$⊢ (C \in ∞Met (X) \land R \in ℝ^{*} \land 0 < R) \to (\forall z \in X \forall r \in ℝ^{+} \exists s \in ℝ^{+} (s \leq r \land z ball (C) s = z ball (D) s) \to J = MetOpen (D))$
45	39 44	mpd	$⊢ (C \in ∞Met (X) \land R \in ℝ^{*} \land 0 < R) \to J = MetOpen (D)$

Metamath Proof Explorer

Theorem stdbdmopn

Proof