Theorem hvmul2negi

Description: Double negative in scalar multiplication. (Contributed by NM, 3-Sep-1999) (New usage is discouraged.)

	Ref	Expression
Hypotheses	hvmulcom.1	$$⊢A\in ℂ$$
	hvmulcom.2	$$⊢B\in ℂ$$
	hvmulcom.3	$$⊢C\in \mathscr{H}$$
Assertion	hvmul2negi	$$⊢\left(-A\right){\cdot }_{ℎ}\left(\left(-B\right){\cdot }_{ℎ}C\right)=A{\cdot }_{ℎ}\left(B{\cdot }_{ℎ}C\right)$$

Proof

Step	Hyp	Ref	Expression
1		hvmulcom.1	$$⊢A\in ℂ$$
2		hvmulcom.2	$$⊢B\in ℂ$$
3		hvmulcom.3	$$⊢C\in \mathscr{H}$$
4	1 2	mul2negi	$$⊢\left(-A\right)\left(-B\right)=AB$$
5	4	oveq1i	$$⊢\left(-A\right)\left(-B\right){\cdot }_{ℎ}C=AB{\cdot }_{ℎ}C$$
6	1	negcli	$$⊢-A\in ℂ$$
7	2	negcli	$$⊢-B\in ℂ$$
8	6 7 3	hvmulassi	$$⊢\left(-A\right)\left(-B\right){\cdot }_{ℎ}C=\left(-A\right){\cdot }_{ℎ}\left(\left(-B\right){\cdot }_{ℎ}C\right)$$
9	1 2 3	hvmulassi	$$⊢AB{\cdot }_{ℎ}C=A{\cdot }_{ℎ}\left(B{\cdot }_{ℎ}C\right)$$
10	5 8 9	3eqtr3i	$$⊢\left(-A\right){\cdot }_{ℎ}\left(\left(-B\right){\cdot }_{ℎ}C\right)=A{\cdot }_{ℎ}\left(B{\cdot }_{ℎ}C\right)$$