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

Theorem crngring 18604
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 2651 . . 3 (mulGrp‘𝑅) = (mulGrp‘𝑅)
21iscrng 18600 . 2 (𝑅 ∈ CRing ↔ (𝑅 ∈ Ring ∧ (mulGrp‘𝑅) ∈ CMnd))
32simplbi 475 1 (𝑅 ∈ CRing → 𝑅 ∈ Ring)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2030  cfv 5926  CMndccmn 18239  mulGrpcmgp 18535  Ringcrg 18593  CRingccrg 18594
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-rex 2947  df-rab 2950  df-v 3233  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-sn 4211  df-pr 4213  df-op 4217  df-uni 4469  df-br 4686  df-iota 5889  df-fv 5934  df-cring 18596
This theorem is referenced by:  gsummgp0  18654  prdscrngd  18659  crngbinom  18667  dvdsunit  18709  unitmulclb  18711  unitabl  18714  idsrngd  18910  rmodislmod  18979  quscrng  19288  assa2ass  19370  sraassa  19373  rlmassa  19374  asclrhm  19390  assamulgscmlem2  19397  psrcrng  19461  psrassa  19462  mplcrng  19501  mplassa  19502  mplcoe2  19517  mplbas2  19518  mplmon2mul  19549  mplind  19550  evlslem2  19560  evlslem6  19561  evlslem3  19562  evlslem1  19563  evlseu  19564  evlsval2  19568  evlrhm  19573  evlsscasrng  19574  evlsca  19575  evlsvarsrng  19576  evlvar  19577  mpfind  19584  ply1crng  19616  ply1assa  19617  lply1binom  19724  lply1binomsc  19725  evls1rhmlem  19734  evls1gsumadd  19737  evls1gsummul  19738  evl1val  19741  evl1sca  19746  evl1scad  19747  evl1var  19748  evl1vard  19749  evls1var  19750  evls1scasrng  19751  evls1varsrng  19752  evl1subd  19754  evl1expd  19757  pf1const  19758  pf1id  19759  pf1ind  19767  evl1gsumdlem  19768  evl1gsumd  19769  evl1gsumadd  19770  evl1gsummul  19772  evl1varpw  19773  evl1scvarpw  19775  evl1scvarpwval  19776  evl1gsummon  19777  cnring  19816  zringring  19869  zring0  19876  znzrh2  19942  zncyg  19945  zndvds0  19947  znf1o  19948  zzngim  19949  znfld  19957  znchr  19959  znunit  19960  znrrg  19962  cygznlem3  19966  re0g  20006  mamuvs2  20260  matassa  20298  madetsumid  20315  madetsmelbas  20318  madetsmelbas2  20319  mat1dimcrng  20331  dmatcrng  20356  scmatcrng  20375  mdetleib2  20442  mdetf  20449  m1detdiag  20451  mdetdiaglem  20452  mdetdiag  20453  mdet1  20455  mdetrlin  20456  mdetrsca  20457  mdetrsca2  20458  mdetr0  20459  mdet0  20460  mdetrlin2  20461  mdetralt  20462  mdetero  20464  mdetmul  20477  maducoeval2  20494  maduf  20495  madutpos  20496  madugsum  20497  madurid  20498  madulid  20499  marep01ma  20514  smadiadetlem0  20515  smadiadetlem1a  20517  smadiadetlem3lem2  20521  smadiadetlem3  20522  smadiadetlem4  20523  smadiadet  20524  smadiadetglem1  20525  smadiadetglem2  20526  smadiadetg  20527  matinv  20531  matunit  20532  slesolinv  20534  slesolinvbi  20535  slesolex  20536  cramerimplem1  20537  cramerimplem2  20538  cramerimplem3  20539  cramerimp  20540  cramer  20545  mat2pmatmul  20584  mat2pmatmhm  20586  mat2pmatrhm  20587  mat2pmatlin  20588  m2cpmmhm  20598  m2cpmrhm  20599  m2pmfzgsumcl  20601  m2cpmrngiso  20611  monmatcollpw  20632  pmatcollpwlem  20633  pmatcollpw  20634  pmatcollpwfi  20635  pmatcollpw3fi1lem2  20640  pmatcollpwscmat  20644  monmat2matmon  20677  pm2mp  20678  chpmatply1  20685  chpmat1d  20689  chpdmat  20694  chpscmat  20695  chpscmatgsumbin  20697  chpscmatgsummon  20698  chp0mat  20699  chpidmat  20700  chmaidscmat  20701  chfacfscmulcl  20710  chfacfscmul0  20711  chfacfscmulgsum  20713  chfacfpmmulcl  20714  chfacfpmmul0  20715  chfacfpmmulgsum  20717  chfacfpmmulgsum2  20718  cayhamlem1  20719  cpmadurid  20720  cpmidgsumm2pm  20722  cpmidpmatlem2  20724  cpmidpmatlem3  20725  cpmadugsumlemB  20727  cpmadugsumlemC  20728  cpmadugsumlemF  20729  cpmadugsumfi  20730  cpmidgsum2  20732  cpmadumatpolylem1  20734  cpmadumatpolylem2  20735  cpmadumatpoly  20736  cayhamlem2  20737  chcoeffeqlem  20738  cayhamlem4  20741  cayleyhamilton0  20742  cayleyhamiltonALT  20744  cayleyhamilton1  20745  recvs  22992  fta1glem1  23970  fta1g  23972  fta1blem  23973  dchrelbas3  25008  dchrelbasd  25009  dchrzrh1  25014  dchrzrhmul  25016  dchrmulcl  25019  dchrn0  25020  dchrfi  25025  dchrghm  25026  dchrabs  25030  dchrinv  25031  dchrptlem1  25034  dchrptlem2  25035  dchrptlem3  25036  dchrsum2  25038  dchrhash  25041  sum2dchr  25044  lgsqrlem1  25116  lgsqrlem2  25117  lgsqrlem3  25118  lgsqrlem4  25119  lgsdchr  25125  lgseisenlem3  25147  lgseisenlem4  25148  dchrisum0flblem1  25242  dchrisum0re  25247  rdivmuldivd  29919  subofld  29944  mdetpmtr1  30017  mdetpmtr12  30019  madjusmdetlem1  30021  madjusmdetlem4  30024  mdetlap  30026  frlmpwfi  37985  isnumbasgrplem3  37992  mendlmod  38080  idomrootle  38090  idomodle  38091  2zrng0  42263  cznabel  42279  cznrng  42280  crhmsubc  42403  fldcat  42407  fldhmsubc  42409  crhmsubcALTV  42421  fldcatALTV  42425  fldhmsubcALTV  42427  mgpsumz  42466  mgpsumn  42467  evl1at0  42504  evl1at1  42505
  Copyright terms: Public domain W3C validator