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	⊢ 𝐺 = ( 1st ‘ 𝑅 )
Assertion	rngogrpo	⊢ ( 𝑅 ∈ RingOps → 𝐺 ∈ GrpOp )

Proof

Step	Hyp	Ref	Expression
1		ringgrp.1	⊢ 𝐺 = ( 1st ‘ 𝑅 )
2	1	rngoablo	⊢ ( 𝑅 ∈ RingOps → 𝐺 ∈ AbelOp )
3		ablogrpo	⊢ ( 𝐺 ∈ AbelOp → 𝐺 ∈ GrpOp )
4	2 3	syl	⊢ ( 𝑅 ∈ RingOps → 𝐺 ∈ GrpOp )