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 ) )