xmetresbl

Description: An extended metric restricted to any ball (in particular the infinity ball) is a proper metric. Together with xmetec , this shows that any extended metric space can be "factored" into the disjoint union of proper metric spaces, with points in the same region measured by that region's metric, and points in different regions being distance +oo from each other. (Contributed by Mario Carneiro, 23-Aug-2015)

		Ref	Expression
	Hypothesis	xmetresbl.1	$⊢ B = P ball (D) R$
	Assertion	xmetresbl	$⊢ (D \in ∞Met (X) \land P \in X \land R \in ℝ^{*}) \to {D ↾}_{(B \times B)} \in Met (B)$

Proof

Step	Hyp	Ref	Expression
1		xmetresbl.1	$⊢ B = P ball (D) R$
2		simp1	$⊢ (D \in ∞Met (X) \land P \in X \land R \in ℝ^{*}) \to D \in ∞Met (X)$
3		blssm	$⊢ (D \in ∞Met (X) \land P \in X \land R \in ℝ^{*}) \to P ball (D) R \subseteq X$
4	1 3	eqsstrid	$⊢ (D \in ∞Met (X) \land P \in X \land R \in ℝ^{*}) \to B \subseteq X$
5		xmetres2	$⊢ (D \in ∞Met (X) \land B \subseteq X) \to {D ↾}_{(B \times B)} \in ∞Met (B)$
6	2 4 5	syl2anc	$⊢ (D \in ∞Met (X) \land P \in X \land R \in ℝ^{*}) \to {D ↾}_{(B \times B)} \in ∞Met (B)$
7		xmetf	$⊢ D \in ∞Met (X) \to D : X \times X ⟶ ℝ^{*}$
8	2 7	syl	$⊢ (D \in ∞Met (X) \land P \in X \land R \in ℝ^{}) \to D : X \times X ⟶ ℝ^{}$
9		xpss12	$⊢ (B \subseteq X \land B \subseteq X) \to B \times B \subseteq X \times X$
10	4 4 9	syl2anc	$⊢ (D \in ∞Met (X) \land P \in X \land R \in ℝ^{*}) \to B \times B \subseteq X \times X$
11	8 10	fssresd	$⊢ (D \in ∞Met (X) \land P \in X \land R \in ℝ^{}) \to ({D ↾}_{(B \times B)}) : B \times B ⟶ ℝ^{}$
12	11	ffnd	$⊢ (D \in ∞Met (X) \land P \in X \land R \in ℝ^{*}) \to ({D ↾}_{(B \times B)}) Fn (B \times B)$
13		ovres	$⊢ (x \in B \land y \in B) \to x ({D ↾}_{(B \times B)}) y = x D y$
14	13	adantl	$⊢ ((D \in ∞Met (X) \land P \in X \land R \in ℝ^{*}) \land (x \in B \land y \in B)) \to x ({D ↾}_{(B \times B)}) y = x D y$
15		simpl1	$⊢ ((D \in ∞Met (X) \land P \in X \land R \in ℝ^{*}) \land (x \in B \land y \in B)) \to D \in ∞Met (X)$
16		eqid	$⊢ D^{-1} [ℝ] = D^{-1} [ℝ]$
17	16	xmeter	$⊢ D \in ∞Met (X) \to D^{-1} [ℝ] Er X$
18	15 17	syl	$⊢ ((D \in ∞Met (X) \land P \in X \land R \in ℝ^{*}) \land (x \in B \land y \in B)) \to D^{-1} [ℝ] Er X$
19	16	blssec	$⊢ (D \in ∞Met (X) \land P \in X \land R \in ℝ^{*}) \to P ball (D) R \subseteq [P] D^{-1} [ℝ]$
20	1 19	eqsstrid	$⊢ (D \in ∞Met (X) \land P \in X \land R \in ℝ^{*}) \to B \subseteq [P] D^{-1} [ℝ]$
21	20	sselda	$⊢ ((D \in ∞Met (X) \land P \in X \land R \in ℝ^{*}) \land x \in B) \to x \in [P] D^{-1} [ℝ]$
22	21	adantrr	$⊢ ((D \in ∞Met (X) \land P \in X \land R \in ℝ^{*}) \land (x \in B \land y \in B)) \to x \in [P] D^{-1} [ℝ]$
23		simpl2	$⊢ ((D \in ∞Met (X) \land P \in X \land R \in ℝ^{*}) \land (x \in B \land y \in B)) \to P \in X$
24		elecg	$⊢ (x \in [P] D^{-1} [ℝ] \land P \in X) \to (x \in [P] D^{-1} [ℝ] \leftrightarrow P D^{-1} [ℝ] x)$
25	22 23 24	syl2anc	$⊢ ((D \in ∞Met (X) \land P \in X \land R \in ℝ^{*}) \land (x \in B \land y \in B)) \to (x \in [P] D^{-1} [ℝ] \leftrightarrow P D^{-1} [ℝ] x)$
26	22 25	mpbid	$⊢ ((D \in ∞Met (X) \land P \in X \land R \in ℝ^{*}) \land (x \in B \land y \in B)) \to P D^{-1} [ℝ] x$
27	20	sselda	$⊢ ((D \in ∞Met (X) \land P \in X \land R \in ℝ^{*}) \land y \in B) \to y \in [P] D^{-1} [ℝ]$
28	27	adantrl	$⊢ ((D \in ∞Met (X) \land P \in X \land R \in ℝ^{*}) \land (x \in B \land y \in B)) \to y \in [P] D^{-1} [ℝ]$
29		elecg	$⊢ (y \in [P] D^{-1} [ℝ] \land P \in X) \to (y \in [P] D^{-1} [ℝ] \leftrightarrow P D^{-1} [ℝ] y)$
30	28 23 29	syl2anc	$⊢ ((D \in ∞Met (X) \land P \in X \land R \in ℝ^{*}) \land (x \in B \land y \in B)) \to (y \in [P] D^{-1} [ℝ] \leftrightarrow P D^{-1} [ℝ] y)$
31	28 30	mpbid	$⊢ ((D \in ∞Met (X) \land P \in X \land R \in ℝ^{*}) \land (x \in B \land y \in B)) \to P D^{-1} [ℝ] y$
32	18 26 31	ertr3d	$⊢ ((D \in ∞Met (X) \land P \in X \land R \in ℝ^{*}) \land (x \in B \land y \in B)) \to x D^{-1} [ℝ] y$
33	16	xmeterval	$⊢ D \in ∞Met (X) \to (x D^{-1} [ℝ] y \leftrightarrow (x \in X \land y \in X \land x D y \in ℝ))$
34	15 33	syl	$⊢ ((D \in ∞Met (X) \land P \in X \land R \in ℝ^{*}) \land (x \in B \land y \in B)) \to (x D^{-1} [ℝ] y \leftrightarrow (x \in X \land y \in X \land x D y \in ℝ))$
35	32 34	mpbid	$⊢ ((D \in ∞Met (X) \land P \in X \land R \in ℝ^{*}) \land (x \in B \land y \in B)) \to (x \in X \land y \in X \land x D y \in ℝ)$
36	35	simp3d	$⊢ ((D \in ∞Met (X) \land P \in X \land R \in ℝ^{*}) \land (x \in B \land y \in B)) \to x D y \in ℝ$
37	14 36	eqeltrd	$⊢ ((D \in ∞Met (X) \land P \in X \land R \in ℝ^{*}) \land (x \in B \land y \in B)) \to x ({D ↾}_{(B \times B)}) y \in ℝ$
38	37	ralrimivva	$⊢ (D \in ∞Met (X) \land P \in X \land R \in ℝ^{*}) \to \forall x \in B \forall y \in B x ({D ↾}_{(B \times B)}) y \in ℝ$
39		ffnov	$⊢ ({D ↾}_{(B \times B)}) : B \times B ⟶ ℝ \leftrightarrow (({D ↾}_{(B \times B)}) Fn (B \times B) \land \forall x \in B \forall y \in B x ({D ↾}_{(B \times B)}) y \in ℝ)$
40	12 38 39	sylanbrc	$⊢ (D \in ∞Met (X) \land P \in X \land R \in ℝ^{*}) \to ({D ↾}_{(B \times B)}) : B \times B ⟶ ℝ$
41		ismet2	$⊢ {D ↾}_{(B \times B)} \in Met (B) \leftrightarrow ({D ↾}_{(B \times B)} \in ∞Met (B) \land ({D ↾}_{(B \times B)}) : B \times B ⟶ ℝ)$
42	6 40 41	sylanbrc	$⊢ (D \in ∞Met (X) \land P \in X \land R \in ℝ^{*}) \to {D ↾}_{(B \times B)} \in Met (B)$

Metamath Proof Explorer

Theorem xmetresbl

Proof