blss

Description: Any point P in a ball B can be centered in another ball that is a subset of B . (Contributed by NM, 31-Aug-2006) (Revised by Mario Carneiro, 24-Aug-2015)

		Ref	Expression
	Assertion	blss	$⊢ (D \in ∞Met (X) \land B \in ran ball (D) \land P \in B) \to \exists x \in ℝ^{+} P ball (D) x \subseteq B$

Proof

Step	Hyp	Ref	Expression
1		blrn	$⊢ D \in ∞Met (X) \to (B \in ran ball (D) \leftrightarrow \exists y \in X \exists r \in ℝ^{*} B = y ball (D) r)$
2		elbl	$⊢ (D \in ∞Met (X) \land y \in X \land r \in ℝ^{*}) \to (P \in (y ball (D) r) \leftrightarrow (P \in X \land y D P < r))$
3		simpl1	$⊢ ((D \in ∞Met (X) \land y \in X \land r \in ℝ^{*}) \land P \in X) \to D \in ∞Met (X)$
4		simpl2	$⊢ ((D \in ∞Met (X) \land y \in X \land r \in ℝ^{*}) \land P \in X) \to y \in X$
5		simpr	$⊢ ((D \in ∞Met (X) \land y \in X \land r \in ℝ^{*}) \land P \in X) \to P \in X$
6		xmetcl	$⊢ (D \in ∞Met (X) \land y \in X \land P \in X) \to y D P \in ℝ^{*}$
7	3 4 5 6	syl3anc	$⊢ ((D \in ∞Met (X) \land y \in X \land r \in ℝ^{}) \land P \in X) \to y D P \in ℝ^{}$
8		simpl3	$⊢ ((D \in ∞Met (X) \land y \in X \land r \in ℝ^{}) \land P \in X) \to r \in ℝ^{}$
9		qbtwnxr	$⊢ (y D P \in ℝ^{} \land r \in ℝ^{} \land y D P < r) \to \exists z \in ℚ (y D P < z \land z < r)$
10	9	3expia	$⊢ (y D P \in ℝ^{} \land r \in ℝ^{}) \to (y D P < r \to \exists z \in ℚ (y D P < z \land z < r))$
11	7 8 10	syl2anc	$⊢ ((D \in ∞Met (X) \land y \in X \land r \in ℝ^{*}) \land P \in X) \to (y D P < r \to \exists z \in ℚ (y D P < z \land z < r))$
12		qre	$⊢ z \in ℚ \to z \in ℝ$
13		simpll1	$⊢ (((D \in ∞Met (X) \land y \in X \land r \in ℝ^{*}) \land P \in X) \land (z \in ℝ \land (y D P < z \land z < r))) \to D \in ∞Met (X)$
14		simplr	$⊢ (((D \in ∞Met (X) \land y \in X \land r \in ℝ^{*}) \land P \in X) \land (z \in ℝ \land (y D P < z \land z < r))) \to P \in X$
15		simpll2	$⊢ (((D \in ∞Met (X) \land y \in X \land r \in ℝ^{*}) \land P \in X) \land (z \in ℝ \land (y D P < z \land z < r))) \to y \in X$
16		xmetsym	$⊢ (D \in ∞Met (X) \land P \in X \land y \in X) \to P D y = y D P$
17	13 14 15 16	syl3anc	$⊢ (((D \in ∞Met (X) \land y \in X \land r \in ℝ^{*}) \land P \in X) \land (z \in ℝ \land (y D P < z \land z < r))) \to P D y = y D P$
18		simprrl	$⊢ (((D \in ∞Met (X) \land y \in X \land r \in ℝ^{*}) \land P \in X) \land (z \in ℝ \land (y D P < z \land z < r))) \to y D P < z$
19	17 18	eqbrtrd	$⊢ (((D \in ∞Met (X) \land y \in X \land r \in ℝ^{*}) \land P \in X) \land (z \in ℝ \land (y D P < z \land z < r))) \to P D y < z$
20		simprl	$⊢ (((D \in ∞Met (X) \land y \in X \land r \in ℝ^{*}) \land P \in X) \land (z \in ℝ \land (y D P < z \land z < r))) \to z \in ℝ$
21		xmetcl	$⊢ (D \in ∞Met (X) \land P \in X \land y \in X) \to P D y \in ℝ^{*}$
22	13 14 15 21	syl3anc	$⊢ (((D \in ∞Met (X) \land y \in X \land r \in ℝ^{}) \land P \in X) \land (z \in ℝ \land (y D P < z \land z < r))) \to P D y \in ℝ^{}$
23		rexr	$⊢ z \in ℝ \to z \in ℝ^{*}$
24	23	ad2antrl	$⊢ (((D \in ∞Met (X) \land y \in X \land r \in ℝ^{}) \land P \in X) \land (z \in ℝ \land (y D P < z \land z < r))) \to z \in ℝ^{}$
25	22 24 19	xrltled	$⊢ (((D \in ∞Met (X) \land y \in X \land r \in ℝ^{*}) \land P \in X) \land (z \in ℝ \land (y D P < z \land z < r))) \to P D y \leq z$
26		xmetlecl	$⊢ (D \in ∞Met (X) \land (P \in X \land y \in X) \land (z \in ℝ \land P D y \leq z)) \to P D y \in ℝ$
27	13 14 15 20 25 26	syl122anc	$⊢ (((D \in ∞Met (X) \land y \in X \land r \in ℝ^{*}) \land P \in X) \land (z \in ℝ \land (y D P < z \land z < r))) \to P D y \in ℝ$
28		difrp	$⊢ (P D y \in ℝ \land z \in ℝ) \to (P D y < z \leftrightarrow z - (P D y) \in ℝ^{+})$
29	27 20 28	syl2anc	$⊢ (((D \in ∞Met (X) \land y \in X \land r \in ℝ^{*}) \land P \in X) \land (z \in ℝ \land (y D P < z \land z < r))) \to (P D y < z \leftrightarrow z - (P D y) \in ℝ^{+})$
30	19 29	mpbid	$⊢ (((D \in ∞Met (X) \land y \in X \land r \in ℝ^{*}) \land P \in X) \land (z \in ℝ \land (y D P < z \land z < r))) \to z - (P D y) \in ℝ^{+}$
31	20 27	resubcld	$⊢ (((D \in ∞Met (X) \land y \in X \land r \in ℝ^{*}) \land P \in X) \land (z \in ℝ \land (y D P < z \land z < r))) \to z - (P D y) \in ℝ$
32	22	xrleidd	$⊢ (((D \in ∞Met (X) \land y \in X \land r \in ℝ^{*}) \land P \in X) \land (z \in ℝ \land (y D P < z \land z < r))) \to P D y \leq P D y$
33	20	recnd	$⊢ (((D \in ∞Met (X) \land y \in X \land r \in ℝ^{*}) \land P \in X) \land (z \in ℝ \land (y D P < z \land z < r))) \to z \in ℂ$
34	27	recnd	$⊢ (((D \in ∞Met (X) \land y \in X \land r \in ℝ^{*}) \land P \in X) \land (z \in ℝ \land (y D P < z \land z < r))) \to P D y \in ℂ$
35	33 34	nncand	$⊢ (((D \in ∞Met (X) \land y \in X \land r \in ℝ^{*}) \land P \in X) \land (z \in ℝ \land (y D P < z \land z < r))) \to z - (z - (P D y)) = P D y$
36	32 35	breqtrrd	$⊢ (((D \in ∞Met (X) \land y \in X \land r \in ℝ^{*}) \land P \in X) \land (z \in ℝ \land (y D P < z \land z < r))) \to P D y \leq z - (z - (P D y))$
37		blss2	$⊢ ((D \in ∞Met (X) \land P \in X \land y \in X) \land (z - (P D y) \in ℝ \land z \in ℝ \land P D y \leq z - (z - (P D y)))) \to P ball (D) (z - (P D y)) \subseteq y ball (D) z$
38	13 14 15 31 20 36 37	syl33anc	$⊢ (((D \in ∞Met (X) \land y \in X \land r \in ℝ^{*}) \land P \in X) \land (z \in ℝ \land (y D P < z \land z < r))) \to P ball (D) (z - (P D y)) \subseteq y ball (D) z$
39		simpll3	$⊢ (((D \in ∞Met (X) \land y \in X \land r \in ℝ^{}) \land P \in X) \land (z \in ℝ \land (y D P < z \land z < r))) \to r \in ℝ^{}$
40		simprrr	$⊢ (((D \in ∞Met (X) \land y \in X \land r \in ℝ^{*}) \land P \in X) \land (z \in ℝ \land (y D P < z \land z < r))) \to z < r$
41	24 39 40	xrltled	$⊢ (((D \in ∞Met (X) \land y \in X \land r \in ℝ^{*}) \land P \in X) \land (z \in ℝ \land (y D P < z \land z < r))) \to z \leq r$
42		ssbl	$⊢ ((D \in ∞Met (X) \land y \in X) \land (z \in ℝ^{} \land r \in ℝ^{}) \land z \leq r) \to y ball (D) z \subseteq y ball (D) r$
43	13 15 24 39 41 42	syl221anc	$⊢ (((D \in ∞Met (X) \land y \in X \land r \in ℝ^{*}) \land P \in X) \land (z \in ℝ \land (y D P < z \land z < r))) \to y ball (D) z \subseteq y ball (D) r$
44	38 43	sstrd	$⊢ (((D \in ∞Met (X) \land y \in X \land r \in ℝ^{*}) \land P \in X) \land (z \in ℝ \land (y D P < z \land z < r))) \to P ball (D) (z - (P D y)) \subseteq y ball (D) r$
45		oveq2	$⊢ x = z - (P D y) \to P ball (D) x = P ball (D) (z - (P D y))$
46	45	sseq1d	$⊢ x = z - (P D y) \to (P ball (D) x \subseteq y ball (D) r \leftrightarrow P ball (D) (z - (P D y)) \subseteq y ball (D) r)$
47	46	rspcev	$⊢ (z - (P D y) \in ℝ^{+} \land P ball (D) (z - (P D y)) \subseteq y ball (D) r) \to \exists x \in ℝ^{+} P ball (D) x \subseteq y ball (D) r$
48	30 44 47	syl2anc	$⊢ (((D \in ∞Met (X) \land y \in X \land r \in ℝ^{*}) \land P \in X) \land (z \in ℝ \land (y D P < z \land z < r))) \to \exists x \in ℝ^{+} P ball (D) x \subseteq y ball (D) r$
49	48	expr	$⊢ (((D \in ∞Met (X) \land y \in X \land r \in ℝ^{*}) \land P \in X) \land z \in ℝ) \to ((y D P < z \land z < r) \to \exists x \in ℝ^{+} P ball (D) x \subseteq y ball (D) r)$
50	12 49	sylan2	$⊢ (((D \in ∞Met (X) \land y \in X \land r \in ℝ^{*}) \land P \in X) \land z \in ℚ) \to ((y D P < z \land z < r) \to \exists x \in ℝ^{+} P ball (D) x \subseteq y ball (D) r)$
51	50	rexlimdva	$⊢ ((D \in ∞Met (X) \land y \in X \land r \in ℝ^{*}) \land P \in X) \to (\exists z \in ℚ (y D P < z \land z < r) \to \exists x \in ℝ^{+} P ball (D) x \subseteq y ball (D) r)$
52	11 51	syld	$⊢ ((D \in ∞Met (X) \land y \in X \land r \in ℝ^{*}) \land P \in X) \to (y D P < r \to \exists x \in ℝ^{+} P ball (D) x \subseteq y ball (D) r)$
53	52	expimpd	$⊢ (D \in ∞Met (X) \land y \in X \land r \in ℝ^{*}) \to ((P \in X \land y D P < r) \to \exists x \in ℝ^{+} P ball (D) x \subseteq y ball (D) r)$
54	2 53	sylbid	$⊢ (D \in ∞Met (X) \land y \in X \land r \in ℝ^{*}) \to (P \in (y ball (D) r) \to \exists x \in ℝ^{+} P ball (D) x \subseteq y ball (D) r)$
55		eleq2	$⊢ B = y ball (D) r \to (P \in B \leftrightarrow P \in (y ball (D) r))$
56		sseq2	$⊢ B = y ball (D) r \to (P ball (D) x \subseteq B \leftrightarrow P ball (D) x \subseteq y ball (D) r)$
57	56	rexbidv	$⊢ B = y ball (D) r \to (\exists x \in ℝ^{+} P ball (D) x \subseteq B \leftrightarrow \exists x \in ℝ^{+} P ball (D) x \subseteq y ball (D) r)$
58	55 57	imbi12d	$⊢ B = y ball (D) r \to ((P \in B \to \exists x \in ℝ^{+} P ball (D) x \subseteq B) \leftrightarrow (P \in (y ball (D) r) \to \exists x \in ℝ^{+} P ball (D) x \subseteq y ball (D) r))$
59	54 58	syl5ibrcom	$⊢ (D \in ∞Met (X) \land y \in X \land r \in ℝ^{*}) \to (B = y ball (D) r \to (P \in B \to \exists x \in ℝ^{+} P ball (D) x \subseteq B))$
60	59	3expib	$⊢ D \in ∞Met (X) \to ((y \in X \land r \in ℝ^{*}) \to (B = y ball (D) r \to (P \in B \to \exists x \in ℝ^{+} P ball (D) x \subseteq B)))$
61	60	rexlimdvv	$⊢ D \in ∞Met (X) \to (\exists y \in X \exists r \in ℝ^{*} B = y ball (D) r \to (P \in B \to \exists x \in ℝ^{+} P ball (D) x \subseteq B))$
62	1 61	sylbid	$⊢ D \in ∞Met (X) \to (B \in ran ball (D) \to (P \in B \to \exists x \in ℝ^{+} P ball (D) x \subseteq B))$
63	62	3imp	$⊢ (D \in ∞Met (X) \land B \in ran ball (D) \land P \in B) \to \exists x \in ℝ^{+} P ball (D) x \subseteq B$

Metamath Proof Explorer

Theorem blss

Proof