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

Metamath Proof Explorer

Theorem hvsubaddi

Description: Relationship between vector subtraction and 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 hvsubaddi 
|- ( ( A -h B ) = C <-> ( B +h C ) = A )

Proof

Step Hyp Ref Expression
1 hvnegdi.1 
 |-  A e. ~H
2 hvnegdi.2 
 |-  B e. ~H
3 hvaddcan.3 
 |-  C e. ~H
4 1 2 hvsubvali 
 |-  ( A -h B ) = ( A +h ( -u 1 .h B ) )
5 4 eqeq1i 
 |-  ( ( A -h B ) = C <-> ( A +h ( -u 1 .h B ) ) = C )
6 neg1cn 
 |-  -u 1 e. CC
7 6 2 hvmulcli 
 |-  ( -u 1 .h B ) e. ~H
8 2 1 7 hvadd12i 
 |-  ( B +h ( A +h ( -u 1 .h B ) ) ) = ( A +h ( B +h ( -u 1 .h B ) ) )
9 2 hvnegidi 
 |-  ( B +h ( -u 1 .h B ) ) = 0h
10 9 oveq2i 
 |-  ( A +h ( B +h ( -u 1 .h B ) ) ) = ( A +h 0h )
11 ax-hvaddid 
 |-  ( A e. ~H -> ( A +h 0h ) = A )
12 1 11 ax-mp 
 |-  ( A +h 0h ) = A
13 8 10 12 3eqtri 
 |-  ( B +h ( A +h ( -u 1 .h B ) ) ) = A
14 13 eqeq1i 
 |-  ( ( B +h ( A +h ( -u 1 .h B ) ) ) = ( B +h C ) <-> A = ( B +h C ) )
15 1 7 hvaddcli 
 |-  ( A +h ( -u 1 .h B ) ) e. ~H
16 2 15 3 hvaddcani 
 |-  ( ( B +h ( A +h ( -u 1 .h B ) ) ) = ( B +h C ) <-> ( A +h ( -u 1 .h B ) ) = C )
17 eqcom 
 |-  ( A = ( B +h C ) <-> ( B +h C ) = A )
18 14 16 17 3bitr3i 
 |-  ( ( A +h ( -u 1 .h B ) ) = C <-> ( B +h C ) = A )
19 5 18 bitri 
 |-  ( ( A -h B ) = C <-> ( B +h C ) = A )