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