Metamath Proof Explorer

Theorem blval2

Description: The ball around a point P , alternative definition. (Contributed by Thierry Arnoux, 7-Dec-2017) (Revised by Thierry Arnoux, 11-Mar-2018)

Ref Expression
Assertion blval2 
|- ( ( D e. ( PsMet ` X ) /\ P e. X /\ R e. RR+ ) -> ( P ( ball ` D ) R ) = ( ( `' D " ( 0 [,) R ) ) " { P } ) )

Proof

Step Hyp Ref Expression
1 rpxr 
 |-  ( R e. RR+ -> R e. RR* )
2 blvalps 
 |-  ( ( D e. ( PsMet ` X ) /\ P e. X /\ R e. RR* ) -> ( P ( ball ` D ) R ) = { x e. X | ( P D x ) < R } )
3 1 2 syl3an3 
 |-  ( ( D e. ( PsMet ` X ) /\ P e. X /\ R e. RR+ ) -> ( P ( ball ` D ) R ) = { x e. X | ( P D x ) < R } )
4 nfv 
 |-  F/ x ( D e. ( PsMet ` X ) /\ P e. X /\ R e. RR+ )
5 nfcv 
 |-  F/_ x ( ( `' D " ( 0 [,) R ) ) " { P } )
6 nfrab1 
 |-  F/_ x { x e. X | ( P D x ) < R }
7 psmetf 
 |-  ( D e. ( PsMet ` X ) -> D : ( X X. X ) --> RR* )
8 ffn 
 |-  ( D : ( X X. X ) --> RR* -> D Fn ( X X. X ) )
9 elpreima 
 |-  ( D Fn ( X X. X ) -> ( <. P , x >. e. ( `' D " ( 0 [,) R ) ) <-> ( <. P , x >. e. ( X X. X ) /\ ( D ` <. P , x >. ) e. ( 0 [,) R ) ) ) )
10 7 8 9 3syl 
 |-  ( D e. ( PsMet ` X ) -> ( <. P , x >. e. ( `' D " ( 0 [,) R ) ) <-> ( <. P , x >. e. ( X X. X ) /\ ( D ` <. P , x >. ) e. ( 0 [,) R ) ) ) )
11 10 3ad2ant1 
 |-  ( ( D e. ( PsMet ` X ) /\ P e. X /\ R e. RR+ ) -> ( <. P , x >. e. ( `' D " ( 0 [,) R ) ) <-> ( <. P , x >. e. ( X X. X ) /\ ( D ` <. P , x >. ) e. ( 0 [,) R ) ) ) )
12 opelxp 
 |-  ( <. P , x >. e. ( X X. X ) <-> ( P e. X /\ x e. X ) )
13 12 baib 
 |-  ( P e. X -> ( <. P , x >. e. ( X X. X ) <-> x e. X ) )
14 13 3ad2ant2 
 |-  ( ( D e. ( PsMet ` X ) /\ P e. X /\ R e. RR+ ) -> ( <. P , x >. e. ( X X. X ) <-> x e. X ) )
15 14 biimpd 
 |-  ( ( D e. ( PsMet ` X ) /\ P e. X /\ R e. RR+ ) -> ( <. P , x >. e. ( X X. X ) -> x e. X ) )
16 15 adantrd 
 |-  ( ( D e. ( PsMet ` X ) /\ P e. X /\ R e. RR+ ) -> ( ( <. P , x >. e. ( X X. X ) /\ ( D ` <. P , x >. ) e. ( 0 [,) R ) ) -> x e. X ) )
17 simprl 
 |-  ( ( ( D e. ( PsMet ` X ) /\ P e. X /\ R e. RR+ ) /\ ( x e. X /\ ( P D x ) < R ) ) -> x e. X )
18 17 ex 
 |-  ( ( D e. ( PsMet ` X ) /\ P e. X /\ R e. RR+ ) -> ( ( x e. X /\ ( P D x ) < R ) -> x e. X ) )
19 simpl2 
 |-  ( ( ( D e. ( PsMet ` X ) /\ P e. X /\ R e. RR+ ) /\ x e. X ) -> P e. X )
20 19 13 syl 
 |-  ( ( ( D e. ( PsMet ` X ) /\ P e. X /\ R e. RR+ ) /\ x e. X ) -> ( <. P , x >. e. ( X X. X ) <-> x e. X ) )
21 df-ov 
 |-  ( P D x ) = ( D ` <. P , x >. )
22 21 eleq1i 
 |-  ( ( P D x ) e. ( 0 [,) R ) <-> ( D ` <. P , x >. ) e. ( 0 [,) R ) )
23 0xr 
 |-  0 e. RR*
24 simpl3 
 |-  ( ( ( D e. ( PsMet ` X ) /\ P e. X /\ R e. RR+ ) /\ x e. X ) -> R e. RR+ )
25 24 rpxrd 
 |-  ( ( ( D e. ( PsMet ` X ) /\ P e. X /\ R e. RR+ ) /\ x e. X ) -> R e. RR* )
26 elico1 
 |-  ( ( 0 e. RR* /\ R e. RR* ) -> ( ( P D x ) e. ( 0 [,) R ) <-> ( ( P D x ) e. RR* /\ 0 <_ ( P D x ) /\ ( P D x ) < R ) ) )
27 23 25 26 sylancr 
 |-  ( ( ( D e. ( PsMet ` X ) /\ P e. X /\ R e. RR+ ) /\ x e. X ) -> ( ( P D x ) e. ( 0 [,) R ) <-> ( ( P D x ) e. RR* /\ 0 <_ ( P D x ) /\ ( P D x ) < R ) ) )
28 df-3an 
 |-  ( ( ( P D x ) e. RR* /\ 0 <_ ( P D x ) /\ ( P D x ) < R ) <-> ( ( ( P D x ) e. RR* /\ 0 <_ ( P D x ) ) /\ ( P D x ) < R ) )
29 simpl1 
 |-  ( ( ( D e. ( PsMet ` X ) /\ P e. X /\ R e. RR+ ) /\ x e. X ) -> D e. ( PsMet ` X ) )
30 simpr 
 |-  ( ( ( D e. ( PsMet ` X ) /\ P e. X /\ R e. RR+ ) /\ x e. X ) -> x e. X )
31 psmetcl 
 |-  ( ( D e. ( PsMet ` X ) /\ P e. X /\ x e. X ) -> ( P D x ) e. RR* )
32 29 19 30 31 syl3anc 
 |-  ( ( ( D e. ( PsMet ` X ) /\ P e. X /\ R e. RR+ ) /\ x e. X ) -> ( P D x ) e. RR* )
33 psmetge0 
 |-  ( ( D e. ( PsMet ` X ) /\ P e. X /\ x e. X ) -> 0 <_ ( P D x ) )
34 29 19 30 33 syl3anc 
 |-  ( ( ( D e. ( PsMet ` X ) /\ P e. X /\ R e. RR+ ) /\ x e. X ) -> 0 <_ ( P D x ) )
35 32 34 jca 
 |-  ( ( ( D e. ( PsMet ` X ) /\ P e. X /\ R e. RR+ ) /\ x e. X ) -> ( ( P D x ) e. RR* /\ 0 <_ ( P D x ) ) )
36 35 biantrurd 
 |-  ( ( ( D e. ( PsMet ` X ) /\ P e. X /\ R e. RR+ ) /\ x e. X ) -> ( ( P D x ) < R <-> ( ( ( P D x ) e. RR* /\ 0 <_ ( P D x ) ) /\ ( P D x ) < R ) ) )
37 28 36 bitr4id 
 |-  ( ( ( D e. ( PsMet ` X ) /\ P e. X /\ R e. RR+ ) /\ x e. X ) -> ( ( ( P D x ) e. RR* /\ 0 <_ ( P D x ) /\ ( P D x ) < R ) <-> ( P D x ) < R ) )
38 27 37 bitrd 
 |-  ( ( ( D e. ( PsMet ` X ) /\ P e. X /\ R e. RR+ ) /\ x e. X ) -> ( ( P D x ) e. ( 0 [,) R ) <-> ( P D x ) < R ) )
39 22 38 bitr3id 
 |-  ( ( ( D e. ( PsMet ` X ) /\ P e. X /\ R e. RR+ ) /\ x e. X ) -> ( ( D ` <. P , x >. ) e. ( 0 [,) R ) <-> ( P D x ) < R ) )
40 20 39 anbi12d 
 |-  ( ( ( D e. ( PsMet ` X ) /\ P e. X /\ R e. RR+ ) /\ x e. X ) -> ( ( <. P , x >. e. ( X X. X ) /\ ( D ` <. P , x >. ) e. ( 0 [,) R ) ) <-> ( x e. X /\ ( P D x ) < R ) ) )
41 40 ex 
 |-  ( ( D e. ( PsMet ` X ) /\ P e. X /\ R e. RR+ ) -> ( x e. X -> ( ( <. P , x >. e. ( X X. X ) /\ ( D ` <. P , x >. ) e. ( 0 [,) R ) ) <-> ( x e. X /\ ( P D x ) < R ) ) ) )
42 16 18 41 pm5.21ndd 
 |-  ( ( D e. ( PsMet ` X ) /\ P e. X /\ R e. RR+ ) -> ( ( <. P , x >. e. ( X X. X ) /\ ( D ` <. P , x >. ) e. ( 0 [,) R ) ) <-> ( x e. X /\ ( P D x ) < R ) ) )
43 11 42 bitrd 
 |-  ( ( D e. ( PsMet ` X ) /\ P e. X /\ R e. RR+ ) -> ( <. P , x >. e. ( `' D " ( 0 [,) R ) ) <-> ( x e. X /\ ( P D x ) < R ) ) )
44 elimasng 
 |-  ( ( P e. X /\ x e. _V ) -> ( x e. ( ( `' D " ( 0 [,) R ) ) " { P } ) <-> <. P , x >. e. ( `' D " ( 0 [,) R ) ) ) )
45 44 elvd 
 |-  ( P e. X -> ( x e. ( ( `' D " ( 0 [,) R ) ) " { P } ) <-> <. P , x >. e. ( `' D " ( 0 [,) R ) ) ) )
46 45 3ad2ant2 
 |-  ( ( D e. ( PsMet ` X ) /\ P e. X /\ R e. RR+ ) -> ( x e. ( ( `' D " ( 0 [,) R ) ) " { P } ) <-> <. P , x >. e. ( `' D " ( 0 [,) R ) ) ) )
47 rabid 
 |-  ( x e. { x e. X | ( P D x ) < R } <-> ( x e. X /\ ( P D x ) < R ) )
48 47 a1i 
 |-  ( ( D e. ( PsMet ` X ) /\ P e. X /\ R e. RR+ ) -> ( x e. { x e. X | ( P D x ) < R } <-> ( x e. X /\ ( P D x ) < R ) ) )
49 43 46 48 3bitr4d 
 |-  ( ( D e. ( PsMet ` X ) /\ P e. X /\ R e. RR+ ) -> ( x e. ( ( `' D " ( 0 [,) R ) ) " { P } ) <-> x e. { x e. X | ( P D x ) < R } ) )
50 4 5 6 49 eqrd 
 |-  ( ( D e. ( PsMet ` X ) /\ P e. X /\ R e. RR+ ) -> ( ( `' D " ( 0 [,) R ) ) " { P } ) = { x e. X | ( P D x ) < R } )
51 3 50 eqtr4d 
 |-  ( ( D e. ( PsMet ` X ) /\ P e. X /\ R e. RR+ ) -> ( P ( ball ` D ) R ) = ( ( `' D " ( 0 [,) R ) ) " { P } ) )