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 )