Metamath Proof Explorer

Theorem metdcnlem

Description: The metric function of a metric space is always continuous in the topology generated by it. (Contributed by Mario Carneiro, 5-May-2014) (Revised by Mario Carneiro, 4-Sep-2015)

Ref Expression
Hypotheses xmetdcn2.1 
|- J = ( MetOpen ` D )
xmetdcn2.2 
|- C = ( dist ` RR*s )
xmetdcn2.3 
|- K = ( MetOpen ` C )
metdcn.d 
|- ( ph -> D e. ( *Met ` X ) )
metdcn.a 
|- ( ph -> A e. X )
metdcn.b 
|- ( ph -> B e. X )
metdcn.r 
|- ( ph -> R e. RR+ )
metdcn.y 
|- ( ph -> Y e. X )
metdcn.z 
|- ( ph -> Z e. X )
metdcn.4 
|- ( ph -> ( A D Y ) < ( R / 2 ) )
metdcn.5 
|- ( ph -> ( B D Z ) < ( R / 2 ) )
Assertion metdcnlem 
|- ( ph -> ( ( A D B ) C ( Y D Z ) ) < R )

Proof

Step Hyp Ref Expression
1 xmetdcn2.1 
 |-  J = ( MetOpen ` D )
2 xmetdcn2.2 
 |-  C = ( dist ` RR*s )
3 xmetdcn2.3 
 |-  K = ( MetOpen ` C )
4 metdcn.d 
 |-  ( ph -> D e. ( *Met ` X ) )
5 metdcn.a 
 |-  ( ph -> A e. X )
6 metdcn.b 
 |-  ( ph -> B e. X )
7 metdcn.r 
 |-  ( ph -> R e. RR+ )
8 metdcn.y 
 |-  ( ph -> Y e. X )
9 metdcn.z 
 |-  ( ph -> Z e. X )
10 metdcn.4 
 |-  ( ph -> ( A D Y ) < ( R / 2 ) )
11 metdcn.5 
 |-  ( ph -> ( B D Z ) < ( R / 2 ) )
12 2 xrsxmet 
 |-  C e. ( *Met ` RR* )
13 12 a1i 
 |-  ( ph -> C e. ( *Met ` RR* ) )
14 xmetcl 
 |-  ( ( D e. ( *Met ` X ) /\ A e. X /\ B e. X ) -> ( A D B ) e. RR* )
15 4 5 6 14 syl3anc 
 |-  ( ph -> ( A D B ) e. RR* )
16 xmetcl 
 |-  ( ( D e. ( *Met ` X ) /\ Y e. X /\ Z e. X ) -> ( Y D Z ) e. RR* )
17 4 8 9 16 syl3anc 
 |-  ( ph -> ( Y D Z ) e. RR* )
18 xmetcl 
 |-  ( ( D e. ( *Met ` X ) /\ Y e. X /\ B e. X ) -> ( Y D B ) e. RR* )
19 4 8 6 18 syl3anc 
 |-  ( ph -> ( Y D B ) e. RR* )
20 7 rphalfcld 
 |-  ( ph -> ( R / 2 ) e. RR+ )
21 20 rpred 
 |-  ( ph -> ( R / 2 ) e. RR )
22 xmetcl 
 |-  ( ( C e. ( *Met ` RR* ) /\ ( A D B ) e. RR* /\ ( Y D B ) e. RR* ) -> ( ( A D B ) C ( Y D B ) ) e. RR* )
23 13 15 19 22 syl3anc 
 |-  ( ph -> ( ( A D B ) C ( Y D B ) ) e. RR* )
24 20 rpxrd 
 |-  ( ph -> ( R / 2 ) e. RR* )
25 xmetcl 
 |-  ( ( D e. ( *Met ` X ) /\ A e. X /\ Y e. X ) -> ( A D Y ) e. RR* )
26 4 5 8 25 syl3anc 
 |-  ( ph -> ( A D Y ) e. RR* )
27 2 xmetrtri2 
 |-  ( ( D e. ( *Met ` X ) /\ ( A e. X /\ Y e. X /\ B e. X ) ) -> ( ( A D B ) C ( Y D B ) ) <_ ( A D Y ) )
28 4 5 8 6 27 syl13anc 
 |-  ( ph -> ( ( A D B ) C ( Y D B ) ) <_ ( A D Y ) )
29 23 26 24 28 10 xrlelttrd 
 |-  ( ph -> ( ( A D B ) C ( Y D B ) ) < ( R / 2 ) )
30 23 24 29 xrltled 
 |-  ( ph -> ( ( A D B ) C ( Y D B ) ) <_ ( R / 2 ) )
31 xmetlecl 
 |-  ( ( C e. ( *Met ` RR* ) /\ ( ( A D B ) e. RR* /\ ( Y D B ) e. RR* ) /\ ( ( R / 2 ) e. RR /\ ( ( A D B ) C ( Y D B ) ) <_ ( R / 2 ) ) ) -> ( ( A D B ) C ( Y D B ) ) e. RR )
32 13 15 19 21 30 31 syl122anc 
 |-  ( ph -> ( ( A D B ) C ( Y D B ) ) e. RR )
33 xmetcl 
 |-  ( ( C e. ( *Met ` RR* ) /\ ( Y D B ) e. RR* /\ ( Y D Z ) e. RR* ) -> ( ( Y D B ) C ( Y D Z ) ) e. RR* )
34 13 19 17 33 syl3anc 
 |-  ( ph -> ( ( Y D B ) C ( Y D Z ) ) e. RR* )
35 xmetcl 
 |-  ( ( D e. ( *Met ` X ) /\ B e. X /\ Z e. X ) -> ( B D Z ) e. RR* )
36 4 6 9 35 syl3anc 
 |-  ( ph -> ( B D Z ) e. RR* )
37 xmetsym 
 |-  ( ( D e. ( *Met ` X ) /\ Y e. X /\ B e. X ) -> ( Y D B ) = ( B D Y ) )
38 4 8 6 37 syl3anc 
 |-  ( ph -> ( Y D B ) = ( B D Y ) )
39 xmetsym 
 |-  ( ( D e. ( *Met ` X ) /\ Y e. X /\ Z e. X ) -> ( Y D Z ) = ( Z D Y ) )
40 4 8 9 39 syl3anc 
 |-  ( ph -> ( Y D Z ) = ( Z D Y ) )
41 38 40 oveq12d 
 |-  ( ph -> ( ( Y D B ) C ( Y D Z ) ) = ( ( B D Y ) C ( Z D Y ) ) )
42 2 xmetrtri2 
 |-  ( ( D e. ( *Met ` X ) /\ ( B e. X /\ Z e. X /\ Y e. X ) ) -> ( ( B D Y ) C ( Z D Y ) ) <_ ( B D Z ) )
43 4 6 9 8 42 syl13anc 
 |-  ( ph -> ( ( B D Y ) C ( Z D Y ) ) <_ ( B D Z ) )
44 41 43 eqbrtrd 
 |-  ( ph -> ( ( Y D B ) C ( Y D Z ) ) <_ ( B D Z ) )
45 34 36 24 44 11 xrlelttrd 
 |-  ( ph -> ( ( Y D B ) C ( Y D Z ) ) < ( R / 2 ) )
46 34 24 45 xrltled 
 |-  ( ph -> ( ( Y D B ) C ( Y D Z ) ) <_ ( R / 2 ) )
47 xmetlecl 
 |-  ( ( C e. ( *Met ` RR* ) /\ ( ( Y D B ) e. RR* /\ ( Y D Z ) e. RR* ) /\ ( ( R / 2 ) e. RR /\ ( ( Y D B ) C ( Y D Z ) ) <_ ( R / 2 ) ) ) -> ( ( Y D B ) C ( Y D Z ) ) e. RR )
48 13 19 17 21 46 47 syl122anc 
 |-  ( ph -> ( ( Y D B ) C ( Y D Z ) ) e. RR )
49 32 48 readdcld 
 |-  ( ph -> ( ( ( A D B ) C ( Y D B ) ) + ( ( Y D B ) C ( Y D Z ) ) ) e. RR )
50 xmettri 
 |-  ( ( C e. ( *Met ` RR* ) /\ ( ( A D B ) e. RR* /\ ( Y D Z ) e. RR* /\ ( Y D B ) e. RR* ) ) -> ( ( A D B ) C ( Y D Z ) ) <_ ( ( ( A D B ) C ( Y D B ) ) +e ( ( Y D B ) C ( Y D Z ) ) ) )
51 13 15 17 19 50 syl13anc 
 |-  ( ph -> ( ( A D B ) C ( Y D Z ) ) <_ ( ( ( A D B ) C ( Y D B ) ) +e ( ( Y D B ) C ( Y D Z ) ) ) )
52 32 48 rexaddd 
 |-  ( ph -> ( ( ( A D B ) C ( Y D B ) ) +e ( ( Y D B ) C ( Y D Z ) ) ) = ( ( ( A D B ) C ( Y D B ) ) + ( ( Y D B ) C ( Y D Z ) ) ) )
53 51 52 breqtrd 
 |-  ( ph -> ( ( A D B ) C ( Y D Z ) ) <_ ( ( ( A D B ) C ( Y D B ) ) + ( ( Y D B ) C ( Y D Z ) ) ) )
54 xmetlecl 
 |-  ( ( C e. ( *Met ` RR* ) /\ ( ( A D B ) e. RR* /\ ( Y D Z ) e. RR* ) /\ ( ( ( ( A D B ) C ( Y D B ) ) + ( ( Y D B ) C ( Y D Z ) ) ) e. RR /\ ( ( A D B ) C ( Y D Z ) ) <_ ( ( ( A D B ) C ( Y D B ) ) + ( ( Y D B ) C ( Y D Z ) ) ) ) ) -> ( ( A D B ) C ( Y D Z ) ) e. RR )
55 13 15 17 49 53 54 syl122anc 
 |-  ( ph -> ( ( A D B ) C ( Y D Z ) ) e. RR )
56 7 rpred 
 |-  ( ph -> R e. RR )
57 32 48 56 29 45 lt2halvesd 
 |-  ( ph -> ( ( ( A D B ) C ( Y D B ) ) + ( ( Y D B ) C ( Y D Z ) ) ) < R )
58 55 49 56 53 57 lelttrd 
 |-  ( ph -> ( ( A D B ) C ( Y D Z ) ) < R )