Theorem hvaddeq0

Description: If the sum of two vectors is zero, one is the negative of the other. (Contributed by NM, 10-Jun-2006) (New usage is discouraged.)

	Ref	Expression
Assertion	hvaddeq0	⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( ( 𝐴 +ℎ 𝐵 ) = 0ℎ ↔ 𝐴 = ( - 1 ·ℎ 𝐵 ) ) )

Proof

Step	Hyp	Ref	Expression
1		hvaddsubval	⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( 𝐴 +ℎ 𝐵 ) = ( 𝐴 −ℎ ( - 1 ·ℎ 𝐵 ) ) )
2	1	eqeq1d	⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( ( 𝐴 +ℎ 𝐵 ) = 0ℎ ↔ ( 𝐴 −ℎ ( - 1 ·ℎ 𝐵 ) ) = 0ℎ ) )
3		neg1cn	⊢ - 1 ∈ ℂ
4		hvmulcl	⊢ ( ( - 1 ∈ ℂ ∧ 𝐵 ∈ ℋ ) → ( - 1 ·ℎ 𝐵 ) ∈ ℋ )
5	3 4	mpan	⊢ ( 𝐵 ∈ ℋ → ( - 1 ·ℎ 𝐵 ) ∈ ℋ )
6		hvsubeq0	⊢ ( ( 𝐴 ∈ ℋ ∧ ( - 1 ·ℎ 𝐵 ) ∈ ℋ ) → ( ( 𝐴 −ℎ ( - 1 ·ℎ 𝐵 ) ) = 0ℎ ↔ 𝐴 = ( - 1 ·ℎ 𝐵 ) ) )
7	5 6	sylan2	⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( ( 𝐴 −ℎ ( - 1 ·ℎ 𝐵 ) ) = 0ℎ ↔ 𝐴 = ( - 1 ·ℎ 𝐵 ) ) )
8	2 7	bitrd	⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( ( 𝐴 +ℎ 𝐵 ) = 0ℎ ↔ 𝐴 = ( - 1 ·ℎ 𝐵 ) ) )