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 )