stdbdmet

Description: The standard bounded metric is a proper metric given an extended metric and a positive real cutoff. (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	stdbdmet	$⊢ (C \in ∞Met (X) \land R \in ℝ^{+}) \to D \in Met (X)$

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		rpxr	$⊢ R \in ℝ^{+} \to R \in ℝ^{*}$
3		rpgt0	$⊢ R \in ℝ^{+} \to 0 < R$
4	2 3	jca	$⊢ R \in ℝ^{+} \to (R \in ℝ^{*} \land 0 < R)$
5	1	stdbdxmet	$⊢ (C \in ∞Met (X) \land R \in ℝ^{*} \land 0 < R) \to D \in ∞Met (X)$
6	5	3expb	$⊢ (C \in ∞Met (X) \land (R \in ℝ^{*} \land 0 < R)) \to D \in ∞Met (X)$
7	4 6	sylan2	$⊢ (C \in ∞Met (X) \land R \in ℝ^{+}) \to D \in ∞Met (X)$
8		xmetcl	$⊢ (C \in ∞Met (X) \land x \in X \land y \in X) \to x C y \in ℝ^{*}$
9	8	3expb	$⊢ (C \in ∞Met (X) \land (x \in X \land y \in X)) \to x C y \in ℝ^{*}$
10	9	adantlr	$⊢ ((C \in ∞Met (X) \land R \in ℝ^{+}) \land (x \in X \land y \in X)) \to x C y \in ℝ^{*}$
11	2	ad2antlr	$⊢ ((C \in ∞Met (X) \land R \in ℝ^{+}) \land (x \in X \land y \in X)) \to R \in ℝ^{*}$
12	10 11	ifcld	$⊢ ((C \in ∞Met (X) \land R \in ℝ^{+}) \land (x \in X \land y \in X)) \to if (x C y \leq R, x C y, R) \in ℝ^{*}$
13		rpre	$⊢ R \in ℝ^{+} \to R \in ℝ$
14	13	ad2antlr	$⊢ ((C \in ∞Met (X) \land R \in ℝ^{+}) \land (x \in X \land y \in X)) \to R \in ℝ$
15		xmetge0	$⊢ (C \in ∞Met (X) \land x \in X \land y \in X) \to 0 \leq x C y$
16	15	3expb	$⊢ (C \in ∞Met (X) \land (x \in X \land y \in X)) \to 0 \leq x C y$
17	16	adantlr	$⊢ ((C \in ∞Met (X) \land R \in ℝ^{+}) \land (x \in X \land y \in X)) \to 0 \leq x C y$
18		rpge0	$⊢ R \in ℝ^{+} \to 0 \leq R$
19	18	ad2antlr	$⊢ ((C \in ∞Met (X) \land R \in ℝ^{+}) \land (x \in X \land y \in X)) \to 0 \leq R$
20		breq2	$⊢ x C y = if (x C y \leq R, x C y, R) \to (0 \leq x C y \leftrightarrow 0 \leq if (x C y \leq R, x C y, R))$
21		breq2	$⊢ R = if (x C y \leq R, x C y, R) \to (0 \leq R \leftrightarrow 0 \leq if (x C y \leq R, x C y, R))$
22	20 21	ifboth	$⊢ (0 \leq x C y \land 0 \leq R) \to 0 \leq if (x C y \leq R, x C y, R)$
23	17 19 22	syl2anc	$⊢ ((C \in ∞Met (X) \land R \in ℝ^{+}) \land (x \in X \land y \in X)) \to 0 \leq if (x C y \leq R, x C y, R)$
24		xrmin2	$⊢ (x C y \in ℝ^{} \land R \in ℝ^{}) \to if (x C y \leq R, x C y, R) \leq R$
25	10 11 24	syl2anc	$⊢ ((C \in ∞Met (X) \land R \in ℝ^{+}) \land (x \in X \land y \in X)) \to if (x C y \leq R, x C y, R) \leq R$
26		xrrege0	$⊢ ((if (x C y \leq R, x C y, R) \in ℝ^{*} \land R \in ℝ) \land (0 \leq if (x C y \leq R, x C y, R) \land if (x C y \leq R, x C y, R) \leq R)) \to if (x C y \leq R, x C y, R) \in ℝ$
27	12 14 23 25 26	syl22anc	$⊢ ((C \in ∞Met (X) \land R \in ℝ^{+}) \land (x \in X \land y \in X)) \to if (x C y \leq R, x C y, R) \in ℝ$
28	27	ralrimivva	$⊢ (C \in ∞Met (X) \land R \in ℝ^{+}) \to \forall x \in X \forall y \in X if (x C y \leq R, x C y, R) \in ℝ$
29	1	fmpo	$⊢ \forall x \in X \forall y \in X if (x C y \leq R, x C y, R) \in ℝ \leftrightarrow D : X \times X ⟶ ℝ$
30	28 29	sylib	$⊢ (C \in ∞Met (X) \land R \in ℝ^{+}) \to D : X \times X ⟶ ℝ$
31		ismet2	$⊢ D \in Met (X) \leftrightarrow (D \in ∞Met (X) \land D : X \times X ⟶ ℝ)$
32	7 30 31	sylanbrc	$⊢ (C \in ∞Met (X) \land R \in ℝ^{+}) \to D \in Met (X)$

Metamath Proof Explorer

Theorem stdbdmet

Proof