Metamath Proof Explorer


Theorem psmetres2

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

Ref Expression
Assertion psmetres2 D PsMet X R X D R × R PsMet R

Proof

Step Hyp Ref Expression
1 psmetf D PsMet X D : X × X *
2 1 adantr D PsMet X R X D : X × X *
3 simpr D PsMet X R X R X
4 xpss12 R X R X R × R X × X
5 3 3 4 syl2anc D PsMet X R X R × R X × X
6 2 5 fssresd D PsMet X R X D R × R : R × R *
7 simpr D PsMet X R X a R a R
8 7 7 ovresd D PsMet X R X a R a D R × R a = a D a
9 simpll D PsMet X R X a R D PsMet X
10 3 sselda D PsMet X R X a R a X
11 psmet0 D PsMet X a X a D a = 0
12 9 10 11 syl2anc D PsMet X R X a R a D a = 0
13 8 12 eqtrd D PsMet X R X a R a D R × R a = 0
14 9 ad2antrr D PsMet X R X a R b R c R D PsMet X
15 3 ad2antrr D PsMet X R X a R b R R X
16 15 sselda D PsMet X R X a R b R c R c X
17 10 ad2antrr D PsMet X R X a R b R c R a X
18 3 adantr D PsMet X R X a R R X
19 18 sselda D PsMet X R X a R b R b X
20 19 adantr D PsMet X R X a R b R c R b X
21 psmettri2 D PsMet X c X a X b X a D b c D a + 𝑒 c D b
22 14 16 17 20 21 syl13anc D PsMet X R X a R b R c R a D b c D a + 𝑒 c D b
23 7 adantr D PsMet X R X a R b R a R
24 simpr D PsMet X R X a R b R b R
25 23 24 ovresd D PsMet X R X a R b R a D R × R b = a D b
26 25 adantr D PsMet X R X a R b R c R a D R × R b = a D b
27 simpr D PsMet X R X a R b R c R c R
28 7 ad2antrr D PsMet X R X a R b R c R a R
29 27 28 ovresd D PsMet X R X a R b R c R c D R × R a = c D a
30 24 adantr D PsMet X R X a R b R c R b R
31 27 30 ovresd D PsMet X R X a R b R c R c D R × R b = c D b
32 29 31 oveq12d D PsMet X R X a R b R c R c D R × R a + 𝑒 c D R × R b = c D a + 𝑒 c D b
33 22 26 32 3brtr4d D PsMet X R X a R b R c R a D R × R b c D R × R a + 𝑒 c D R × R b
34 33 ralrimiva D PsMet X R X a R b R c R a D R × R b c D R × R a + 𝑒 c D R × R b
35 34 ralrimiva D PsMet X R X a R b R c R a D R × R b c D R × R a + 𝑒 c D R × R b
36 13 35 jca D PsMet X R X a R a D R × R a = 0 b R c R a D R × R b c D R × R a + 𝑒 c D R × R b
37 36 ralrimiva D PsMet X R X a R a D R × R a = 0 b R c R a D R × R b c D R × R a + 𝑒 c D R × R b
38 elfvex D PsMet X X V
39 38 adantr D PsMet X R X X V
40 39 3 ssexd D PsMet X R X R V
41 ispsmet R V D R × R PsMet R D R × R : R × R * a R a D R × R a = 0 b R c R a D R × R b c D R × R a + 𝑒 c D R × R b
42 40 41 syl D PsMet X R X D R × R PsMet R D R × R : R × R * a R a D R × R a = 0 b R c R a D R × R b c D R × R a + 𝑒 c D R × R b
43 6 37 42 mpbir2and D PsMet X R X D R × R PsMet R