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

Metamath Proof Explorer

Theorem hvsubeq0i

Description: If the difference between two vectors is zero, they are equal. (Contributed by NM, 18-Aug-1999) (New usage is discouraged.)

Ref Expression
Hypotheses hvnegdi.1 ⊢ A ∈ ℋ
hvnegdi.2 ⊢ B ∈ ℋ
Assertion hvsubeq0i ⊢ A - ℎ B = 0 ℎ ↔ A = B

Proof

Step Hyp Ref Expression
1 hvnegdi.1 ⊢ A ∈ ℋ
2 hvnegdi.2 ⊢ B ∈ ℋ
3 1 2 hvsubvali ⊢ A - ℎ B = A + ℎ -1 ⋅ ℎ B
4 3 eqeq1i ⊢ A - ℎ B = 0 ℎ ↔ A + ℎ -1 ⋅ ℎ B = 0 ℎ
5 oveq1 ⊢ A + ℎ -1 ⋅ ℎ B = 0 ℎ → A + ℎ -1 ⋅ ℎ B + ℎ B = 0 ℎ + ℎ B
6 4 5 sylbi ⊢ A - ℎ B = 0 ℎ → A + ℎ -1 ⋅ ℎ B + ℎ B = 0 ℎ + ℎ B
7 neg1cn ⊢ − 1 ∈ ℂ
8 7 2 hvmulcli ⊢ -1 ⋅ ℎ B ∈ ℋ
9 1 8 2 hvadd32i ⊢ A + ℎ -1 ⋅ ℎ B + ℎ B = A + ℎ B + ℎ -1 ⋅ ℎ B
10 1 2 8 hvassi ⊢ A + ℎ B + ℎ -1 ⋅ ℎ B = A + ℎ B + ℎ -1 ⋅ ℎ B
11 2 hvnegidi ⊢ B + ℎ -1 ⋅ ℎ B = 0 ℎ
12 11 oveq2i ⊢ A + ℎ B + ℎ -1 ⋅ ℎ B = A + ℎ 0 ℎ
13 ax-hvaddid ⊢ A ∈ ℋ → A + ℎ 0 ℎ = A
14 1 13 ax-mp ⊢ A + ℎ 0 ℎ = A
15 12 14 eqtri ⊢ A + ℎ B + ℎ -1 ⋅ ℎ B = A
16 10 15 eqtri ⊢ A + ℎ B + ℎ -1 ⋅ ℎ B = A
17 9 16 eqtri ⊢ A + ℎ -1 ⋅ ℎ B + ℎ B = A
18 2 hvaddlidi ⊢ 0 ℎ + ℎ B = B
19 6 17 18 3eqtr3g ⊢ A - ℎ B = 0 ℎ → A = B
20 oveq1 ⊢ A = B → A - ℎ B = B - ℎ B
21 hvsubid ⊢ B ∈ ℋ → B - ℎ B = 0 ℎ
22 2 21 ax-mp ⊢ B - ℎ B = 0 ℎ
23 20 22 eqtrdi ⊢ A = B → A - ℎ B = 0 ℎ
24 19 23 impbii ⊢ A - ℎ B = 0 ℎ ↔ A = B