blssp

Description: A ball in the subspace metric. (Contributed by Jeff Madsen, 2-Sep-2009) (Revised by Mario Carneiro, 5-Jan-2014)

		Ref	Expression
	Hypothesis	blssp.2	$⊢ N = {M ↾}_{(S \times S)}$
	Assertion	blssp	$⊢ ((M \in Met (X) \land S \subseteq X) \land (Y \in S \land R \in ℝ^{+})) \to Y ball (N) R = (Y ball (M) R) \cap S$

Step	Hyp	Ref	Expression
1		blssp.2	$⊢ N = {M ↾}_{(S \times S)}$
2		metxmet	$⊢ M \in Met (X) \to M \in ∞Met (X)$
3	2	ad2antrr	$⊢ ((M \in Met (X) \land S \subseteq X) \land (Y \in S \land R \in ℝ^{+})) \to M \in ∞Met (X)$
4		simprl	$⊢ ((M \in Met (X) \land S \subseteq X) \land (Y \in S \land R \in ℝ^{+})) \to Y \in S$
5		simplr	$⊢ ((M \in Met (X) \land S \subseteq X) \land (Y \in S \land R \in ℝ^{+})) \to S \subseteq X$
6		sseqin2	$⊢ S \subseteq X \leftrightarrow X \cap S = S$
7	5 6	sylib	$⊢ ((M \in Met (X) \land S \subseteq X) \land (Y \in S \land R \in ℝ^{+})) \to X \cap S = S$
8	4 7	eleqtrrd	$⊢ ((M \in Met (X) \land S \subseteq X) \land (Y \in S \land R \in ℝ^{+})) \to Y \in (X \cap S)$
9		rpxr	$⊢ R \in ℝ^{+} \to R \in ℝ^{*}$
10	9	ad2antll	$⊢ ((M \in Met (X) \land S \subseteq X) \land (Y \in S \land R \in ℝ^{+})) \to R \in ℝ^{*}$
11	1	blres	$⊢ (M \in ∞Met (X) \land Y \in (X \cap S) \land R \in ℝ^{*}) \to Y ball (N) R = (Y ball (M) R) \cap S$
12	3 8 10 11	syl3anc	$⊢ ((M \in Met (X) \land S \subseteq X) \land (Y \in S \land R \in ℝ^{+})) \to Y ball (N) R = (Y ball (M) R) \cap S$

Metamath Proof Explorer