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

Metamath Proof Explorer

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 ‘ 𝑅 ) )