Metamath Proof Explorer

Theorem rngoablo

Description: A ring's addition operation is an Abelian group operation. (Contributed by Steve Rodriguez, 9-Sep-2007) (Revised by Mario Carneiro, 21-Dec-2013) (New usage is discouraged.)

		Ref	Expression
	Hypothesis	ringabl.1	$⊢ G = 1^{st} (R)$
	Assertion	rngoablo	$⊢ R \in RingOps \to G \in AbelOp$

Proof

Step	Hyp	Ref	Expression
1		ringabl.1	$⊢ G = 1^{st} (R)$
2		eqid	$⊢ 2^{nd} (R) = 2^{nd} (R)$
3		eqid	$⊢ ran G = ran G$
4	1 2 3	rngoi	$⊢ R \in RingOps \to ((G \in AbelOp \land 2^{nd} (R) : ran G \times ran G ⟶ ran G) \land (\forall x \in ran G \forall y \in ran G \forall z \in ran G ((x 2^{nd} (R) y) 2^{nd} (R) z = x 2^{nd} (R) (y 2^{nd} (R) z) \land x 2^{nd} (R) (y G z) = (x 2^{nd} (R) y) G (x 2^{nd} (R) z) \land (x G y) 2^{nd} (R) z = (x 2^{nd} (R) z) G (y 2^{nd} (R) z)) \land \exists x \in ran G \forall y \in ran G (x 2^{nd} (R) y = y \land y 2^{nd} (R) x = y)))$
5	4	simplld	$⊢ R \in RingOps \to G \in AbelOp$