blin

Description: The intersection of two balls with the same center is the smaller of them. (Contributed by NM, 1-Sep-2006) (Revised by Mario Carneiro, 12-Nov-2013)

		Ref	Expression
	Assertion	blin	$⊢ ((D \in ∞Met (X) \land P \in X) \land (R \in ℝ^{} \land S \in ℝ^{})) \to (P ball (D) R) \cap (P ball (D) S) = P ball (D) if (R \leq S, R, S)$

Proof

Step	Hyp	Ref	Expression
1		xmetcl	$⊢ (D \in ∞Met (X) \land P \in X \land x \in X) \to P D x \in ℝ^{*}$
2	1	ad4ant124	$⊢ (((D \in ∞Met (X) \land P \in X) \land (R \in ℝ^{} \land S \in ℝ^{})) \land x \in X) \to P D x \in ℝ^{*}$
3		simplrl	$⊢ (((D \in ∞Met (X) \land P \in X) \land (R \in ℝ^{} \land S \in ℝ^{})) \land x \in X) \to R \in ℝ^{*}$
4		simplrr	$⊢ (((D \in ∞Met (X) \land P \in X) \land (R \in ℝ^{} \land S \in ℝ^{})) \land x \in X) \to S \in ℝ^{*}$
5		xrltmin	$⊢ (P D x \in ℝ^{} \land R \in ℝ^{} \land S \in ℝ^{*}) \to (P D x < if (R \leq S, R, S) \leftrightarrow (P D x < R \land P D x < S))$
6	2 3 4 5	syl3anc	$⊢ (((D \in ∞Met (X) \land P \in X) \land (R \in ℝ^{} \land S \in ℝ^{})) \land x \in X) \to (P D x < if (R \leq S, R, S) \leftrightarrow (P D x < R \land P D x < S))$
7	6	pm5.32da	$⊢ ((D \in ∞Met (X) \land P \in X) \land (R \in ℝ^{} \land S \in ℝ^{})) \to ((x \in X \land P D x < if (R \leq S, R, S)) \leftrightarrow (x \in X \land (P D x < R \land P D x < S)))$
8		ifcl	$⊢ (R \in ℝ^{} \land S \in ℝ^{}) \to if (R \leq S, R, S) \in ℝ^{*}$
9		elbl	$⊢ (D \in ∞Met (X) \land P \in X \land if (R \leq S, R, S) \in ℝ^{*}) \to (x \in (P ball (D) if (R \leq S, R, S)) \leftrightarrow (x \in X \land P D x < if (R \leq S, R, S)))$
10	9	3expa	$⊢ ((D \in ∞Met (X) \land P \in X) \land if (R \leq S, R, S) \in ℝ^{*}) \to (x \in (P ball (D) if (R \leq S, R, S)) \leftrightarrow (x \in X \land P D x < if (R \leq S, R, S)))$
11	8 10	sylan2	$⊢ ((D \in ∞Met (X) \land P \in X) \land (R \in ℝ^{} \land S \in ℝ^{})) \to (x \in (P ball (D) if (R \leq S, R, S)) \leftrightarrow (x \in X \land P D x < if (R \leq S, R, S)))$
12		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))$
13	12	3expa	$⊢ ((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))$
14	13	adantrr	$⊢ ((D \in ∞Met (X) \land P \in X) \land (R \in ℝ^{} \land S \in ℝ^{})) \to (x \in (P ball (D) R) \leftrightarrow (x \in X \land P D x < R))$
15		elbl	$⊢ (D \in ∞Met (X) \land P \in X \land S \in ℝ^{*}) \to (x \in (P ball (D) S) \leftrightarrow (x \in X \land P D x < S))$
16	15	3expa	$⊢ ((D \in ∞Met (X) \land P \in X) \land S \in ℝ^{*}) \to (x \in (P ball (D) S) \leftrightarrow (x \in X \land P D x < S))$
17	16	adantrl	$⊢ ((D \in ∞Met (X) \land P \in X) \land (R \in ℝ^{} \land S \in ℝ^{})) \to (x \in (P ball (D) S) \leftrightarrow (x \in X \land P D x < S))$
18	14 17	anbi12d	$⊢ ((D \in ∞Met (X) \land P \in X) \land (R \in ℝ^{} \land S \in ℝ^{})) \to ((x \in (P ball (D) R) \land x \in (P ball (D) S)) \leftrightarrow ((x \in X \land P D x < R) \land (x \in X \land P D x < S)))$
19		elin	$⊢ x \in ((P ball (D) R) \cap (P ball (D) S)) \leftrightarrow (x \in (P ball (D) R) \land x \in (P ball (D) S))$
20		anandi	$⊢ (x \in X \land (P D x < R \land P D x < S)) \leftrightarrow ((x \in X \land P D x < R) \land (x \in X \land P D x < S))$
21	18 19 20	3bitr4g	$⊢ ((D \in ∞Met (X) \land P \in X) \land (R \in ℝ^{} \land S \in ℝ^{})) \to (x \in ((P ball (D) R) \cap (P ball (D) S)) \leftrightarrow (x \in X \land (P D x < R \land P D x < S)))$
22	7 11 21	3bitr4rd	$⊢ ((D \in ∞Met (X) \land P \in X) \land (R \in ℝ^{} \land S \in ℝ^{})) \to (x \in ((P ball (D) R) \cap (P ball (D) S)) \leftrightarrow x \in (P ball (D) if (R \leq S, R, S)))$
23	22	eqrdv	$⊢ ((D \in ∞Met (X) \land P \in X) \land (R \in ℝ^{} \land S \in ℝ^{})) \to (P ball (D) R) \cap (P ball (D) S) = P ball (D) if (R \leq S, R, S)$

Metamath Proof Explorer

Theorem blin

Proof