Theorem crngring 20523

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2147  ‘cfv 6566  CMndccmn 20045  mulGrpcmgp 20411  Ringcrg 20510  CRingccrg 20511

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

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 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4841  df-uni 4873  df-br 5109  df-iota 6520  df-fv 6574  df-cring 20513

This theorem is used by:  crngringd  20524  gsummgp0  20598  prdscrngd  20602  crngbinom  20616  dvdsunit  20660  unitmulclb  20662  unitabl  20665  rdivmuldivd  20694  crhmsubc  20985  fldcat  21091  fldhmsubc  21093  idsrngd  21164  subofld  21185  rmodislmod  21256  isfieldidl  21591  isfieldidl2  21592  df2idl2crng  21628  quscrng  21630  isprmidlc  21679  cmprmidlmcl  21682  prmidl0  21685  qsidomlem1  21687  qsidomlem2  21688  prmidlsubm  21694  cnring  21752  zringring  21809  zring0  21819  znzrh2  21906  zncyg  21909  zndvds0  21911  znf1o  21912  zzngim  21913  znfld  21921  znchr  21923  znunit  21924  znrrg  21926  cygznlem3  21930  freshmansdream  21935  re0g  21973  sraassa  22232  rlmassa  22233  psrcrng  22334  mplcrng  22383  mplassa  22384  mplcoe2  22405  mplbas2  22406  mplmon2mul  22433  mplind  22434  evlslem2  22443  evlslem3  22444  evlslem6  22445  evlseu  22447  evlsval2  22451  evlsgsumadd  22460  evlsgsummul  22461  evlrhm  22465  evlsscasrng  22469  evlsca  22470  evlsvarsrng  22471  evlvar  22472  mpfind  22479  ply1crng  22571  ply1assa  22572  ply1chr  22679  lply1binom  22683  lply1binomsc  22684  evls1rhmlem  22694  evls1gsumadd  22697  evls1gsummul  22698  evl1val  22702  evl1sca  22707  evl1scad  22708  evl1var  22709  evl1vard  22710  evls1var  22711  evls1scasrng  22712  evls1varsrng  22713  evl1subd  22715  evl1expd  22718  pf1const  22719  pf1id  22720  pf1ind  22728  evl1gsumdlem  22729  evl1gsumd  22730  evl1gsumadd  22731  evl1gsummul  22733  evl1varpw  22734  evl1scvarpw  22736  evl1scvarpwval  22737  evl1gsummon  22738  evls1vsca  22746  mamuvs2  22776  matassa  22814  madetsumid  22831  madetsmelbas  22834  madetsmelbas2  22835  mat1dimcrng  22847  dmatcrng  22872  scmatcrng  22891  mdetleib2  22958  mdetf  22965  m1detdiag  22967  mdetdiaglem  22968  mdetdiag  22969  mdet1  22971  mdetrlin  22972  mdetrsca2  22974  mdetr0  22975  mdet0  22976  mdetrlin2  22977  mdetralt  22978  mdetero  22980  mdetmul  22993  maducoeval2  23010  maduf  23011  madutpos  23012  madugsum  23013  madurid  23014  madulid  23015  marep01ma  23030  smadiadetlem0  23031  smadiadetlem1a  23033  smadiadetlem3lem2  23037  smadiadetlem3  23038  smadiadetlem4  23039  smadiadet  23040  smadiadetglem1  23041  smadiadetglem2  23042  smadiadetg  23043  matinv  23047  matunit  23048  slesolinv  23053  slesolinvbi  23054  slesolex  23055  cramerimplem1  23056  cramerimplem2  23057  cramerimplem3  23058  cramerimp  23059  cramer  23064  mat2pmatmul  23104  mat2pmatmhm  23106  mat2pmatrhm  23107  mat2pmatlin  23108  m2cpmmhm  23118  m2cpmrhm  23119  m2pmfzgsumcl  23121  m2cpmrngiso  23131  monmatcollpw  23152  pmatcollpwlem  23153  pmatcollpw  23154  pmatcollpwfi  23155  pmatcollpw3fi1lem2  23160  pmatcollpwscmat  23164  monmat2matmon  23197  pm2mp  23198  chpmatply1  23205  chpmat1d  23209  chpdmat  23214  chpscmat  23215  chpscmatgsumbin  23217  chpscmatgsummon  23218  chp0mat  23219  chpidmat  23220  chmaidscmat  23221  chfacfscmulcl  23230  chfacfscmul0  23231  chfacfscmulgsum  23233  chfacfpmmulcl  23234  chfacfpmmul0  23235  chfacfpmmulgsum  23237  chfacfpmmulgsum2  23238  cayhamlem1  23239  cpmadurid  23240  cpmidgsumm2pm  23242  cpmidpmatlem2  23244  cpmidpmatlem3  23245  cpmadugsumlemB  23247  cpmadugsumlemC  23248  cpmadugsumlemF  23249  cpmadugsumfi  23250  cpmidgsum2  23252  cpmadumatpolylem1  23254  cpmadumatpolylem2  23255  cpmadumatpoly  23256  cayhamlem2  23257  chcoeffeqlem  23258  cayhamlem4  23261  cayleyhamilton0  23262  cayleyhamiltonALT  23264  cayleyhamilton1  23265  fta1glem1  26541  fta1g  26543  fta1blem  26544  idomrootle  26546  dchrelbas3  27622  dchrelbasd  27623  dchrzrh1  27628  dchrzrhmul  27630  dchrmulcl  27633  dchrn0  27634  dchrfi  27639  dchrghm  27640  dchrabs  27644  dchrinv  27645  dchrptlem1  27648  dchrptlem2  27649  dchrptlem3  27650  dchrsum2  27652  dchrhash  27655  sum2dchr  27658  lgsqrlem1  27730  lgsqrlem2  27731  lgsqrlem3  27732  lgsqrlem4  27733  lgsdchr  27739  lgseisenlem3  27761  lgseisenlem4  27762  dchrisum0flblem1  27892  dchrisum0re  27897  unitprodclb  34048  ringlsmss1  34053  crngmxidl  34098  mxidlprm  34099  dflringlem3  34132  dflring3  34133  idlsrgmulrss1  34147  psrmonprod  34295  esplyfvaln  34317  mdetpmtr1  34566  mdetpmtr12  34568  madjusmdetlem1  34570  madjusmdetlem4  34573  mdetlap  34575  zarcls1  34612  zarclsint  34615  zarclssn  34616  zartopn  34618  zart0  34622  zarcmplem  34624  rspectps  34626  aks6d1c1p2  43425  aks6d1c1p7  43429  aks6d1c1p6  43430  aks6d1c1  43432  hashscontpowcl  43436  hashscontpow  43438  aks6d1c4  43440  aks6d1c2lem3  43442  aks6d1c2  43446  aks6d1c5lem1  43452  aks6d1c5lem3  43453  aks6d1c6lem1  43486  aks6d1c6lem3  43488  aks6d1c6lem5  43493  aks6d1c7lem1  43496  aks5lem1  43502  aks5lem2  43503  aks5lem5a  43507  frlmpwfi  44366  isnumbasgrplem3  44372  mendlmod  44452  idomodle  44454  2zrng0  49614  cznabel  49630  cznrng  49631  crhmsubcALTV  49697  fldcatALTV  49701  fldhmsubcALTV  49703  subrgccnzr  49708  crngprmringidom  49769  isidom3  49773  idomcanl  49775  mgpsumz  49805  mgpsumn  49806  evl1at0  49834  evl1at1  49835