Theorem xmulid2

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

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

Proof

Step	Hyp	Ref	Expression
1		1xr	$$⊢1\in {ℝ}^{*}$$
2		xmulcom	$$⊢\left(1\in {ℝ}^{*}\wedge A\in {ℝ}^{*}\right)\to 1{\cdot }_{𝑒}A=A{\cdot }_{𝑒}1$$
3	1 2	mpan	$$⊢A\in {ℝ}^{*}\to 1{\cdot }_{𝑒}A=A{\cdot }_{𝑒}1$$
4		xmulid1	$$⊢A\in {ℝ}^{*}\to A{\cdot }_{𝑒}1=A$$
5	3 4	eqtrd	$$⊢A\in {ℝ}^{*}\to 1{\cdot }_{𝑒}A=A$$