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

Metamath Proof Explorer

Theorem xmetresbl

Description: An extended metric restricted to any ball (in particular the infinity ball) is a proper metric. Together with xmetec , this shows that any extended metric space can be "factored" into the disjoint union of proper metric spaces, with points in the same region measured by that region's metric, and points in different regions being distance +oo from each other. (Contributed by Mario Carneiro, 23-Aug-2015)

Ref Expression
Hypothesis xmetresbl.1 
|- B = ( P ( ball ` D ) R )
Assertion xmetresbl 
|- ( ( D e. ( *Met ` X ) /\ P e. X /\ R e. RR* ) -> ( D |` ( B X. B ) ) e. ( Met ` B ) )

Proof

Step Hyp Ref Expression
1 xmetresbl.1 
 |-  B = ( P ( ball ` D ) R )
2 simp1 
 |-  ( ( D e. ( *Met ` X ) /\ P e. X /\ R e. RR* ) -> D e. ( *Met ` X ) )
3 blssm 
 |-  ( ( D e. ( *Met ` X ) /\ P e. X /\ R e. RR* ) -> ( P ( ball ` D ) R ) C_ X )
4 1 3 eqsstrid 
 |-  ( ( D e. ( *Met ` X ) /\ P e. X /\ R e. RR* ) -> B C_ X )
5 xmetres2 
 |-  ( ( D e. ( *Met ` X ) /\ B C_ X ) -> ( D |` ( B X. B ) ) e. ( *Met ` B ) )
6 2 4 5 syl2anc 
 |-  ( ( D e. ( *Met ` X ) /\ P e. X /\ R e. RR* ) -> ( D |` ( B X. B ) ) e. ( *Met ` B ) )
7 xmetf 
 |-  ( D e. ( *Met ` X ) -> D : ( X X. X ) --> RR* )
8 2 7 syl 
 |-  ( ( D e. ( *Met ` X ) /\ P e. X /\ R e. RR* ) -> D : ( X X. X ) --> RR* )
9 xpss12 
 |-  ( ( B C_ X /\ B C_ X ) -> ( B X. B ) C_ ( X X. X ) )
10 4 4 9 syl2anc 
 |-  ( ( D e. ( *Met ` X ) /\ P e. X /\ R e. RR* ) -> ( B X. B ) C_ ( X X. X ) )
11 8 10 fssresd 
 |-  ( ( D e. ( *Met ` X ) /\ P e. X /\ R e. RR* ) -> ( D |` ( B X. B ) ) : ( B X. B ) --> RR* )
12 11 ffnd 
 |-  ( ( D e. ( *Met ` X ) /\ P e. X /\ R e. RR* ) -> ( D |` ( B X. B ) ) Fn ( B X. B ) )
13 ovres 
 |-  ( ( x e. B /\ y e. B ) -> ( x ( D |` ( B X. B ) ) y ) = ( x D y ) )
14 13 adantl 
 |-  ( ( ( D e. ( *Met ` X ) /\ P e. X /\ R e. RR* ) /\ ( x e. B /\ y e. B ) ) -> ( x ( D |` ( B X. B ) ) y ) = ( x D y ) )
15 simpl1 
 |-  ( ( ( D e. ( *Met ` X ) /\ P e. X /\ R e. RR* ) /\ ( x e. B /\ y e. B ) ) -> D e. ( *Met ` X ) )
16 eqid 
 |-  ( `' D " RR ) = ( `' D " RR )
17 16 xmeter 
 |-  ( D e. ( *Met ` X ) -> ( `' D " RR ) Er X )
18 15 17 syl 
 |-  ( ( ( D e. ( *Met ` X ) /\ P e. X /\ R e. RR* ) /\ ( x e. B /\ y e. B ) ) -> ( `' D " RR ) Er X )
19 16 blssec 
 |-  ( ( D e. ( *Met ` X ) /\ P e. X /\ R e. RR* ) -> ( P ( ball ` D ) R ) C_ [ P ] ( `' D " RR ) )
20 1 19 eqsstrid 
 |-  ( ( D e. ( *Met ` X ) /\ P e. X /\ R e. RR* ) -> B C_ [ P ] ( `' D " RR ) )
21 20 sselda 
 |-  ( ( ( D e. ( *Met ` X ) /\ P e. X /\ R e. RR* ) /\ x e. B ) -> x e. [ P ] ( `' D " RR ) )
22 21 adantrr 
 |-  ( ( ( D e. ( *Met ` X ) /\ P e. X /\ R e. RR* ) /\ ( x e. B /\ y e. B ) ) -> x e. [ P ] ( `' D " RR ) )
23 simpl2 
 |-  ( ( ( D e. ( *Met ` X ) /\ P e. X /\ R e. RR* ) /\ ( x e. B /\ y e. B ) ) -> P e. X )
24 elecg 
 |-  ( ( x e. [ P ] ( `' D " RR ) /\ P e. X ) -> ( x e. [ P ] ( `' D " RR ) <-> P ( `' D " RR ) x ) )
25 22 23 24 syl2anc 
 |-  ( ( ( D e. ( *Met ` X ) /\ P e. X /\ R e. RR* ) /\ ( x e. B /\ y e. B ) ) -> ( x e. [ P ] ( `' D " RR ) <-> P ( `' D " RR ) x ) )
26 22 25 mpbid 
 |-  ( ( ( D e. ( *Met ` X ) /\ P e. X /\ R e. RR* ) /\ ( x e. B /\ y e. B ) ) -> P ( `' D " RR ) x )
27 20 sselda 
 |-  ( ( ( D e. ( *Met ` X ) /\ P e. X /\ R e. RR* ) /\ y e. B ) -> y e. [ P ] ( `' D " RR ) )
28 27 adantrl 
 |-  ( ( ( D e. ( *Met ` X ) /\ P e. X /\ R e. RR* ) /\ ( x e. B /\ y e. B ) ) -> y e. [ P ] ( `' D " RR ) )
29 elecg 
 |-  ( ( y e. [ P ] ( `' D " RR ) /\ P e. X ) -> ( y e. [ P ] ( `' D " RR ) <-> P ( `' D " RR ) y ) )
30 28 23 29 syl2anc 
 |-  ( ( ( D e. ( *Met ` X ) /\ P e. X /\ R e. RR* ) /\ ( x e. B /\ y e. B ) ) -> ( y e. [ P ] ( `' D " RR ) <-> P ( `' D " RR ) y ) )
31 28 30 mpbid 
 |-  ( ( ( D e. ( *Met ` X ) /\ P e. X /\ R e. RR* ) /\ ( x e. B /\ y e. B ) ) -> P ( `' D " RR ) y )
32 18 26 31 ertr3d 
 |-  ( ( ( D e. ( *Met ` X ) /\ P e. X /\ R e. RR* ) /\ ( x e. B /\ y e. B ) ) -> x ( `' D " RR ) y )
33 16 xmeterval 
 |-  ( D e. ( *Met ` X ) -> ( x ( `' D " RR ) y <-> ( x e. X /\ y e. X /\ ( x D y ) e. RR ) ) )
34 15 33 syl 
 |-  ( ( ( D e. ( *Met ` X ) /\ P e. X /\ R e. RR* ) /\ ( x e. B /\ y e. B ) ) -> ( x ( `' D " RR ) y <-> ( x e. X /\ y e. X /\ ( x D y ) e. RR ) ) )
35 32 34 mpbid 
 |-  ( ( ( D e. ( *Met ` X ) /\ P e. X /\ R e. RR* ) /\ ( x e. B /\ y e. B ) ) -> ( x e. X /\ y e. X /\ ( x D y ) e. RR ) )
36 35 simp3d 
 |-  ( ( ( D e. ( *Met ` X ) /\ P e. X /\ R e. RR* ) /\ ( x e. B /\ y e. B ) ) -> ( x D y ) e. RR )
37 14 36 eqeltrd 
 |-  ( ( ( D e. ( *Met ` X ) /\ P e. X /\ R e. RR* ) /\ ( x e. B /\ y e. B ) ) -> ( x ( D |` ( B X. B ) ) y ) e. RR )
38 37 ralrimivva 
 |-  ( ( D e. ( *Met ` X ) /\ P e. X /\ R e. RR* ) -> A. x e. B A. y e. B ( x ( D |` ( B X. B ) ) y ) e. RR )
39 ffnov 
 |-  ( ( D |` ( B X. B ) ) : ( B X. B ) --> RR <-> ( ( D |` ( B X. B ) ) Fn ( B X. B ) /\ A. x e. B A. y e. B ( x ( D |` ( B X. B ) ) y ) e. RR ) )
40 12 38 39 sylanbrc 
 |-  ( ( D e. ( *Met ` X ) /\ P e. X /\ R e. RR* ) -> ( D |` ( B X. B ) ) : ( B X. B ) --> RR )
41 ismet2 
 |-  ( ( D |` ( B X. B ) ) e. ( Met ` B ) <-> ( ( D |` ( B X. B ) ) e. ( *Met ` B ) /\ ( D |` ( B X. B ) ) : ( B X. B ) --> RR ) )
42 6 40 41 sylanbrc 
 |-  ( ( D e. ( *Met ` X ) /\ P e. X /\ R e. RR* ) -> ( D |` ( B X. B ) ) e. ( Met ` B ) )