blres

Description: A ball in a restricted metric space. (Contributed by Mario Carneiro, 5-Jan-2014)

		Ref	Expression
	Hypothesis	blres.2	$⊢ C = {D ↾}_{(Y \times Y)}$
	Assertion	blres	$⊢ (D \in ∞Met (X) \land P \in (X \cap Y) \land R \in ℝ^{*}) \to P ball (C) R = (P ball (D) R) \cap Y$

Proof

Step	Hyp	Ref	Expression
1		blres.2	$⊢ C = {D ↾}_{(Y \times Y)}$
2		elinel2	$⊢ P \in (X \cap Y) \to P \in Y$
3	1	oveqi	$⊢ P C x = P ({D ↾}_{(Y \times Y)}) x$
4		ovres	$⊢ (P \in Y \land x \in Y) \to P ({D ↾}_{(Y \times Y)}) x = P D x$
5	3 4	eqtrid	$⊢ (P \in Y \land x \in Y) \to P C x = P D x$
6	2 5	sylan	$⊢ (P \in (X \cap Y) \land x \in Y) \to P C x = P D x$
7	6	breq1d	$⊢ (P \in (X \cap Y) \land x \in Y) \to (P C x < R \leftrightarrow P D x < R)$
8	7	anbi2d	$⊢ (P \in (X \cap Y) \land x \in Y) \to ((x \in X \land P C x < R) \leftrightarrow (x \in X \land P D x < R))$
9	8	pm5.32da	$⊢ P \in (X \cap Y) \to ((x \in Y \land (x \in X \land P C x < R)) \leftrightarrow (x \in Y \land (x \in X \land P D x < R)))$
10	9	3ad2ant2	$⊢ (D \in ∞Met (X) \land P \in (X \cap Y) \land R \in ℝ^{*}) \to ((x \in Y \land (x \in X \land P C x < R)) \leftrightarrow (x \in Y \land (x \in X \land P D x < R)))$
11		elin	$⊢ x \in (X \cap Y) \leftrightarrow (x \in X \land x \in Y)$
12	11	biancomi	$⊢ x \in (X \cap Y) \leftrightarrow (x \in Y \land x \in X)$
13	12	anbi1i	$⊢ (x \in (X \cap Y) \land P C x < R) \leftrightarrow ((x \in Y \land x \in X) \land P C x < R)$
14		anass	$⊢ ((x \in Y \land x \in X) \land P C x < R) \leftrightarrow (x \in Y \land (x \in X \land P C x < R))$
15	13 14	bitri	$⊢ (x \in (X \cap Y) \land P C x < R) \leftrightarrow (x \in Y \land (x \in X \land P C x < R))$
16		ancom	$⊢ ((x \in X \land P D x < R) \land x \in Y) \leftrightarrow (x \in Y \land (x \in X \land P D x < R))$
17	10 15 16	3bitr4g	$⊢ (D \in ∞Met (X) \land P \in (X \cap Y) \land R \in ℝ^{*}) \to ((x \in (X \cap Y) \land P C x < R) \leftrightarrow ((x \in X \land P D x < R) \land x \in Y))$
18		xmetres	$⊢ D \in ∞Met (X) \to {D ↾}_{(Y \times Y)} \in ∞Met (X \cap Y)$
19	1 18	eqeltrid	$⊢ D \in ∞Met (X) \to C \in ∞Met (X \cap Y)$
20		elbl	$⊢ (C \in ∞Met (X \cap Y) \land P \in (X \cap Y) \land R \in ℝ^{*}) \to (x \in (P ball (C) R) \leftrightarrow (x \in (X \cap Y) \land P C x < R))$
21	19 20	syl3an1	$⊢ (D \in ∞Met (X) \land P \in (X \cap Y) \land R \in ℝ^{*}) \to (x \in (P ball (C) R) \leftrightarrow (x \in (X \cap Y) \land P C x < R))$
22		elin	$⊢ x \in ((P ball (D) R) \cap Y) \leftrightarrow (x \in (P ball (D) R) \land x \in Y)$
23		elinel1	$⊢ P \in (X \cap Y) \to P \in X$
24		elbl	$⊢ (D \in ∞Met (X) \land P \in X \land R \in ℝ^{*}) \to (x \in (P ball (D) R) \leftrightarrow (x \in X \land P D x < R))$
25	23 24	syl3an2	$⊢ (D \in ∞Met (X) \land P \in (X \cap Y) \land R \in ℝ^{*}) \to (x \in (P ball (D) R) \leftrightarrow (x \in X \land P D x < R))$
26	25	anbi1d	$⊢ (D \in ∞Met (X) \land P \in (X \cap Y) \land R \in ℝ^{*}) \to ((x \in (P ball (D) R) \land x \in Y) \leftrightarrow ((x \in X \land P D x < R) \land x \in Y))$
27	22 26	bitrid	$⊢ (D \in ∞Met (X) \land P \in (X \cap Y) \land R \in ℝ^{*}) \to (x \in ((P ball (D) R) \cap Y) \leftrightarrow ((x \in X \land P D x < R) \land x \in Y))$
28	17 21 27	3bitr4d	$⊢ (D \in ∞Met (X) \land P \in (X \cap Y) \land R \in ℝ^{*}) \to (x \in (P ball (C) R) \leftrightarrow x \in ((P ball (D) R) \cap Y))$
29	28	eqrdv	$⊢ (D \in ∞Met (X) \land P \in (X \cap Y) \land R \in ℝ^{*}) \to P ball (C) R = (P ball (D) R) \cap Y$

Metamath Proof Explorer

Theorem blres

Proof