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 ⊢ 𝐴 ∈ ℋ
hvnegdi.2 ⊢ 𝐵 ∈ ℋ
Assertion hvnegdii ( - 1 ·ℎ ( 𝐴 −ℎ 𝐵 ) ) = ( 𝐵 −ℎ 𝐴 )

Proof

Step Hyp Ref Expression
1 hvnegdi.1 ⊢ 𝐴 ∈ ℋ
2 hvnegdi.2 ⊢ 𝐵 ∈ ℋ
3 1 2 hvsubvali ⊢ ( 𝐴 −ℎ 𝐵 ) = ( 𝐴 +ℎ ( - 1 ·ℎ 𝐵 ) )
4 3 oveq2i ⊢ ( - 1 ·ℎ ( 𝐴 −ℎ 𝐵 ) ) = ( - 1 ·ℎ ( 𝐴 +ℎ ( - 1 ·ℎ 𝐵 ) ) )
5 neg1cn ⊢ - 1 ∈ ℂ
6 5 2 hvmulcli ⊢ ( - 1 ·ℎ 𝐵 ) ∈ ℋ
7 5 1 6 hvdistr1i ⊢ ( - 1 ·ℎ ( 𝐴 +ℎ ( - 1 ·ℎ 𝐵 ) ) ) = ( ( - 1 ·ℎ 𝐴 ) +ℎ ( - 1 ·ℎ ( - 1 ·ℎ 𝐵 ) ) )
8 neg1mulneg1e1 ⊢ ( - 1 · - 1 ) = 1
9 8 oveq1i ⊢ ( ( - 1 · - 1 ) ·ℎ 𝐵 ) = ( 1 ·ℎ 𝐵 )
10 5 5 2 hvmulassi ⊢ ( ( - 1 · - 1 ) ·ℎ 𝐵 ) = ( - 1 ·ℎ ( - 1 ·ℎ 𝐵 ) )
11 ax-hvmulid ⊢ ( 𝐵 ∈ ℋ → ( 1 ·ℎ 𝐵 ) = 𝐵 )
12 2 11 ax-mp ⊢ ( 1 ·ℎ 𝐵 ) = 𝐵
13 9 10 12 3eqtr3i ⊢ ( - 1 ·ℎ ( - 1 ·ℎ 𝐵 ) ) = 𝐵
14 13 oveq1i ⊢ ( ( - 1 ·ℎ ( - 1 ·ℎ 𝐵 ) ) +ℎ ( - 1 ·ℎ 𝐴 ) ) = ( 𝐵 +ℎ ( - 1 ·ℎ 𝐴 ) )
15 5 1 hvmulcli ⊢ ( - 1 ·ℎ 𝐴 ) ∈ ℋ
16 5 6 hvmulcli ⊢ ( - 1 ·ℎ ( - 1 ·ℎ 𝐵 ) ) ∈ ℋ
17 15 16 hvcomi ⊢ ( ( - 1 ·ℎ 𝐴 ) +ℎ ( - 1 ·ℎ ( - 1 ·ℎ 𝐵 ) ) ) = ( ( - 1 ·ℎ ( - 1 ·ℎ 𝐵 ) ) +ℎ ( - 1 ·ℎ 𝐴 ) )
18 2 1 hvsubvali ⊢ ( 𝐵 −ℎ 𝐴 ) = ( 𝐵 +ℎ ( - 1 ·ℎ 𝐴 ) )
19 14 17 18 3eqtr4i ⊢ ( ( - 1 ·ℎ 𝐴 ) +ℎ ( - 1 ·ℎ ( - 1 ·ℎ 𝐵 ) ) ) = ( 𝐵 −ℎ 𝐴 )
20 4 7 19 3eqtri ⊢ ( - 1 ·ℎ ( 𝐴 −ℎ 𝐵 ) ) = ( 𝐵 −ℎ 𝐴 )