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

Metamath Proof Explorer

Theorem hvsubcan2i

Description: Vector cancellation law. (Contributed by NM, 3-Sep-1999) (New usage is discouraged.)

Ref Expression
Hypotheses hvnegdi.1 
|- A e. ~H
hvnegdi.2 
|- B e. ~H
Assertion hvsubcan2i 
|- ( ( A +h B ) +h ( A -h B ) ) = ( 2 .h A )

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 oveq2i 
 |-  ( ( A +h B ) +h ( A -h B ) ) = ( ( A +h B ) +h ( A +h ( -u 1 .h B ) ) )
5 neg1cn 
 |-  -u 1 e. CC
6 5 2 hvmulcli 
 |-  ( -u 1 .h B ) e. ~H
7 1 2 1 6 hvadd4i 
 |-  ( ( A +h B ) +h ( A +h ( -u 1 .h B ) ) ) = ( ( A +h A ) +h ( B +h ( -u 1 .h B ) ) )
8 hv2times 
 |-  ( A e. ~H -> ( 2 .h A ) = ( A +h A ) )
9 1 8 ax-mp 
 |-  ( 2 .h A ) = ( A +h A )
10 9 eqcomi 
 |-  ( A +h A ) = ( 2 .h A )
11 2 hvnegidi 
 |-  ( B +h ( -u 1 .h B ) ) = 0h
12 10 11 oveq12i 
 |-  ( ( A +h A ) +h ( B +h ( -u 1 .h B ) ) ) = ( ( 2 .h A ) +h 0h )
13 7 12 eqtri 
 |-  ( ( A +h B ) +h ( A +h ( -u 1 .h B ) ) ) = ( ( 2 .h A ) +h 0h )
14 2cn 
 |-  2 e. CC
15 14 1 hvmulcli 
 |-  ( 2 .h A ) e. ~H
16 ax-hvaddid 
 |-  ( ( 2 .h A ) e. ~H -> ( ( 2 .h A ) +h 0h ) = ( 2 .h A ) )
17 15 16 ax-mp 
 |-  ( ( 2 .h A ) +h 0h ) = ( 2 .h A )
18 13 17 eqtri 
 |-  ( ( A +h B ) +h ( A +h ( -u 1 .h B ) ) ) = ( 2 .h A )
19 4 18 eqtri 
 |-  ( ( A +h B ) +h ( A -h B ) ) = ( 2 .h A )