Theorem ringgrp 19797

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 2739	. . 3 ⊢ (Base‘𝑅) = (Base‘𝑅)
2		eqid 2739	. . 3 ⊢ (mulGrp‘𝑅) = (mulGrp‘𝑅)
3		eqid 2739	. . 3 ⊢ (+g‘𝑅) = (+g‘𝑅)
4		eqid 2739	. . 3 ⊢ (.r‘𝑅) = (.r‘𝑅)
5	1, 2, 3, 4	isring 19796	. 2 ⊢ (𝑅 ∈ Ring ↔ (𝑅 ∈ Grp ∧ (mulGrp‘𝑅) ∈ Mnd ∧ ∀𝑥 ∈ (Base‘𝑅)∀𝑦 ∈ (Base‘𝑅)∀𝑧 ∈ (Base‘𝑅)((𝑥(.r‘𝑅)(𝑦(+g‘𝑅)𝑧)) = ((𝑥(.r‘𝑅)𝑦)(+g‘𝑅)(𝑥(.r‘𝑅)𝑧)) ∧ ((𝑥(+g‘𝑅)𝑦)(.r‘𝑅)𝑧) = ((𝑥(.r‘𝑅)𝑧)(+g‘𝑅)(𝑦(.r‘𝑅)𝑧)))))
6	5	simp1bi 1144	1 ⊢ (𝑅 ∈ Ring → 𝑅 ∈ Grp)

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1539   ∈ wcel 2107  ∀wral 3065  ‘cfv 6437  (class class class)co 7284  Basecbs 16921  +_gcplusg 16971  ._rcmulr 16972  Mndcmnd 18394  Grpcgrp 18586  mulGrpcmgp 19729  Ringcrg 19792

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2710  ax-nul 5231

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2817  df-ral 3070  df-rex 3071  df-rab 3074  df-v 3435  df-sbc 3718  df-dif 3891  df-un 3893  df-in 3895  df-ss 3905  df-nul 4258  df-if 4461  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4841  df-br 5076  df-iota 6395  df-fv 6445  df-ov 7287  df-ring 19794

This theorem is referenced by:  ringgrpd  19801  ringmnd  19802  ring0cl  19817  ringacl  19826  ringcom  19827  ringabl  19828  ringlz  19835  ringrz  19836  ringnegl  19842  rngnegr  19843  ringmneg1  19844  ringmneg2  19845  ringm2neg  19846  ringsubdi  19847  rngsubdir  19848  mulgass2  19849  ringlghm  19852  ringrghm  19853  prdsringd  19860  imasring  19867  opprring  19882  dvdsrneg  19905  dvdsr02  19907  unitnegcl  19932  irrednegb  19962  dfrhm2  19970  isrhmd  19982  idrhm  19984  pwsco1rhm  19991  pwsco2rhm  19992  drnggrp  20008  subrgsubg  20039  cntzsubr  20066  pwsdiagrhm  20067  subrgacs  20077  isabvd  20089  abvneg  20103  abvsubtri  20104  abvtrivd  20109  srng0  20129  idsrngd  20131  lmodfgrp  20141  lmod0vs  20165  lmodvsneg  20176  lmodsubvs  20188  lmodsubdi  20189  lmodsubdir  20190  rmodislmodlem  20199  rmodislmod  20200  rmodislmodOLD  20201  lssvnegcl  20227  lmodvsinv  20307  sralmod  20466  issubrngd2  20468  lidlsubg  20495  2idlcpbl  20514  0ringnnzr  20549  cnfld0  20631  cnfldneg  20633  cnfldsub  20635  cnsubglem  20656  zringgrp  20684  mulgrhm  20708  chrdvds  20741  chrcong  20742  zncyg  20765  cygznlem3  20786  zrhpsgnelbas  20808  ip2subdi  20858  asclghm  21096  psrlmod  21179  psrdi  21184  psrdir  21185  psrring  21189  mpllsslem  21215  mplsubrg  21220  mplcoe1  21247  mplind  21287  evlslem2  21298  mhplss  21354  coe1z  21443  coe1subfv  21446  evl1subd  21517  evl1gsumd  21532  matinvgcell  21593  mat0dim0  21625  mat1ghm  21641  dmatsubcl  21656  dmatsgrp  21657  scmataddcl  21674  scmatsubcl  21675  scmatsgrp  21677  scmatsgrp1  21680  scmatghm  21691  mdetralt  21766  mdetero  21768  mdetunilem6  21775  mdetunilem9  21778  mdetuni0  21779  m2detleiblem6  21784  cpmatinvcl  21875  cpmatsubgpmat  21878  mat2pmatghm  21888  pm2mpghm  21974  chmatcl  21986  chpmat0d  21992  chpmat1d  21994  chpdmatlem1  21996  chpdmatlem2  21997  chpscmat  22000  chpscmatgsumbin  22002  chpscmatgsummon  22003  chp0mat  22004  chpidmat  22005  chfacfisf  22012  chfacfscmulgsum  22018  chfacfpmmulgsum  22022  cayhamlem1  22024  cpmadugsumlemF  22034  cpmidgsum2  22037  trggrp  23332  tlmtgp  23356  abvmet  23740  nrgdsdi  23838  nrgdsdir  23839  tngnrg  23847  cnngp  23952  cnfldtgp  24041  cnncvsaddassdemo  24336  cphsubrglem  24350  mdegldg  25240  mdeg0  25244  mdegaddle  25248  deg1add  25277  deg1suble  25281  deg1sub  25282  deg1sublt  25284  ply1nzb  25296  ply1divmo  25309  ply1divex  25310  r1pcl  25331  r1pid  25333  dvdsq1p  25334  dvdsr1p  25335  ply1remlem  25336  ply1rem  25337  ig1peu  25345  reefgim  25618  lgsqrlem1  26503  lgsqrlem2  26504  lgsqrlem3  26505  lgsqrlem4  26506  abvcxp  26772  dvdschrmulg  31492  freshmansdream  31493  dvrdir  31496  rmfsupp2  31501  orngsqr  31512  ornglmulle  31513  orngrmulle  31514  ornglmullt  31515  orngrmullt  31516  orngmullt  31517  ofldchr  31522  suborng  31523  isarchiofld  31525  rhmopp  31527  reofld  31553  linds2eq  31584  qsidomlem1  31637  qsidomlem2  31638  mxidlprm  31649  fedgmullem1  31719  ccfldsrarelvec  31750  zrhchr  31935  matunitlindflem1  35782  lfl0  37086  lflsub  37088  lfl0f  37090  lfladdass  37094  lfladd0l  37095  lflnegcl  37096  lflnegl  37097  ldualvsubcl  37177  ldualvsubval  37178  lkrin  37185  erng0g  39015  lclkrlem2m  39540  lcfrlem2  39564  lcdvsubval  39639  mapdpglem30  39723  baerlem3lem1  39728  baerlem5alem1  39729  baerlem5blem1  39730  baerlem5blem2  39733  hdmapinvlem3  39941  hdmapinvlem4  39942  hdmapglem7b  39949  hbtlem5  40960  mendlmod  41025  idomrootle  41027  c0rhm  45481  c0rnghm  45482  zrrnghm  45486  lidldomn1  45490  invginvrid  45714  evl1at0  45743  linply1  45745