Metamath Proof Explorer

Theorem xmetdcn2

Description: The metric function of an extended metric space is always continuous in the topology generated by it. In this variation of xmetdcn we use the metric topology instead of the order topology on RR* , which makes the theorem a bit stronger. Since +oo is an isolated point in the metric topology, this is saying that for any points A , B which are an infinite distance apart, there is a product neighborhood around <. A , B >. such that d ( a , b ) = +oo for any a near A and b near B , i.e., the distance function is locally constant +oo . (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 )
Assertion xmetdcn2 
|- ( D e. ( *Met ` X ) -> D e. ( ( J tX J ) Cn K ) )

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 xmetf 
 |-  ( D e. ( *Met ` X ) -> D : ( X X. X ) --> RR* )
5 rphalfcl 
 |-  ( r e. RR+ -> ( r / 2 ) e. RR+ )
6 simp-4l 
 |-  ( ( ( ( ( D e. ( *Met ` X ) /\ ( x e. X /\ y e. X ) ) /\ r e. RR+ ) /\ ( z e. X /\ w e. X ) ) /\ ( ( x D z ) < ( r / 2 ) /\ ( y D w ) < ( r / 2 ) ) ) -> D e. ( *Met ` X ) )
7 simplrl 
 |-  ( ( ( D e. ( *Met ` X ) /\ ( x e. X /\ y e. X ) ) /\ r e. RR+ ) -> x e. X )
8 7 ad2antrr 
 |-  ( ( ( ( ( D e. ( *Met ` X ) /\ ( x e. X /\ y e. X ) ) /\ r e. RR+ ) /\ ( z e. X /\ w e. X ) ) /\ ( ( x D z ) < ( r / 2 ) /\ ( y D w ) < ( r / 2 ) ) ) -> x e. X )
9 simplrr 
 |-  ( ( ( D e. ( *Met ` X ) /\ ( x e. X /\ y e. X ) ) /\ r e. RR+ ) -> y e. X )
10 9 ad2antrr 
 |-  ( ( ( ( ( D e. ( *Met ` X ) /\ ( x e. X /\ y e. X ) ) /\ r e. RR+ ) /\ ( z e. X /\ w e. X ) ) /\ ( ( x D z ) < ( r / 2 ) /\ ( y D w ) < ( r / 2 ) ) ) -> y e. X )
11 simpllr 
 |-  ( ( ( ( ( D e. ( *Met ` X ) /\ ( x e. X /\ y e. X ) ) /\ r e. RR+ ) /\ ( z e. X /\ w e. X ) ) /\ ( ( x D z ) < ( r / 2 ) /\ ( y D w ) < ( r / 2 ) ) ) -> r e. RR+ )
12 simplrl 
 |-  ( ( ( ( ( D e. ( *Met ` X ) /\ ( x e. X /\ y e. X ) ) /\ r e. RR+ ) /\ ( z e. X /\ w e. X ) ) /\ ( ( x D z ) < ( r / 2 ) /\ ( y D w ) < ( r / 2 ) ) ) -> z e. X )
13 simplrr 
 |-  ( ( ( ( ( D e. ( *Met ` X ) /\ ( x e. X /\ y e. X ) ) /\ r e. RR+ ) /\ ( z e. X /\ w e. X ) ) /\ ( ( x D z ) < ( r / 2 ) /\ ( y D w ) < ( r / 2 ) ) ) -> w e. X )
14 simprl 
 |-  ( ( ( ( ( D e. ( *Met ` X ) /\ ( x e. X /\ y e. X ) ) /\ r e. RR+ ) /\ ( z e. X /\ w e. X ) ) /\ ( ( x D z ) < ( r / 2 ) /\ ( y D w ) < ( r / 2 ) ) ) -> ( x D z ) < ( r / 2 ) )
15 simprr 
 |-  ( ( ( ( ( D e. ( *Met ` X ) /\ ( x e. X /\ y e. X ) ) /\ r e. RR+ ) /\ ( z e. X /\ w e. X ) ) /\ ( ( x D z ) < ( r / 2 ) /\ ( y D w ) < ( r / 2 ) ) ) -> ( y D w ) < ( r / 2 ) )
16 1 2 3 6 8 10 11 12 13 14 15 metdcnlem 
 |-  ( ( ( ( ( D e. ( *Met ` X ) /\ ( x e. X /\ y e. X ) ) /\ r e. RR+ ) /\ ( z e. X /\ w e. X ) ) /\ ( ( x D z ) < ( r / 2 ) /\ ( y D w ) < ( r / 2 ) ) ) -> ( ( x D y ) C ( z D w ) ) < r )
17 16 ex 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ ( x e. X /\ y e. X ) ) /\ r e. RR+ ) /\ ( z e. X /\ w e. X ) ) -> ( ( ( x D z ) < ( r / 2 ) /\ ( y D w ) < ( r / 2 ) ) -> ( ( x D y ) C ( z D w ) ) < r ) )
18 17 ralrimivva 
 |-  ( ( ( D e. ( *Met ` X ) /\ ( x e. X /\ y e. X ) ) /\ r e. RR+ ) -> A. z e. X A. w e. X ( ( ( x D z ) < ( r / 2 ) /\ ( y D w ) < ( r / 2 ) ) -> ( ( x D y ) C ( z D w ) ) < r ) )
19 breq2 
 |-  ( s = ( r / 2 ) -> ( ( x D z ) < s <-> ( x D z ) < ( r / 2 ) ) )
20 breq2 
 |-  ( s = ( r / 2 ) -> ( ( y D w ) < s <-> ( y D w ) < ( r / 2 ) ) )
21 19 20 anbi12d 
 |-  ( s = ( r / 2 ) -> ( ( ( x D z ) < s /\ ( y D w ) < s ) <-> ( ( x D z ) < ( r / 2 ) /\ ( y D w ) < ( r / 2 ) ) ) )
22 21 imbi1d 
 |-  ( s = ( r / 2 ) -> ( ( ( ( x D z ) < s /\ ( y D w ) < s ) -> ( ( x D y ) C ( z D w ) ) < r ) <-> ( ( ( x D z ) < ( r / 2 ) /\ ( y D w ) < ( r / 2 ) ) -> ( ( x D y ) C ( z D w ) ) < r ) ) )
23 22 2ralbidv 
 |-  ( s = ( r / 2 ) -> ( A. z e. X A. w e. X ( ( ( x D z ) < s /\ ( y D w ) < s ) -> ( ( x D y ) C ( z D w ) ) < r ) <-> A. z e. X A. w e. X ( ( ( x D z ) < ( r / 2 ) /\ ( y D w ) < ( r / 2 ) ) -> ( ( x D y ) C ( z D w ) ) < r ) ) )
24 23 rspcev 
 |-  ( ( ( r / 2 ) e. RR+ /\ A. z e. X A. w e. X ( ( ( x D z ) < ( r / 2 ) /\ ( y D w ) < ( r / 2 ) ) -> ( ( x D y ) C ( z D w ) ) < r ) ) -> E. s e. RR+ A. z e. X A. w e. X ( ( ( x D z ) < s /\ ( y D w ) < s ) -> ( ( x D y ) C ( z D w ) ) < r ) )
25 5 18 24 syl2an2 
 |-  ( ( ( D e. ( *Met ` X ) /\ ( x e. X /\ y e. X ) ) /\ r e. RR+ ) -> E. s e. RR+ A. z e. X A. w e. X ( ( ( x D z ) < s /\ ( y D w ) < s ) -> ( ( x D y ) C ( z D w ) ) < r ) )
26 25 ralrimiva 
 |-  ( ( D e. ( *Met ` X ) /\ ( x e. X /\ y e. X ) ) -> A. r e. RR+ E. s e. RR+ A. z e. X A. w e. X ( ( ( x D z ) < s /\ ( y D w ) < s ) -> ( ( x D y ) C ( z D w ) ) < r ) )
27 26 ralrimivva 
 |-  ( D e. ( *Met ` X ) -> A. x e. X A. y e. X A. r e. RR+ E. s e. RR+ A. z e. X A. w e. X ( ( ( x D z ) < s /\ ( y D w ) < s ) -> ( ( x D y ) C ( z D w ) ) < r ) )
28 id 
 |-  ( D e. ( *Met ` X ) -> D e. ( *Met ` X ) )
29 2 xrsxmet 
 |-  C e. ( *Met ` RR* )
30 29 a1i 
 |-  ( D e. ( *Met ` X ) -> C e. ( *Met ` RR* ) )
31 1 1 3 txmetcn 
 |-  ( ( D e. ( *Met ` X ) /\ D e. ( *Met ` X ) /\ C e. ( *Met ` RR* ) ) -> ( D e. ( ( J tX J ) Cn K ) <-> ( D : ( X X. X ) --> RR* /\ A. x e. X A. y e. X A. r e. RR+ E. s e. RR+ A. z e. X A. w e. X ( ( ( x D z ) < s /\ ( y D w ) < s ) -> ( ( x D y ) C ( z D w ) ) < r ) ) ) )
32 28 30 31 mpd3an23 
 |-  ( D e. ( *Met ` X ) -> ( D e. ( ( J tX J ) Cn K ) <-> ( D : ( X X. X ) --> RR* /\ A. x e. X A. y e. X A. r e. RR+ E. s e. RR+ A. z e. X A. w e. X ( ( ( x D z ) < s /\ ( y D w ) < s ) -> ( ( x D y ) C ( z D w ) ) < r ) ) ) )
33 4 27 32 mpbir2and 
 |-  ( D e. ( *Met ` X ) -> D e. ( ( J tX J ) Cn K ) )