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 ) )