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=xX,yXifxCyRxCyR
Assertion stdbdmet C∞MetXR+DMetX

Proof

Step Hyp Ref Expression
1 stdbdmet.1 D=xX,yXifxCyRxCyR
2 rpxr R+R*
3 rpgt0 R+0<R
4 2 3 jca R+R*0<R
5 1 stdbdxmet C∞MetXR*0<RD∞MetX
6 5 3expb C∞MetXR*0<RD∞MetX
7 4 6 sylan2 C∞MetXR+D∞MetX
8 xmetcl C∞MetXxXyXxCy*
9 8 3expb C∞MetXxXyXxCy*
10 9 adantlr C∞MetXR+xXyXxCy*
11 2 ad2antlr C∞MetXR+xXyXR*
12 10 11 ifcld C∞MetXR+xXyXifxCyRxCyR*
13 rpre R+R
14 13 ad2antlr C∞MetXR+xXyXR
15 xmetge0 C∞MetXxXyX0xCy
16 15 3expb C∞MetXxXyX0xCy
17 16 adantlr C∞MetXR+xXyX0xCy
18 rpge0 R+0R
19 18 ad2antlr C∞MetXR+xXyX0R
20 breq2 xCy=ifxCyRxCyR0xCy0ifxCyRxCyR
21 breq2 R=ifxCyRxCyR0R0ifxCyRxCyR
22 20 21 ifboth 0xCy0R0ifxCyRxCyR
23 17 19 22 syl2anc C∞MetXR+xXyX0ifxCyRxCyR
24 xrmin2 xCy*R*ifxCyRxCyRR
25 10 11 24 syl2anc C∞MetXR+xXyXifxCyRxCyRR
26 xrrege0 ifxCyRxCyR*R0ifxCyRxCyRifxCyRxCyRRifxCyRxCyR
27 12 14 23 25 26 syl22anc C∞MetXR+xXyXifxCyRxCyR
28 27 ralrimivva C∞MetXR+xXyXifxCyRxCyR
29 1 fmpo xXyXifxCyRxCyRD:X×X
30 28 29 sylib C∞MetXR+D:X×X
31 ismet2 DMetXD∞MetXD:X×X
32 7 30 31 sylanbrc C∞MetXR+DMetX