MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  crngring Structured version   Visualization version   GIF version

Theorem crngring 19297
Description: A commutative ring is a ring. (Contributed by Mario Carneiro, 7-Jan-2015.)
Assertion
Ref Expression
crngring (𝑅 ∈ CRing → 𝑅 ∈ Ring)

Proof of Theorem crngring
StepHypRef Expression
1 eqid 2824 . . 3 (mulGrp‘𝑅) = (mulGrp‘𝑅)
21iscrng 19293 . 2 (𝑅 ∈ CRing ↔ (𝑅 ∈ Ring ∧ (mulGrp‘𝑅) ∈ CMnd))
32simplbi 501 1 (𝑅 ∈ CRing → 𝑅 ∈ Ring)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2115  cfv 6336  CMndccmn 18895  mulGrpcmgp 19228  Ringcrg 19286  CRingccrg 19287
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2179  ax-ext 2796
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2071  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2964  df-rab 3141  df-v 3481  df-dif 3921  df-un 3923  df-in 3925  df-ss 3935  df-nul 4275  df-if 4449  df-sn 4549  df-pr 4551  df-op 4555  df-uni 4820  df-br 5048  df-iota 6295  df-fv 6344  df-cring 19289
This theorem is referenced by:  gsummgp0  19347  prdscrngd  19352  crngbinom  19360  dvdsunit  19402  unitmulclb  19404  unitabl  19407  idsrngd  19619  rmodislmod  19688  quscrng  19999  assa2ass  20081  sraassa  20085  rlmassa  20086  ascldimulOLD  20103  asclrhm  20105  assamulgscmlem2  20115  psrcrng  20179  psrassa  20180  mplcrng  20220  mplassa  20221  mplcoe2  20236  mplbas2  20237  mplmon2mul  20267  mplind  20268  evlslem2  20278  evlslem3  20279  evlslem6  20280  evlslem1  20281  evlseu  20282  evlsval2  20286  evlsgsumadd  20290  evlsgsummul  20291  evlrhm  20295  evlsscasrng  20296  evlsca  20297  evlsvarsrng  20298  evlvar  20299  mpfind  20306  ply1crng  20352  ply1assa  20353  lply1binom  20460  lply1binomsc  20461  evls1rhmlem  20470  evls1gsumadd  20473  evls1gsummul  20474  evl1val  20478  evl1sca  20483  evl1scad  20484  evl1var  20485  evl1vard  20486  evls1var  20487  evls1scasrng  20488  evls1varsrng  20489  evl1subd  20491  evl1expd  20494  pf1const  20495  pf1id  20496  pf1ind  20504  evl1gsumdlem  20505  evl1gsumd  20506  evl1gsumadd  20507  evl1gsummul  20509  evl1varpw  20510  evl1scvarpw  20512  evl1scvarpwval  20513  evl1gsummon  20514  cnring  20553  zringring  20606  zring0  20613  znzrh2  20678  zncyg  20681  zndvds0  20683  znf1o  20684  zzngim  20685  znfld  20693  znchr  20695  znunit  20696  znrrg  20698  cygznlem3  20702  re0g  20742  mamuvs2  21001  matassa  21039  madetsumid  21056  madetsmelbas  21059  madetsmelbas2  21060  mat1dimcrng  21072  dmatcrng  21097  scmatcrng  21116  mdetleib2  21183  mdetf  21190  m1detdiag  21192  mdetdiaglem  21193  mdetdiag  21194  mdet1  21196  mdetrlin  21197  mdetrsca  21198  mdetrsca2  21199  mdetr0  21200  mdet0  21201  mdetrlin2  21202  mdetralt  21203  mdetero  21205  mdetmul  21218  maducoeval2  21235  maduf  21236  madutpos  21237  madugsum  21238  madurid  21239  madulid  21240  marep01ma  21255  smadiadetlem0  21256  smadiadetlem1a  21258  smadiadetlem3lem2  21262  smadiadetlem3  21263  smadiadetlem4  21264  smadiadet  21265  smadiadetglem1  21266  smadiadetglem2  21267  smadiadetg  21268  matinv  21272  matunit  21273  slesolinv  21275  slesolinvbi  21276  slesolex  21277  cramerimplem1  21278  cramerimplem2  21279  cramerimplem3  21280  cramerimp  21281  cramer  21286  mat2pmatmul  21325  mat2pmatmhm  21327  mat2pmatrhm  21328  mat2pmatlin  21329  m2cpmmhm  21339  m2cpmrhm  21340  m2pmfzgsumcl  21342  m2cpmrngiso  21352  monmatcollpw  21373  pmatcollpwlem  21374  pmatcollpw  21375  pmatcollpwfi  21376  pmatcollpw3fi1lem2  21381  pmatcollpwscmat  21385  monmat2matmon  21418  pm2mp  21419  chpmatply1  21426  chpmat1d  21430  chpdmat  21435  chpscmat  21436  chpscmatgsumbin  21438  chpscmatgsummon  21439  chp0mat  21440  chpidmat  21441  chmaidscmat  21442  chfacfscmulcl  21451  chfacfscmul0  21452  chfacfscmulgsum  21454  chfacfpmmulcl  21455  chfacfpmmul0  21456  chfacfpmmulgsum  21458  chfacfpmmulgsum2  21459  cayhamlem1  21460  cpmadurid  21461  cpmidgsumm2pm  21463  cpmidpmatlem2  21465  cpmidpmatlem3  21466  cpmadugsumlemB  21468  cpmadugsumlemC  21469  cpmadugsumlemF  21470  cpmadugsumfi  21471  cpmidgsum2  21473  cpmadumatpolylem1  21475  cpmadumatpolylem2  21476  cpmadumatpoly  21477  cayhamlem2  21478  chcoeffeqlem  21479  cayhamlem4  21482  cayleyhamilton0  21483  cayleyhamiltonALT  21485  cayleyhamilton1  21486  recvs  23740  fta1glem1  24755  fta1g  24757  fta1blem  24758  dchrelbas3  25811  dchrelbasd  25812  dchrzrh1  25817  dchrzrhmul  25819  dchrmulcl  25822  dchrn0  25823  dchrfi  25828  dchrghm  25829  dchrabs  25833  dchrinv  25834  dchrptlem1  25837  dchrptlem2  25838  dchrptlem3  25839  dchrsum2  25841  dchrhash  25844  sum2dchr  25847  lgsqrlem1  25919  lgsqrlem2  25920  lgsqrlem3  25921  lgsqrlem4  25922  lgsdchr  25928  lgseisenlem3  25950  lgseisenlem4  25951  dchrisum0flblem1  26081  dchrisum0re  26086  freshmansdream  30877  rdivmuldivd  30880  subofld  30907  isprmidlc  30984  qsidomlem1  30986  qsidomlem2  30987  mxidlprm  30998  mdetpmtr1  31109  mdetpmtr12  31111  madjusmdetlem1  31113  madjusmdetlem4  31116  mdetlap  31118  selvval2lem4  39287  selvval2lem5  39288  crngringd  39300  frlmpwfi  39874  isnumbasgrplem3  39881  mendlmod  39969  idomrootle  39971  idomodle  39972  2zrng0  44404  cznabel  44420  cznrng  44421  crhmsubc  44544  fldcat  44548  fldhmsubc  44550  crhmsubcALTV  44562  fldcatALTV  44566  fldhmsubcALTV  44568  mgpsumz  44605  mgpsumn  44606  evl1at0  44640  evl1at1  44641
  Copyright terms: Public domain W3C validator