stdbdbl

Description: The standard bounded metric corresponding to C generates the same balls as C for radii less than R . (Contributed by Mario Carneiro, 26-Aug-2015)

		Ref	Expression
	Hypothesis	stdbdmet.1	$⊢ D = (x \in X, y \in X ⟼ if (x C y \leq R, x C y, R))$
	Assertion	stdbdbl	$⊢ ((C \in ∞Met (X) \land R \in ℝ^{} \land 0 < R) \land (P \in X \land S \in ℝ^{} \land S \leq R)) \to P ball (D) S = P ball (C) S$

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		simpll2	$⊢ (((C \in ∞Met (X) \land R \in ℝ^{} \land 0 < R) \land (P \in X \land S \in ℝ^{} \land S \leq R)) \land z \in X) \to R \in ℝ^{*}$
3		simpr1	$⊢ ((C \in ∞Met (X) \land R \in ℝ^{} \land 0 < R) \land (P \in X \land S \in ℝ^{} \land S \leq R)) \to P \in X$
4	3	adantr	$⊢ (((C \in ∞Met (X) \land R \in ℝ^{} \land 0 < R) \land (P \in X \land S \in ℝ^{} \land S \leq R)) \land z \in X) \to P \in X$
5		simpr	$⊢ (((C \in ∞Met (X) \land R \in ℝ^{} \land 0 < R) \land (P \in X \land S \in ℝ^{} \land S \leq R)) \land z \in X) \to z \in X$
6	1	stdbdmetval	$⊢ (R \in ℝ^{*} \land P \in X \land z \in X) \to P D z = if (P C z \leq R, P C z, R)$
7	2 4 5 6	syl3anc	$⊢ (((C \in ∞Met (X) \land R \in ℝ^{} \land 0 < R) \land (P \in X \land S \in ℝ^{} \land S \leq R)) \land z \in X) \to P D z = if (P C z \leq R, P C z, R)$
8	7	breq1d	$⊢ (((C \in ∞Met (X) \land R \in ℝ^{} \land 0 < R) \land (P \in X \land S \in ℝ^{} \land S \leq R)) \land z \in X) \to (P D z < S \leftrightarrow if (P C z \leq R, P C z, R) < S)$
9		simplr3	$⊢ (((C \in ∞Met (X) \land R \in ℝ^{} \land 0 < R) \land (P \in X \land S \in ℝ^{} \land S \leq R)) \land z \in X) \to S \leq R$
10	9	biantrud	$⊢ (((C \in ∞Met (X) \land R \in ℝ^{} \land 0 < R) \land (P \in X \land S \in ℝ^{} \land S \leq R)) \land z \in X) \to (S \leq P C z \leftrightarrow (S \leq P C z \land S \leq R))$
11		simpr2	$⊢ ((C \in ∞Met (X) \land R \in ℝ^{} \land 0 < R) \land (P \in X \land S \in ℝ^{} \land S \leq R)) \to S \in ℝ^{*}$
12	11	adantr	$⊢ (((C \in ∞Met (X) \land R \in ℝ^{} \land 0 < R) \land (P \in X \land S \in ℝ^{} \land S \leq R)) \land z \in X) \to S \in ℝ^{*}$
13		simpl1	$⊢ ((C \in ∞Met (X) \land R \in ℝ^{} \land 0 < R) \land (P \in X \land S \in ℝ^{} \land S \leq R)) \to C \in ∞Met (X)$
14	13	adantr	$⊢ (((C \in ∞Met (X) \land R \in ℝ^{} \land 0 < R) \land (P \in X \land S \in ℝ^{} \land S \leq R)) \land z \in X) \to C \in ∞Met (X)$
15		xmetcl	$⊢ (C \in ∞Met (X) \land P \in X \land z \in X) \to P C z \in ℝ^{*}$
16	14 4 5 15	syl3anc	$⊢ (((C \in ∞Met (X) \land R \in ℝ^{} \land 0 < R) \land (P \in X \land S \in ℝ^{} \land S \leq R)) \land z \in X) \to P C z \in ℝ^{*}$
17		xrlemin	$⊢ (S \in ℝ^{} \land P C z \in ℝ^{} \land R \in ℝ^{*}) \to (S \leq if (P C z \leq R, P C z, R) \leftrightarrow (S \leq P C z \land S \leq R))$
18	12 16 2 17	syl3anc	$⊢ (((C \in ∞Met (X) \land R \in ℝ^{} \land 0 < R) \land (P \in X \land S \in ℝ^{} \land S \leq R)) \land z \in X) \to (S \leq if (P C z \leq R, P C z, R) \leftrightarrow (S \leq P C z \land S \leq R))$
19	10 18	bitr4d	$⊢ (((C \in ∞Met (X) \land R \in ℝ^{} \land 0 < R) \land (P \in X \land S \in ℝ^{} \land S \leq R)) \land z \in X) \to (S \leq P C z \leftrightarrow S \leq if (P C z \leq R, P C z, R))$
20	19	notbid	$⊢ (((C \in ∞Met (X) \land R \in ℝ^{} \land 0 < R) \land (P \in X \land S \in ℝ^{} \land S \leq R)) \land z \in X) \to (\neg S \leq P C z \leftrightarrow \neg S \leq if (P C z \leq R, P C z, R))$
21		xrltnle	$⊢ (P C z \in ℝ^{} \land S \in ℝ^{}) \to (P C z < S \leftrightarrow \neg S \leq P C z)$
22	16 12 21	syl2anc	$⊢ (((C \in ∞Met (X) \land R \in ℝ^{} \land 0 < R) \land (P \in X \land S \in ℝ^{} \land S \leq R)) \land z \in X) \to (P C z < S \leftrightarrow \neg S \leq P C z)$
23	16 2	ifcld	$⊢ (((C \in ∞Met (X) \land R \in ℝ^{} \land 0 < R) \land (P \in X \land S \in ℝ^{} \land S \leq R)) \land z \in X) \to if (P C z \leq R, P C z, R) \in ℝ^{*}$
24		xrltnle	$⊢ (if (P C z \leq R, P C z, R) \in ℝ^{} \land S \in ℝ^{}) \to (if (P C z \leq R, P C z, R) < S \leftrightarrow \neg S \leq if (P C z \leq R, P C z, R))$
25	23 12 24	syl2anc	$⊢ (((C \in ∞Met (X) \land R \in ℝ^{} \land 0 < R) \land (P \in X \land S \in ℝ^{} \land S \leq R)) \land z \in X) \to (if (P C z \leq R, P C z, R) < S \leftrightarrow \neg S \leq if (P C z \leq R, P C z, R))$
26	20 22 25	3bitr4d	$⊢ (((C \in ∞Met (X) \land R \in ℝ^{} \land 0 < R) \land (P \in X \land S \in ℝ^{} \land S \leq R)) \land z \in X) \to (P C z < S \leftrightarrow if (P C z \leq R, P C z, R) < S)$
27	8 26	bitr4d	$⊢ (((C \in ∞Met (X) \land R \in ℝ^{} \land 0 < R) \land (P \in X \land S \in ℝ^{} \land S \leq R)) \land z \in X) \to (P D z < S \leftrightarrow P C z < S)$
28	27	rabbidva	$⊢ ((C \in ∞Met (X) \land R \in ℝ^{} \land 0 < R) \land (P \in X \land S \in ℝ^{} \land S \leq R)) \to \{z \in X \| P D z < S\} = \{z \in X \| P C z < S\}$
29	1	stdbdxmet	$⊢ (C \in ∞Met (X) \land R \in ℝ^{*} \land 0 < R) \to D \in ∞Met (X)$
30	29	adantr	$⊢ ((C \in ∞Met (X) \land R \in ℝ^{} \land 0 < R) \land (P \in X \land S \in ℝ^{} \land S \leq R)) \to D \in ∞Met (X)$
31		blval	$⊢ (D \in ∞Met (X) \land P \in X \land S \in ℝ^{*}) \to P ball (D) S = \{z \in X \| P D z < S\}$
32	30 3 11 31	syl3anc	$⊢ ((C \in ∞Met (X) \land R \in ℝ^{} \land 0 < R) \land (P \in X \land S \in ℝ^{} \land S \leq R)) \to P ball (D) S = \{z \in X \| P D z < S\}$
33		blval	$⊢ (C \in ∞Met (X) \land P \in X \land S \in ℝ^{*}) \to P ball (C) S = \{z \in X \| P C z < S\}$
34	13 3 11 33	syl3anc	$⊢ ((C \in ∞Met (X) \land R \in ℝ^{} \land 0 < R) \land (P \in X \land S \in ℝ^{} \land S \leq R)) \to P ball (C) S = \{z \in X \| P C z < S\}$
35	28 32 34	3eqtr4d	$⊢ ((C \in ∞Met (X) \land R \in ℝ^{} \land 0 < R) \land (P \in X \land S \in ℝ^{} \land S \leq R)) \to P ball (D) S = P ball (C) S$

Metamath Proof Explorer

Theorem stdbdbl

Proof