Theorem crngring 20478

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 2760	. . 3 ⊢ (mulGrp‘𝑅) = (mulGrp‘𝑅)
2	1	iscrng 20472	. 2 ⊢ (𝑅 ∈ CRing ↔ (𝑅 ∈ Ring ∧ (mulGrp‘𝑅) ∈ CMnd))
3	2	simplbi 502	1 ⊢ (𝑅 ∈ CRing → 𝑅 ∈ Ring)

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2144  ‘cfv 6539  CMndccmn 20000  mulGrpcmgp 20366  Ringcrg 20465  CRingccrg 20466

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-un 4151  df-nul 4279  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-br 5103  df-iota 6494  df-fv 6547  df-cring 20468

This theorem is used by:  crngringd  20479  gsummgp0  20553  prdscrngd  20557  crngbinom  20571  dvdsunit  20615  unitmulclb  20617  unitabl  20620  rdivmuldivd  20649  crhmsubc  20940  fldcat  21046  fldhmsubc  21048  idsrngd  21119  subofld  21140  rmodislmod  21211  isfieldidl  21546  isfieldidl2  21547  df2idl2crng  21583  quscrng  21585  isprmidlc  21634  cmprmidlmcl  21637  prmidl0  21640  qsidomlem1  21642  qsidomlem2  21643  prmidlsubm  21649  cnring  21706  zringring  21761  zring0  21770  znzrh2  21857  zncyg  21860  zndvds0  21862  znf1o  21863  zzngim  21864  znfld  21872  znchr  21874  znunit  21875  znrrg  21877  cygznlem3  21881  freshmansdream  21886  re0g  21924  sraassa  22183  rlmassa  22184  psrcrng  22285  mplcrng  22334  mplassa  22335  mplcoe2  22356  mplbas2  22357  mplmon2mul  22384  mplind  22385  evlslem2  22394  evlslem3  22395  evlslem6  22396  evlseu  22398  evlsval2  22402  evlsgsumadd  22411  evlsgsummul  22412  evlrhm  22416  evlsscasrng  22420  evlsca  22421  evlsvarsrng  22422  evlvar  22423  mpfind  22430  ply1crng  22522  ply1assa  22523  ply1chr  22630  lply1binom  22634  lply1binomsc  22635  evls1rhmlem  22645  evls1gsumadd  22648  evls1gsummul  22649  evl1val  22653  evl1sca  22658  evl1scad  22659  evl1var  22660  evl1vard  22661  evls1var  22662  evls1scasrng  22663  evls1varsrng  22664  evl1subd  22666  evl1expd  22669  pf1const  22670  pf1id  22671  pf1ind  22679  evl1gsumdlem  22680  evl1gsumd  22681  evl1gsumadd  22682  evl1gsummul  22684  evl1varpw  22685  evl1scvarpw  22687  evl1scvarpwval  22688  evl1gsummon  22689  evls1vsca  22697  mamuvs2  22727  matassa  22765  madetsumid  22782  madetsmelbas  22785  madetsmelbas2  22786  mat1dimcrng  22798  dmatcrng  22823  scmatcrng  22842  mdetleib2  22909  mdetf  22916  m1detdiag  22918  mdetdiaglem  22919  mdetdiag  22920  mdet1  22922  mdetrlin  22923  mdetrsca2  22925  mdetr0  22926  mdet0  22927  mdetrlin2  22928  mdetralt  22929  mdetero  22931  mdetmul  22944  maducoeval2  22961  maduf  22962  madutpos  22963  madugsum  22964  madurid  22965  madulid  22966  marep01ma  22981  smadiadetlem0  22982  smadiadetlem1a  22984  smadiadetlem3lem2  22988  smadiadetlem3  22989  smadiadetlem4  22990  smadiadet  22991  smadiadetglem1  22992  smadiadetglem2  22993  smadiadetg  22994  matinv  22998  matunit  22999  slesolinv  23004  slesolinvbi  23005  slesolex  23006  cramerimplem1  23007  cramerimplem2  23008  cramerimplem3  23009  cramerimp  23010  cramer  23015  mat2pmatmul  23055  mat2pmatmhm  23057  mat2pmatrhm  23058  mat2pmatlin  23059  m2cpmmhm  23069  m2cpmrhm  23070  m2pmfzgsumcl  23072  m2cpmrngiso  23082  monmatcollpw  23103  pmatcollpwlem  23104  pmatcollpw  23105  pmatcollpwfi  23106  pmatcollpw3fi1lem2  23111  pmatcollpwscmat  23115  monmat2matmon  23148  pm2mp  23149  chpmatply1  23156  chpmat1d  23160  chpdmat  23165  chpscmat  23166  chpscmatgsumbin  23168  chpscmatgsummon  23169  chp0mat  23170  chpidmat  23171  chmaidscmat  23172  chfacfscmulcl  23181  chfacfscmul0  23182  chfacfscmulgsum  23184  chfacfpmmulcl  23185  chfacfpmmul0  23186  chfacfpmmulgsum  23188  chfacfpmmulgsum2  23189  cayhamlem1  23190  cpmadurid  23191  cpmidgsumm2pm  23193  cpmidpmatlem2  23195  cpmidpmatlem3  23196  cpmadugsumlemB  23198  cpmadugsumlemC  23199  cpmadugsumlemF  23200  cpmadugsumfi  23201  cpmidgsum2  23203  cpmadumatpolylem1  23205  cpmadumatpolylem2  23206  cpmadumatpoly  23207  cayhamlem2  23208  chcoeffeqlem  23209  cayhamlem4  23212  cayleyhamilton0  23213  cayleyhamiltonALT  23215  cayleyhamilton1  23216  fta1glem1  26492  fta1g  26494  fta1blem  26495  idomrootle  26497  dchrelbas3  27571  dchrelbasd  27572  dchrzrh1  27577  dchrzrhmul  27579  dchrmulcl  27582  dchrn0  27583  dchrfi  27588  dchrghm  27589  dchrabs  27593  dchrinv  27594  dchrptlem1  27597  dchrptlem2  27598  dchrptlem3  27599  dchrsum2  27601  dchrhash  27604  sum2dchr  27607  lgsqrlem1  27679  lgsqrlem2  27680  lgsqrlem3  27681  lgsqrlem4  27682  lgsdchr  27688  lgseisenlem3  27710  lgseisenlem4  27711  dchrisum0flblem1  27841  dchrisum0re  27846  unitprodclb  33991  ringlsmss1  33996  crngmxidl  34041  mxidlprm  34042  dflringlem3  34075  dflring3  34076  idlsrgmulrss1  34090  psrmonprod  34231  esplyfvaln  34253  mdetpmtr1  34502  mdetpmtr12  34504  madjusmdetlem1  34506  madjusmdetlem4  34509  mdetlap  34511  zarcls1  34548  zarclsint  34551  zarclssn  34552  zartopn  34554  zart0  34558  zarcmplem  34560  rspectps  34562  aks6d1c1p2  43253  aks6d1c1p7  43257  aks6d1c1p6  43258  aks6d1c1  43260  hashscontpowcl  43264  hashscontpow  43266  aks6d1c4  43268  aks6d1c2lem3  43270  aks6d1c2  43274  aks6d1c5lem1  43280  aks6d1c5lem3  43281  aks6d1c6lem1  43314  aks6d1c6lem3  43316  aks6d1c6lem5  43321  aks6d1c7lem1  43324  aks5lem1  43330  aks5lem2  43331  aks5lem5a  43335  frlmpwfi  44194  isnumbasgrplem3  44201  mendlmod  44285  idomodle  44287  2zrng0  49435  cznabel  49451  cznrng  49452  crhmsubcALTV  49518  fldcatALTV  49522  fldhmsubcALTV  49524  crngprmringidom  49532  isidom3  49536  idomcanl  49538  mgpsumz  49568  mgpsumn  49569  evl1at0  49597  evl1at1  49598