Theorem elblps

Description: Membership in a ball. (Contributed by NM, 2-Sep-2006) (Revised by Mario Carneiro, 11-Nov-2013) (Revised by Thierry Arnoux, 11-Mar-2018)

	Ref	Expression
Assertion	elblps	$$⊢\left(D\in \mathrm{PsMet}\left(X\right)\wedge P\in X\wedge R\in {ℝ}^{*}\right)\to \left(A\in \left(P\mathrm{ball}\left(D\right)R\right)\leftrightarrow \left(A\in X\wedge PDA<R\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		blvalps	$$⊢\left(D\in \mathrm{PsMet}\left(X\right)\wedge P\in X\wedge R\in {ℝ}^{*}\right)\to P\mathrm{ball}\left(D\right)R=\left\{x\in X|PDx<R\right\}$$
2	1	eleq2d	$$⊢\left(D\in \mathrm{PsMet}\left(X\right)\wedge P\in X\wedge R\in {ℝ}^{*}\right)\to \left(A\in \left(P\mathrm{ball}\left(D\right)R\right)\leftrightarrow A\in \left\{x\in X|PDx<R\right\}\right)$$
3		oveq2	$$⊢x=A\to PDx=PDA$$
4	3	breq1d	$$⊢x=A\to \left(PDx<R\leftrightarrow PDA<R\right)$$
5	4	elrab	$$⊢A\in \left\{x\in X|PDx<R\right\}\leftrightarrow \left(A\in X\wedge PDA<R\right)$$
6	2 5	bitrdi	$$⊢\left(D\in \mathrm{PsMet}\left(X\right)\wedge P\in X\wedge R\in {ℝ}^{*}\right)\to \left(A\in \left(P\mathrm{ball}\left(D\right)R\right)\leftrightarrow \left(A\in X\wedge PDA<R\right)\right)$$