Description: Mapping of the vector subtraction operation on a subspace. (Contributed by NM, 10Apr2008) (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 
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  axmp   ( h ` ( H X. H ) ) : ( H X. H ) > H 