blcomps

Description: Commute the arguments to the ball function. (Contributed by Mario Carneiro, 22-Jan-2014) (Revised by Thierry Arnoux, 11-Mar-2018)

		Ref	Expression
	Assertion	blcomps	$⊢ ((D \in PsMet (X) \land R \in ℝ^{*}) \land (P \in X \land A \in X)) \to (A \in (P ball (D) R) \leftrightarrow P \in (A ball (D) R))$

Step	Hyp	Ref	Expression
1		elbl2ps	$⊢ ((D \in PsMet (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		elbl3ps	$⊢ ((D \in PsMet (X) \land R \in ℝ^{*}) \land (A \in X \land P \in X)) \to (P \in (A ball (D) R) \leftrightarrow P D A < R)$
3	2	ancom2s	$⊢ ((D \in PsMet (X) \land R \in ℝ^{*}) \land (P \in X \land A \in X)) \to (P \in (A ball (D) R) \leftrightarrow P D A < R)$
4	1 3	bitr4d	$⊢ ((D \in PsMet (X) \land R \in ℝ^{*}) \land (P \in X \land A \in X)) \to (A \in (P ball (D) R) \leftrightarrow P \in (A ball (D) R))$

Metamath Proof Explorer