Metamath Proof Explorer

Theorem cnbl0

Description: Two ways to write the open ball centered at zero. (Contributed by Mario Carneiro, 8-Sep-2015)

Ref Expression
Hypothesis cnblcld.1 
|- D = ( abs o. - )
Assertion cnbl0 
|- ( R e. RR* -> ( `' abs " ( 0 [,) R ) ) = ( 0 ( ball ` D ) R ) )

Proof

Step Hyp Ref Expression
1 cnblcld.1 
 |-  D = ( abs o. - )
2 abscl 
 |-  ( x e. CC -> ( abs ` x ) e. RR )
3 absge0 
 |-  ( x e. CC -> 0 <_ ( abs ` x ) )
4 2 3 jca 
 |-  ( x e. CC -> ( ( abs ` x ) e. RR /\ 0 <_ ( abs ` x ) ) )
5 4 adantl 
 |-  ( ( R e. RR* /\ x e. CC ) -> ( ( abs ` x ) e. RR /\ 0 <_ ( abs ` x ) ) )
6 5 biantrurd 
 |-  ( ( R e. RR* /\ x e. CC ) -> ( ( abs ` x ) < R <-> ( ( ( abs ` x ) e. RR /\ 0 <_ ( abs ` x ) ) /\ ( abs ` x ) < R ) ) )
7 df-3an 
 |-  ( ( ( abs ` x ) e. RR /\ 0 <_ ( abs ` x ) /\ ( abs ` x ) < R ) <-> ( ( ( abs ` x ) e. RR /\ 0 <_ ( abs ` x ) ) /\ ( abs ` x ) < R ) )
8 6 7 syl6rbbr 
 |-  ( ( R e. RR* /\ x e. CC ) -> ( ( ( abs ` x ) e. RR /\ 0 <_ ( abs ` x ) /\ ( abs ` x ) < R ) <-> ( abs ` x ) < R ) )
9 0re 
 |-  0 e. RR
10 simpl 
 |-  ( ( R e. RR* /\ x e. CC ) -> R e. RR* )
11 elico2 
 |-  ( ( 0 e. RR /\ R e. RR* ) -> ( ( abs ` x ) e. ( 0 [,) R ) <-> ( ( abs ` x ) e. RR /\ 0 <_ ( abs ` x ) /\ ( abs ` x ) < R ) ) )
12 9 10 11 sylancr 
 |-  ( ( R e. RR* /\ x e. CC ) -> ( ( abs ` x ) e. ( 0 [,) R ) <-> ( ( abs ` x ) e. RR /\ 0 <_ ( abs ` x ) /\ ( abs ` x ) < R ) ) )
13 0cn 
 |-  0 e. CC
14 1 cnmetdval 
 |-  ( ( 0 e. CC /\ x e. CC ) -> ( 0 D x ) = ( abs ` ( 0 - x ) ) )
15 abssub 
 |-  ( ( 0 e. CC /\ x e. CC ) -> ( abs ` ( 0 - x ) ) = ( abs ` ( x - 0 ) ) )
16 14 15 eqtrd 
 |-  ( ( 0 e. CC /\ x e. CC ) -> ( 0 D x ) = ( abs ` ( x - 0 ) ) )
17 13 16 mpan 
 |-  ( x e. CC -> ( 0 D x ) = ( abs ` ( x - 0 ) ) )
18 subid1 
 |-  ( x e. CC -> ( x - 0 ) = x )
19 18 fveq2d 
 |-  ( x e. CC -> ( abs ` ( x - 0 ) ) = ( abs ` x ) )
20 17 19 eqtrd 
 |-  ( x e. CC -> ( 0 D x ) = ( abs ` x ) )
21 20 adantl 
 |-  ( ( R e. RR* /\ x e. CC ) -> ( 0 D x ) = ( abs ` x ) )
22 21 breq1d 
 |-  ( ( R e. RR* /\ x e. CC ) -> ( ( 0 D x ) < R <-> ( abs ` x ) < R ) )
23 8 12 22 3bitr4d 
 |-  ( ( R e. RR* /\ x e. CC ) -> ( ( abs ` x ) e. ( 0 [,) R ) <-> ( 0 D x ) < R ) )
24 23 pm5.32da 
 |-  ( R e. RR* -> ( ( x e. CC /\ ( abs ` x ) e. ( 0 [,) R ) ) <-> ( x e. CC /\ ( 0 D x ) < R ) ) )
25 absf 
 |-  abs : CC --> RR
26 ffn 
 |-  ( abs : CC --> RR -> abs Fn CC )
27 25 26 ax-mp 
 |-  abs Fn CC
28 elpreima 
 |-  ( abs Fn CC -> ( x e. ( `' abs " ( 0 [,) R ) ) <-> ( x e. CC /\ ( abs ` x ) e. ( 0 [,) R ) ) ) )
29 27 28 mp1i 
 |-  ( R e. RR* -> ( x e. ( `' abs " ( 0 [,) R ) ) <-> ( x e. CC /\ ( abs ` x ) e. ( 0 [,) R ) ) ) )
30 cnxmet 
 |-  ( abs o. - ) e. ( *Met ` CC )
31 1 30 eqeltri 
 |-  D e. ( *Met ` CC )
32 elbl 
 |-  ( ( D e. ( *Met ` CC ) /\ 0 e. CC /\ R e. RR* ) -> ( x e. ( 0 ( ball ` D ) R ) <-> ( x e. CC /\ ( 0 D x ) < R ) ) )
33 31 13 32 mp3an12 
 |-  ( R e. RR* -> ( x e. ( 0 ( ball ` D ) R ) <-> ( x e. CC /\ ( 0 D x ) < R ) ) )
34 24 29 33 3bitr4d 
 |-  ( R e. RR* -> ( x e. ( `' abs " ( 0 [,) R ) ) <-> x e. ( 0 ( ball ` D ) R ) ) )
35 34 eqrdv 
 |-  ( R e. RR* -> ( `' abs " ( 0 [,) R ) ) = ( 0 ( ball ` D ) R ) )