Theorem crngring 20130

Description: A commutative ring is a ring. (Contributed by Mario Carneiro, 7-Jan-2015.)

Assertion

Ref	Expression
crngring	⊢ (𝑅 ∈ CRing → 𝑅 ∈ Ring)

Proof of Theorem crngring

Step	Hyp	Ref	Expression
1		eqid 2729	. . 3 ⊢ (mulGrp‘𝑅) = (mulGrp‘𝑅)
2	1	iscrng 20125	. 2 ⊢ (𝑅 ∈ CRing ↔ (𝑅 ∈ Ring ∧ (mulGrp‘𝑅) ∈ CMnd))
3	2	simplbi 497	1 ⊢ (𝑅 ∈ CRing → 𝑅 ∈ Ring)

Syntax hints:   → wi 4   ∈ wcel 2109  ‘cfv 6499  CMndccmn 19686  mulGrpcmgp 20025  Ringcrg 20118  CRingccrg 20119

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3403  df-v 3446  df-dif 3914  df-un 3916  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-br 5103  df-iota 6452  df-fv 6507  df-cring 20121

This theorem is referenced by:  crngringd  20131  gsummgp0  20203  prdscrngd  20207  crngbinom  20220  dvdsunit  20264  unitmulclb  20266  unitabl  20269  rdivmuldivd  20298  crhmsubc  20567  fldcat  20668  fldhmsubc  20670  idsrngd  20741  rmodislmod  20812  quscrng  21169  cnring  21278  zringring  21335  zring0  21344  znzrh2  21431  zncyg  21434  zndvds0  21436  znf1o  21437  zzngim  21438  znfld  21446  znchr  21448  znunit  21449  znrrg  21451  cygznlem3  21455  freshmansdream  21460  re0g  21497  sraassa  21754  sraassaOLD  21755  rlmassa  21756  psrcrng  21857  mplcrng  21906  mplassa  21907  mplcoe2  21924  mplbas2  21925  mplmon2mul  21952  mplind  21953  evlslem2  21962  evlslem3  21963  evlslem6  21964  evlseu  21966  evlsval2  21970  evlsgsumadd  21974  evlsgsummul  21975  evlrhm  21979  evlsscasrng  21980  evlsca  21981  evlsvarsrng  21982  evlvar  21983  mpfind  21990  ply1crng  22059  ply1assa  22060  ply1chr  22169  lply1binom  22173  lply1binomsc  22174  evls1rhmlem  22184  evls1gsumadd  22187  evls1gsummul  22188  evl1val  22192  evl1sca  22197  evl1scad  22198  evl1var  22199  evl1vard  22200  evls1var  22201  evls1scasrng  22202  evls1varsrng  22203  evl1subd  22205  evl1expd  22208  pf1const  22209  pf1id  22210  pf1ind  22218  evl1gsumdlem  22219  evl1gsumd  22220  evl1gsumadd  22221  evl1gsummul  22223  evl1varpw  22224  evl1scvarpw  22226  evl1scvarpwval  22227  evl1gsummon  22228  evls1vsca  22236  mamuvs2  22269  matassa  22307  madetsumid  22324  madetsmelbas  22327  madetsmelbas2  22328  mat1dimcrng  22340  dmatcrng  22365  scmatcrng  22384  mdetleib2  22451  mdetf  22458  m1detdiag  22460  mdetdiaglem  22461  mdetdiag  22462  mdet1  22464  mdetrlin  22465  mdetrsca2  22467  mdetr0  22468  mdet0  22469  mdetrlin2  22470  mdetralt  22471  mdetero  22473  mdetmul  22486  maducoeval2  22503  maduf  22504  madutpos  22505  madugsum  22506  madurid  22507  madulid  22508  marep01ma  22523  smadiadetlem0  22524  smadiadetlem1a  22526  smadiadetlem3lem2  22530  smadiadetlem3  22531  smadiadetlem4  22532  smadiadet  22533  smadiadetglem1  22534  smadiadetglem2  22535  smadiadetg  22536  matinv  22540  matunit  22541  slesolinv  22543  slesolinvbi  22544  slesolex  22545  cramerimplem1  22546  cramerimplem2  22547  cramerimplem3  22548  cramerimp  22549  cramer  22554  mat2pmatmul  22594  mat2pmatmhm  22596  mat2pmatrhm  22597  mat2pmatlin  22598  m2cpmmhm  22608  m2cpmrhm  22609  m2pmfzgsumcl  22611  m2cpmrngiso  22621  monmatcollpw  22642  pmatcollpwlem  22643  pmatcollpw  22644  pmatcollpwfi  22645  pmatcollpw3fi1lem2  22650  pmatcollpwscmat  22654  monmat2matmon  22687  pm2mp  22688  chpmatply1  22695  chpmat1d  22699  chpdmat  22704  chpscmat  22705  chpscmatgsumbin  22707  chpscmatgsummon  22708  chp0mat  22709  chpidmat  22710  chmaidscmat  22711  chfacfscmulcl  22720  chfacfscmul0  22721  chfacfscmulgsum  22723  chfacfpmmulcl  22724  chfacfpmmul0  22725  chfacfpmmulgsum  22727  chfacfpmmulgsum2  22728  cayhamlem1  22729  cpmadurid  22730  cpmidgsumm2pm  22732  cpmidpmatlem2  22734  cpmidpmatlem3  22735  cpmadugsumlemB  22737  cpmadugsumlemC  22738  cpmadugsumlemF  22739  cpmadugsumfi  22740  cpmidgsum2  22742  cpmadumatpolylem1  22744  cpmadumatpolylem2  22745  cpmadumatpoly  22746  cayhamlem2  22747  chcoeffeqlem  22748  cayhamlem4  22751  cayleyhamilton0  22752  cayleyhamiltonALT  22754  cayleyhamilton1  22755  fta1glem1  26049  fta1g  26051  fta1blem  26052  idomrootle  26054  dchrelbas3  27125  dchrelbasd  27126  dchrzrh1  27131  dchrzrhmul  27133  dchrmulcl  27136  dchrn0  27137  dchrfi  27142  dchrghm  27143  dchrabs  27147  dchrinv  27148  dchrptlem1  27151  dchrptlem2  27152  dchrptlem3  27153  dchrsum2  27155  dchrhash  27158  sum2dchr  27161  lgsqrlem1  27233  lgsqrlem2  27234  lgsqrlem3  27235  lgsqrlem4  27236  lgsdchr  27242  lgseisenlem3  27264  lgseisenlem4  27265  dchrisum0flblem1  27395  dchrisum0re  27400  subofld  33267  unitprodclb  33333  ringlsmss1  33340  isprmidlc  33391  prmidl0  33394  qsidomlem1  33396  qsidomlem2  33397  crngmxidl  33413  mxidlprm  33414  idlsrgmulrss1  33455  mdetpmtr1  33786  mdetpmtr12  33788  madjusmdetlem1  33790  madjusmdetlem4  33793  mdetlap  33795  zarcls1  33832  zarclsint  33835  zarclssn  33836  zartopn  33838  zart0  33842  zarcmplem  33844  rspectps  33846  aks6d1c1p2  42070  aks6d1c1p7  42074  aks6d1c1p6  42075  aks6d1c1  42077  hashscontpowcl  42081  hashscontpow  42083  aks6d1c4  42085  aks6d1c2lem3  42087  aks6d1c2  42091  aks6d1c5lem1  42097  aks6d1c5lem3  42098  aks6d1c6lem1  42131  aks6d1c6lem3  42133  aks6d1c6lem5  42138  aks6d1c7lem1  42141  aks5lem1  42147  aks5lem2  42148  aks5lem5a  42152  frlmpwfi  43060  isnumbasgrplem3  43067  mendlmod  43151  idomodle  43153  2zrng0  48205  cznabel  48221  cznrng  48222  crhmsubcALTV  48288  fldcatALTV  48292  fldhmsubcALTV  48294  mgpsumz  48323  mgpsumn  48324  evl1at0  48353  evl1at1  48354