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 df-3an
 |-  ( ( ( abs ` x ) e. RR /\ 0 <_ ( abs ` x ) /\ ( abs ` x ) < R ) <-> ( ( ( abs ` x ) e. RR /\ 0 <_ ( abs ` x ) ) /\ ( abs ` x ) < R ) )
3 abscl
 |-  ( x e. CC -> ( abs ` x ) e. RR )
4 absge0
 |-  ( x e. CC -> 0 <_ ( abs ` x ) )
5 3 4 jca
 |-  ( x e. CC -> ( ( abs ` x ) e. RR /\ 0 <_ ( abs ` x ) ) )
6 5 adantl
 |-  ( ( R e. RR* /\ x e. CC ) -> ( ( abs ` x ) e. RR /\ 0 <_ ( abs ` x ) ) )
7 6 biantrurd
 |-  ( ( R e. RR* /\ x e. CC ) -> ( ( abs ` x ) < R <-> ( ( ( abs ` x ) e. RR /\ 0 <_ ( abs ` x ) ) /\ ( abs ` x ) < R ) ) )
8 2 7 bitr4id
 |-  ( ( 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 ) )