This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem xmetres

Description: A restriction of an extended metric is an extended metric. (Contributed by Mario Carneiro, 24-Aug-2015)

Ref Expression
Assertion xmetres ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ( 𝐷 ↾ ( 𝑅 × 𝑅 ) ) ∈ ( ∞Met ‘ ( 𝑋 ∩ 𝑅 ) ) )

Proof

Step Hyp Ref Expression
1 xmetf ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → 𝐷 : ( 𝑋 × 𝑋 ) ⟶ ℝ* )
2 fdm ⊢ ( 𝐷 : ( 𝑋 × 𝑋 ) ⟶ ℝ* → dom 𝐷 = ( 𝑋 × 𝑋 ) )
3 metreslem ⊢ ( dom 𝐷 = ( 𝑋 × 𝑋 ) → ( 𝐷 ↾ ( 𝑅 × 𝑅 ) ) = ( 𝐷 ↾ ( ( 𝑋 ∩ 𝑅 ) × ( 𝑋 ∩ 𝑅 ) ) ) )
4 1 2 3 3syl ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ( 𝐷 ↾ ( 𝑅 × 𝑅 ) ) = ( 𝐷 ↾ ( ( 𝑋 ∩ 𝑅 ) × ( 𝑋 ∩ 𝑅 ) ) ) )
5 inss1 ⊢ ( 𝑋 ∩ 𝑅 ) ⊆ 𝑋
6 xmetres2 ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝑋 ∩ 𝑅 ) ⊆ 𝑋 ) → ( 𝐷 ↾ ( ( 𝑋 ∩ 𝑅 ) × ( 𝑋 ∩ 𝑅 ) ) ) ∈ ( ∞Met ‘ ( 𝑋 ∩ 𝑅 ) ) )
7 5 6 mpan2 ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ( 𝐷 ↾ ( ( 𝑋 ∩ 𝑅 ) × ( 𝑋 ∩ 𝑅 ) ) ) ∈ ( ∞Met ‘ ( 𝑋 ∩ 𝑅 ) ) )
8 4 7 eqeltrd ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ( 𝐷 ↾ ( 𝑅 × 𝑅 ) ) ∈ ( ∞Met ‘ ( 𝑋 ∩ 𝑅 ) ) )