# Metamath Proof Explorer

## 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}↔\left({R}\in \mathrm{Grp}\wedge {\mathrm{mulGrp}}_{{R}}\in \mathrm{Mnd}\wedge \forall {x}\in {\mathrm{Base}}_{{R}}\phantom{\rule{.4em}{0ex}}\forall {y}\in {\mathrm{Base}}_{{R}}\phantom{\rule{.4em}{0ex}}\forall {z}\in {\mathrm{Base}}_{{R}}\phantom{\rule{.4em}{0ex}}\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}$