Metamath Proof Explorer

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 β€˜ 𝐡 ) )