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 = ( BaseSet ` W )
	sspm.m	|- M = ( -v ` U )
	sspm.l	|- L = ( -v ` W )
	sspm.h	|- H = ( SubSp ` U )
Assertion	sspm	|- ( ( U e. NrmCVec /\ W e. H ) -> L = ( M |` ( Y X. Y ) ) )

Proof

Step	Hyp	Ref	Expression
1		sspm.y	|- Y = ( BaseSet ` W )
2		sspm.m	|- M = ( -v ` U )
3		sspm.l	|- L = ( -v ` W )
4		sspm.h	|- H = ( SubSp ` U )
5	1 2 3 4	sspmval	|- ( ( ( U e. NrmCVec /\ W e. H ) /\ ( x e. Y /\ y e. Y ) ) -> ( x L y ) = ( x M y ) )
6	1 3	nvmf	|- ( W e. NrmCVec -> L : ( Y X. Y ) --> Y )
7		eqid	|- ( BaseSet ` U ) = ( BaseSet ` U )
8	7 2	nvmf	|- ( U e. NrmCVec -> M : ( ( BaseSet ` U ) X. ( BaseSet ` U ) ) --> ( BaseSet ` U ) )
9	1 4 5 6 8	sspmlem	|- ( ( U e. NrmCVec /\ W e. H ) -> L = ( M |` ( Y X. Y ) ) )