Theorem ringgrp 20185

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

Syntax hints:   → wi 4   ∧ wa 394   = wceq 1533   ∈ wcel 2098  ∀wral 3058  ‘cfv 6553  (class class class)co 7426  Basecbs 17187  +_gcplusg 17240  ._rcmulr 17241  Mndcmnd 18701  Grpcgrp 18897  mulGrpcmgp 20081  Ringcrg 20180

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2699  ax-nul 5310

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-sb 2060  df-clab 2706  df-cleq 2720  df-clel 2806  df-ne 2938  df-ral 3059  df-rab 3431  df-v 3475  df-sbc 3779  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4327  df-if 4533  df-sn 4633  df-pr 4635  df-op 4639  df-uni 4913  df-br 5153  df-iota 6505  df-fv 6561  df-ov 7429  df-ring 20182

This theorem is referenced by:  ringgrpd  20189  ringmnd  20190  ring0cl  20210  ringacl  20221  ringabl  20224  ringnegl  20245  ringnegr  20246  ringmneg1  20247  ringmneg2  20248  mulgass2  20252  ringlghm  20255  ringrghm  20256  prdsringd  20264  imasring  20273  dvdsrneg  20316  dvdsr02  20318  unitnegcl  20343  dvrdir  20358  irrednegb  20377  dfrhm2  20420  isrhmd  20434  idrhm  20436  pwsco1rhm  20448  pwsco2rhm  20449  rhmopp  20455  0ringnnzr  20469  c0rhm  20478  c0rnghm  20479  zrrnghm  20480  subrgsubg  20523  cntzsubr  20552  pwsdiagrhm  20553  subrgacs  20695  isabvd  20707  abvneg  20721  abvsubtri  20722  abvtrivd  20727  srng0  20747  idsrngd  20749  lmodfgrp  20759  lmod0vs  20785  lmodvsneg  20796  lmodsubvs  20808  lmodsubdi  20809  lmodsubdir  20810  rmodislmodlem  20819  rmodislmod  20820  rmodislmodOLD  20821  lmodvsinv  20928  sralmod  21087  issubrgd  21089  lidlsubg  21126  cnfld0  21327  cnfldneg  21330  cnfldsub  21332  cnsubglem  21355  zringgrp  21385  mulgrhm  21410  chrdvds  21463  chrcong  21464  dvdschrmulg  21465  zncyg  21489  cygznlem3  21510  freshmansdream  21515  zrhpsgnelbas  21533  ip2subdi  21583  asclghm  21823  psrlmod  21910  psrring  21920  mpllsslem  21949  mplsubrg  21954  mplcoe1  21982  mplind  22021  evlslem2  22032  mhplss  22086  coe1z  22189  coe1subfv  22192  evl1subd  22268  evl1gsumd  22283  matinvgcell  22357  mat0dim0  22389  mat1ghm  22405  dmatsubcl  22420  dmatsgrp  22421  scmataddcl  22438  scmatsubcl  22439  scmatsgrp  22441  scmatsgrp1  22444  scmatghm  22455  mdetralt  22530  mdetero  22532  mdetunilem6  22539  mdetunilem9  22542  mdetuni0  22543  m2detleiblem6  22548  cpmatinvcl  22639  cpmatsubgpmat  22642  mat2pmatghm  22652  pm2mpghm  22738  chmatcl  22750  chpmat0d  22756  chpmat1d  22758  chpdmatlem1  22760  chpdmatlem2  22761  chpscmat  22764  chpscmatgsumbin  22766  chpscmatgsummon  22767  chp0mat  22768  chpidmat  22769  chfacfisf  22776  chfacfscmulgsum  22782  chfacfpmmulgsum  22786  cayhamlem1  22788  cpmadugsumlemF  22798  cpmidgsum2  22801  trggrp  24096  tlmtgp  24120  abvmet  24504  nrgdsdi  24602  nrgdsdir  24603  tngnrg  24611  cnngp  24716  cnfldtgp  24807  cnncvsaddassdemo  25111  cphsubrglem  25125  mdegldg  26022  mdeg0  26026  mdegaddle  26030  deg1add  26059  deg1suble  26063  deg1sub  26064  deg1sublt  26066  ply1nzb  26078  ply1divmo  26091  ply1divex  26092  r1pcl  26114  r1pid  26116  dvdsq1p  26117  dvdsr1p  26118  ply1remlem  26119  ply1rem  26120  idomrootle  26127  ig1peu  26129  reefgim  26407  lgsqrlem1  27299  lgsqrlem2  27300  lgsqrlem3  27301  lgsqrlem4  27302  abvcxp  27568  rmfsupp2  32966  orngsqr  33043  ornglmulle  33044  orngrmulle  33045  ornglmullt  33046  orngrmullt  33047  orngmullt  33048  suborng  33054  isarchiofld  33056  reofld  33080  linds2eq  33121  qsidomlem1  33193  qsidomlem2  33194  qsnzr  33196  mxidlprm  33208  zringfrac  33277  fedgmullem1  33360  ccfldsrarelvec  33392  zrhchr  33610  matunitlindflem1  37122  lfl0  38569  lflsub  38571  lfl0f  38573  lfladdass  38577  lfladd0l  38578  lflnegcl  38579  lflnegl  38580  ldualvsubcl  38660  ldualvsubval  38661  lkrin  38668  erng0g  40499  lclkrlem2m  41024  lcfrlem2  41048  lcdvsubval  41123  mapdpglem30  41207  baerlem3lem1  41212  baerlem5alem1  41213  baerlem5blem1  41214  baerlem5blem2  41217  hdmapinvlem3  41425  hdmapinvlem4  41426  hdmapglem7b  41433  aks6d1c6lem2  41675  aks6d1c6lem3  41676  aks6d1c6isolem2  41679  hbtlem5  42583  mendlmod  42648  lidldomn1  47371  invginvrid  47509  evl1at0  47537  linply1  47539