Metamath Proof Explorer

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 \in PsMet (X) \land P \in X \land R \in ℝ^{*}) \to P ball (D) R = \{x \in X \| P D x < R\}$

Proof

Step	Hyp	Ref	Expression
1		blfvalps	$⊢ D \in PsMet (X) \to ball (D) = (y \in X, r \in ℝ^{*} ⟼ \{x \in X \| y D x < r\})$
2	1	3ad2ant1	$⊢ (D \in PsMet (X) \land P \in X \land R \in ℝ^{}) \to ball (D) = (y \in X, r \in ℝ^{} ⟼ \{x \in X \| y D x < r\})$
3		simprl	$⊢ ((D \in PsMet (X) \land P \in X \land R \in ℝ^{*}) \land (y = P \land r = R)) \to y = P$
4	3	oveq1d	$⊢ ((D \in PsMet (X) \land P \in X \land R \in ℝ^{*}) \land (y = P \land r = R)) \to y D x = P D x$
5		simprr	$⊢ ((D \in PsMet (X) \land P \in X \land R \in ℝ^{*}) \land (y = P \land r = R)) \to r = R$
6	4 5	breq12d	$⊢ ((D \in PsMet (X) \land P \in X \land R \in ℝ^{*}) \land (y = P \land r = R)) \to (y D x < r \leftrightarrow P D x < R)$
7	6	rabbidv	$⊢ ((D \in PsMet (X) \land P \in X \land R \in ℝ^{*}) \land (y = P \land r = R)) \to \{x \in X \| y D x < r\} = \{x \in X \| P D x < R\}$
8		simp2	$⊢ (D \in PsMet (X) \land P \in X \land R \in ℝ^{*}) \to P \in X$
9		simp3	$⊢ (D \in PsMet (X) \land P \in X \land R \in ℝ^{}) \to R \in ℝ^{}$
10		elfvdm	$⊢ D \in PsMet (X) \to X \in dom PsMet$
11	10	3ad2ant1	$⊢ (D \in PsMet (X) \land P \in X \land R \in ℝ^{*}) \to X \in dom PsMet$
12		rabexg	$⊢ X \in dom PsMet \to \{x \in X \| P D x < R\} \in V$
13	11 12	syl	$⊢ (D \in PsMet (X) \land P \in X \land R \in ℝ^{*}) \to \{x \in X \| P D x < R\} \in V$
14	2 7 8 9 13	ovmpod	$⊢ (D \in PsMet (X) \land P \in X \land R \in ℝ^{*}) \to P ball (D) R = \{x \in X \| P D x < R\}$