Metamath Proof Explorer

Theorem elbl4

Description: Membership in a ball, alternative definition. (Contributed by Thierry Arnoux, 26-Jan-2018) (Revised by Thierry Arnoux, 11-Mar-2018)

		Ref	Expression
	Assertion	elbl4	$⊢ ((D \in PsMet (X) \land R \in ℝ^{+}) \land (A \in X \land B \in X)) \to (B \in (A ball (D) R) \leftrightarrow B D^{-1} [[0, R)] A)$

Proof

Step	Hyp	Ref	Expression
1		rpxr	$⊢ R \in ℝ^{+} \to R \in ℝ^{*}$
2		blcomps	$⊢ ((D \in PsMet (X) \land R \in ℝ^{*}) \land (A \in X \land B \in X)) \to (B \in (A ball (D) R) \leftrightarrow A \in (B ball (D) R))$
3	1 2	sylanl2	$⊢ ((D \in PsMet (X) \land R \in ℝ^{+}) \land (A \in X \land B \in X)) \to (B \in (A ball (D) R) \leftrightarrow A \in (B ball (D) R))$
4		simpll	$⊢ ((D \in PsMet (X) \land R \in ℝ^{+}) \land (A \in X \land B \in X)) \to D \in PsMet (X)$
5		simprr	$⊢ ((D \in PsMet (X) \land R \in ℝ^{+}) \land (A \in X \land B \in X)) \to B \in X$
6		simplr	$⊢ ((D \in PsMet (X) \land R \in ℝ^{+}) \land (A \in X \land B \in X)) \to R \in ℝ^{+}$
7		blval2	$⊢ (D \in PsMet (X) \land B \in X \land R \in ℝ^{+}) \to B ball (D) R = D^{-1} [[0, R)] [\{B\}]$
8	7	eleq2d	$⊢ (D \in PsMet (X) \land B \in X \land R \in ℝ^{+}) \to (A \in (B ball (D) R) \leftrightarrow A \in D^{-1} [[0, R)] [\{B\}])$
9	4 5 6 8	syl3anc	$⊢ ((D \in PsMet (X) \land R \in ℝ^{+}) \land (A \in X \land B \in X)) \to (A \in (B ball (D) R) \leftrightarrow A \in D^{-1} [[0, R)] [\{B\}])$
10		elimasng	$⊢ (B \in X \land A \in X) \to (A \in D^{-1} [[0, R)] [\{B\}] \leftrightarrow ⟨B, A⟩ \in D^{-1} [[0, R)])$
11		df-br	$⊢ B D^{-1} [[0, R)] A \leftrightarrow ⟨B, A⟩ \in D^{-1} [[0, R)]$
12	10 11	bitr4di	$⊢ (B \in X \land A \in X) \to (A \in D^{-1} [[0, R)] [\{B\}] \leftrightarrow B D^{-1} [[0, R)] A)$
13	12	ancoms	$⊢ (A \in X \land B \in X) \to (A \in D^{-1} [[0, R)] [\{B\}] \leftrightarrow B D^{-1} [[0, R)] A)$
14	13	adantl	$⊢ ((D \in PsMet (X) \land R \in ℝ^{+}) \land (A \in X \land B \in X)) \to (A \in D^{-1} [[0, R)] [\{B\}] \leftrightarrow B D^{-1} [[0, R)] A)$
15	3 9 14	3bitrd	$⊢ ((D \in PsMet (X) \land R \in ℝ^{+}) \land (A \in X \land B \in X)) \to (B \in (A ball (D) R) \leftrightarrow B D^{-1} [[0, R)] A)$