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

Metamath Proof Explorer

Theorem ringabl

Description: A ring is an Abelian group. (Contributed by NM, 26-Aug-2011)

		Ref	Expression
	Assertion	ringabl	$⊢ R \in Ring \to R \in Abel$

Step	Hyp	Ref	Expression
1		eqidd	$⊢ R \in Ring \to {Base}_{R} = {Base}_{R}$
2		eqidd	$⊢ R \in Ring \to +_{R} = +_{R}$
3		ringgrp	$⊢ R \in Ring \to R \in Grp$
4		eqid	$⊢ {Base}_{R} = {Base}_{R}$
5		eqid	$⊢ +_{R} = +_{R}$
6	4 5	ringcom	$⊢ (R \in Ring \land x \in {Base}_{R} \land y \in {Base}_{R}) \to x +_{R} y = y +_{R} x$
7	1 2 3 6	isabld	$⊢ R \in Ring \to R \in Abel$