Theorem xmul02

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

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

Proof

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