This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem h2hvs

Description: The vector subtraction operation of Hilbert space. (Contributed by NM, 6-Jun-2008) (Revised by Mario Carneiro, 23-Dec-2013) (New usage is discouraged.)

Ref Expression
Hypotheses h2h.1 
|- U = <. <. +h , .h >. , normh >.
h2h.2 
|- U e. NrmCVec
h2h.4 
|- ~H = ( BaseSet ` U )
Assertion h2hvs 
|- -h = ( -v ` U )

Proof

Step Hyp Ref Expression
1 h2h.1 
 |-  U = <. <. +h , .h >. , normh >.
2 h2h.2 
 |-  U e. NrmCVec
3 h2h.4 
 |-  ~H = ( BaseSet ` U )
4 df-hvsub 
 |-  -h = ( x e. ~H , y e. ~H |-> ( x +h ( -u 1 .h y ) ) )
5 1 2 h2hva 
 |-  +h = ( +v ` U )
6 1 2 h2hsm 
 |-  .h = ( .sOLD ` U )
7 eqid 
 |-  ( -v ` U ) = ( -v ` U )
8 3 5 6 7 nvmfval 
 |-  ( U e. NrmCVec -> ( -v ` U ) = ( x e. ~H , y e. ~H |-> ( x +h ( -u 1 .h y ) ) ) )
9 2 8 ax-mp 
 |-  ( -v ` U ) = ( x e. ~H , y e. ~H |-> ( x +h ( -u 1 .h y ) ) )
10 4 9 eqtr4i 
 |-  -h = ( -v ` U )