Metamath Proof Explorer

Theorem xmetres2

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

Ref Expression
Assertion xmetres2 
|- ( ( D e. ( *Met ` X ) /\ R C_ X ) -> ( D |` ( R X. R ) ) e. ( *Met ` R ) )

Proof

Step Hyp Ref Expression
1 elfvdm 
 |-  ( D e. ( *Met ` X ) -> X e. dom *Met )
2 1 adantr 
 |-  ( ( D e. ( *Met ` X ) /\ R C_ X ) -> X e. dom *Met )
3 simpr 
 |-  ( ( D e. ( *Met ` X ) /\ R C_ X ) -> R C_ X )
4 2 3 ssexd 
 |-  ( ( D e. ( *Met ` X ) /\ R C_ X ) -> R e. _V )
5 xmetf 
 |-  ( D e. ( *Met ` X ) -> D : ( X X. X ) --> RR* )
6 5 adantr 
 |-  ( ( D e. ( *Met ` X ) /\ R C_ X ) -> D : ( X X. X ) --> RR* )
7 xpss12 
 |-  ( ( R C_ X /\ R C_ X ) -> ( R X. R ) C_ ( X X. X ) )
8 3 7 sylancom 
 |-  ( ( D e. ( *Met ` X ) /\ R C_ X ) -> ( R X. R ) C_ ( X X. X ) )
9 6 8 fssresd 
 |-  ( ( D e. ( *Met ` X ) /\ R C_ X ) -> ( D |` ( R X. R ) ) : ( R X. R ) --> RR* )
10 ovres 
 |-  ( ( x e. R /\ y e. R ) -> ( x ( D |` ( R X. R ) ) y ) = ( x D y ) )
11 10 adantl 
 |-  ( ( ( D e. ( *Met ` X ) /\ R C_ X ) /\ ( x e. R /\ y e. R ) ) -> ( x ( D |` ( R X. R ) ) y ) = ( x D y ) )
12 11 eqeq1d 
 |-  ( ( ( D e. ( *Met ` X ) /\ R C_ X ) /\ ( x e. R /\ y e. R ) ) -> ( ( x ( D |` ( R X. R ) ) y ) = 0 <-> ( x D y ) = 0 ) )
13 simpll 
 |-  ( ( ( D e. ( *Met ` X ) /\ R C_ X ) /\ ( x e. R /\ y e. R ) ) -> D e. ( *Met ` X ) )
14 simplr 
 |-  ( ( ( D e. ( *Met ` X ) /\ R C_ X ) /\ ( x e. R /\ y e. R ) ) -> R C_ X )
15 simprl 
 |-  ( ( ( D e. ( *Met ` X ) /\ R C_ X ) /\ ( x e. R /\ y e. R ) ) -> x e. R )
16 14 15 sseldd 
 |-  ( ( ( D e. ( *Met ` X ) /\ R C_ X ) /\ ( x e. R /\ y e. R ) ) -> x e. X )
17 simprr 
 |-  ( ( ( D e. ( *Met ` X ) /\ R C_ X ) /\ ( x e. R /\ y e. R ) ) -> y e. R )
18 14 17 sseldd 
 |-  ( ( ( D e. ( *Met ` X ) /\ R C_ X ) /\ ( x e. R /\ y e. R ) ) -> y e. X )
19 xmeteq0 
 |-  ( ( D e. ( *Met ` X ) /\ x e. X /\ y e. X ) -> ( ( x D y ) = 0 <-> x = y ) )
20 13 16 18 19 syl3anc 
 |-  ( ( ( D e. ( *Met ` X ) /\ R C_ X ) /\ ( x e. R /\ y e. R ) ) -> ( ( x D y ) = 0 <-> x = y ) )
21 12 20 bitrd 
 |-  ( ( ( D e. ( *Met ` X ) /\ R C_ X ) /\ ( x e. R /\ y e. R ) ) -> ( ( x ( D |` ( R X. R ) ) y ) = 0 <-> x = y ) )
22 simpll 
 |-  ( ( ( D e. ( *Met ` X ) /\ R C_ X ) /\ ( x e. R /\ y e. R /\ z e. R ) ) -> D e. ( *Met ` X ) )
23 simplr 
 |-  ( ( ( D e. ( *Met ` X ) /\ R C_ X ) /\ ( x e. R /\ y e. R /\ z e. R ) ) -> R C_ X )
24 simpr3 
 |-  ( ( ( D e. ( *Met ` X ) /\ R C_ X ) /\ ( x e. R /\ y e. R /\ z e. R ) ) -> z e. R )
25 23 24 sseldd 
 |-  ( ( ( D e. ( *Met ` X ) /\ R C_ X ) /\ ( x e. R /\ y e. R /\ z e. R ) ) -> z e. X )
26 16 3adantr3 
 |-  ( ( ( D e. ( *Met ` X ) /\ R C_ X ) /\ ( x e. R /\ y e. R /\ z e. R ) ) -> x e. X )
27 18 3adantr3 
 |-  ( ( ( D e. ( *Met ` X ) /\ R C_ X ) /\ ( x e. R /\ y e. R /\ z e. R ) ) -> y e. X )
28 xmettri2 
 |-  ( ( D e. ( *Met ` X ) /\ ( z e. X /\ x e. X /\ y e. X ) ) -> ( x D y ) <_ ( ( z D x ) +e ( z D y ) ) )
29 22 25 26 27 28 syl13anc 
 |-  ( ( ( D e. ( *Met ` X ) /\ R C_ X ) /\ ( x e. R /\ y e. R /\ z e. R ) ) -> ( x D y ) <_ ( ( z D x ) +e ( z D y ) ) )
30 11 3adantr3 
 |-  ( ( ( D e. ( *Met ` X ) /\ R C_ X ) /\ ( x e. R /\ y e. R /\ z e. R ) ) -> ( x ( D |` ( R X. R ) ) y ) = ( x D y ) )
31 simpr1 
 |-  ( ( ( D e. ( *Met ` X ) /\ R C_ X ) /\ ( x e. R /\ y e. R /\ z e. R ) ) -> x e. R )
32 24 31 ovresd 
 |-  ( ( ( D e. ( *Met ` X ) /\ R C_ X ) /\ ( x e. R /\ y e. R /\ z e. R ) ) -> ( z ( D |` ( R X. R ) ) x ) = ( z D x ) )
33 simpr2 
 |-  ( ( ( D e. ( *Met ` X ) /\ R C_ X ) /\ ( x e. R /\ y e. R /\ z e. R ) ) -> y e. R )
34 24 33 ovresd 
 |-  ( ( ( D e. ( *Met ` X ) /\ R C_ X ) /\ ( x e. R /\ y e. R /\ z e. R ) ) -> ( z ( D |` ( R X. R ) ) y ) = ( z D y ) )
35 32 34 oveq12d 
 |-  ( ( ( D e. ( *Met ` X ) /\ R C_ X ) /\ ( x e. R /\ y e. R /\ z e. R ) ) -> ( ( z ( D |` ( R X. R ) ) x ) +e ( z ( D |` ( R X. R ) ) y ) ) = ( ( z D x ) +e ( z D y ) ) )
36 29 30 35 3brtr4d 
 |-  ( ( ( D e. ( *Met ` X ) /\ R C_ X ) /\ ( x e. R /\ y e. R /\ z e. R ) ) -> ( x ( D |` ( R X. R ) ) y ) <_ ( ( z ( D |` ( R X. R ) ) x ) +e ( z ( D |` ( R X. R ) ) y ) ) )
37 4 9 21 36 isxmetd 
 |-  ( ( D e. ( *Met ` X ) /\ R C_ X ) -> ( D |` ( R X. R ) ) e. ( *Met ` R ) )