Theorem ringgrp

Description: A ring is a group. (Contributed by NM, 15-Sep-2011)

	Ref	Expression
Assertion	ringgrp	$$⊢R\in \mathrm{Ring}\to R\in \mathrm{Grp}$$

Proof

Step	Hyp	Ref	Expression
1		eqid	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_R$$
2		eqid	$$⊢{\mathrm{mulGrp}}_R={\mathrm{mulGrp}}_R$$
3		eqid	$$⊢{+}_R={+}_R$$
4		eqid	$$⊢{\cdot }_R={\cdot }_R$$
5	1 2 3 4	isring	$$⊢R\in \mathrm{Ring}\leftrightarrow \left(R\in \mathrm{Grp}\wedge {\mathrm{mulGrp}}_R\in \mathrm{Mnd}\wedge \forall x\in {\mathrm{Base}}_R\forall y\in {\mathrm{Base}}_R\forall z\in {\mathrm{Base}}_R\left(x{\cdot }_R\left(y{+}_{R}z\right)=\left(x{\cdot }_{R}y\right){+}_R\left(x{\cdot }_{R}z\right)\wedge \left(x{+}_{R}y\right){\cdot }_{R}z=\left(x{\cdot }_{R}z\right){+}_R\left(y{\cdot }_{R}z\right)\right)\right)$$
6	5	simp1bi	$$⊢R\in \mathrm{Ring}\to R\in \mathrm{Grp}$$