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 
|- D = ( x e. X , y e. X |-> if ( ( x C y ) <_ R , ( x C y ) , R ) )
Assertion stdbdmet 
|- ( ( C e. ( *Met ` X ) /\ R e. RR+ ) -> D e. ( Met ` X ) )

Proof

Step Hyp Ref Expression
1 stdbdmet.1 
 |-  D = ( x e. X , y e. X |-> if ( ( x C y ) <_ R , ( x C y ) , R ) )
2 rpxr 
 |-  ( R e. RR+ -> R e. RR* )
3 rpgt0 
 |-  ( R e. RR+ -> 0 < R )
4 2 3 jca 
 |-  ( R e. RR+ -> ( R e. RR* /\ 0 < R ) )
5 1 stdbdxmet 
 |-  ( ( C e. ( *Met ` X ) /\ R e. RR* /\ 0 < R ) -> D e. ( *Met ` X ) )
6 5 3expb 
 |-  ( ( C e. ( *Met ` X ) /\ ( R e. RR* /\ 0 < R ) ) -> D e. ( *Met ` X ) )
7 4 6 sylan2 
 |-  ( ( C e. ( *Met ` X ) /\ R e. RR+ ) -> D e. ( *Met ` X ) )
8 xmetcl 
 |-  ( ( C e. ( *Met ` X ) /\ x e. X /\ y e. X ) -> ( x C y ) e. RR* )
9 8 3expb 
 |-  ( ( C e. ( *Met ` X ) /\ ( x e. X /\ y e. X ) ) -> ( x C y ) e. RR* )
10 9 adantlr 
 |-  ( ( ( C e. ( *Met ` X ) /\ R e. RR+ ) /\ ( x e. X /\ y e. X ) ) -> ( x C y ) e. RR* )
11 2 ad2antlr 
 |-  ( ( ( C e. ( *Met ` X ) /\ R e. RR+ ) /\ ( x e. X /\ y e. X ) ) -> R e. RR* )
12 10 11 ifcld 
 |-  ( ( ( C e. ( *Met ` X ) /\ R e. RR+ ) /\ ( x e. X /\ y e. X ) ) -> if ( ( x C y ) <_ R , ( x C y ) , R ) e. RR* )
13 rpre 
 |-  ( R e. RR+ -> R e. RR )
14 13 ad2antlr 
 |-  ( ( ( C e. ( *Met ` X ) /\ R e. RR+ ) /\ ( x e. X /\ y e. X ) ) -> R e. RR )
15 xmetge0 
 |-  ( ( C e. ( *Met ` X ) /\ x e. X /\ y e. X ) -> 0 <_ ( x C y ) )
16 15 3expb 
 |-  ( ( C e. ( *Met ` X ) /\ ( x e. X /\ y e. X ) ) -> 0 <_ ( x C y ) )
17 16 adantlr 
 |-  ( ( ( C e. ( *Met ` X ) /\ R e. RR+ ) /\ ( x e. X /\ y e. X ) ) -> 0 <_ ( x C y ) )
18 rpge0 
 |-  ( R e. RR+ -> 0 <_ R )
19 18 ad2antlr 
 |-  ( ( ( C e. ( *Met ` X ) /\ R e. RR+ ) /\ ( x e. X /\ y e. X ) ) -> 0 <_ R )
20 breq2 
 |-  ( ( x C y ) = if ( ( x C y ) <_ R , ( x C y ) , R ) -> ( 0 <_ ( x C y ) <-> 0 <_ if ( ( x C y ) <_ R , ( x C y ) , R ) ) )
21 breq2 
 |-  ( R = if ( ( x C y ) <_ R , ( x C y ) , R ) -> ( 0 <_ R <-> 0 <_ if ( ( x C y ) <_ R , ( x C y ) , R ) ) )
22 20 21 ifboth 
 |-  ( ( 0 <_ ( x C y ) /\ 0 <_ R ) -> 0 <_ if ( ( x C y ) <_ R , ( x C y ) , R ) )
23 17 19 22 syl2anc 
 |-  ( ( ( C e. ( *Met ` X ) /\ R e. RR+ ) /\ ( x e. X /\ y e. X ) ) -> 0 <_ if ( ( x C y ) <_ R , ( x C y ) , R ) )
24 xrmin2 
 |-  ( ( ( x C y ) e. RR* /\ R e. RR* ) -> if ( ( x C y ) <_ R , ( x C y ) , R ) <_ R )
25 10 11 24 syl2anc 
 |-  ( ( ( C e. ( *Met ` X ) /\ R e. RR+ ) /\ ( x e. X /\ y e. X ) ) -> if ( ( x C y ) <_ R , ( x C y ) , R ) <_ R )
26 xrrege0 
 |-  ( ( ( if ( ( x C y ) <_ R , ( x C y ) , R ) e. RR* /\ R e. RR ) /\ ( 0 <_ if ( ( x C y ) <_ R , ( x C y ) , R ) /\ if ( ( x C y ) <_ R , ( x C y ) , R ) <_ R ) ) -> if ( ( x C y ) <_ R , ( x C y ) , R ) e. RR )
27 12 14 23 25 26 syl22anc 
 |-  ( ( ( C e. ( *Met ` X ) /\ R e. RR+ ) /\ ( x e. X /\ y e. X ) ) -> if ( ( x C y ) <_ R , ( x C y ) , R ) e. RR )
28 27 ralrimivva 
 |-  ( ( C e. ( *Met ` X ) /\ R e. RR+ ) -> A. x e. X A. y e. X if ( ( x C y ) <_ R , ( x C y ) , R ) e. RR )
29 1 fmpo 
 |-  ( A. x e. X A. y e. X if ( ( x C y ) <_ R , ( x C y ) , R ) e. RR <-> D : ( X X. X ) --> RR )
30 28 29 sylib 
 |-  ( ( C e. ( *Met ` X ) /\ R e. RR+ ) -> D : ( X X. X ) --> RR )
31 ismet2 
 |-  ( D e. ( Met ` X ) <-> ( D e. ( *Met ` X ) /\ D : ( X X. X ) --> RR ) )
32 7 30 31 sylanbrc 
 |-  ( ( C e. ( *Met ` X ) /\ R e. RR+ ) -> D e. ( Met ` X ) )