Theorem xmulneg2

Description: Extended real version of mulneg2 . (Contributed by Mario Carneiro, 20-Aug-2015)

	Ref	Expression
Assertion	xmulneg2	$$⊢\left(A\in {ℝ}^{*}\wedge B\in {ℝ}^{*}\right)\to A{\cdot }_{𝑒}\left(-B\right)=-\left(A{\cdot }_{𝑒}B\right)$$

Proof

Step	Hyp	Ref	Expression
1		xmulneg1	$$⊢\left(B\in {ℝ}^{*}\wedge A\in {ℝ}^{*}\right)\to \left(-B\right){\cdot }_{𝑒}A=-\left(B{\cdot }_{𝑒}A\right)$$
2	1	ancoms	$$⊢\left(A\in {ℝ}^{*}\wedge B\in {ℝ}^{*}\right)\to \left(-B\right){\cdot }_{𝑒}A=-\left(B{\cdot }_{𝑒}A\right)$$
3		xnegcl	$$⊢B\in {ℝ}^{*}\to -B\in {ℝ}^{*}$$
4		xmulcom	$$⊢\left(A\in {ℝ}^{*}\wedge -B\in {ℝ}^{*}\right)\to A{\cdot }_{𝑒}\left(-B\right)=\left(-B\right){\cdot }_{𝑒}A$$
5	3 4	sylan2	$$⊢\left(A\in {ℝ}^{*}\wedge B\in {ℝ}^{*}\right)\to A{\cdot }_{𝑒}\left(-B\right)=\left(-B\right){\cdot }_{𝑒}A$$
6		xmulcom	$$⊢\left(A\in {ℝ}^{*}\wedge B\in {ℝ}^{*}\right)\to A{\cdot }_{𝑒}B=B{\cdot }_{𝑒}A$$
7		xnegeq	$$⊢A{\cdot }_{𝑒}B=B{\cdot }_{𝑒}A\to -\left(A{\cdot }_{𝑒}B\right)=-\left(B{\cdot }_{𝑒}A\right)$$
8	6 7	syl	$$⊢\left(A\in {ℝ}^{*}\wedge B\in {ℝ}^{*}\right)\to -\left(A{\cdot }_{𝑒}B\right)=-\left(B{\cdot }_{𝑒}A\right)$$
9	2 5 8	3eqtr4d	$$⊢\left(A\in {ℝ}^{*}\wedge B\in {ℝ}^{*}\right)\to A{\cdot }_{𝑒}\left(-B\right)=-\left(A{\cdot }_{𝑒}B\right)$$