Theorem crngring 20384

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  ‘cfv 6533  CMndccmn 19907  mulGrpcmgp 20273  Ringcrg 20372  CRingccrg 20373

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-iota 6489  df-fv 6541  df-cring 20375

This theorem is used by:  crngringd  20385  gsummgp0  20458  prdscrngd  20462  crngbinom  20476  dvdsunit  20520  unitmulclb  20522  unitabl  20525  rdivmuldivd  20554  crhmsubc  20844  fldcat  20949  fldhmsubc  20951  idsrngd  21022  subofld  21043  rmodislmod  21114  isfieldidl  21449  isfieldidl2  21450  df2idl2crng  21484  quscrng  21486  isprmidlc  21535  cmprmidlmcl  21538  prmidl0  21541  qsidomlem1  21543  qsidomlem2  21544  prmidlsubm  21550  cnring  21607  zringring  21662  zring0  21671  znzrh2  21758  zncyg  21761  zndvds0  21763  znf1o  21764  zzngim  21765  znfld  21773  znchr  21775  znunit  21776  znrrg  21778  cygznlem3  21782  freshmansdream  21787  re0g  21825  sraassa  22084  rlmassa  22085  psrcrng  22186  mplcrng  22235  mplassa  22236  mplcoe2  22257  mplbas2  22258  mplmon2mul  22285  mplind  22286  evlslem2  22295  evlslem3  22296  evlslem6  22297  evlseu  22299  evlsval2  22303  evlsgsumadd  22312  evlsgsummul  22313  evlrhm  22317  evlsscasrng  22321  evlsca  22322  evlsvarsrng  22323  evlvar  22324  mpfind  22331  ply1crng  22423  ply1assa  22424  ply1chr  22531  lply1binom  22535  lply1binomsc  22536  evls1rhmlem  22546  evls1gsumadd  22549  evls1gsummul  22550  evl1val  22554  evl1sca  22559  evl1scad  22560  evl1var  22561  evl1vard  22562  evls1var  22563  evls1scasrng  22564  evls1varsrng  22565  evl1subd  22567  evl1expd  22570  pf1const  22571  pf1id  22572  pf1ind  22580  evl1gsumdlem  22581  evl1gsumd  22582  evl1gsumadd  22583  evl1gsummul  22585  evl1varpw  22586  evl1scvarpw  22588  evl1scvarpwval  22589  evl1gsummon  22590  evls1vsca  22598  mamuvs2  22628  matassa  22666  madetsumid  22683  madetsmelbas  22686  madetsmelbas2  22687  mat1dimcrng  22699  dmatcrng  22724  scmatcrng  22743  mdetleib2  22810  mdetf  22817  m1detdiag  22819  mdetdiaglem  22820  mdetdiag  22821  mdet1  22823  mdetrlin  22824  mdetrsca2  22826  mdetr0  22827  mdet0  22828  mdetrlin2  22829  mdetralt  22830  mdetero  22832  mdetmul  22845  maducoeval2  22862  maduf  22863  madutpos  22864  madugsum  22865  madurid  22866  madulid  22867  marep01ma  22882  smadiadetlem0  22883  smadiadetlem1a  22885  smadiadetlem3lem2  22889  smadiadetlem3  22890  smadiadetlem4  22891  smadiadet  22892  smadiadetglem1  22893  smadiadetglem2  22894  smadiadetg  22895  matinv  22899  matunit  22900  slesolinv  22905  slesolinvbi  22906  slesolex  22907  cramerimplem1  22908  cramerimplem2  22909  cramerimplem3  22910  cramerimp  22911  cramer  22916  mat2pmatmul  22956  mat2pmatmhm  22958  mat2pmatrhm  22959  mat2pmatlin  22960  m2cpmmhm  22970  m2cpmrhm  22971  m2pmfzgsumcl  22973  m2cpmrngiso  22983  monmatcollpw  23004  pmatcollpwlem  23005  pmatcollpw  23006  pmatcollpwfi  23007  pmatcollpw3fi1lem2  23012  pmatcollpwscmat  23016  monmat2matmon  23049  pm2mp  23050  chpmatply1  23057  chpmat1d  23061  chpdmat  23066  chpscmat  23067  chpscmatgsumbin  23069  chpscmatgsummon  23070  chp0mat  23071  chpidmat  23072  chmaidscmat  23073  chfacfscmulcl  23082  chfacfscmul0  23083  chfacfscmulgsum  23085  chfacfpmmulcl  23086  chfacfpmmul0  23087  chfacfpmmulgsum  23089  chfacfpmmulgsum2  23090  cayhamlem1  23091  cpmadurid  23092  cpmidgsumm2pm  23094  cpmidpmatlem2  23096  cpmidpmatlem3  23097  cpmadugsumlemB  23099  cpmadugsumlemC  23100  cpmadugsumlemF  23101  cpmadugsumfi  23102  cpmidgsum2  23104  cpmadumatpolylem1  23106  cpmadumatpolylem2  23107  cpmadumatpoly  23108  cayhamlem2  23109  chcoeffeqlem  23110  cayhamlem4  23113  cayleyhamilton0  23114  cayleyhamiltonALT  23116  cayleyhamilton1  23117  fta1glem1  26393  fta1g  26395  fta1blem  26396  idomrootle  26398  dchrelbas3  27474  dchrelbasd  27475  dchrzrh1  27480  dchrzrhmul  27482  dchrmulcl  27485  dchrn0  27486  dchrfi  27491  dchrghm  27492  dchrabs  27496  dchrinv  27497  dchrptlem1  27500  dchrptlem2  27501  dchrptlem3  27502  dchrsum2  27504  dchrhash  27507  sum2dchr  27510  lgsqrlem1  27582  lgsqrlem2  27583  lgsqrlem3  27584  lgsqrlem4  27585  lgsdchr  27591  lgseisenlem3  27613  lgseisenlem4  27614  dchrisum0flblem1  27744  dchrisum0re  27749  unitprodclb  33822  ringlsmss1  33827  crngmxidl  33872  mxidlprm  33873  dflringlem3  33906  dflring3  33907  idlsrgmulrss1  33921  psrmonprod  34062  esplyfvaln  34084  mdetpmtr1  34333  mdetpmtr12  34335  madjusmdetlem1  34337  madjusmdetlem4  34340  mdetlap  34342  zarcls1  34379  zarclsint  34382  zarclssn  34383  zartopn  34385  zart0  34389  zarcmplem  34391  rspectps  34393  aks6d1c1p2  42975  aks6d1c1p7  42979  aks6d1c1p6  42980  aks6d1c1  42982  hashscontpowcl  42986  hashscontpow  42988  aks6d1c4  42990  aks6d1c2lem3  42992  aks6d1c2  42996  aks6d1c5lem1  43002  aks6d1c5lem3  43003  aks6d1c6lem1  43036  aks6d1c6lem3  43038  aks6d1c6lem5  43043  aks6d1c7lem1  43046  aks5lem1  43052  aks5lem2  43053  aks5lem5a  43057  frlmpwfi  43939  isnumbasgrplem3  43946  mendlmod  44030  idomodle  44032  2zrng0  49159  cznabel  49175  cznrng  49176  crhmsubcALTV  49242  fldcatALTV  49246  fldhmsubcALTV  49248  crngprmringidom  49256  isidom3  49260  idomcanl  49262  mgpsumz  49292  mgpsumn  49293  evl1at0  49321  evl1at1  49322