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 ⊢ 𝐴 ∈ ℋ
hvnegdi.2 ⊢ 𝐵 ∈ ℋ
Assertion hvsubeq0i ( ( 𝐴 −ℎ 𝐵 ) = 0ℎ ↔ 𝐴 = 𝐵 )

Proof

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