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 = ( 1st ` R )
Assertion	rngogrpo	|- ( R e. RingOps -> G e. GrpOp )

Proof

Step	Hyp	Ref	Expression
1		ringgrp.1	|- G = ( 1st ` R )
2	1	rngoablo	|- ( R e. RingOps -> G e. AbelOp )
3		ablogrpo	|- ( G e. AbelOp -> G e. GrpOp )
4	2 3	syl	|- ( R e. RingOps -> G e. GrpOp )