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 e. ~H
hvnegdi.2 
|- B e. ~H
hvaddcan.3 
|- C e. ~H
Assertion hvaddcani 
|- ( ( A +h B ) = ( A +h C ) <-> B = C )

Proof

Step Hyp Ref Expression
1 hvnegdi.1 
 |-  A e. ~H
2 hvnegdi.2 
 |-  B e. ~H
3 hvaddcan.3 
 |-  C e. ~H
4 oveq1 
 |-  ( ( A +h B ) = ( A +h C ) -> ( ( A +h B ) +h ( -u 1 .h A ) ) = ( ( A +h C ) +h ( -u 1 .h A ) ) )
5 neg1cn 
 |-  -u 1 e. CC
6 5 1 hvmulcli 
 |-  ( -u 1 .h A ) e. ~H
7 1 2 6 hvadd32i 
 |-  ( ( A +h B ) +h ( -u 1 .h A ) ) = ( ( A +h ( -u 1 .h A ) ) +h B )
8 1 hvnegidi 
 |-  ( A +h ( -u 1 .h A ) ) = 0h
9 8 oveq1i 
 |-  ( ( A +h ( -u 1 .h A ) ) +h B ) = ( 0h +h B )
10 2 hvaddlidi 
 |-  ( 0h +h B ) = B
11 7 9 10 3eqtri 
 |-  ( ( A +h B ) +h ( -u 1 .h A ) ) = B
12 1 3 6 hvadd32i 
 |-  ( ( A +h C ) +h ( -u 1 .h A ) ) = ( ( A +h ( -u 1 .h A ) ) +h C )
13 8 oveq1i 
 |-  ( ( A +h ( -u 1 .h A ) ) +h C ) = ( 0h +h C )
14 3 hvaddlidi 
 |-  ( 0h +h C ) = C
15 12 13 14 3eqtri 
 |-  ( ( A +h C ) +h ( -u 1 .h A ) ) = C
16 4 11 15 3eqtr3g 
 |-  ( ( A +h B ) = ( A +h C ) -> B = C )
17 oveq2 
 |-  ( B = C -> ( A +h B ) = ( A +h C ) )
18 16 17 impbii 
 |-  ( ( A +h B ) = ( A +h C ) <-> B = C )