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=\mathrm{BaseSet}\left(W\right)$$
	sspims.d	$$⊢D=\mathrm{IndMet}\left(U\right)$$
	sspims.c	$$⊢C=\mathrm{IndMet}\left(W\right)$$
	sspims.h	$$⊢H=\mathrm{SubSp}\left(U\right)$$
Assertion	sspims	$$⊢\left(U\in \mathrm{NrmCVec}\wedge W\in H\right)\to C={D\upharpoonright }_{\left(Y\times Y\right)}$$

Proof

Step	Hyp	Ref	Expression
1		sspims.y	$$⊢Y=\mathrm{BaseSet}\left(W\right)$$
2		sspims.d	$$⊢D=\mathrm{IndMet}\left(U\right)$$
3		sspims.c	$$⊢C=\mathrm{IndMet}\left(W\right)$$
4		sspims.h	$$⊢H=\mathrm{SubSp}\left(U\right)$$
5	1 2 3 4	sspimsval	$$⊢\left(\left(U\in \mathrm{NrmCVec}\wedge W\in H\right)\wedge \left(x\in Y\wedge y\in Y\right)\right)\to xCy=xDy$$
6	1 3	imsdf	$$⊢W\in \mathrm{NrmCVec}\to C:Y\times Y⟶ℝ$$
7		eqid	$$⊢\mathrm{BaseSet}\left(U\right)=\mathrm{BaseSet}\left(U\right)$$
8	7 2	imsdf	$$⊢U\in \mathrm{NrmCVec}\to D:\mathrm{BaseSet}\left(U\right)\times \mathrm{BaseSet}\left(U\right)⟶ℝ$$
9	1 4 5 6 8	sspmlem	$$⊢\left(U\in \mathrm{NrmCVec}\wedge W\in H\right)\to C={D\upharpoonright }_{\left(Y\times Y\right)}$$