Theorem hhssims2

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	hhssims2	|- D = ( ( normh o. -h ) |` ( H X. 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		eqid	|- ( ( normh o. -h ) |` ( H X. H ) ) = ( ( normh o. -h ) |` ( H X. H ) )
5	1 3 4	hhssims	|- ( ( normh o. -h ) |` ( H X. H ) ) = ( IndMet ` W )
6	2 5	eqtr4i	|- D = ( ( normh o. -h ) |` ( H X. H ) )