Metamath Proof Explorer

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 ⊢ A ∈ ℋ ∧ B ∈ ℋ → A + ℎ B = 0 ℎ ↔ A = -1 ⋅ ℎ B

Proof

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