Theorem hhssims

Description: Induced metric of a subspace. (Contributed by NM, 10-Apr-2008) (New usage is discouraged.)

	Ref	Expression
Hypotheses	hhsssh2.1	|- W = <. <. ( +h |` ( H X. H ) ) , ( .h |` ( CC X. H ) ) >. , ( normh |` H ) >.
	hhssims.2	|- H e. SH
	hhssims.3	|- D = ( ( normh o. -h ) |` ( H X. H ) )
Assertion	hhssims	|- D = ( IndMet ` W )

Proof

Step	Hyp	Ref	Expression
1		hhsssh2.1	|- W = <. <. ( +h |` ( H X. H ) ) , ( .h |` ( CC X. H ) ) >. , ( normh |` H ) >.
2		hhssims.2	|- H e. SH
3		hhssims.3	|- D = ( ( normh o. -h ) |` ( H X. H ) )
4	1 2	hhssnv	|- W e. NrmCVec
5	1 2	hhssvs	|- ( -h |` ( H X. H ) ) = ( -v ` W )
6	1	hhssnm	|- ( normh |` H ) = ( normCV ` W )
7		eqid	|- ( IndMet ` W ) = ( IndMet ` W )
8	5 6 7	imsval	|- ( W e. NrmCVec -> ( IndMet ` W ) = ( ( normh |` H ) o. ( -h |` ( H X. H ) ) ) )
9	4 8	ax-mp	|- ( IndMet ` W ) = ( ( normh |` H ) o. ( -h |` ( H X. H ) ) )
10		resco	|- ( ( normh o. -h ) |` ( H X. H ) ) = ( normh o. ( -h |` ( H X. H ) ) )
11	1 2	hhssvsf	|- ( -h |` ( H X. H ) ) : ( H X. H ) --> H
12		frn	|- ( ( -h |` ( H X. H ) ) : ( H X. H ) --> H -> ran ( -h |` ( H X. H ) ) C_ H )
13	11 12	ax-mp	|- ran ( -h |` ( H X. H ) ) C_ H
14		cores	|- ( ran ( -h |` ( H X. H ) ) C_ H -> ( ( normh |` H ) o. ( -h |` ( H X. H ) ) ) = ( normh o. ( -h |` ( H X. H ) ) ) )
15	13 14	ax-mp	|- ( ( normh |` H ) o. ( -h |` ( H X. H ) ) ) = ( normh o. ( -h |` ( H X. H ) ) )
16	10 15	eqtr4i	|- ( ( normh o. -h ) |` ( H X. H ) ) = ( ( normh |` H ) o. ( -h |` ( H X. H ) ) )
17	9 16	eqtr4i	|- ( IndMet ` W ) = ( ( normh o. -h ) |` ( H X. H ) )
18	3 17	eqtr4i	|- D = ( IndMet ` W )