Step |
Hyp |
Ref |
Expression |
1 |
|
mscl.x |
|- X = ( Base ` M ) |
2 |
|
mscl.d |
|- D = ( dist ` M ) |
3 |
1 2
|
msmet2 |
|- ( M e. MetSp -> ( D |` ( X X. X ) ) e. ( Met ` X ) ) |
4 |
|
mettri2 |
|- ( ( ( D |` ( X X. X ) ) e. ( Met ` X ) /\ ( C e. X /\ A e. X /\ B e. X ) ) -> ( A ( D |` ( X X. X ) ) B ) <_ ( ( C ( D |` ( X X. X ) ) A ) + ( C ( D |` ( X X. X ) ) B ) ) ) |
5 |
3 4
|
sylan |
|- ( ( M e. MetSp /\ ( C e. X /\ A e. X /\ B e. X ) ) -> ( A ( D |` ( X X. X ) ) B ) <_ ( ( C ( D |` ( X X. X ) ) A ) + ( C ( D |` ( X X. X ) ) B ) ) ) |
6 |
|
simpr2 |
|- ( ( M e. MetSp /\ ( C e. X /\ A e. X /\ B e. X ) ) -> A e. X ) |
7 |
|
simpr3 |
|- ( ( M e. MetSp /\ ( C e. X /\ A e. X /\ B e. X ) ) -> B e. X ) |
8 |
6 7
|
ovresd |
|- ( ( M e. MetSp /\ ( C e. X /\ A e. X /\ B e. X ) ) -> ( A ( D |` ( X X. X ) ) B ) = ( A D B ) ) |
9 |
|
simpr1 |
|- ( ( M e. MetSp /\ ( C e. X /\ A e. X /\ B e. X ) ) -> C e. X ) |
10 |
9 6
|
ovresd |
|- ( ( M e. MetSp /\ ( C e. X /\ A e. X /\ B e. X ) ) -> ( C ( D |` ( X X. X ) ) A ) = ( C D A ) ) |
11 |
9 7
|
ovresd |
|- ( ( M e. MetSp /\ ( C e. X /\ A e. X /\ B e. X ) ) -> ( C ( D |` ( X X. X ) ) B ) = ( C D B ) ) |
12 |
10 11
|
oveq12d |
|- ( ( M e. MetSp /\ ( C e. X /\ A e. X /\ B e. X ) ) -> ( ( C ( D |` ( X X. X ) ) A ) + ( C ( D |` ( X X. X ) ) B ) ) = ( ( C D A ) + ( C D B ) ) ) |
13 |
5 8 12
|
3brtr3d |
|- ( ( M e. MetSp /\ ( C e. X /\ A e. X /\ B e. X ) ) -> ( A D B ) <_ ( ( C D A ) + ( C D B ) ) ) |