Metamath Proof Explorer

Theorem xmetres2

Description: Restriction of an extended metric. (Contributed by Mario Carneiro, 20-Aug-2015)

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

Proof

Step Hyp Ref Expression
1 elfvdm ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → 𝑋 ∈ dom ∞Met )
2 1 adantr ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑅 ⊆ 𝑋 ) → 𝑋 ∈ dom ∞Met )
3 simpr ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑅 ⊆ 𝑋 ) → 𝑅 ⊆ 𝑋 )
4 2 3 ssexd ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑅 ⊆ 𝑋 ) → 𝑅 ∈ V )
5 xmetf ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → 𝐷 : ( 𝑋 × 𝑋 ) ⟶ ℝ* )
6 5 adantr ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑅 ⊆ 𝑋 ) → 𝐷 : ( 𝑋 × 𝑋 ) ⟶ ℝ* )
7 xpss12 ⊢ ( ( 𝑅 ⊆ 𝑋 ∧ 𝑅 ⊆ 𝑋 ) → ( 𝑅 × 𝑅 ) ⊆ ( 𝑋 × 𝑋 ) )
8 3 7 sylancom ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑅 ⊆ 𝑋 ) → ( 𝑅 × 𝑅 ) ⊆ ( 𝑋 × 𝑋 ) )
9 6 8 fssresd ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑅 ⊆ 𝑋 ) → ( 𝐷 ↾ ( 𝑅 × 𝑅 ) ) : ( 𝑅 × 𝑅 ) ⟶ ℝ* )
10 ovres ⊢ ( ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅 ) → ( 𝑥 ( 𝐷 ↾ ( 𝑅 × 𝑅 ) ) 𝑦 ) = ( 𝑥 𝐷 𝑦 ) )
11 10 adantl ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑅 ⊆ 𝑋 ) ∧ ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅 ) ) → ( 𝑥 ( 𝐷 ↾ ( 𝑅 × 𝑅 ) ) 𝑦 ) = ( 𝑥 𝐷 𝑦 ) )
12 11 eqeq1d ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑅 ⊆ 𝑋 ) ∧ ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅 ) ) → ( ( 𝑥 ( 𝐷 ↾ ( 𝑅 × 𝑅 ) ) 𝑦 ) = 0 ↔ ( 𝑥 𝐷 𝑦 ) = 0 ) )
13 simpll ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑅 ⊆ 𝑋 ) ∧ ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅 ) ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
14 simplr ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑅 ⊆ 𝑋 ) ∧ ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅 ) ) → 𝑅 ⊆ 𝑋 )
15 simprl ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑅 ⊆ 𝑋 ) ∧ ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅 ) ) → 𝑥 ∈ 𝑅 )
16 14 15 sseldd ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑅 ⊆ 𝑋 ) ∧ ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅 ) ) → 𝑥 ∈ 𝑋 )
17 simprr ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑅 ⊆ 𝑋 ) ∧ ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅 ) ) → 𝑦 ∈ 𝑅 )
18 14 17 sseldd ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑅 ⊆ 𝑋 ) ∧ ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅 ) ) → 𝑦 ∈ 𝑋 )
19 xmeteq0 ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( ( 𝑥 𝐷 𝑦 ) = 0 ↔ 𝑥 = 𝑦 ) )
20 13 16 18 19 syl3anc ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑅 ⊆ 𝑋 ) ∧ ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅 ) ) → ( ( 𝑥 𝐷 𝑦 ) = 0 ↔ 𝑥 = 𝑦 ) )
21 12 20 bitrd ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑅 ⊆ 𝑋 ) ∧ ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅 ) ) → ( ( 𝑥 ( 𝐷 ↾ ( 𝑅 × 𝑅 ) ) 𝑦 ) = 0 ↔ 𝑥 = 𝑦 ) )
22 simpll ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑅 ⊆ 𝑋 ) ∧ ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅 ∧ 𝑧 ∈ 𝑅 ) ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
23 simplr ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑅 ⊆ 𝑋 ) ∧ ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅 ∧ 𝑧 ∈ 𝑅 ) ) → 𝑅 ⊆ 𝑋 )
24 simpr3 ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑅 ⊆ 𝑋 ) ∧ ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅 ∧ 𝑧 ∈ 𝑅 ) ) → 𝑧 ∈ 𝑅 )
25 23 24 sseldd ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑅 ⊆ 𝑋 ) ∧ ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅 ∧ 𝑧 ∈ 𝑅 ) ) → 𝑧 ∈ 𝑋 )
26 16 3adantr3 ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑅 ⊆ 𝑋 ) ∧ ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅 ∧ 𝑧 ∈ 𝑅 ) ) → 𝑥 ∈ 𝑋 )
27 18 3adantr3 ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑅 ⊆ 𝑋 ) ∧ ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅 ∧ 𝑧 ∈ 𝑅 ) ) → 𝑦 ∈ 𝑋 )
28 xmettri2 ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( 𝑥 𝐷 𝑦 ) ≤ ( ( 𝑧 𝐷 𝑥 ) +𝑒 ( 𝑧 𝐷 𝑦 ) ) )
29 22 25 26 27 28 syl13anc ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑅 ⊆ 𝑋 ) ∧ ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅 ∧ 𝑧 ∈ 𝑅 ) ) → ( 𝑥 𝐷 𝑦 ) ≤ ( ( 𝑧 𝐷 𝑥 ) +𝑒 ( 𝑧 𝐷 𝑦 ) ) )
30 11 3adantr3 ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑅 ⊆ 𝑋 ) ∧ ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅 ∧ 𝑧 ∈ 𝑅 ) ) → ( 𝑥 ( 𝐷 ↾ ( 𝑅 × 𝑅 ) ) 𝑦 ) = ( 𝑥 𝐷 𝑦 ) )
31 simpr1 ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑅 ⊆ 𝑋 ) ∧ ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅 ∧ 𝑧 ∈ 𝑅 ) ) → 𝑥 ∈ 𝑅 )
32 24 31 ovresd ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑅 ⊆ 𝑋 ) ∧ ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅 ∧ 𝑧 ∈ 𝑅 ) ) → ( 𝑧 ( 𝐷 ↾ ( 𝑅 × 𝑅 ) ) 𝑥 ) = ( 𝑧 𝐷 𝑥 ) )
33 simpr2 ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑅 ⊆ 𝑋 ) ∧ ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅 ∧ 𝑧 ∈ 𝑅 ) ) → 𝑦 ∈ 𝑅 )
34 24 33 ovresd ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑅 ⊆ 𝑋 ) ∧ ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅 ∧ 𝑧 ∈ 𝑅 ) ) → ( 𝑧 ( 𝐷 ↾ ( 𝑅 × 𝑅 ) ) 𝑦 ) = ( 𝑧 𝐷 𝑦 ) )
35 32 34 oveq12d ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑅 ⊆ 𝑋 ) ∧ ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅 ∧ 𝑧 ∈ 𝑅 ) ) → ( ( 𝑧 ( 𝐷 ↾ ( 𝑅 × 𝑅 ) ) 𝑥 ) +𝑒 ( 𝑧 ( 𝐷 ↾ ( 𝑅 × 𝑅 ) ) 𝑦 ) ) = ( ( 𝑧 𝐷 𝑥 ) +𝑒 ( 𝑧 𝐷 𝑦 ) ) )
36 29 30 35 3brtr4d ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑅 ⊆ 𝑋 ) ∧ ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅 ∧ 𝑧 ∈ 𝑅 ) ) → ( 𝑥 ( 𝐷 ↾ ( 𝑅 × 𝑅 ) ) 𝑦 ) ≤ ( ( 𝑧 ( 𝐷 ↾ ( 𝑅 × 𝑅 ) ) 𝑥 ) +𝑒 ( 𝑧 ( 𝐷 ↾ ( 𝑅 × 𝑅 ) ) 𝑦 ) ) )
37 4 9 21 36 isxmetd ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑅 ⊆ 𝑋 ) → ( 𝐷 ↾ ( 𝑅 × 𝑅 ) ) ∈ ( ∞Met ‘ 𝑅 ) )