elbl3

Description: Membership in a ball, with reversed distance function arguments. (Contributed by NM, 10-Nov-2007)

		Ref	Expression
	Assertion	elbl3	$⊢ ((D \in ∞Met (X) \land R \in ℝ^{*}) \land (P \in X \land A \in X)) \to (A \in (P ball (D) R) \leftrightarrow A D P < R)$

Step	Hyp	Ref	Expression
1		elbl2	$⊢ ((D \in ∞Met (X) \land R \in ℝ^{*}) \land (P \in X \land A \in X)) \to (A \in (P ball (D) R) \leftrightarrow P D A < R)$
2		xmetsym	$⊢ (D \in ∞Met (X) \land P \in X \land A \in X) \to P D A = A D P$
3	2	3expb	$⊢ (D \in ∞Met (X) \land (P \in X \land A \in X)) \to P D A = A D P$
4	3	adantlr	$⊢ ((D \in ∞Met (X) \land R \in ℝ^{*}) \land (P \in X \land A \in X)) \to P D A = A D P$
5	4	breq1d	$⊢ ((D \in ∞Met (X) \land R \in ℝ^{*}) \land (P \in X \land A \in X)) \to (P D A < R \leftrightarrow A D P < R)$
6	1 5	bitrd	$⊢ ((D \in ∞Met (X) \land R \in ℝ^{*}) \land (P \in X \land A \in X)) \to (A \in (P ball (D) R) \leftrightarrow A D P < R)$

Metamath Proof Explorer