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	⊢ 𝐷 = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑋 ↦ if ( ( 𝑥 𝐶 𝑦 ) ≤ 𝑅 , ( 𝑥 𝐶 𝑦 ) , 𝑅 ) )
	Assertion	stdbdmet	⊢ ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑅 ∈ ℝ⁺ ) → 𝐷 ∈ ( Met ‘ 𝑋 ) )

Proof

Step	Hyp	Ref	Expression
1		stdbdmet.1	⊢ 𝐷 = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑋 ↦ if ( ( 𝑥 𝐶 𝑦 ) ≤ 𝑅 , ( 𝑥 𝐶 𝑦 ) , 𝑅 ) )
2		rpxr	⊢ ( 𝑅 ∈ ℝ⁺ → 𝑅 ∈ ℝ^* )
3		rpgt0	⊢ ( 𝑅 ∈ ℝ⁺ → 0 < 𝑅 )
4	2 3	jca	⊢ ( 𝑅 ∈ ℝ⁺ → ( 𝑅 ∈ ℝ^* ∧ 0 < 𝑅 ) )
5	1	stdbdxmet	⊢ ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑅 ∈ ℝ^* ∧ 0 < 𝑅 ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
6	5	3expb	⊢ ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝑅 ∈ ℝ^* ∧ 0 < 𝑅 ) ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
7	4 6	sylan2	⊢ ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑅 ∈ ℝ⁺ ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
8		xmetcl	⊢ ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( 𝑥 𝐶 𝑦 ) ∈ ℝ^* )
9	8	3expb	⊢ ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( 𝑥 𝐶 𝑦 ) ∈ ℝ^* )
10	9	adantlr	⊢ ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑅 ∈ ℝ⁺ ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( 𝑥 𝐶 𝑦 ) ∈ ℝ^* )
11	2	ad2antlr	⊢ ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑅 ∈ ℝ⁺ ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → 𝑅 ∈ ℝ^* )
12	10 11	ifcld	⊢ ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑅 ∈ ℝ⁺ ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → if ( ( 𝑥 𝐶 𝑦 ) ≤ 𝑅 , ( 𝑥 𝐶 𝑦 ) , 𝑅 ) ∈ ℝ^* )
13		rpre	⊢ ( 𝑅 ∈ ℝ⁺ → 𝑅 ∈ ℝ )
14	13	ad2antlr	⊢ ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑅 ∈ ℝ⁺ ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → 𝑅 ∈ ℝ )
15		xmetge0	⊢ ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → 0 ≤ ( 𝑥 𝐶 𝑦 ) )
16	15	3expb	⊢ ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → 0 ≤ ( 𝑥 𝐶 𝑦 ) )
17	16	adantlr	⊢ ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑅 ∈ ℝ⁺ ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → 0 ≤ ( 𝑥 𝐶 𝑦 ) )
18		rpge0	⊢ ( 𝑅 ∈ ℝ⁺ → 0 ≤ 𝑅 )
19	18	ad2antlr	⊢ ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑅 ∈ ℝ⁺ ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → 0 ≤ 𝑅 )
20		breq2	⊢ ( ( 𝑥 𝐶 𝑦 ) = if ( ( 𝑥 𝐶 𝑦 ) ≤ 𝑅 , ( 𝑥 𝐶 𝑦 ) , 𝑅 ) → ( 0 ≤ ( 𝑥 𝐶 𝑦 ) ↔ 0 ≤ if ( ( 𝑥 𝐶 𝑦 ) ≤ 𝑅 , ( 𝑥 𝐶 𝑦 ) , 𝑅 ) ) )
21		breq2	⊢ ( 𝑅 = if ( ( 𝑥 𝐶 𝑦 ) ≤ 𝑅 , ( 𝑥 𝐶 𝑦 ) , 𝑅 ) → ( 0 ≤ 𝑅 ↔ 0 ≤ if ( ( 𝑥 𝐶 𝑦 ) ≤ 𝑅 , ( 𝑥 𝐶 𝑦 ) , 𝑅 ) ) )
22	20 21	ifboth	⊢ ( ( 0 ≤ ( 𝑥 𝐶 𝑦 ) ∧ 0 ≤ 𝑅 ) → 0 ≤ if ( ( 𝑥 𝐶 𝑦 ) ≤ 𝑅 , ( 𝑥 𝐶 𝑦 ) , 𝑅 ) )
23	17 19 22	syl2anc	⊢ ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑅 ∈ ℝ⁺ ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → 0 ≤ if ( ( 𝑥 𝐶 𝑦 ) ≤ 𝑅 , ( 𝑥 𝐶 𝑦 ) , 𝑅 ) )
24		xrmin2	⊢ ( ( ( 𝑥 𝐶 𝑦 ) ∈ ℝ^* ∧ 𝑅 ∈ ℝ^* ) → if ( ( 𝑥 𝐶 𝑦 ) ≤ 𝑅 , ( 𝑥 𝐶 𝑦 ) , 𝑅 ) ≤ 𝑅 )
25	10 11 24	syl2anc	⊢ ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑅 ∈ ℝ⁺ ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → if ( ( 𝑥 𝐶 𝑦 ) ≤ 𝑅 , ( 𝑥 𝐶 𝑦 ) , 𝑅 ) ≤ 𝑅 )
26		xrrege0	⊢ ( ( ( if ( ( 𝑥 𝐶 𝑦 ) ≤ 𝑅 , ( 𝑥 𝐶 𝑦 ) , 𝑅 ) ∈ ℝ^* ∧ 𝑅 ∈ ℝ ) ∧ ( 0 ≤ if ( ( 𝑥 𝐶 𝑦 ) ≤ 𝑅 , ( 𝑥 𝐶 𝑦 ) , 𝑅 ) ∧ if ( ( 𝑥 𝐶 𝑦 ) ≤ 𝑅 , ( 𝑥 𝐶 𝑦 ) , 𝑅 ) ≤ 𝑅 ) ) → if ( ( 𝑥 𝐶 𝑦 ) ≤ 𝑅 , ( 𝑥 𝐶 𝑦 ) , 𝑅 ) ∈ ℝ )
27	12 14 23 25 26	syl22anc	⊢ ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑅 ∈ ℝ⁺ ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → if ( ( 𝑥 𝐶 𝑦 ) ≤ 𝑅 , ( 𝑥 𝐶 𝑦 ) , 𝑅 ) ∈ ℝ )
28	27	ralrimivva	⊢ ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑅 ∈ ℝ⁺ ) → ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 if ( ( 𝑥 𝐶 𝑦 ) ≤ 𝑅 , ( 𝑥 𝐶 𝑦 ) , 𝑅 ) ∈ ℝ )
29	1	fmpo	⊢ ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 if ( ( 𝑥 𝐶 𝑦 ) ≤ 𝑅 , ( 𝑥 𝐶 𝑦 ) , 𝑅 ) ∈ ℝ ↔ 𝐷 : ( 𝑋 × 𝑋 ) ⟶ ℝ )
30	28 29	sylib	⊢ ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑅 ∈ ℝ⁺ ) → 𝐷 : ( 𝑋 × 𝑋 ) ⟶ ℝ )
31		ismet2	⊢ ( 𝐷 ∈ ( Met ‘ 𝑋 ) ↔ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 : ( 𝑋 × 𝑋 ) ⟶ ℝ ) )
32	7 30 31	sylanbrc	⊢ ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑅 ∈ ℝ⁺ ) → 𝐷 ∈ ( Met ‘ 𝑋 ) )

Metamath Proof Explorer

Theorem stdbdmet

Proof