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

Theorem crngring 19984
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 2733 . . 3 (mulGrp‘𝑅) = (mulGrp‘𝑅)
21iscrng 19979 . 2 (𝑅 ∈ CRing ↔ (𝑅 ∈ Ring ∧ (mulGrp‘𝑅) ∈ CMnd))
32simplbi 499 1 (𝑅 ∈ CRing → 𝑅 ∈ Ring)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2107  cfv 6500  CMndccmn 19570  mulGrpcmgp 19904  Ringcrg 19972  CRingccrg 19973
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-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3407  df-v 3449  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4287  df-if 4491  df-sn 4591  df-pr 4593  df-op 4597  df-uni 4870  df-br 5110  df-iota 6452  df-fv 6508  df-cring 19975
This theorem is referenced by:  crngringd  19985  gsummgp0  20040  prdscrngd  20045  crngbinom  20055  dvdsunit  20100  unitmulclb  20102  unitabl  20105  rdivmuldivd  20132  idsrngd  20364  rmodislmod  20434  rmodislmodOLD  20435  quscrng  20755  cnring  20842  zringring  20895  zring0  20902  znzrh2  20975  zncyg  20978  zndvds0  20980  znf1o  20981  zzngim  20982  znfld  20990  znchr  20992  znunit  20993  znrrg  20995  cygznlem3  20999  re0g  21039  assa2ass  21292  sraassa  21296  rlmassa  21297  assamulgscmlem2  21326  psrcrng  21405  psrassa  21406  mplcrng  21449  mplassa  21450  mplcoe2  21465  mplbas2  21466  mplmon2mul  21500  mplind  21501  evlslem2  21512  evlslem3  21513  evlslem6  21514  evlseu  21516  evlsval2  21520  evlsgsumadd  21524  evlsgsummul  21525  evlrhm  21529  evlsscasrng  21530  evlsca  21531  evlsvarsrng  21532  evlvar  21533  mpfind  21540  ply1crng  21592  ply1assa  21593  lply1binom  21700  lply1binomsc  21701  evls1rhmlem  21710  evls1gsumadd  21713  evls1gsummul  21714  evl1val  21718  evl1sca  21723  evl1scad  21724  evl1var  21725  evl1vard  21726  evls1var  21727  evls1scasrng  21728  evls1varsrng  21729  evl1subd  21731  evl1expd  21734  pf1const  21735  pf1id  21736  pf1ind  21744  evl1gsumdlem  21745  evl1gsumd  21746  evl1gsumadd  21747  evl1gsummul  21749  evl1varpw  21750  evl1scvarpw  21752  evl1scvarpwval  21753  evl1gsummon  21754  mamuvs2  21776  matassa  21816  madetsumid  21833  madetsmelbas  21836  madetsmelbas2  21837  mat1dimcrng  21849  dmatcrng  21874  scmatcrng  21893  mdetleib2  21960  mdetf  21967  m1detdiag  21969  mdetdiaglem  21970  mdetdiag  21971  mdet1  21973  mdetrlin  21974  mdetrsca  21975  mdetrsca2  21976  mdetr0  21977  mdet0  21978  mdetrlin2  21979  mdetralt  21980  mdetero  21982  mdetmul  21995  maducoeval2  22012  maduf  22013  madutpos  22014  madugsum  22015  madurid  22016  madulid  22017  marep01ma  22032  smadiadetlem0  22033  smadiadetlem1a  22035  smadiadetlem3lem2  22039  smadiadetlem3  22040  smadiadetlem4  22041  smadiadet  22042  smadiadetglem1  22043  smadiadetglem2  22044  smadiadetg  22045  matinv  22049  matunit  22050  slesolinv  22052  slesolinvbi  22053  slesolex  22054  cramerimplem1  22055  cramerimplem2  22056  cramerimplem3  22057  cramerimp  22058  cramer  22063  mat2pmatmul  22103  mat2pmatmhm  22105  mat2pmatrhm  22106  mat2pmatlin  22107  m2cpmmhm  22117  m2cpmrhm  22118  m2pmfzgsumcl  22120  m2cpmrngiso  22130  monmatcollpw  22151  pmatcollpwlem  22152  pmatcollpw  22153  pmatcollpwfi  22154  pmatcollpw3fi1lem2  22159  pmatcollpwscmat  22163  monmat2matmon  22196  pm2mp  22197  chpmatply1  22204  chpmat1d  22208  chpdmat  22213  chpscmat  22214  chpscmatgsumbin  22216  chpscmatgsummon  22217  chp0mat  22218  chpidmat  22219  chmaidscmat  22220  chfacfscmulcl  22229  chfacfscmul0  22230  chfacfscmulgsum  22232  chfacfpmmulcl  22233  chfacfpmmul0  22234  chfacfpmmulgsum  22236  chfacfpmmulgsum2  22237  cayhamlem1  22238  cpmadurid  22239  cpmidgsumm2pm  22241  cpmidpmatlem2  22243  cpmidpmatlem3  22244  cpmadugsumlemB  22246  cpmadugsumlemC  22247  cpmadugsumlemF  22248  cpmadugsumfi  22249  cpmidgsum2  22251  cpmadumatpolylem1  22253  cpmadumatpolylem2  22254  cpmadumatpoly  22255  cayhamlem2  22256  chcoeffeqlem  22257  cayhamlem4  22260  cayleyhamilton0  22261  cayleyhamiltonALT  22263  cayleyhamilton1  22264  recvsOLD  24533  fta1glem1  25553  fta1g  25555  fta1blem  25556  dchrelbas3  26609  dchrelbasd  26610  dchrzrh1  26615  dchrzrhmul  26617  dchrmulcl  26620  dchrn0  26621  dchrfi  26626  dchrghm  26627  dchrabs  26631  dchrinv  26632  dchrptlem1  26635  dchrptlem2  26636  dchrptlem3  26637  dchrsum2  26639  dchrhash  26642  sum2dchr  26645  lgsqrlem1  26717  lgsqrlem2  26718  lgsqrlem3  26719  lgsqrlem4  26720  lgsdchr  26726  lgseisenlem3  26748  lgseisenlem4  26749  dchrisum0flblem1  26879  dchrisum0re  26884  freshmansdream  32123  subofld  32165  ringlsmss1  32232  isprmidlc  32275  prmidl0  32278  qsidomlem1  32280  qsidomlem2  32281  mxidlprm  32292  idlsrgmulrss1  32308  ply1chr  32338  mdetpmtr1  32468  mdetpmtr12  32470  madjusmdetlem1  32472  madjusmdetlem4  32475  mdetlap  32477  zarcls1  32514  zarclsint  32517  zarclssn  32518  zartopn  32520  zart0  32524  zarcmplem  32526  rspectps  32528  selvcllem5  40807  frlmpwfi  41472  isnumbasgrplem3  41479  mendlmod  41567  idomrootle  41569  idomodle  41570  2zrng0  46326  cznabel  46342  cznrng  46343  crhmsubc  46466  fldcat  46470  fldhmsubc  46472  crhmsubcALTV  46484  fldcatALTV  46488  fldhmsubcALTV  46490  mgpsumz  46528  mgpsumn  46529  evl1at0  46562  evl1at1  46563
  Copyright terms: Public domain W3C validator