Step |
Hyp |
Ref |
Expression |
1 |
|
elfvdm |
|- ( D e. ( *Met ` X ) -> X e. dom *Met ) |
2 |
|
isxmet |
|- ( X e. dom *Met -> ( D e. ( *Met ` X ) <-> ( D : ( X X. X ) --> RR* /\ A. x e. X A. y e. X ( ( ( x D y ) = 0 <-> x = y ) /\ A. z e. X ( x D y ) <_ ( ( z D x ) +e ( z D y ) ) ) ) ) ) |
3 |
1 2
|
syl |
|- ( D e. ( *Met ` X ) -> ( D e. ( *Met ` X ) <-> ( D : ( X X. X ) --> RR* /\ A. x e. X A. y e. X ( ( ( x D y ) = 0 <-> x = y ) /\ A. z e. X ( x D y ) <_ ( ( z D x ) +e ( z D y ) ) ) ) ) ) |
4 |
3
|
ibi |
|- ( D e. ( *Met ` X ) -> ( D : ( X X. X ) --> RR* /\ A. x e. X A. y e. X ( ( ( x D y ) = 0 <-> x = y ) /\ A. z e. X ( x D y ) <_ ( ( z D x ) +e ( z D y ) ) ) ) ) |
5 |
|
simpr |
|- ( ( ( ( x D y ) = 0 <-> x = y ) /\ A. z e. X ( x D y ) <_ ( ( z D x ) +e ( z D y ) ) ) -> A. z e. X ( x D y ) <_ ( ( z D x ) +e ( z D y ) ) ) |
6 |
5
|
2ralimi |
|- ( A. x e. X A. y e. X ( ( ( x D y ) = 0 <-> x = y ) /\ A. z e. X ( x D y ) <_ ( ( z D x ) +e ( z D y ) ) ) -> A. x e. X A. y e. X A. z e. X ( x D y ) <_ ( ( z D x ) +e ( z D y ) ) ) |
7 |
4 6
|
simpl2im |
|- ( D e. ( *Met ` X ) -> A. x e. X A. y e. X A. z e. X ( x D y ) <_ ( ( z D x ) +e ( z D y ) ) ) |
8 |
|
oveq1 |
|- ( x = A -> ( x D y ) = ( A D y ) ) |
9 |
|
oveq2 |
|- ( x = A -> ( z D x ) = ( z D A ) ) |
10 |
9
|
oveq1d |
|- ( x = A -> ( ( z D x ) +e ( z D y ) ) = ( ( z D A ) +e ( z D y ) ) ) |
11 |
8 10
|
breq12d |
|- ( x = A -> ( ( x D y ) <_ ( ( z D x ) +e ( z D y ) ) <-> ( A D y ) <_ ( ( z D A ) +e ( z D y ) ) ) ) |
12 |
|
oveq2 |
|- ( y = B -> ( A D y ) = ( A D B ) ) |
13 |
|
oveq2 |
|- ( y = B -> ( z D y ) = ( z D B ) ) |
14 |
13
|
oveq2d |
|- ( y = B -> ( ( z D A ) +e ( z D y ) ) = ( ( z D A ) +e ( z D B ) ) ) |
15 |
12 14
|
breq12d |
|- ( y = B -> ( ( A D y ) <_ ( ( z D A ) +e ( z D y ) ) <-> ( A D B ) <_ ( ( z D A ) +e ( z D B ) ) ) ) |
16 |
|
oveq1 |
|- ( z = C -> ( z D A ) = ( C D A ) ) |
17 |
|
oveq1 |
|- ( z = C -> ( z D B ) = ( C D B ) ) |
18 |
16 17
|
oveq12d |
|- ( z = C -> ( ( z D A ) +e ( z D B ) ) = ( ( C D A ) +e ( C D B ) ) ) |
19 |
18
|
breq2d |
|- ( z = C -> ( ( A D B ) <_ ( ( z D A ) +e ( z D B ) ) <-> ( A D B ) <_ ( ( C D A ) +e ( C D B ) ) ) ) |
20 |
11 15 19
|
rspc3v |
|- ( ( A e. X /\ B e. X /\ C e. X ) -> ( A. x e. X A. y e. X A. z e. X ( x D y ) <_ ( ( z D x ) +e ( z D y ) ) -> ( A D B ) <_ ( ( C D A ) +e ( C D B ) ) ) ) |
21 |
7 20
|
syl5 |
|- ( ( A e. X /\ B e. X /\ C e. X ) -> ( D e. ( *Met ` X ) -> ( A D B ) <_ ( ( C D A ) +e ( C D B ) ) ) ) |
22 |
21
|
3comr |
|- ( ( C e. X /\ A e. X /\ B e. X ) -> ( D e. ( *Met ` X ) -> ( A D B ) <_ ( ( C D A ) +e ( C D B ) ) ) ) |
23 |
22
|
impcom |
|- ( ( D e. ( *Met ` X ) /\ ( C e. X /\ A e. X /\ B e. X ) ) -> ( A D B ) <_ ( ( C D A ) +e ( C D B ) ) ) |