Theorem hvsub0

Description: Subtraction of a zero vector. (Contributed by NM, 2-Apr-2000) (New usage is discouraged.)

	Ref	Expression
Assertion	hvsub0	|- ( A e. ~H -> ( A -h 0h ) = A )

Proof

Step	Hyp	Ref	Expression
1		ax-hv0cl	|- 0h e. ~H
2		hvsubval	|- ( ( A e. ~H /\ 0h e. ~H ) -> ( A -h 0h ) = ( A +h ( -u 1 .h 0h ) ) )
3	1 2	mpan2	|- ( A e. ~H -> ( A -h 0h ) = ( A +h ( -u 1 .h 0h ) ) )
4		neg1cn	|- -u 1 e. CC
5		hvmul0	|- ( -u 1 e. CC -> ( -u 1 .h 0h ) = 0h )
6	4 5	ax-mp	|- ( -u 1 .h 0h ) = 0h
7	6	oveq2i	|- ( A +h ( -u 1 .h 0h ) ) = ( A +h 0h )
8	3 7	eqtrdi	|- ( A e. ~H -> ( A -h 0h ) = ( A +h 0h ) )
9		ax-hvaddid	|- ( A e. ~H -> ( A +h 0h ) = A )
10	8 9	eqtrd	|- ( A e. ~H -> ( A -h 0h ) = A )