Metamath Proof Explorer

Theorem hvaddsubval

Description: Value of vector addition in terms of vector subtraction. (Contributed by NM, 10-Jun-2006) (New usage is discouraged.)

Ref Expression
Assertion hvaddsubval ⊢ A ∈ ℋ ∧ B ∈ ℋ → A + ℎ B = A - ℎ -1 ⋅ ℎ B

Proof

Step Hyp Ref Expression
1 neg1cn ⊢ − 1 ∈ ℂ
2 hvmulcl ⊢ − 1 ∈ ℂ ∧ B ∈ ℋ → -1 ⋅ ℎ B ∈ ℋ
3 1 2 mpan ⊢ B ∈ ℋ → -1 ⋅ ℎ B ∈ ℋ
4 hvsubval ⊢ A ∈ ℋ ∧ -1 ⋅ ℎ B ∈ ℋ → A - ℎ -1 ⋅ ℎ B = A + ℎ -1 ⋅ ℎ -1 ⋅ ℎ B
5 3 4 sylan2 ⊢ A ∈ ℋ ∧ B ∈ ℋ → A - ℎ -1 ⋅ ℎ B = A + ℎ -1 ⋅ ℎ -1 ⋅ ℎ B
6 hvm1neg ⊢ − 1 ∈ ℂ ∧ B ∈ ℋ → -1 ⋅ ℎ -1 ⋅ ℎ B = − -1 ⋅ ℎ B
7 1 6 mpan ⊢ B ∈ ℋ → -1 ⋅ ℎ -1 ⋅ ℎ B = − -1 ⋅ ℎ B
8 negneg1e1 ⊢ − -1 = 1
9 8 oveq1i ⊢ − -1 ⋅ ℎ B = 1 ⋅ ℎ B
10 7 9 eqtrdi ⊢ B ∈ ℋ → -1 ⋅ ℎ -1 ⋅ ℎ B = 1 ⋅ ℎ B
11 ax-hvmulid ⊢ B ∈ ℋ → 1 ⋅ ℎ B = B
12 10 11 eqtrd ⊢ B ∈ ℋ → -1 ⋅ ℎ -1 ⋅ ℎ B = B
13 12 adantl ⊢ A ∈ ℋ ∧ B ∈ ℋ → -1 ⋅ ℎ -1 ⋅ ℎ B = B
14 13 oveq2d ⊢ A ∈ ℋ ∧ B ∈ ℋ → A + ℎ -1 ⋅ ℎ -1 ⋅ ℎ B = A + ℎ B
15 5 14 eqtr2d ⊢ A ∈ ℋ ∧ B ∈ ℋ → A + ℎ B = A - ℎ -1 ⋅ ℎ B