Theorem metres2

Description: Lemma for metres . (Contributed by FL, 12-Oct-2006) (Proof shortened by Mario Carneiro, 14-Aug-2015)

	Ref	Expression
Assertion	metres2	⊢ ( ( 𝐷 ∈ ( Met ‘ 𝑋 ) ∧ 𝑅 ⊆ 𝑋 ) → ( 𝐷 ↾ ( 𝑅 × 𝑅 ) ) ∈ ( Met ‘ 𝑅 ) )

Proof

Step	Hyp	Ref	Expression
1		metxmet	⊢ ( 𝐷 ∈ ( Met ‘ 𝑋 ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
2		xmetres2	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑅 ⊆ 𝑋 ) → ( 𝐷 ↾ ( 𝑅 × 𝑅 ) ) ∈ ( ∞Met ‘ 𝑅 ) )
3	1 2	sylan	⊢ ( ( 𝐷 ∈ ( Met ‘ 𝑋 ) ∧ 𝑅 ⊆ 𝑋 ) → ( 𝐷 ↾ ( 𝑅 × 𝑅 ) ) ∈ ( ∞Met ‘ 𝑅 ) )
4		metf	⊢ ( 𝐷 ∈ ( Met ‘ 𝑋 ) → 𝐷 : ( 𝑋 × 𝑋 ) ⟶ ℝ )
5	4	adantr	⊢ ( ( 𝐷 ∈ ( Met ‘ 𝑋 ) ∧ 𝑅 ⊆ 𝑋 ) → 𝐷 : ( 𝑋 × 𝑋 ) ⟶ ℝ )
6		simpr	⊢ ( ( 𝐷 ∈ ( Met ‘ 𝑋 ) ∧ 𝑅 ⊆ 𝑋 ) → 𝑅 ⊆ 𝑋 )
7		xpss12	⊢ ( ( 𝑅 ⊆ 𝑋 ∧ 𝑅 ⊆ 𝑋 ) → ( 𝑅 × 𝑅 ) ⊆ ( 𝑋 × 𝑋 ) )
8	6 7	sylancom	⊢ ( ( 𝐷 ∈ ( Met ‘ 𝑋 ) ∧ 𝑅 ⊆ 𝑋 ) → ( 𝑅 × 𝑅 ) ⊆ ( 𝑋 × 𝑋 ) )
9	5 8	fssresd	⊢ ( ( 𝐷 ∈ ( Met ‘ 𝑋 ) ∧ 𝑅 ⊆ 𝑋 ) → ( 𝐷 ↾ ( 𝑅 × 𝑅 ) ) : ( 𝑅 × 𝑅 ) ⟶ ℝ )
10		ismet2	⊢ ( ( 𝐷 ↾ ( 𝑅 × 𝑅 ) ) ∈ ( Met ‘ 𝑅 ) ↔ ( ( 𝐷 ↾ ( 𝑅 × 𝑅 ) ) ∈ ( ∞Met ‘ 𝑅 ) ∧ ( 𝐷 ↾ ( 𝑅 × 𝑅 ) ) : ( 𝑅 × 𝑅 ) ⟶ ℝ ) )
11	3 9 10	sylanbrc	⊢ ( ( 𝐷 ∈ ( Met ‘ 𝑋 ) ∧ 𝑅 ⊆ 𝑋 ) → ( 𝐷 ↾ ( 𝑅 × 𝑅 ) ) ∈ ( Met ‘ 𝑅 ) )