Metamath Proof Explorer

Theorem sblpnf

Description: The infinity ball in the absolute value metric is just the whole space. S analogue of blpnf . (Contributed by Steve Rodriguez, 8-Nov-2015)

Ref Expression
Hypotheses sblpnf.s 
|- ( ph -> S e. { RR , CC } )
sblpnf.d 
|- D = ( ( abs o. - ) |` ( S X. S ) )
Assertion sblpnf 
|- ( ( ph /\ P e. S ) -> ( P ( ball ` D ) +oo ) = S )

Proof

Step Hyp Ref Expression
1 sblpnf.s 
 |-  ( ph -> S e. { RR , CC } )
2 sblpnf.d 
 |-  D = ( ( abs o. - ) |` ( S X. S ) )
3 elpri 
 |-  ( S e. { RR , CC } -> ( S = RR \/ S = CC ) )
4 eqid 
 |-  ( ( abs o. - ) |` ( RR X. RR ) ) = ( ( abs o. - ) |` ( RR X. RR ) )
5 4 remet 
 |-  ( ( abs o. - ) |` ( RR X. RR ) ) e. ( Met ` RR )
6 xpeq12 
 |-  ( ( S = RR /\ S = RR ) -> ( S X. S ) = ( RR X. RR ) )
7 6 anidms 
 |-  ( S = RR -> ( S X. S ) = ( RR X. RR ) )
8 7 reseq2d 
 |-  ( S = RR -> ( ( abs o. - ) |` ( S X. S ) ) = ( ( abs o. - ) |` ( RR X. RR ) ) )
9 fveq2 
 |-  ( S = RR -> ( Met ` S ) = ( Met ` RR ) )
10 8 9 eleq12d 
 |-  ( S = RR -> ( ( ( abs o. - ) |` ( S X. S ) ) e. ( Met ` S ) <-> ( ( abs o. - ) |` ( RR X. RR ) ) e. ( Met ` RR ) ) )
11 5 10 mpbiri 
 |-  ( S = RR -> ( ( abs o. - ) |` ( S X. S ) ) e. ( Met ` S ) )
12 2 11 eqeltrid 
 |-  ( S = RR -> D e. ( Met ` S ) )
13 relco 
 |-  Rel ( abs o. - )
14 resdm 
 |-  ( Rel ( abs o. - ) -> ( ( abs o. - ) |` dom ( abs o. - ) ) = ( abs o. - ) )
15 13 14 ax-mp 
 |-  ( ( abs o. - ) |` dom ( abs o. - ) ) = ( abs o. - )
16 absf 
 |-  abs : CC --> RR
17 ax-resscn 
 |-  RR C_ CC
18 fss 
 |-  ( ( abs : CC --> RR /\ RR C_ CC ) -> abs : CC --> CC )
19 16 17 18 mp2an 
 |-  abs : CC --> CC
20 subf 
 |-  - : ( CC X. CC ) --> CC
21 fco 
 |-  ( ( abs : CC --> CC /\ - : ( CC X. CC ) --> CC ) -> ( abs o. - ) : ( CC X. CC ) --> CC )
22 19 20 21 mp2an 
 |-  ( abs o. - ) : ( CC X. CC ) --> CC
23 22 fdmi 
 |-  dom ( abs o. - ) = ( CC X. CC )
24 23 reseq2i 
 |-  ( ( abs o. - ) |` dom ( abs o. - ) ) = ( ( abs o. - ) |` ( CC X. CC ) )
25 15 24 eqtr3i 
 |-  ( abs o. - ) = ( ( abs o. - ) |` ( CC X. CC ) )
26 cnmet 
 |-  ( abs o. - ) e. ( Met ` CC )
27 25 26 eqeltrri 
 |-  ( ( abs o. - ) |` ( CC X. CC ) ) e. ( Met ` CC )
28 xpeq12 
 |-  ( ( S = CC /\ S = CC ) -> ( S X. S ) = ( CC X. CC ) )
29 28 anidms 
 |-  ( S = CC -> ( S X. S ) = ( CC X. CC ) )
30 29 reseq2d 
 |-  ( S = CC -> ( ( abs o. - ) |` ( S X. S ) ) = ( ( abs o. - ) |` ( CC X. CC ) ) )
31 fveq2 
 |-  ( S = CC -> ( Met ` S ) = ( Met ` CC ) )
32 30 31 eleq12d 
 |-  ( S = CC -> ( ( ( abs o. - ) |` ( S X. S ) ) e. ( Met ` S ) <-> ( ( abs o. - ) |` ( CC X. CC ) ) e. ( Met ` CC ) ) )
33 27 32 mpbiri 
 |-  ( S = CC -> ( ( abs o. - ) |` ( S X. S ) ) e. ( Met ` S ) )
34 2 33 eqeltrid 
 |-  ( S = CC -> D e. ( Met ` S ) )
35 12 34 jaoi 
 |-  ( ( S = RR \/ S = CC ) -> D e. ( Met ` S ) )
36 1 3 35 3syl 
 |-  ( ph -> D e. ( Met ` S ) )
37 blpnf 
 |-  ( ( D e. ( Met ` S ) /\ P e. S ) -> ( P ( ball ` D ) +oo ) = S )
38 36 37 sylan 
 |-  ( ( ph /\ P e. S ) -> ( P ( ball ` D ) +oo ) = S )