Theorem sspims

Description: The induced metric on a subspace is a restriction of the induced metric on the parent space. (Contributed by NM, 1-Feb-2008) (New usage is discouraged.)

	Ref	Expression
Hypotheses	sspims.y	|- Y = ( BaseSet ` W )
	sspims.d	|- D = ( IndMet ` U )
	sspims.c	|- C = ( IndMet ` W )
	sspims.h	|- H = ( SubSp ` U )
Assertion	sspims	|- ( ( U e. NrmCVec /\ W e. H ) -> C = ( D |` ( Y X. Y ) ) )

Proof

Step	Hyp	Ref	Expression
1		sspims.y	|- Y = ( BaseSet ` W )
2		sspims.d	|- D = ( IndMet ` U )
3		sspims.c	|- C = ( IndMet ` W )
4		sspims.h	|- H = ( SubSp ` U )
5	1 2 3 4	sspimsval	|- ( ( ( U e. NrmCVec /\ W e. H ) /\ ( x e. Y /\ y e. Y ) ) -> ( x C y ) = ( x D y ) )
6	1 3	imsdf	|- ( W e. NrmCVec -> C : ( Y X. Y ) --> RR )
7		eqid	|- ( BaseSet ` U ) = ( BaseSet ` U )
8	7 2	imsdf	|- ( U e. NrmCVec -> D : ( ( BaseSet ` U ) X. ( BaseSet ` U ) ) --> RR )
9	1 4 5 6 8	sspmlem	|- ( ( U e. NrmCVec /\ W e. H ) -> C = ( D |` ( Y X. Y ) ) )