Metamath Proof Explorer

Theorem psmetres2

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

Ref Expression
Assertion psmetres2 
|- ( ( D e. ( PsMet ` X ) /\ R C_ X ) -> ( D |` ( R X. R ) ) e. ( PsMet ` R ) )

Proof

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