Step |
Hyp |
Ref |
Expression |
1 |
|
mscl.x |
|- X = ( Base ` M ) |
2 |
|
mscl.d |
|- D = ( dist ` M ) |
3 |
|
ovres |
|- ( ( A e. X /\ B e. X ) -> ( A ( D |` ( X X. X ) ) B ) = ( A D B ) ) |
4 |
3
|
3adant1 |
|- ( ( M e. *MetSp /\ A e. X /\ B e. X ) -> ( A ( D |` ( X X. X ) ) B ) = ( A D B ) ) |
5 |
1 2
|
xmsxmet2 |
|- ( M e. *MetSp -> ( D |` ( X X. X ) ) e. ( *Met ` X ) ) |
6 |
|
xmetcl |
|- ( ( ( D |` ( X X. X ) ) e. ( *Met ` X ) /\ A e. X /\ B e. X ) -> ( A ( D |` ( X X. X ) ) B ) e. RR* ) |
7 |
5 6
|
syl3an1 |
|- ( ( M e. *MetSp /\ A e. X /\ B e. X ) -> ( A ( D |` ( X X. X ) ) B ) e. RR* ) |
8 |
4 7
|
eqeltrrd |
|- ( ( M e. *MetSp /\ A e. X /\ B e. X ) -> ( A D B ) e. RR* ) |