Metamath Proof Explorer

Theorem blpnfctr

Description: The infinity ball in an extended metric acts like an ultrametric ball in that every point in the ball is also its center. (Contributed by Mario Carneiro, 21-Aug-2015)

Ref Expression
Assertion blpnfctr 
|- ( ( D e. ( *Met ` X ) /\ P e. X /\ A e. ( P ( ball ` D ) +oo ) ) -> ( P ( ball ` D ) +oo ) = ( A ( ball ` D ) +oo ) )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( `' D " RR ) = ( `' D " RR )
2 1 xmeter 
 |-  ( D e. ( *Met ` X ) -> ( `' D " RR ) Er X )
3 2 3ad2ant1 
 |-  ( ( D e. ( *Met ` X ) /\ P e. X /\ A e. ( P ( ball ` D ) +oo ) ) -> ( `' D " RR ) Er X )
4 simp3 
 |-  ( ( D e. ( *Met ` X ) /\ P e. X /\ A e. ( P ( ball ` D ) +oo ) ) -> A e. ( P ( ball ` D ) +oo ) )
5 1 xmetec 
 |-  ( ( D e. ( *Met ` X ) /\ P e. X ) -> [ P ] ( `' D " RR ) = ( P ( ball ` D ) +oo ) )
6 5 3adant3 
 |-  ( ( D e. ( *Met ` X ) /\ P e. X /\ A e. ( P ( ball ` D ) +oo ) ) -> [ P ] ( `' D " RR ) = ( P ( ball ` D ) +oo ) )
7 4 6 eleqtrrd 
 |-  ( ( D e. ( *Met ` X ) /\ P e. X /\ A e. ( P ( ball ` D ) +oo ) ) -> A e. [ P ] ( `' D " RR ) )
8 elecg 
 |-  ( ( A e. ( P ( ball ` D ) +oo ) /\ P e. X ) -> ( A e. [ P ] ( `' D " RR ) <-> P ( `' D " RR ) A ) )
9 8 ancoms 
 |-  ( ( P e. X /\ A e. ( P ( ball ` D ) +oo ) ) -> ( A e. [ P ] ( `' D " RR ) <-> P ( `' D " RR ) A ) )
10 9 3adant1 
 |-  ( ( D e. ( *Met ` X ) /\ P e. X /\ A e. ( P ( ball ` D ) +oo ) ) -> ( A e. [ P ] ( `' D " RR ) <-> P ( `' D " RR ) A ) )
11 7 10 mpbid 
 |-  ( ( D e. ( *Met ` X ) /\ P e. X /\ A e. ( P ( ball ` D ) +oo ) ) -> P ( `' D " RR ) A )
12 3 11 erthi 
 |-  ( ( D e. ( *Met ` X ) /\ P e. X /\ A e. ( P ( ball ` D ) +oo ) ) -> [ P ] ( `' D " RR ) = [ A ] ( `' D " RR ) )
13 pnfxr 
 |-  +oo e. RR*
14 blssm 
 |-  ( ( D e. ( *Met ` X ) /\ P e. X /\ +oo e. RR* ) -> ( P ( ball ` D ) +oo ) C_ X )
15 13 14 mp3an3 
 |-  ( ( D e. ( *Met ` X ) /\ P e. X ) -> ( P ( ball ` D ) +oo ) C_ X )
16 15 sselda 
 |-  ( ( ( D e. ( *Met ` X ) /\ P e. X ) /\ A e. ( P ( ball ` D ) +oo ) ) -> A e. X )
17 1 xmetec 
 |-  ( ( D e. ( *Met ` X ) /\ A e. X ) -> [ A ] ( `' D " RR ) = ( A ( ball ` D ) +oo ) )
18 17 adantlr 
 |-  ( ( ( D e. ( *Met ` X ) /\ P e. X ) /\ A e. X ) -> [ A ] ( `' D " RR ) = ( A ( ball ` D ) +oo ) )
19 16 18 syldan 
 |-  ( ( ( D e. ( *Met ` X ) /\ P e. X ) /\ A e. ( P ( ball ` D ) +oo ) ) -> [ A ] ( `' D " RR ) = ( A ( ball ` D ) +oo ) )
20 19 3impa 
 |-  ( ( D e. ( *Met ` X ) /\ P e. X /\ A e. ( P ( ball ` D ) +oo ) ) -> [ A ] ( `' D " RR ) = ( A ( ball ` D ) +oo ) )
21 12 6 20 3eqtr3d 
 |-  ( ( D e. ( *Met ` X ) /\ P e. X /\ A e. ( P ( ball ` D ) +oo ) ) -> ( P ( ball ` D ) +oo ) = ( A ( ball ` D ) +oo ) )