Theorem rngolidm

Description: The unity element of a ring is an identity element for the multiplication. (Contributed by FL, 18-Apr-2010) (New usage is discouraged.)

	Ref	Expression
Hypotheses	uridm.1	$$⊢H=2^{nd}\left(R\right)$$
	uridm.2	$$⊢X=\mathrm{ran}{1}^{st}\left(R\right)$$
	uridm.3	$$⊢U=\mathrm{GId}\left(H\right)$$
Assertion	rngolidm	$$⊢\left(R\in \mathrm{RingOps}\wedge A\in X\right)\to UHA=A$$

Proof

Step	Hyp	Ref	Expression
1		uridm.1	$$⊢H=2^{nd}\left(R\right)$$
2		uridm.2	$$⊢X=\mathrm{ran}{1}^{st}\left(R\right)$$
3		uridm.3	$$⊢U=\mathrm{GId}\left(H\right)$$
4	1 2 3	rngoidmlem	$$⊢\left(R\in \mathrm{RingOps}\wedge A\in X\right)\to \left(UHA=A\wedge AHU=A\right)$$
5	4	simpld	$$⊢\left(R\in \mathrm{RingOps}\wedge A\in X\right)\to UHA=A$$