This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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} (R)$
	Assertion	rngogrpo	$⊢ R \in RingOps \to G \in GrpOp$

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