Metamath Proof Explorer


Theorem psmetres2

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

Ref Expression
Assertion psmetres2 DPsMetXRXDR×RPsMetR

Proof

Step Hyp Ref Expression
1 psmetf DPsMetXD:X×X*
2 1 adantr DPsMetXRXD:X×X*
3 simpr DPsMetXRXRX
4 xpss12 RXRXR×RX×X
5 3 3 4 syl2anc DPsMetXRXR×RX×X
6 2 5 fssresd DPsMetXRXDR×R:R×R*
7 simpr DPsMetXRXaRaR
8 7 7 ovresd DPsMetXRXaRaDR×Ra=aDa
9 simpll DPsMetXRXaRDPsMetX
10 3 sselda DPsMetXRXaRaX
11 psmet0 DPsMetXaXaDa=0
12 9 10 11 syl2anc DPsMetXRXaRaDa=0
13 8 12 eqtrd DPsMetXRXaRaDR×Ra=0
14 9 ad2antrr DPsMetXRXaRbRcRDPsMetX
15 3 ad2antrr DPsMetXRXaRbRRX
16 15 sselda DPsMetXRXaRbRcRcX
17 10 ad2antrr DPsMetXRXaRbRcRaX
18 3 adantr DPsMetXRXaRRX
19 18 sselda DPsMetXRXaRbRbX
20 19 adantr DPsMetXRXaRbRcRbX
21 psmettri2 DPsMetXcXaXbXaDbcDa+𝑒cDb
22 14 16 17 20 21 syl13anc DPsMetXRXaRbRcRaDbcDa+𝑒cDb
23 7 adantr DPsMetXRXaRbRaR
24 simpr DPsMetXRXaRbRbR
25 23 24 ovresd DPsMetXRXaRbRaDR×Rb=aDb
26 25 adantr DPsMetXRXaRbRcRaDR×Rb=aDb
27 simpr DPsMetXRXaRbRcRcR
28 7 ad2antrr DPsMetXRXaRbRcRaR
29 27 28 ovresd DPsMetXRXaRbRcRcDR×Ra=cDa
30 24 adantr DPsMetXRXaRbRcRbR
31 27 30 ovresd DPsMetXRXaRbRcRcDR×Rb=cDb
32 29 31 oveq12d DPsMetXRXaRbRcRcDR×Ra+𝑒cDR×Rb=cDa+𝑒cDb
33 22 26 32 3brtr4d DPsMetXRXaRbRcRaDR×RbcDR×Ra+𝑒cDR×Rb
34 33 ralrimiva DPsMetXRXaRbRcRaDR×RbcDR×Ra+𝑒cDR×Rb
35 34 ralrimiva DPsMetXRXaRbRcRaDR×RbcDR×Ra+𝑒cDR×Rb
36 13 35 jca DPsMetXRXaRaDR×Ra=0bRcRaDR×RbcDR×Ra+𝑒cDR×Rb
37 36 ralrimiva DPsMetXRXaRaDR×Ra=0bRcRaDR×RbcDR×Ra+𝑒cDR×Rb
38 elfvex DPsMetXXV
39 38 adantr DPsMetXRXXV
40 39 3 ssexd DPsMetXRXRV
41 ispsmet RVDR×RPsMetRDR×R:R×R*aRaDR×Ra=0bRcRaDR×RbcDR×Ra+𝑒cDR×Rb
42 40 41 syl DPsMetXRXDR×RPsMetRDR×R:R×R*aRaDR×Ra=0bRcRaDR×RbcDR×Ra+𝑒cDR×Rb
43 6 37 42 mpbir2and DPsMetXRXDR×RPsMetR