This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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