Theorem sspm

Description: Vector subtraction on a subspace is a restriction of vector subtraction on the parent space. (Contributed by NM, 28-Jan-2008) (New usage is discouraged.)

	Ref	Expression
Hypotheses	sspm.y	$$⊢Y=\mathrm{BaseSet}\left(W\right)$$
	sspm.m	$$⊢M={-}_v\left(U\right)$$
	sspm.l	$$⊢L={-}_v\left(W\right)$$
	sspm.h	$$⊢H=\mathrm{SubSp}\left(U\right)$$
Assertion	sspm	$$⊢\left(U\in \mathrm{NrmCVec}\wedge W\in H\right)\to L={M\upharpoonright }_{\left(Y\times Y\right)}$$

Proof

Step	Hyp	Ref	Expression
1		sspm.y	$$⊢Y=\mathrm{BaseSet}\left(W\right)$$
2		sspm.m	$$⊢M={-}_v\left(U\right)$$
3		sspm.l	$$⊢L={-}_v\left(W\right)$$
4		sspm.h	$$⊢H=\mathrm{SubSp}\left(U\right)$$
5	1 2 3 4	sspmval	$$⊢\left(\left(U\in \mathrm{NrmCVec}\wedge W\in H\right)\wedge \left(x\in Y\wedge y\in Y\right)\right)\to xLy=xMy$$
6	1 3	nvmf	$$⊢W\in \mathrm{NrmCVec}\to L:Y\times Y⟶Y$$
7		eqid	$$⊢\mathrm{BaseSet}\left(U\right)=\mathrm{BaseSet}\left(U\right)$$
8	7 2	nvmf	$$⊢U\in \mathrm{NrmCVec}\to M:\mathrm{BaseSet}\left(U\right)\times \mathrm{BaseSet}\left(U\right)⟶\mathrm{BaseSet}\left(U\right)$$
9	1 4 5 6 8	sspmlem	$$⊢\left(U\in \mathrm{NrmCVec}\wedge W\in H\right)\to L={M\upharpoonright }_{\left(Y\times Y\right)}$$