Theorem rngogrpo

Description: A ring's addition operation is a group operation. (Contributed by Steve Rodriguez, 9-Sep-2007) (New usage is discouraged.)

	Ref	Expression
Hypothesis	ringgrp.1	$$⊢G=1^{st}\left(R\right)$$
Assertion	rngogrpo	$$⊢R\in \mathrm{RingOps}\to G\in \mathrm{GrpOp}$$

Proof

Step	Hyp	Ref	Expression
1		ringgrp.1	$$⊢G=1^{st}\left(R\right)$$
2	1	rngoablo	$$⊢R\in \mathrm{RingOps}\to G\in \mathrm{AbelOp}$$
3		ablogrpo	$$⊢G\in \mathrm{AbelOp}\to G\in \mathrm{GrpOp}$$
4	2 3	syl	$$⊢R\in \mathrm{RingOps}\to G\in \mathrm{GrpOp}$$