This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem hvaddcani

Description: Cancellation law for vector addition. (Contributed by NM, 11-Sep-1999) (New usage is discouraged.)

Ref Expression
Hypotheses hvnegdi.1 ⊢ A ∈ ℋ
hvnegdi.2 ⊢ B ∈ ℋ
hvaddcan.3 ⊢ C ∈ ℋ
Assertion hvaddcani ⊢ A + ℎ B = A + ℎ C ↔ B = C

Proof

Step Hyp Ref Expression
1 hvnegdi.1 ⊢ A ∈ ℋ
2 hvnegdi.2 ⊢ B ∈ ℋ
3 hvaddcan.3 ⊢ C ∈ ℋ
4 oveq1 ⊢ A + ℎ B = A + ℎ C → A + ℎ B + ℎ -1 ⋅ ℎ A = A + ℎ C + ℎ -1 ⋅ ℎ A
5 neg1cn ⊢ − 1 ∈ ℂ
6 5 1 hvmulcli ⊢ -1 ⋅ ℎ A ∈ ℋ
7 1 2 6 hvadd32i ⊢ A + ℎ B + ℎ -1 ⋅ ℎ A = A + ℎ -1 ⋅ ℎ A + ℎ B
8 1 hvnegidi ⊢ A + ℎ -1 ⋅ ℎ A = 0 ℎ
9 8 oveq1i ⊢ A + ℎ -1 ⋅ ℎ A + ℎ B = 0 ℎ + ℎ B
10 2 hvaddlidi ⊢ 0 ℎ + ℎ B = B
11 7 9 10 3eqtri ⊢ A + ℎ B + ℎ -1 ⋅ ℎ A = B
12 1 3 6 hvadd32i ⊢ A + ℎ C + ℎ -1 ⋅ ℎ A = A + ℎ -1 ⋅ ℎ A + ℎ C
13 8 oveq1i ⊢ A + ℎ -1 ⋅ ℎ A + ℎ C = 0 ℎ + ℎ C
14 3 hvaddlidi ⊢ 0 ℎ + ℎ C = C
15 12 13 14 3eqtri ⊢ A + ℎ C + ℎ -1 ⋅ ℎ A = C
16 4 11 15 3eqtr3g ⊢ A + ℎ B = A + ℎ C → B = C
17 oveq2 ⊢ B = C → A + ℎ B = A + ℎ C
18 16 17 impbii ⊢ A + ℎ B = A + ℎ C ↔ B = C