Metamath Proof Explorer

Theorem psmetres2

Description: Restriction of a pseudometric. (Contributed by Thierry Arnoux, 11-Feb-2018)

Ref Expression
Assertion psmetres2 ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑅 ⊆ 𝑋 ) → ( 𝐷 ↾ ( 𝑅 × 𝑅 ) ) ∈ ( PsMet ‘ 𝑅 ) )

Proof

Step Hyp Ref Expression
1 psmetf ⊢ ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → 𝐷 : ( 𝑋 × 𝑋 ) ⟶ ℝ* )
2 1 adantr ⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑅 ⊆ 𝑋 ) → 𝐷 : ( 𝑋 × 𝑋 ) ⟶ ℝ* )
3 simpr ⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑅 ⊆ 𝑋 ) → 𝑅 ⊆ 𝑋 )
4 xpss12 ⊢ ( ( 𝑅 ⊆ 𝑋 ∧ 𝑅 ⊆ 𝑋 ) → ( 𝑅 × 𝑅 ) ⊆ ( 𝑋 × 𝑋 ) )
5 3 3 4 syl2anc ⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑅 ⊆ 𝑋 ) → ( 𝑅 × 𝑅 ) ⊆ ( 𝑋 × 𝑋 ) )
6 2 5 fssresd ⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑅 ⊆ 𝑋 ) → ( 𝐷 ↾ ( 𝑅 × 𝑅 ) ) : ( 𝑅 × 𝑅 ) ⟶ ℝ* )
7 simpr ⊢ ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑅 ⊆ 𝑋 ) ∧ 𝑎 ∈ 𝑅 ) → 𝑎 ∈ 𝑅 )
8 7 7 ovresd ⊢ ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑅 ⊆ 𝑋 ) ∧ 𝑎 ∈ 𝑅 ) → ( 𝑎 ( 𝐷 ↾ ( 𝑅 × 𝑅 ) ) 𝑎 ) = ( 𝑎 𝐷 𝑎 ) )
9 simpll ⊢ ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑅 ⊆ 𝑋 ) ∧ 𝑎 ∈ 𝑅 ) → 𝐷 ∈ ( PsMet ‘ 𝑋 ) )
10 3 sselda ⊢ ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑅 ⊆ 𝑋 ) ∧ 𝑎 ∈ 𝑅 ) → 𝑎 ∈ 𝑋 )
11 psmet0 ⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑎 ∈ 𝑋 ) → ( 𝑎 𝐷 𝑎 ) = 0 )
12 9 10 11 syl2anc ⊢ ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑅 ⊆ 𝑋 ) ∧ 𝑎 ∈ 𝑅 ) → ( 𝑎 𝐷 𝑎 ) = 0 )
13 8 12 eqtrd ⊢ ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑅 ⊆ 𝑋 ) ∧ 𝑎 ∈ 𝑅 ) → ( 𝑎 ( 𝐷 ↾ ( 𝑅 × 𝑅 ) ) 𝑎 ) = 0 )
14 9 ad2antrr ⊢ ( ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑅 ⊆ 𝑋 ) ∧ 𝑎 ∈ 𝑅 ) ∧ 𝑏 ∈ 𝑅 ) ∧ 𝑐 ∈ 𝑅 ) → 𝐷 ∈ ( PsMet ‘ 𝑋 ) )
15 3 ad2antrr ⊢ ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑅 ⊆ 𝑋 ) ∧ 𝑎 ∈ 𝑅 ) ∧ 𝑏 ∈ 𝑅 ) → 𝑅 ⊆ 𝑋 )
16 15 sselda ⊢ ( ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑅 ⊆ 𝑋 ) ∧ 𝑎 ∈ 𝑅 ) ∧ 𝑏 ∈ 𝑅 ) ∧ 𝑐 ∈ 𝑅 ) → 𝑐 ∈ 𝑋 )
17 10 ad2antrr ⊢ ( ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑅 ⊆ 𝑋 ) ∧ 𝑎 ∈ 𝑅 ) ∧ 𝑏 ∈ 𝑅 ) ∧ 𝑐 ∈ 𝑅 ) → 𝑎 ∈ 𝑋 )
18 3 adantr ⊢ ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑅 ⊆ 𝑋 ) ∧ 𝑎 ∈ 𝑅 ) → 𝑅 ⊆ 𝑋 )
19 18 sselda ⊢ ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑅 ⊆ 𝑋 ) ∧ 𝑎 ∈ 𝑅 ) ∧ 𝑏 ∈ 𝑅 ) → 𝑏 ∈ 𝑋 )
20 19 adantr ⊢ ( ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑅 ⊆ 𝑋 ) ∧ 𝑎 ∈ 𝑅 ) ∧ 𝑏 ∈ 𝑅 ) ∧ 𝑐 ∈ 𝑅 ) → 𝑏 ∈ 𝑋 )
21 psmettri2 ⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ ( 𝑐 ∈ 𝑋 ∧ 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ) → ( 𝑎 𝐷 𝑏 ) ≤ ( ( 𝑐 𝐷 𝑎 ) +𝑒 ( 𝑐 𝐷 𝑏 ) ) )
22 14 16 17 20 21 syl13anc ⊢ ( ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑅 ⊆ 𝑋 ) ∧ 𝑎 ∈ 𝑅 ) ∧ 𝑏 ∈ 𝑅 ) ∧ 𝑐 ∈ 𝑅 ) → ( 𝑎 𝐷 𝑏 ) ≤ ( ( 𝑐 𝐷 𝑎 ) +𝑒 ( 𝑐 𝐷 𝑏 ) ) )
23 7 adantr ⊢ ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑅 ⊆ 𝑋 ) ∧ 𝑎 ∈ 𝑅 ) ∧ 𝑏 ∈ 𝑅 ) → 𝑎 ∈ 𝑅 )
24 simpr ⊢ ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑅 ⊆ 𝑋 ) ∧ 𝑎 ∈ 𝑅 ) ∧ 𝑏 ∈ 𝑅 ) → 𝑏 ∈ 𝑅 )
25 23 24 ovresd ⊢ ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑅 ⊆ 𝑋 ) ∧ 𝑎 ∈ 𝑅 ) ∧ 𝑏 ∈ 𝑅 ) → ( 𝑎 ( 𝐷 ↾ ( 𝑅 × 𝑅 ) ) 𝑏 ) = ( 𝑎 𝐷 𝑏 ) )
26 25 adantr ⊢ ( ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑅 ⊆ 𝑋 ) ∧ 𝑎 ∈ 𝑅 ) ∧ 𝑏 ∈ 𝑅 ) ∧ 𝑐 ∈ 𝑅 ) → ( 𝑎 ( 𝐷 ↾ ( 𝑅 × 𝑅 ) ) 𝑏 ) = ( 𝑎 𝐷 𝑏 ) )
27 simpr ⊢ ( ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑅 ⊆ 𝑋 ) ∧ 𝑎 ∈ 𝑅 ) ∧ 𝑏 ∈ 𝑅 ) ∧ 𝑐 ∈ 𝑅 ) → 𝑐 ∈ 𝑅 )
28 7 ad2antrr ⊢ ( ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑅 ⊆ 𝑋 ) ∧ 𝑎 ∈ 𝑅 ) ∧ 𝑏 ∈ 𝑅 ) ∧ 𝑐 ∈ 𝑅 ) → 𝑎 ∈ 𝑅 )
29 27 28 ovresd ⊢ ( ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑅 ⊆ 𝑋 ) ∧ 𝑎 ∈ 𝑅 ) ∧ 𝑏 ∈ 𝑅 ) ∧ 𝑐 ∈ 𝑅 ) → ( 𝑐 ( 𝐷 ↾ ( 𝑅 × 𝑅 ) ) 𝑎 ) = ( 𝑐 𝐷 𝑎 ) )
30 24 adantr ⊢ ( ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑅 ⊆ 𝑋 ) ∧ 𝑎 ∈ 𝑅 ) ∧ 𝑏 ∈ 𝑅 ) ∧ 𝑐 ∈ 𝑅 ) → 𝑏 ∈ 𝑅 )
31 27 30 ovresd ⊢ ( ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑅 ⊆ 𝑋 ) ∧ 𝑎 ∈ 𝑅 ) ∧ 𝑏 ∈ 𝑅 ) ∧ 𝑐 ∈ 𝑅 ) → ( 𝑐 ( 𝐷 ↾ ( 𝑅 × 𝑅 ) ) 𝑏 ) = ( 𝑐 𝐷 𝑏 ) )
32 29 31 oveq12d ⊢ ( ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑅 ⊆ 𝑋 ) ∧ 𝑎 ∈ 𝑅 ) ∧ 𝑏 ∈ 𝑅 ) ∧ 𝑐 ∈ 𝑅 ) → ( ( 𝑐 ( 𝐷 ↾ ( 𝑅 × 𝑅 ) ) 𝑎 ) +𝑒 ( 𝑐 ( 𝐷 ↾ ( 𝑅 × 𝑅 ) ) 𝑏 ) ) = ( ( 𝑐 𝐷 𝑎 ) +𝑒 ( 𝑐 𝐷 𝑏 ) ) )
33 22 26 32 3brtr4d ⊢ ( ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑅 ⊆ 𝑋 ) ∧ 𝑎 ∈ 𝑅 ) ∧ 𝑏 ∈ 𝑅 ) ∧ 𝑐 ∈ 𝑅 ) → ( 𝑎 ( 𝐷 ↾ ( 𝑅 × 𝑅 ) ) 𝑏 ) ≤ ( ( 𝑐 ( 𝐷 ↾ ( 𝑅 × 𝑅 ) ) 𝑎 ) +𝑒 ( 𝑐 ( 𝐷 ↾ ( 𝑅 × 𝑅 ) ) 𝑏 ) ) )
34 33 ralrimiva ⊢ ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑅 ⊆ 𝑋 ) ∧ 𝑎 ∈ 𝑅 ) ∧ 𝑏 ∈ 𝑅 ) → ∀ 𝑐 ∈ 𝑅 ( 𝑎 ( 𝐷 ↾ ( 𝑅 × 𝑅 ) ) 𝑏 ) ≤ ( ( 𝑐 ( 𝐷 ↾ ( 𝑅 × 𝑅 ) ) 𝑎 ) +𝑒 ( 𝑐 ( 𝐷 ↾ ( 𝑅 × 𝑅 ) ) 𝑏 ) ) )
35 34 ralrimiva ⊢ ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑅 ⊆ 𝑋 ) ∧ 𝑎 ∈ 𝑅 ) → ∀ 𝑏 ∈ 𝑅 ∀ 𝑐 ∈ 𝑅 ( 𝑎 ( 𝐷 ↾ ( 𝑅 × 𝑅 ) ) 𝑏 ) ≤ ( ( 𝑐 ( 𝐷 ↾ ( 𝑅 × 𝑅 ) ) 𝑎 ) +𝑒 ( 𝑐 ( 𝐷 ↾ ( 𝑅 × 𝑅 ) ) 𝑏 ) ) )
36 13 35 jca ⊢ ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑅 ⊆ 𝑋 ) ∧ 𝑎 ∈ 𝑅 ) → ( ( 𝑎 ( 𝐷 ↾ ( 𝑅 × 𝑅 ) ) 𝑎 ) = 0 ∧ ∀ 𝑏 ∈ 𝑅 ∀ 𝑐 ∈ 𝑅 ( 𝑎 ( 𝐷 ↾ ( 𝑅 × 𝑅 ) ) 𝑏 ) ≤ ( ( 𝑐 ( 𝐷 ↾ ( 𝑅 × 𝑅 ) ) 𝑎 ) +𝑒 ( 𝑐 ( 𝐷 ↾ ( 𝑅 × 𝑅 ) ) 𝑏 ) ) ) )
37 36 ralrimiva ⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑅 ⊆ 𝑋 ) → ∀ 𝑎 ∈ 𝑅 ( ( 𝑎 ( 𝐷 ↾ ( 𝑅 × 𝑅 ) ) 𝑎 ) = 0 ∧ ∀ 𝑏 ∈ 𝑅 ∀ 𝑐 ∈ 𝑅 ( 𝑎 ( 𝐷 ↾ ( 𝑅 × 𝑅 ) ) 𝑏 ) ≤ ( ( 𝑐 ( 𝐷 ↾ ( 𝑅 × 𝑅 ) ) 𝑎 ) +𝑒 ( 𝑐 ( 𝐷 ↾ ( 𝑅 × 𝑅 ) ) 𝑏 ) ) ) )
38 elfvex ⊢ ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → 𝑋 ∈ V )
39 38 adantr ⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑅 ⊆ 𝑋 ) → 𝑋 ∈ V )
40 39 3 ssexd ⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑅 ⊆ 𝑋 ) → 𝑅 ∈ V )
41 ispsmet ⊢ ( 𝑅 ∈ V → ( ( 𝐷 ↾ ( 𝑅 × 𝑅 ) ) ∈ ( PsMet ‘ 𝑅 ) ↔ ( ( 𝐷 ↾ ( 𝑅 × 𝑅 ) ) : ( 𝑅 × 𝑅 ) ⟶ ℝ* ∧ ∀ 𝑎 ∈ 𝑅 ( ( 𝑎 ( 𝐷 ↾ ( 𝑅 × 𝑅 ) ) 𝑎 ) = 0 ∧ ∀ 𝑏 ∈ 𝑅 ∀ 𝑐 ∈ 𝑅 ( 𝑎 ( 𝐷 ↾ ( 𝑅 × 𝑅 ) ) 𝑏 ) ≤ ( ( 𝑐 ( 𝐷 ↾ ( 𝑅 × 𝑅 ) ) 𝑎 ) +𝑒 ( 𝑐 ( 𝐷 ↾ ( 𝑅 × 𝑅 ) ) 𝑏 ) ) ) ) ) )
42 40 41 syl ⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑅 ⊆ 𝑋 ) → ( ( 𝐷 ↾ ( 𝑅 × 𝑅 ) ) ∈ ( PsMet ‘ 𝑅 ) ↔ ( ( 𝐷 ↾ ( 𝑅 × 𝑅 ) ) : ( 𝑅 × 𝑅 ) ⟶ ℝ* ∧ ∀ 𝑎 ∈ 𝑅 ( ( 𝑎 ( 𝐷 ↾ ( 𝑅 × 𝑅 ) ) 𝑎 ) = 0 ∧ ∀ 𝑏 ∈ 𝑅 ∀ 𝑐 ∈ 𝑅 ( 𝑎 ( 𝐷 ↾ ( 𝑅 × 𝑅 ) ) 𝑏 ) ≤ ( ( 𝑐 ( 𝐷 ↾ ( 𝑅 × 𝑅 ) ) 𝑎 ) +𝑒 ( 𝑐 ( 𝐷 ↾ ( 𝑅 × 𝑅 ) ) 𝑏 ) ) ) ) ) )
43 6 37 42 mpbir2and ⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑅 ⊆ 𝑋 ) → ( 𝐷 ↾ ( 𝑅 × 𝑅 ) ) ∈ ( PsMet ‘ 𝑅 ) )