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

Proof

Step	Hyp	Ref	Expression
1		hvnegdi.1	$$⊢A\in \mathscr{H}$$
2		hvnegdi.2	$$⊢B\in \mathscr{H}$$
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 \mathscr{H}$$
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 \mathscr{H}\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 \mathscr{H}$$
16	5 6	hvmulcli	$$⊢-1{\cdot }_{ℎ}\left(-1{\cdot }_{ℎ}B\right)\in \mathscr{H}$$
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$$