Metamath Proof Explorer

Theorem hhvs

Description: The vector subtraction operation of Hilbert space. (Contributed by NM, 13-Dec-2007) (New usage is discouraged.)

Ref Expression
Hypothesis hhnv.1 
|- U = <. <. +h , .h >. , normh >.
Assertion hhvs 
|- -h = ( -v ` U )

Proof

Step Hyp Ref Expression
1 hhnv.1 
 |-  U = <. <. +h , .h >. , normh >.
2 1 hhnv 
 |-  U e. NrmCVec
3 1 hhba 
 |-  ~H = ( BaseSet ` U )
4 1 2 3 h2hvs 
 |-  -h = ( -v ` U )