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

Metamath Proof Explorer

Theorem hvnegdii

Description: Distribution of negative over subtraction. (Contributed by NM, 31-Oct-1999) (New usage is discouraged.)

Ref Expression
Hypotheses hvnegdi.1 
|- A e. ~H
hvnegdi.2 
|- B e. ~H
Assertion hvnegdii 
|- ( -u 1 .h ( A -h B ) ) = ( B -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 
 |-  ( -u 1 .h ( A -h B ) ) = ( -u 1 .h ( A +h ( -u 1 .h B ) ) )
5 neg1cn 
 |-  -u 1 e. CC
6 5 2 hvmulcli 
 |-  ( -u 1 .h B ) e. ~H
7 5 1 6 hvdistr1i 
 |-  ( -u 1 .h ( A +h ( -u 1 .h B ) ) ) = ( ( -u 1 .h A ) +h ( -u 1 .h ( -u 1 .h B ) ) )
8 neg1mulneg1e1 
 |-  ( -u 1 x. -u 1 ) = 1
9 8 oveq1i 
 |-  ( ( -u 1 x. -u 1 ) .h B ) = ( 1 .h B )
10 5 5 2 hvmulassi 
 |-  ( ( -u 1 x. -u 1 ) .h B ) = ( -u 1 .h ( -u 1 .h B ) )
11 ax-hvmulid 
 |-  ( B e. ~H -> ( 1 .h B ) = B )
12 2 11 ax-mp 
 |-  ( 1 .h B ) = B
13 9 10 12 3eqtr3i 
 |-  ( -u 1 .h ( -u 1 .h B ) ) = B
14 13 oveq1i 
 |-  ( ( -u 1 .h ( -u 1 .h B ) ) +h ( -u 1 .h A ) ) = ( B +h ( -u 1 .h A ) )
15 5 1 hvmulcli 
 |-  ( -u 1 .h A ) e. ~H
16 5 6 hvmulcli 
 |-  ( -u 1 .h ( -u 1 .h B ) ) e. ~H
17 15 16 hvcomi 
 |-  ( ( -u 1 .h A ) +h ( -u 1 .h ( -u 1 .h B ) ) ) = ( ( -u 1 .h ( -u 1 .h B ) ) +h ( -u 1 .h A ) )
18 2 1 hvsubvali 
 |-  ( B -h A ) = ( B +h ( -u 1 .h A ) )
19 14 17 18 3eqtr4i 
 |-  ( ( -u 1 .h A ) +h ( -u 1 .h ( -u 1 .h B ) ) ) = ( B -h A )
20 4 7 19 3eqtri 
 |-  ( -u 1 .h ( A -h B ) ) = ( B -h A )