Theorem rngo0lid

Description: The additive identity of a ring is a left identity element. (Contributed by Steve Rodriguez, 9-Sep-2007) (New usage is discouraged.)

	Ref	Expression
Hypotheses	ring0cl.1	$$⊢G=1^{st}\left(R\right)$$
	ring0cl.2	$$⊢X=\mathrm{ran}G$$
	ring0cl.3	$$⊢Z=\mathrm{GId}\left(G\right)$$
Assertion	rngo0lid	$$⊢\left(R\in \mathrm{RingOps}\wedge A\in X\right)\to ZGA=A$$

Proof

Step	Hyp	Ref	Expression
1		ring0cl.1	$$⊢G=1^{st}\left(R\right)$$
2		ring0cl.2	$$⊢X=\mathrm{ran}G$$
3		ring0cl.3	$$⊢Z=\mathrm{GId}\left(G\right)$$
4	1	rngogrpo	$$⊢R\in \mathrm{RingOps}\to G\in \mathrm{GrpOp}$$
5	2 3	grpolid	$$⊢\left(G\in \mathrm{GrpOp}\wedge A\in X\right)\to ZGA=A$$
6	4 5	sylan	$$⊢\left(R\in \mathrm{RingOps}\wedge A\in X\right)\to ZGA=A$$