Theorem ringgrp 20311

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

Assertion

Ref	Expression
ringgrp	⊢ (𝑅 ∈ Ring → 𝑅 ∈ Grp)

Proof of Theorem ringgrp

Dummy variables 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		eqid 2765	. . 3 ⊢ (Base‘𝑅) = (Base‘𝑅)
2		eqid 2765	. . 3 ⊢ (mulGrp‘𝑅) = (mulGrp‘𝑅)
3		eqid 2765	. . 3 ⊢ (+g‘𝑅) = (+g‘𝑅)
4		eqid 2765	. . 3 ⊢ (.r‘𝑅) = (.r‘𝑅)
5	1, 2, 3, 4	isring 20310	. 2 ⊢ (𝑅 ∈ Ring ↔ (𝑅 ∈ Grp ∧ (mulGrp‘𝑅) ∈ Mnd ∧ ∀𝑥 ∈ (Base‘𝑅)∀𝑦 ∈ (Base‘𝑅)∀𝑧 ∈ (Base‘𝑅)((𝑥(.r‘𝑅)(𝑦(+g‘𝑅)𝑧)) = ((𝑥(.r‘𝑅)𝑦)(+g‘𝑅)(𝑥(.r‘𝑅)𝑧)) ∧ ((𝑥(+g‘𝑅)𝑦)(.r‘𝑅)𝑧) = ((𝑥(.r‘𝑅)𝑧)(+g‘𝑅)(𝑦(.r‘𝑅)𝑧)))))
6	5	simp1bi 1161	1 ⊢ (𝑅 ∈ Ring → 𝑅 ∈ Grp)

Syntax hints:   → wi 4   ∧ wa 400   = wceq 1563   ∈ wcel 2145  ∀wral 3079  ‘cfv 6525  (class class class)co 7400  Basecbs 17259  +_gcplusg 17300  ._rcmulr 17301  Mndcmnd 18782  Grpcgrp 18990  mulGrpcmgp 20207  Ringcrg 20306

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737  ax-nul 5261

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-ne 2961  df-ral 3080  df-rab 3418  df-v 3459  df-sbc 3748  df-dif 3910  df-un 3912  df-ss 3924  df-nul 4289  df-if 4484  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4869  df-br 5106  df-iota 6481  df-fv 6533  df-ov 7403  df-ring 20308

This theorem is referenced by:  ringgrpd  20315  ringmnd  20316  ring0cl  20341  ringacl  20352  ringabl  20355  ringnegl  20376  ringnegr  20377  ringmneg1  20378  ringmneg2  20379  mulgass2  20383  ringlghm  20386  ringrghm  20387  prdsringd  20393  imasring  20403  dvdsrneg  20443  dvdsr02  20445  unitnegcl  20470  dvrdir  20485  irrednegb  20504  dfrhm2  20547  isrhmd  20561  idrhm  20563  pwsco1rhm  20575  pwsco2rhm  20576  rhmopp  20583  0ringnnzr  20600  c0rhm  20610  c0rnghm  20611  zrrnghm  20612  subrgsubg  20653  cntzsubr  20682  pwsdiagrhm  20683  subrgacs  20872  isabvd  20884  abvneg  20898  abvsubtri  20899  abvtrivd  20904  srng0  20926  idsrngd  20928  orngsqr  20938  ornglmulle  20939  orngrmulle  20940  ornglmullt  20941  orngrmullt  20942  orngmullt  20943  suborng  20948  lmodfgrp  20959  lmod0vs  20985  lmodvsneg  20996  lmodsubvs  21008  lmodsubdi  21009  lmodsubdir  21010  rmodislmodlem  21019  rmodislmod  21020  lmodvsinv  21126  sralmod  21277  issubrgd  21279  lidlsubg  21317  qsidomlem1  21440  qsidomlem2  21441  qsnzr  21443  cnfld0  21506  cnfldneg  21508  cnfldsub  21510  cnsubglem  21526  zringgrp  21562  mulgrhm  21587  chrdvds  21636  chrcong  21637  dvdschrmulg  21638  zncyg  21658  cygznlem3  21679  freshmansdream  21684  zrhpsgnelbas  21704  ip2subdi  21754  asclghm  21992  psrlmod  22069  psrring  22079  mpllsslem  22109  mplsubrg  22114  mplcoe1  22148  mplind  22181  evlslem2  22190  coe1z  22384  coe1subfv  22387  evl1subd  22463  evl1gsumd  22478  matinvgcell  22553  mat0dim0  22585  mat1ghm  22601  dmatsubcl  22616  dmatsgrp  22617  scmataddcl  22634  scmatsubcl  22635  scmatsgrp  22637  scmatsgrp1  22640  scmatghm  22651  mdetralt  22726  mdetero  22728  mdetunilem6  22735  mdetunilem9  22738  mdetuni0  22739  m2detleiblem6  22744  cpmatinvcl  22835  cpmatsubgpmat  22838  mat2pmatghm  22848  pm2mpghm  22934  chmatcl  22946  chpmat0d  22952  chpmat1d  22954  chpdmatlem1  22956  chpdmatlem2  22957  chpscmat  22960  chpscmatgsumbin  22962  chpscmatgsummon  22963  chp0mat  22964  chpidmat  22965  chfacfisf  22972  chfacfscmulgsum  22978  chfacfpmmulgsum  22982  cayhamlem1  22984  cpmadugsumlemF  22994  cpmidgsum2  22997  trggrp  24290  tlmtgp  24314  abvmet  24693  nrgdsdi  24783  nrgdsdir  24784  tngnrg  24792  cnngp  24897  cnfldtgp  24989  cnncvsaddassdemo  25283  cphsubrglem  25297  mdegldg  26184  mdeg0  26188  mdegaddle  26192  deg1add  26221  deg1suble  26225  deg1sub  26226  deg1sublt  26228  ply1nzb  26241  ply1divmo  26254  ply1divex  26255  r1pcl  26277  r1pid  26279  dvdsq1p  26281  dvdsr1p  26282  ply1remlem  26283  ply1rem  26284  idomrootle  26291  ig1peu  26293  reefgim  26571  lgsqrlem1  27468  lgsqrlem2  27469  lgsqrlem3  27470  lgsqrlem4  27471  abvcxp  27737  isarchiofld  33432  rmfsupp2  33470  reofld  33578  linds2eq  33610  mxidlprm  33670  zringfrac  33761  esplyind  33882  vietadeg1  33885  fedgmullem1  33936  ccfldsrarelvec  33978  zrhchr  34281  matunitlindflem1  38127  lfl0  39701  lflsub  39703  lfl0f  39705  lfladdass  39709  lfladd0l  39710  lflnegcl  39711  lflnegl  39712  ldualvsubcl  39792  ldualvsubval  39793  lkrin  39800  erng0g  41630  lclkrlem2m  42155  lcfrlem2  42179  lcdvsubval  42254  mapdpglem30  42338  baerlem3lem1  42343  baerlem5alem1  42344  baerlem5blem1  42345  baerlem5blem2  42348  hdmapinvlem3  42556  hdmapinvlem4  42557  hdmapglem7b  42564  aks6d1c6lem2  42800  aks6d1c6lem3  42801  aks6d1c6isolem2  42804  aks5lem3a  42818  aks5lem7  42829  hbtlem5  43717  mendlmod  43778  lidldomn1  48851  invginvrid  48998  evl1at0  49022  linply1  49024