Theorem blvalps

Description: The ball around a point P is the set of all points whose distance from P is less than the ball's radius R . (Contributed by NM, 31-Aug-2006) (Revised by Mario Carneiro, 11-Nov-2013) (Revised by Thierry Arnoux, 11-Mar-2018)

	Ref	Expression
Assertion	blvalps	|- ( ( D e. ( PsMet ` X ) /\ P e. X /\ R e. RR* ) -> ( P ( ball ` D ) R ) = { x e. X | ( P D x ) < R } )

Proof

Step	Hyp	Ref	Expression
1		blfvalps	|- ( D e. ( PsMet ` X ) -> ( ball ` D ) = ( y e. X , r e. RR* |-> { x e. X | ( y D x ) < r } ) )
2	1	3ad2ant1	|- ( ( D e. ( PsMet ` X ) /\ P e. X /\ R e. RR* ) -> ( ball ` D ) = ( y e. X , r e. RR* |-> { x e. X | ( y D x ) < r } ) )
3		simprl	|- ( ( ( D e. ( PsMet ` X ) /\ P e. X /\ R e. RR* ) /\ ( y = P /\ r = R ) ) -> y = P )
4	3	oveq1d	|- ( ( ( D e. ( PsMet ` X ) /\ P e. X /\ R e. RR* ) /\ ( y = P /\ r = R ) ) -> ( y D x ) = ( P D x ) )
5		simprr	|- ( ( ( D e. ( PsMet ` X ) /\ P e. X /\ R e. RR* ) /\ ( y = P /\ r = R ) ) -> r = R )
6	4 5	breq12d	|- ( ( ( D e. ( PsMet ` X ) /\ P e. X /\ R e. RR* ) /\ ( y = P /\ r = R ) ) -> ( ( y D x ) < r <-> ( P D x ) < R ) )
7	6	rabbidv	|- ( ( ( D e. ( PsMet ` X ) /\ P e. X /\ R e. RR* ) /\ ( y = P /\ r = R ) ) -> { x e. X | ( y D x ) < r } = { x e. X | ( P D x ) < R } )
8		simp2	|- ( ( D e. ( PsMet ` X ) /\ P e. X /\ R e. RR* ) -> P e. X )
9		simp3	|- ( ( D e. ( PsMet ` X ) /\ P e. X /\ R e. RR* ) -> R e. RR* )
10		elfvdm	|- ( D e. ( PsMet ` X ) -> X e. dom PsMet )
11	10	3ad2ant1	|- ( ( D e. ( PsMet ` X ) /\ P e. X /\ R e. RR* ) -> X e. dom PsMet )
12		rabexg	|- ( X e. dom PsMet -> { x e. X | ( P D x ) < R } e. _V )
13	11 12	syl	|- ( ( D e. ( PsMet ` X ) /\ P e. X /\ R e. RR* ) -> { x e. X | ( P D x ) < R } e. _V )
14	2 7 8 9 13	ovmpod	|- ( ( D e. ( PsMet ` X ) /\ P e. X /\ R e. RR* ) -> ( P ( ball ` D ) R ) = { x e. X | ( P D x ) < R } )