Metamath Proof Explorer


Theorem ringgrp

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

Ref Expression
Assertion ringgrp RRingRGrp

Proof

Step Hyp Ref Expression
1 eqid BaseR=BaseR
2 eqid mulGrpR=mulGrpR
3 eqid +R=+R
4 eqid R=R
5 1 2 3 4 isring RRingRGrpmulGrpRMndxBaseRyBaseRzBaseRxRy+Rz=xRy+RxRzx+RyRz=xRz+RyRz
6 5 simp1bi RRingRGrp