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