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 ∈ ℋ
hvnegdi.2 ⊢ B ∈ ℋ
Assertion hvnegdii ⊢ -1 ⋅ ℎ A - ℎ B = B - ℎ A

Proof

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