Theorem hhssmet

Description: Induced metric 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	hhssmet	|- D e. ( Met ` H )

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	5 2	imsmet	|- ( W e. NrmCVec -> D e. ( Met ` H ) )
7	4 6	ax-mp	|- D e. ( Met ` H )