Theorem hvsub0

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

	Ref	Expression
Assertion	hvsub0	⊢ ( 𝐴 ∈ ℋ → ( 𝐴 −ℎ 0ℎ ) = 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		ax-hv0cl	⊢ 0ℎ ∈ ℋ
2		hvsubval	⊢ ( ( 𝐴 ∈ ℋ ∧ 0ℎ ∈ ℋ ) → ( 𝐴 −ℎ 0ℎ ) = ( 𝐴 +ℎ ( - 1 ·ℎ 0ℎ ) ) )
3	1 2	mpan2	⊢ ( 𝐴 ∈ ℋ → ( 𝐴 −ℎ 0ℎ ) = ( 𝐴 +ℎ ( - 1 ·ℎ 0ℎ ) ) )
4		neg1cn	⊢ - 1 ∈ ℂ
5		hvmul0	⊢ ( - 1 ∈ ℂ → ( - 1 ·ℎ 0ℎ ) = 0ℎ )
6	4 5	ax-mp	⊢ ( - 1 ·ℎ 0ℎ ) = 0ℎ
7	6	oveq2i	⊢ ( 𝐴 +ℎ ( - 1 ·ℎ 0ℎ ) ) = ( 𝐴 +ℎ 0ℎ )
8	3 7	eqtrdi	⊢ ( 𝐴 ∈ ℋ → ( 𝐴 −ℎ 0ℎ ) = ( 𝐴 +ℎ 0ℎ ) )
9		ax-hvaddid	⊢ ( 𝐴 ∈ ℋ → ( 𝐴 +ℎ 0ℎ ) = 𝐴 )
10	8 9	eqtrd	⊢ ( 𝐴 ∈ ℋ → ( 𝐴 −ℎ 0ℎ ) = 𝐴 )