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 ‘ ( 𝑋 ∩ 𝑅 ) ) )