# 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}\in ℋ$
hvnegdi.2 ${⊢}{B}\in ℋ$
Assertion hvnegdii ${⊢}-1{\cdot }_{ℎ}\left({A}{-}_{ℎ}{B}\right)={B}{-}_{ℎ}{A}$

### Proof

Step Hyp Ref Expression
1 hvnegdi.1 ${⊢}{A}\in ℋ$
2 hvnegdi.2 ${⊢}{B}\in ℋ$
3 1 2 hvsubvali ${⊢}{A}{-}_{ℎ}{B}={A}{+}_{ℎ}\left(-1{\cdot }_{ℎ}{B}\right)$
4 3 oveq2i ${⊢}-1{\cdot }_{ℎ}\left({A}{-}_{ℎ}{B}\right)=-1{\cdot }_{ℎ}\left({A}{+}_{ℎ}\left(-1{\cdot }_{ℎ}{B}\right)\right)$
5 neg1cn ${⊢}-1\in ℂ$
6 5 2 hvmulcli ${⊢}-1{\cdot }_{ℎ}{B}\in ℋ$
7 5 1 6 hvdistr1i ${⊢}-1{\cdot }_{ℎ}\left({A}{+}_{ℎ}\left(-1{\cdot }_{ℎ}{B}\right)\right)=\left(-1{\cdot }_{ℎ}{A}\right){+}_{ℎ}\left(-1{\cdot }_{ℎ}\left(-1{\cdot }_{ℎ}{B}\right)\right)$
8 neg1mulneg1e1 ${⊢}-1-1=1$
9 8 oveq1i ${⊢}-1-1{\cdot }_{ℎ}{B}=1{\cdot }_{ℎ}{B}$
10 5 5 2 hvmulassi ${⊢}-1-1{\cdot }_{ℎ}{B}=-1{\cdot }_{ℎ}\left(-1{\cdot }_{ℎ}{B}\right)$
11 ax-hvmulid ${⊢}{B}\in ℋ\to 1{\cdot }_{ℎ}{B}={B}$
12 2 11 ax-mp ${⊢}1{\cdot }_{ℎ}{B}={B}$
13 9 10 12 3eqtr3i ${⊢}-1{\cdot }_{ℎ}\left(-1{\cdot }_{ℎ}{B}\right)={B}$
14 13 oveq1i ${⊢}\left(-1{\cdot }_{ℎ}\left(-1{\cdot }_{ℎ}{B}\right)\right){+}_{ℎ}\left(-1{\cdot }_{ℎ}{A}\right)={B}{+}_{ℎ}\left(-1{\cdot }_{ℎ}{A}\right)$
15 5 1 hvmulcli ${⊢}-1{\cdot }_{ℎ}{A}\in ℋ$
16 5 6 hvmulcli ${⊢}-1{\cdot }_{ℎ}\left(-1{\cdot }_{ℎ}{B}\right)\in ℋ$
17 15 16 hvcomi ${⊢}\left(-1{\cdot }_{ℎ}{A}\right){+}_{ℎ}\left(-1{\cdot }_{ℎ}\left(-1{\cdot }_{ℎ}{B}\right)\right)=\left(-1{\cdot }_{ℎ}\left(-1{\cdot }_{ℎ}{B}\right)\right){+}_{ℎ}\left(-1{\cdot }_{ℎ}{A}\right)$
18 2 1 hvsubvali ${⊢}{B}{-}_{ℎ}{A}={B}{+}_{ℎ}\left(-1{\cdot }_{ℎ}{A}\right)$
19 14 17 18 3eqtr4i ${⊢}\left(-1{\cdot }_{ℎ}{A}\right){+}_{ℎ}\left(-1{\cdot }_{ℎ}\left(-1{\cdot }_{ℎ}{B}\right)\right)={B}{-}_{ℎ}{A}$
20 4 7 19 3eqtri ${⊢}-1{\cdot }_{ℎ}\left({A}{-}_{ℎ}{B}\right)={B}{-}_{ℎ}{A}$