Theorem rngo0cl

Description: A ring has an additive 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	rngo0cl	$$⊢R\in \mathrm{RingOps}\to Z\in X$$

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	grpoidcl	$$⊢G\in \mathrm{GrpOp}\to Z\in X$$
6	4 5	syl	$$⊢R\in \mathrm{RingOps}\to Z\in X$$