Theorem 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	⊢ 𝐵 = ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 )
Assertion	xmetresbl	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) → ( 𝐷 ↾ ( 𝐵 × 𝐵 ) ) ∈ ( Met ‘ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		xmetresbl.1	⊢ 𝐵 = ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 )
2		simp1	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
3		blssm	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) → ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ⊆ 𝑋 )
4	1 3	eqsstrid	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) → 𝐵 ⊆ 𝑋 )
5		xmetres2	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐵 ⊆ 𝑋 ) → ( 𝐷 ↾ ( 𝐵 × 𝐵 ) ) ∈ ( ∞Met ‘ 𝐵 ) )
6	2 4 5	syl2anc	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) → ( 𝐷 ↾ ( 𝐵 × 𝐵 ) ) ∈ ( ∞Met ‘ 𝐵 ) )
7		xmetf	⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → 𝐷 : ( 𝑋 × 𝑋 ) ⟶ ℝ* )
8	2 7	syl	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) → 𝐷 : ( 𝑋 × 𝑋 ) ⟶ ℝ* )
9		xpss12	⊢ ( ( 𝐵 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑋 ) → ( 𝐵 × 𝐵 ) ⊆ ( 𝑋 × 𝑋 ) )
10	4 4 9	syl2anc	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) → ( 𝐵 × 𝐵 ) ⊆ ( 𝑋 × 𝑋 ) )
11	8 10	fssresd	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) → ( 𝐷 ↾ ( 𝐵 × 𝐵 ) ) : ( 𝐵 × 𝐵 ) ⟶ ℝ* )
12	11	ffnd	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) → ( 𝐷 ↾ ( 𝐵 × 𝐵 ) ) Fn ( 𝐵 × 𝐵 ) )
13		ovres	⊢ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑥 ( 𝐷 ↾ ( 𝐵 × 𝐵 ) ) 𝑦 ) = ( 𝑥 𝐷 𝑦 ) )
14	13	adantl	⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ( 𝐷 ↾ ( 𝐵 × 𝐵 ) ) 𝑦 ) = ( 𝑥 𝐷 𝑦 ) )
15		simpl1	⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
16		eqid	⊢ ( ◡ 𝐷 “ ℝ ) = ( ◡ 𝐷 “ ℝ )
17	16	xmeter	⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ( ◡ 𝐷 “ ℝ ) Er 𝑋 )
18	15 17	syl	⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( ◡ 𝐷 “ ℝ ) Er 𝑋 )
19	16	blssec	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) → ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ⊆ [ 𝑃 ] ( ◡ 𝐷 “ ℝ ) )
20	1 19	eqsstrid	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) → 𝐵 ⊆ [ 𝑃 ] ( ◡ 𝐷 “ ℝ ) )
21	20	sselda	⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) ∧ 𝑥 ∈ 𝐵 ) → 𝑥 ∈ [ 𝑃 ] ( ◡ 𝐷 “ ℝ ) )
22	21	adantrr	⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → 𝑥 ∈ [ 𝑃 ] ( ◡ 𝐷 “ ℝ ) )
23		simpl2	⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → 𝑃 ∈ 𝑋 )
24		elecg	⊢ ( ( 𝑥 ∈ [ 𝑃 ] ( ◡ 𝐷 “ ℝ ) ∧ 𝑃 ∈ 𝑋 ) → ( 𝑥 ∈ [ 𝑃 ] ( ◡ 𝐷 “ ℝ ) ↔ 𝑃 ( ◡ 𝐷 “ ℝ ) 𝑥 ) )
25	22 23 24	syl2anc	⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ∈ [ 𝑃 ] ( ◡ 𝐷 “ ℝ ) ↔ 𝑃 ( ◡ 𝐷 “ ℝ ) 𝑥 ) )
26	22 25	mpbid	⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → 𝑃 ( ◡ 𝐷 “ ℝ ) 𝑥 )
27	20	sselda	⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) ∧ 𝑦 ∈ 𝐵 ) → 𝑦 ∈ [ 𝑃 ] ( ◡ 𝐷 “ ℝ ) )
28	27	adantrl	⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → 𝑦 ∈ [ 𝑃 ] ( ◡ 𝐷 “ ℝ ) )
29		elecg	⊢ ( ( 𝑦 ∈ [ 𝑃 ] ( ◡ 𝐷 “ ℝ ) ∧ 𝑃 ∈ 𝑋 ) → ( 𝑦 ∈ [ 𝑃 ] ( ◡ 𝐷 “ ℝ ) ↔ 𝑃 ( ◡ 𝐷 “ ℝ ) 𝑦 ) )
30	28 23 29	syl2anc	⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑦 ∈ [ 𝑃 ] ( ◡ 𝐷 “ ℝ ) ↔ 𝑃 ( ◡ 𝐷 “ ℝ ) 𝑦 ) )
31	28 30	mpbid	⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → 𝑃 ( ◡ 𝐷 “ ℝ ) 𝑦 )
32	18 26 31	ertr3d	⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → 𝑥 ( ◡ 𝐷 “ ℝ ) 𝑦 )
33	16	xmeterval	⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ( 𝑥 ( ◡ 𝐷 “ ℝ ) 𝑦 ↔ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ ( 𝑥 𝐷 𝑦 ) ∈ ℝ ) ) )
34	15 33	syl	⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ( ◡ 𝐷 “ ℝ ) 𝑦 ↔ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ ( 𝑥 𝐷 𝑦 ) ∈ ℝ ) ) )
35	32 34	mpbid	⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ ( 𝑥 𝐷 𝑦 ) ∈ ℝ ) )
36	35	simp3d	⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 𝐷 𝑦 ) ∈ ℝ )
37	14 36	eqeltrd	⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ( 𝐷 ↾ ( 𝐵 × 𝐵 ) ) 𝑦 ) ∈ ℝ )
38	37	ralrimivva	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) → ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( 𝐷 ↾ ( 𝐵 × 𝐵 ) ) 𝑦 ) ∈ ℝ )
39		ffnov	⊢ ( ( 𝐷 ↾ ( 𝐵 × 𝐵 ) ) : ( 𝐵 × 𝐵 ) ⟶ ℝ ↔ ( ( 𝐷 ↾ ( 𝐵 × 𝐵 ) ) Fn ( 𝐵 × 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( 𝐷 ↾ ( 𝐵 × 𝐵 ) ) 𝑦 ) ∈ ℝ ) )
40	12 38 39	sylanbrc	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) → ( 𝐷 ↾ ( 𝐵 × 𝐵 ) ) : ( 𝐵 × 𝐵 ) ⟶ ℝ )
41		ismet2	⊢ ( ( 𝐷 ↾ ( 𝐵 × 𝐵 ) ) ∈ ( Met ‘ 𝐵 ) ↔ ( ( 𝐷 ↾ ( 𝐵 × 𝐵 ) ) ∈ ( ∞Met ‘ 𝐵 ) ∧ ( 𝐷 ↾ ( 𝐵 × 𝐵 ) ) : ( 𝐵 × 𝐵 ) ⟶ ℝ ) )
42	6 40 41	sylanbrc	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) → ( 𝐷 ↾ ( 𝐵 × 𝐵 ) ) ∈ ( Met ‘ 𝐵 ) )