Theorem hhssvsf

Description: Mapping of the vector subtraction operation on 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 ) >.
	hhssba.2	|- H e. SH
Assertion	hhssvsf	|- ( -h |` ( H X. H ) ) : ( H X. H ) --> H

Proof

Step	Hyp	Ref	Expression
1		hhsssh2.1	|- W = <. <. ( +h |` ( H X. H ) ) , ( .h |` ( CC X. H ) ) >. , ( normh |` H ) >.
2		hhssba.2	|- H e. SH
3	1 2	hhssnv	|- W e. NrmCVec
4	1 2	hhssba	|- H = ( BaseSet ` W )
5	1 2	hhssvs	|- ( -h |` ( H X. H ) ) = ( -v ` W )
6	4 5	nvmf	|- ( W e. NrmCVec -> ( -h |` ( H X. H ) ) : ( H X. H ) --> H )
7	3 6	ax-mp	|- ( -h |` ( H X. H ) ) : ( H X. H ) --> H