Theorem hvsubval

Description: Value of vector subtraction. (Contributed by NM, 5-Sep-1999) (Revised by Mario Carneiro, 23-Dec-2013) (New usage is discouraged.)

	Ref	Expression
Assertion	hvsubval	|- ( ( A e. ~H /\ B e. ~H ) -> ( A -h B ) = ( A +h ( -u 1 .h B ) ) )

Proof

Step	Hyp	Ref	Expression
1		oveq1	|- ( x = A -> ( x +h ( -u 1 .h y ) ) = ( A +h ( -u 1 .h y ) ) )
2		oveq2	|- ( y = B -> ( -u 1 .h y ) = ( -u 1 .h B ) )
3	2	oveq2d	|- ( y = B -> ( A +h ( -u 1 .h y ) ) = ( A +h ( -u 1 .h B ) ) )
4		df-hvsub	|- -h = ( x e. ~H , y e. ~H |-> ( x +h ( -u 1 .h y ) ) )
5		ovex	|- ( A +h ( -u 1 .h B ) ) e. _V
6	1 3 4 5	ovmpo	|- ( ( A e. ~H /\ B e. ~H ) -> ( A -h B ) = ( A +h ( -u 1 .h B ) ) )