This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem 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 ‘ 𝑋 ) )