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 DPsMetXPXR+PballDR=D-10RP

Proof

Step Hyp Ref Expression
1 rpxr R+R*
2 blvalps DPsMetXPXR*PballDR=xX|PDx<R
3 1 2 syl3an3 DPsMetXPXR+PballDR=xX|PDx<R
4 nfv xDPsMetXPXR+
5 nfcv _xD-10RP
6 nfrab1 _xxX|PDx<R
7 psmetf DPsMetXD:X×X*
8 ffn D:X×X*DFnX×X
9 elpreima DFnX×XPxD-10RPxX×XDPx0R
10 7 8 9 3syl DPsMetXPxD-10RPxX×XDPx0R
11 10 3ad2ant1 DPsMetXPXR+PxD-10RPxX×XDPx0R
12 opelxp PxX×XPXxX
13 12 baib PXPxX×XxX
14 13 3ad2ant2 DPsMetXPXR+PxX×XxX
15 14 biimpd DPsMetXPXR+PxX×XxX
16 15 adantrd DPsMetXPXR+PxX×XDPx0RxX
17 simprl DPsMetXPXR+xXPDx<RxX
18 17 ex DPsMetXPXR+xXPDx<RxX
19 simpl2 DPsMetXPXR+xXPX
20 19 13 syl DPsMetXPXR+xXPxX×XxX
21 df-ov PDx=DPx
22 21 eleq1i PDx0RDPx0R
23 0xr 0*
24 simpl3 DPsMetXPXR+xXR+
25 24 rpxrd DPsMetXPXR+xXR*
26 elico1 0*R*PDx0RPDx*0PDxPDx<R
27 23 25 26 sylancr DPsMetXPXR+xXPDx0RPDx*0PDxPDx<R
28 df-3an PDx*0PDxPDx<RPDx*0PDxPDx<R
29 simpl1 DPsMetXPXR+xXDPsMetX
30 simpr DPsMetXPXR+xXxX
31 psmetcl DPsMetXPXxXPDx*
32 29 19 30 31 syl3anc DPsMetXPXR+xXPDx*
33 psmetge0 DPsMetXPXxX0PDx
34 29 19 30 33 syl3anc DPsMetXPXR+xX0PDx
35 32 34 jca DPsMetXPXR+xXPDx*0PDx
36 35 biantrurd DPsMetXPXR+xXPDx<RPDx*0PDxPDx<R
37 28 36 bitr4id DPsMetXPXR+xXPDx*0PDxPDx<RPDx<R
38 27 37 bitrd DPsMetXPXR+xXPDx0RPDx<R
39 22 38 bitr3id DPsMetXPXR+xXDPx0RPDx<R
40 20 39 anbi12d DPsMetXPXR+xXPxX×XDPx0RxXPDx<R
41 40 ex DPsMetXPXR+xXPxX×XDPx0RxXPDx<R
42 16 18 41 pm5.21ndd DPsMetXPXR+PxX×XDPx0RxXPDx<R
43 11 42 bitrd DPsMetXPXR+PxD-10RxXPDx<R
44 elimasng PXxVxD-10RPPxD-10R
45 44 elvd PXxD-10RPPxD-10R
46 45 3ad2ant2 DPsMetXPXR+xD-10RPPxD-10R
47 rabid xxX|PDx<RxXPDx<R
48 47 a1i DPsMetXPXR+xxX|PDx<RxXPDx<R
49 43 46 48 3bitr4d DPsMetXPXR+xD-10RPxxX|PDx<R
50 4 5 6 49 eqrd DPsMetXPXR+D-10RP=xX|PDx<R
51 3 50 eqtr4d DPsMetXPXR+PballDR=D-10RP