blval2

Description: The ball around a point P , alternative definition. (Contributed by Thierry Arnoux, 7-Dec-2017) (Revised by Thierry Arnoux, 11-Mar-2018)

		Ref	Expression
	Assertion	blval2	$⊢ (D \in PsMet (X) \land P \in X \land R \in ℝ^{+}) \to P ball (D) R = D^{-1} [[0, R)] [\{P\}]$

Proof

Step	Hyp	Ref	Expression
1		rpxr	$⊢ R \in ℝ^{+} \to R \in ℝ^{*}$
2		blvalps	$⊢ (D \in PsMet (X) \land P \in X \land R \in ℝ^{*}) \to P ball (D) R = \{x \in X \| P D x < R\}$
3	1 2	syl3an3	$⊢ (D \in PsMet (X) \land P \in X \land R \in ℝ^{+}) \to P ball (D) R = \{x \in X \| P D x < R\}$
4		nfv	$⊢ Ⅎ x (D \in PsMet (X) \land P \in X \land R \in ℝ^{+})$
5		nfcv	$⊢ \underline{Ⅎ} x D^{-1} [[0, R)] [\{P\}]$
6		nfrab1	$⊢ \underline{Ⅎ} x \{x \in X \| P D x < R\}$
7		psmetf	$⊢ D \in PsMet (X) \to D : X \times X ⟶ ℝ^{*}$
8		ffn	$⊢ D : X \times X ⟶ ℝ^{*} \to D Fn (X \times X)$
9		elpreima	$⊢ D Fn (X \times X) \to (⟨P, x⟩ \in D^{-1} [[0, R)] \leftrightarrow (⟨P, x⟩ \in (X \times X) \land D (⟨P, x⟩) \in [0, R)))$
10	7 8 9	3syl	$⊢ D \in PsMet (X) \to (⟨P, x⟩ \in D^{-1} [[0, R)] \leftrightarrow (⟨P, x⟩ \in (X \times X) \land D (⟨P, x⟩) \in [0, R)))$
11	10	3ad2ant1	$⊢ (D \in PsMet (X) \land P \in X \land R \in ℝ^{+}) \to (⟨P, x⟩ \in D^{-1} [[0, R)] \leftrightarrow (⟨P, x⟩ \in (X \times X) \land D (⟨P, x⟩) \in [0, R)))$
12		opelxp	$⊢ ⟨P, x⟩ \in (X \times X) \leftrightarrow (P \in X \land x \in X)$
13	12	baib	$⊢ P \in X \to (⟨P, x⟩ \in (X \times X) \leftrightarrow x \in X)$
14	13	3ad2ant2	$⊢ (D \in PsMet (X) \land P \in X \land R \in ℝ^{+}) \to (⟨P, x⟩ \in (X \times X) \leftrightarrow x \in X)$
15	14	biimpd	$⊢ (D \in PsMet (X) \land P \in X \land R \in ℝ^{+}) \to (⟨P, x⟩ \in (X \times X) \to x \in X)$
16	15	adantrd	$⊢ (D \in PsMet (X) \land P \in X \land R \in ℝ^{+}) \to ((⟨P, x⟩ \in (X \times X) \land D (⟨P, x⟩) \in [0, R)) \to x \in X)$
17		simprl	$⊢ ((D \in PsMet (X) \land P \in X \land R \in ℝ^{+}) \land (x \in X \land P D x < R)) \to x \in X$
18	17	ex	$⊢ (D \in PsMet (X) \land P \in X \land R \in ℝ^{+}) \to ((x \in X \land P D x < R) \to x \in X)$
19		simpl2	$⊢ ((D \in PsMet (X) \land P \in X \land R \in ℝ^{+}) \land x \in X) \to P \in X$
20	19 13	syl	$⊢ ((D \in PsMet (X) \land P \in X \land R \in ℝ^{+}) \land x \in X) \to (⟨P, x⟩ \in (X \times X) \leftrightarrow x \in X)$
21		df-ov	$⊢ P D x = D (⟨P, x⟩)$
22	21	eleq1i	$⊢ P D x \in [0, R) \leftrightarrow D (⟨P, x⟩) \in [0, R)$
23		0xr	$⊢ 0 \in ℝ^{*}$
24		simpl3	$⊢ ((D \in PsMet (X) \land P \in X \land R \in ℝ^{+}) \land x \in X) \to R \in ℝ^{+}$
25	24	rpxrd	$⊢ ((D \in PsMet (X) \land P \in X \land R \in ℝ^{+}) \land x \in X) \to R \in ℝ^{*}$
26		elico1	$⊢ (0 \in ℝ^{} \land R \in ℝ^{}) \to (P D x \in [0, R) \leftrightarrow (P D x \in ℝ^{*} \land 0 \leq P D x \land P D x < R))$
27	23 25 26	sylancr	$⊢ ((D \in PsMet (X) \land P \in X \land R \in ℝ^{+}) \land x \in X) \to (P D x \in [0, R) \leftrightarrow (P D x \in ℝ^{*} \land 0 \leq P D x \land P D x < R))$
28		df-3an	$⊢ (P D x \in ℝ^{} \land 0 \leq P D x \land P D x < R) \leftrightarrow ((P D x \in ℝ^{} \land 0 \leq P D x) \land P D x < R)$
29		simpl1	$⊢ ((D \in PsMet (X) \land P \in X \land R \in ℝ^{+}) \land x \in X) \to D \in PsMet (X)$
30		simpr	$⊢ ((D \in PsMet (X) \land P \in X \land R \in ℝ^{+}) \land x \in X) \to x \in X$
31		psmetcl	$⊢ (D \in PsMet (X) \land P \in X \land x \in X) \to P D x \in ℝ^{*}$
32	29 19 30 31	syl3anc	$⊢ ((D \in PsMet (X) \land P \in X \land R \in ℝ^{+}) \land x \in X) \to P D x \in ℝ^{*}$
33		psmetge0	$⊢ (D \in PsMet (X) \land P \in X \land x \in X) \to 0 \leq P D x$
34	29 19 30 33	syl3anc	$⊢ ((D \in PsMet (X) \land P \in X \land R \in ℝ^{+}) \land x \in X) \to 0 \leq P D x$
35	32 34	jca	$⊢ ((D \in PsMet (X) \land P \in X \land R \in ℝ^{+}) \land x \in X) \to (P D x \in ℝ^{*} \land 0 \leq P D x)$
36	35	biantrurd	$⊢ ((D \in PsMet (X) \land P \in X \land R \in ℝ^{+}) \land x \in X) \to (P D x < R \leftrightarrow ((P D x \in ℝ^{*} \land 0 \leq P D x) \land P D x < R))$
37	28 36	bitr4id	$⊢ ((D \in PsMet (X) \land P \in X \land R \in ℝ^{+}) \land x \in X) \to ((P D x \in ℝ^{*} \land 0 \leq P D x \land P D x < R) \leftrightarrow P D x < R)$
38	27 37	bitrd	$⊢ ((D \in PsMet (X) \land P \in X \land R \in ℝ^{+}) \land x \in X) \to (P D x \in [0, R) \leftrightarrow P D x < R)$
39	22 38	bitr3id	$⊢ ((D \in PsMet (X) \land P \in X \land R \in ℝ^{+}) \land x \in X) \to (D (⟨P, x⟩) \in [0, R) \leftrightarrow P D x < R)$
40	20 39	anbi12d	$⊢ ((D \in PsMet (X) \land P \in X \land R \in ℝ^{+}) \land x \in X) \to ((⟨P, x⟩ \in (X \times X) \land D (⟨P, x⟩) \in [0, R)) \leftrightarrow (x \in X \land P D x < R))$
41	40	ex	$⊢ (D \in PsMet (X) \land P \in X \land R \in ℝ^{+}) \to (x \in X \to ((⟨P, x⟩ \in (X \times X) \land D (⟨P, x⟩) \in [0, R)) \leftrightarrow (x \in X \land P D x < R)))$
42	16 18 41	pm5.21ndd	$⊢ (D \in PsMet (X) \land P \in X \land R \in ℝ^{+}) \to ((⟨P, x⟩ \in (X \times X) \land D (⟨P, x⟩) \in [0, R)) \leftrightarrow (x \in X \land P D x < R))$
43	11 42	bitrd	$⊢ (D \in PsMet (X) \land P \in X \land R \in ℝ^{+}) \to (⟨P, x⟩ \in D^{-1} [[0, R)] \leftrightarrow (x \in X \land P D x < R))$
44		elimasng	$⊢ (P \in X \land x \in V) \to (x \in D^{-1} [[0, R)] [\{P\}] \leftrightarrow ⟨P, x⟩ \in D^{-1} [[0, R)])$
45	44	elvd	$⊢ P \in X \to (x \in D^{-1} [[0, R)] [\{P\}] \leftrightarrow ⟨P, x⟩ \in D^{-1} [[0, R)])$
46	45	3ad2ant2	$⊢ (D \in PsMet (X) \land P \in X \land R \in ℝ^{+}) \to (x \in D^{-1} [[0, R)] [\{P\}] \leftrightarrow ⟨P, x⟩ \in D^{-1} [[0, R)])$
47		rabid	$⊢ x \in \{x \in X \| P D x < R\} \leftrightarrow (x \in X \land P D x < R)$
48	47	a1i	$⊢ (D \in PsMet (X) \land P \in X \land R \in ℝ^{+}) \to (x \in \{x \in X \| P D x < R\} \leftrightarrow (x \in X \land P D x < R))$
49	43 46 48	3bitr4d	$⊢ (D \in PsMet (X) \land P \in X \land R \in ℝ^{+}) \to (x \in D^{-1} [[0, R)] [\{P\}] \leftrightarrow x \in \{x \in X \| P D x < R\})$
50	4 5 6 49	eqrd	$⊢ (D \in PsMet (X) \land P \in X \land R \in ℝ^{+}) \to D^{-1} [[0, R)] [\{P\}] = \{x \in X \| P D x < R\}$
51	3 50	eqtr4d	$⊢ (D \in PsMet (X) \land P \in X \land R \in ℝ^{+}) \to P ball (D) R = D^{-1} [[0, R)] [\{P\}]$

Metamath Proof Explorer

Theorem blval2

Proof