Theorem hvnegidi

Description: Addition of negative of a vector to itself. (Contributed by NM, 18-Aug-1999) (New usage is discouraged.)

	Ref	Expression
Hypothesis	hvaddlid.1	|- A e. ~H
Assertion	hvnegidi	|- ( A +h ( -u 1 .h A ) ) = 0h

Proof

Step	Hyp	Ref	Expression
1		hvaddlid.1	|- A e. ~H
2		hvnegid	|- ( A e. ~H -> ( A +h ( -u 1 .h A ) ) = 0h )
3	1 2	ax-mp	|- ( A +h ( -u 1 .h A ) ) = 0h