Metamath Proof Explorer

Theorem blval

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)

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

Proof

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