Theorem ringgrp 20267

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

Syntax hints:   → wi 4   ∧ wa 399   = wceq 1559   ∈ wcel 2141  ∀wral 3075  ‘cfv 6517  (class class class)co 7392  Basecbs 17228  +_gcplusg 17269  ._rcmulr 17270  Mndcmnd 18751  Grpcgrp 18958  mulGrpcmgp 20169  Ringcrg 20262

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733  ax-nul 5255

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-ne 2957  df-ral 3076  df-rab 3414  df-v 3455  df-sbc 3745  df-dif 3907  df-un 3909  df-ss 3921  df-nul 4286  df-if 4480  df-sn 4582  df-pr 4584  df-op 4588  df-uni 4865  df-br 5100  df-iota 6473  df-fv 6525  df-ov 7395  df-ring 20264

This theorem is referenced by:  ringgrpd  20271  ringmnd  20272  ring0cl  20296  ringacl  20307  ringabl  20310  ringnegl  20331  ringnegr  20332  ringmneg1  20333  ringmneg2  20334  mulgass2  20338  ringlghm  20341  ringrghm  20342  prdsringd  20348  imasring  20358  dvdsrneg  20398  dvdsr02  20400  unitnegcl  20425  dvrdir  20440  irrednegb  20459  dfrhm2  20502  isrhmd  20516  idrhm  20518  pwsco1rhm  20530  pwsco2rhm  20531  rhmopp  20538  0ringnnzr  20554  c0rhm  20563  c0rnghm  20564  zrrnghm  20565  subrgsubg  20606  cntzsubr  20635  pwsdiagrhm  20636  subrgacs  20829  isabvd  20841  abvneg  20855  abvsubtri  20856  abvtrivd  20861  srng0  20883  idsrngd  20885  orngsqr  20895  ornglmulle  20896  orngrmulle  20897  ornglmullt  20898  orngrmullt  20899  orngmullt  20900  suborng  20905  lmodfgrp  20916  lmod0vs  20942  lmodvsneg  20953  lmodsubvs  20965  lmodsubdi  20966  lmodsubdir  20967  rmodislmodlem  20976  rmodislmod  20977  lmodvsinv  21083  sralmod  21234  issubrgd  21236  lidlsubg  21273  cnfld0  21428  cnfldneg  21430  cnfldsub  21432  cnsubglem  21448  zringgrp  21484  mulgrhm  21509  chrdvds  21558  chrcong  21559  dvdschrmulg  21560  zncyg  21580  cygznlem3  21601  freshmansdream  21606  zrhpsgnelbas  21626  ip2subdi  21676  asclghm  21914  psrlmod  21991  psrring  22001  mpllsslem  22031  mplsubrg  22036  mplcoe1  22070  mplind  22103  evlslem2  22112  coe1z  22306  coe1subfv  22309  evl1subd  22385  evl1gsumd  22400  matinvgcell  22475  mat0dim0  22507  mat1ghm  22523  dmatsubcl  22538  dmatsgrp  22539  scmataddcl  22556  scmatsubcl  22557  scmatsgrp  22559  scmatsgrp1  22562  scmatghm  22573  mdetralt  22648  mdetero  22650  mdetunilem6  22657  mdetunilem9  22660  mdetuni0  22661  m2detleiblem6  22666  cpmatinvcl  22757  cpmatsubgpmat  22760  mat2pmatghm  22770  pm2mpghm  22856  chmatcl  22868  chpmat0d  22874  chpmat1d  22876  chpdmatlem1  22878  chpdmatlem2  22879  chpscmat  22882  chpscmatgsumbin  22884  chpscmatgsummon  22885  chp0mat  22886  chpidmat  22887  chfacfisf  22894  chfacfscmulgsum  22900  chfacfpmmulgsum  22904  cayhamlem1  22906  cpmadugsumlemF  22916  cpmidgsum2  22919  trggrp  24212  tlmtgp  24236  abvmet  24615  nrgdsdi  24705  nrgdsdir  24706  tngnrg  24714  cnngp  24819  cnfldtgp  24911  cnncvsaddassdemo  25205  cphsubrglem  25219  mdegldg  26106  mdeg0  26110  mdegaddle  26114  deg1add  26143  deg1suble  26147  deg1sub  26148  deg1sublt  26150  ply1nzb  26163  ply1divmo  26176  ply1divex  26177  r1pcl  26199  r1pid  26201  dvdsq1p  26203  dvdsr1p  26204  ply1remlem  26205  ply1rem  26206  idomrootle  26213  ig1peu  26215  reefgim  26490  lgsqrlem1  27387  lgsqrlem2  27388  lgsqrlem3  27389  lgsqrlem4  27390  abvcxp  27656  isarchiofld  33340  rmfsupp2  33379  reofld  33490  linds2eq  33528  qsidomlem1  33600  qsidomlem2  33601  qsnzr  33603  mxidlprm  33619  zringfrac  33711  esplyind  33833  vietadeg1  33836  fedgmullem1  33887  ccfldsrarelvec  33929  zrhchr  34232  matunitlindflem1  38079  lfl0  39653  lflsub  39655  lfl0f  39657  lfladdass  39661  lfladd0l  39662  lflnegcl  39663  lflnegl  39664  ldualvsubcl  39744  ldualvsubval  39745  lkrin  39752  erng0g  41582  lclkrlem2m  42107  lcfrlem2  42131  lcdvsubval  42206  mapdpglem30  42290  baerlem3lem1  42295  baerlem5alem1  42296  baerlem5blem1  42297  baerlem5blem2  42300  hdmapinvlem3  42508  hdmapinvlem4  42509  hdmapglem7b  42516  aks6d1c6lem2  42752  aks6d1c6lem3  42753  aks6d1c6isolem2  42756  aks5lem3a  42770  aks5lem7  42781  hbtlem5  43669  mendlmod  43730  lidldomn1  48817  invginvrid  48953  evl1at0  48977  linply1  48979