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 PsMet X P X R + P ball D R = D -1 0 R P

Proof

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