# Metamath Proof Explorer

## Theorem hhssmetdval

Description: Value of the distance function of the metric space of a subspace. (Contributed by NM, 10-Apr-2008) (New usage is discouraged.)

Ref Expression
Hypotheses hhssims2.1
`|- W = <. <. ( +h |` ( H X. H ) ) , ( .h |` ( CC X. H ) ) >. , ( normh |` H ) >.`
hhssims2.3
`|- D = ( IndMet ` W )`
hhssims2.2
`|- H e. SH`
Assertion hhssmetdval
`|- ( ( A e. H /\ B e. H ) -> ( A D B ) = ( normh ` ( A -h B ) ) )`

### Proof

Step Hyp Ref Expression
1 hhssims2.1
` |-  W = <. <. ( +h |` ( H X. H ) ) , ( .h |` ( CC X. H ) ) >. , ( normh |` H ) >.`
2 hhssims2.3
` |-  D = ( IndMet ` W )`
3 hhssims2.2
` |-  H e. SH`
4 1 3 hhssnv
` |-  W e. NrmCVec`
5 1 3 hhssba
` |-  H = ( BaseSet ` W )`
6 1 3 hhssvs
` |-  ( -h |` ( H X. H ) ) = ( -v ` W )`
7 1 hhssnm
` |-  ( normh |` H ) = ( normCV ` W )`
8 5 6 7 2 imsdval
` |-  ( ( W e. NrmCVec /\ A e. H /\ B e. H ) -> ( A D B ) = ( ( normh |` H ) ` ( A ( -h |` ( H X. H ) ) B ) ) )`
9 4 8 mp3an1
` |-  ( ( A e. H /\ B e. H ) -> ( A D B ) = ( ( normh |` H ) ` ( A ( -h |` ( H X. H ) ) B ) ) )`
10 ovres
` |-  ( ( A e. H /\ B e. H ) -> ( A ( -h |` ( H X. H ) ) B ) = ( A -h B ) )`
11 10 fveq2d
` |-  ( ( A e. H /\ B e. H ) -> ( ( normh |` H ) ` ( A ( -h |` ( H X. H ) ) B ) ) = ( ( normh |` H ) ` ( A -h B ) ) )`
12 shsubcl
` |-  ( ( H e. SH /\ A e. H /\ B e. H ) -> ( A -h B ) e. H )`
13 3 12 mp3an1
` |-  ( ( A e. H /\ B e. H ) -> ( A -h B ) e. H )`
14 fvres
` |-  ( ( A -h B ) e. H -> ( ( normh |` H ) ` ( A -h B ) ) = ( normh ` ( A -h B ) ) )`
15 13 14 syl
` |-  ( ( A e. H /\ B e. H ) -> ( ( normh |` H ) ` ( A -h B ) ) = ( normh ` ( A -h B ) ) )`
16 9 11 15 3eqtrd
` |-  ( ( A e. H /\ B e. H ) -> ( A D B ) = ( normh ` ( A -h B ) ) )`