Theorem ringabl

Description: A ring is an Abelian group. (Contributed by Steve Rodriguez, 9-Sep-2007) (Revised by NM, 26-Aug-2011)

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

Proof

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