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