Metamath Proof Explorer

Theorem hhssvs

Description: 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 hhssvs 
|- ( -h |` ( H X. H ) ) = ( -v ` W )

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 eqid 
 |-  <. <. +h , .h >. , normh >. = <. <. +h , .h >. , normh >.
4 3 hhnv 
 |-  <. <. +h , .h >. , normh >. e. NrmCVec
5 3 1 hhsst 
 |-  ( H e. SH -> W e. ( SubSp ` <. <. +h , .h >. , normh >. ) )
6 2 5 ax-mp 
 |-  W e. ( SubSp ` <. <. +h , .h >. , normh >. )
7 1 2 hhssba 
 |-  H = ( BaseSet ` W )
8 3 hhvs 
 |-  -h = ( -v ` <. <. +h , .h >. , normh >. )
9 eqid 
 |-  ( -v ` W ) = ( -v ` W )
10 eqid 
 |-  ( SubSp ` <. <. +h , .h >. , normh >. ) = ( SubSp ` <. <. +h , .h >. , normh >. )
11 7 8 9 10 sspm 
 |-  ( ( <. <. +h , .h >. , normh >. e. NrmCVec /\ W e. ( SubSp ` <. <. +h , .h >. , normh >. ) ) -> ( -v ` W ) = ( -h |` ( H X. H ) ) )
12 4 6 11 mp2an 
 |-  ( -v ` W ) = ( -h |` ( H X. H ) )
13 12 eqcomi 
 |-  ( -h |` ( H X. H ) ) = ( -v ` W )