Theorem xmulm1

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

	Ref	Expression
Assertion	xmulm1	$$⊢A\in {ℝ}^{*}\to -1{\cdot }_{𝑒}A=-A$$

Proof

Step	Hyp	Ref	Expression
1		1re	$$⊢1\in ℝ$$
2		rexneg	$$⊢1\in ℝ\to -1=-1$$
3	1 2	ax-mp	$$⊢-1=-1$$
4	3	oveq1i	$$⊢\left(-1\right){\cdot }_{𝑒}A=-1{\cdot }_{𝑒}A$$
5		1xr	$$⊢1\in {ℝ}^{*}$$
6		xmulneg1	$$⊢\left(1\in {ℝ}^{*}\wedge A\in {ℝ}^{*}\right)\to \left(-1\right){\cdot }_{𝑒}A=-\left(1{\cdot }_{𝑒}A\right)$$
7	5 6	mpan	$$⊢A\in {ℝ}^{*}\to \left(-1\right){\cdot }_{𝑒}A=-\left(1{\cdot }_{𝑒}A\right)$$
8	4 7	eqtr3id	$$⊢A\in {ℝ}^{*}\to -1{\cdot }_{𝑒}A=-\left(1{\cdot }_{𝑒}A\right)$$
9		xmulid2	$$⊢A\in {ℝ}^{*}\to 1{\cdot }_{𝑒}A=A$$
10		xnegeq	$$⊢1{\cdot }_{𝑒}A=A\to -\left(1{\cdot }_{𝑒}A\right)=-A$$
11	9 10	syl	$$⊢A\in {ℝ}^{*}\to -\left(1{\cdot }_{𝑒}A\right)=-A$$
12	8 11	eqtrd	$$⊢A\in {ℝ}^{*}\to -1{\cdot }_{𝑒}A=-A$$