Theorem metres

Description: A restriction of a metric is a metric. (Contributed by NM, 26-Aug-2007) (Revised by Mario Carneiro, 14-Aug-2015)

	Ref	Expression
Assertion	metres	⊢ ( 𝐷 ∈ ( Met ‘ 𝑋 ) → ( 𝐷 ↾ ( 𝑅 × 𝑅 ) ) ∈ ( Met ‘ ( 𝑋 ∩ 𝑅 ) ) )

Proof

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