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 e. ~H
hvnegdi.2 
|- B e. ~H
Assertion hvsubeq0i 
|- ( ( A -h B ) = 0h <-> A = B )

Proof

Step Hyp Ref Expression
1 hvnegdi.1 
 |-  A e. ~H
2 hvnegdi.2 
 |-  B e. ~H
3 1 2 hvsubvali 
 |-  ( A -h B ) = ( A +h ( -u 1 .h B ) )
4 3 eqeq1i 
 |-  ( ( A -h B ) = 0h <-> ( A +h ( -u 1 .h B ) ) = 0h )
5 oveq1 
 |-  ( ( A +h ( -u 1 .h B ) ) = 0h -> ( ( A +h ( -u 1 .h B ) ) +h B ) = ( 0h +h B ) )
6 4 5 sylbi 
 |-  ( ( A -h B ) = 0h -> ( ( A +h ( -u 1 .h B ) ) +h B ) = ( 0h +h B ) )
7 neg1cn 
 |-  -u 1 e. CC
8 7 2 hvmulcli 
 |-  ( -u 1 .h B ) e. ~H
9 1 8 2 hvadd32i 
 |-  ( ( A +h ( -u 1 .h B ) ) +h B ) = ( ( A +h B ) +h ( -u 1 .h B ) )
10 1 2 8 hvassi 
 |-  ( ( A +h B ) +h ( -u 1 .h B ) ) = ( A +h ( B +h ( -u 1 .h B ) ) )
11 2 hvnegidi 
 |-  ( B +h ( -u 1 .h B ) ) = 0h
12 11 oveq2i 
 |-  ( A +h ( B +h ( -u 1 .h B ) ) ) = ( A +h 0h )
13 ax-hvaddid 
 |-  ( A e. ~H -> ( A +h 0h ) = A )
14 1 13 ax-mp 
 |-  ( A +h 0h ) = A
15 12 14 eqtri 
 |-  ( A +h ( B +h ( -u 1 .h B ) ) ) = A
16 10 15 eqtri 
 |-  ( ( A +h B ) +h ( -u 1 .h B ) ) = A
17 9 16 eqtri 
 |-  ( ( A +h ( -u 1 .h B ) ) +h B ) = A
18 2 hvaddlidi 
 |-  ( 0h +h B ) = B
19 6 17 18 3eqtr3g 
 |-  ( ( A -h B ) = 0h -> A = B )
20 oveq1 
 |-  ( A = B -> ( A -h B ) = ( B -h B ) )
21 hvsubid 
 |-  ( B e. ~H -> ( B -h B ) = 0h )
22 2 21 ax-mp 
 |-  ( B -h B ) = 0h
23 20 22 eqtrdi 
 |-  ( A = B -> ( A -h B ) = 0h )
24 19 23 impbii 
 |-  ( ( A -h B ) = 0h <-> A = B )