# 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 )`