Theorem hv2neg

Description: Two ways to express the negative of a vector. (Contributed by NM, 23-May-2005) (New usage is discouraged.)

	Ref	Expression
Assertion	hv2neg	⊢ ( 𝐴 ∈ ℋ → ( 0ℎ −ℎ 𝐴 ) = ( - 1 ·ℎ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		ax-hv0cl	⊢ 0ℎ ∈ ℋ
2		hvsubval	⊢ ( ( 0ℎ ∈ ℋ ∧ 𝐴 ∈ ℋ ) → ( 0ℎ −ℎ 𝐴 ) = ( 0ℎ +ℎ ( - 1 ·ℎ 𝐴 ) ) )
3	1 2	mpan	⊢ ( 𝐴 ∈ ℋ → ( 0ℎ −ℎ 𝐴 ) = ( 0ℎ +ℎ ( - 1 ·ℎ 𝐴 ) ) )
4		neg1cn	⊢ - 1 ∈ ℂ
5		hvmulcl	⊢ ( ( - 1 ∈ ℂ ∧ 𝐴 ∈ ℋ ) → ( - 1 ·ℎ 𝐴 ) ∈ ℋ )
6	4 5	mpan	⊢ ( 𝐴 ∈ ℋ → ( - 1 ·ℎ 𝐴 ) ∈ ℋ )
7		hvaddid2	⊢ ( ( - 1 ·ℎ 𝐴 ) ∈ ℋ → ( 0ℎ +ℎ ( - 1 ·ℎ 𝐴 ) ) = ( - 1 ·ℎ 𝐴 ) )
8	6 7	syl	⊢ ( 𝐴 ∈ ℋ → ( 0ℎ +ℎ ( - 1 ·ℎ 𝐴 ) ) = ( - 1 ·ℎ 𝐴 ) )
9	3 8	eqtrd	⊢ ( 𝐴 ∈ ℋ → ( 0ℎ −ℎ 𝐴 ) = ( - 1 ·ℎ 𝐴 ) )