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