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

Theorem crngring 19237
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 2818 . . 3 (mulGrp‘𝑅) = (mulGrp‘𝑅)
21iscrng 19233 . 2 (𝑅 ∈ CRing ↔ (𝑅 ∈ Ring ∧ (mulGrp‘𝑅) ∈ CMnd))
32simplbi 498 1 (𝑅 ∈ CRing → 𝑅 ∈ Ring)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2105  cfv 6348  CMndccmn 18835  mulGrpcmgp 19168  Ringcrg 19226  CRingccrg 19227
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-rex 3141  df-rab 3144  df-v 3494  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-nul 4289  df-if 4464  df-sn 4558  df-pr 4560  df-op 4564  df-uni 4831  df-br 5058  df-iota 6307  df-fv 6356  df-cring 19229
This theorem is referenced by:  gsummgp0  19287  prdscrngd  19292  crngbinom  19300  dvdsunit  19342  unitmulclb  19344  unitabl  19347  idsrngd  19562  rmodislmod  19631  quscrng  19941  assa2ass  20023  sraassa  20027  rlmassa  20028  ascldimulOLD  20045  asclrhm  20047  assamulgscmlem2  20057  psrcrng  20121  psrassa  20122  mplcrng  20162  mplassa  20163  mplcoe2  20178  mplbas2  20179  mplmon2mul  20209  mplind  20210  evlslem2  20220  evlslem3  20221  evlslem6  20222  evlslem1  20223  evlseu  20224  evlsval2  20228  evlsgsumadd  20232  evlsgsummul  20233  evlrhm  20237  evlsscasrng  20238  evlsca  20239  evlsvarsrng  20240  evlvar  20241  mpfind  20248  ply1crng  20294  ply1assa  20295  lply1binom  20402  lply1binomsc  20403  evls1rhmlem  20412  evls1gsumadd  20415  evls1gsummul  20416  evl1val  20420  evl1sca  20425  evl1scad  20426  evl1var  20427  evl1vard  20428  evls1var  20429  evls1scasrng  20430  evls1varsrng  20431  evl1subd  20433  evl1expd  20436  pf1const  20437  pf1id  20438  pf1ind  20446  evl1gsumdlem  20447  evl1gsumd  20448  evl1gsumadd  20449  evl1gsummul  20451  evl1varpw  20452  evl1scvarpw  20454  evl1scvarpwval  20455  evl1gsummon  20456  cnring  20495  zringring  20548  zring0  20555  znzrh2  20620  zncyg  20623  zndvds0  20625  znf1o  20626  zzngim  20627  znfld  20635  znchr  20637  znunit  20638  znrrg  20640  cygznlem3  20644  re0g  20684  mamuvs2  20943  matassa  20981  madetsumid  20998  madetsmelbas  21001  madetsmelbas2  21002  mat1dimcrng  21014  dmatcrng  21039  scmatcrng  21058  mdetleib2  21125  mdetf  21132  m1detdiag  21134  mdetdiaglem  21135  mdetdiag  21136  mdet1  21138  mdetrlin  21139  mdetrsca  21140  mdetrsca2  21141  mdetr0  21142  mdet0  21143  mdetrlin2  21144  mdetralt  21145  mdetero  21147  mdetmul  21160  maducoeval2  21177  maduf  21178  madutpos  21179  madugsum  21180  madurid  21181  madulid  21182  marep01ma  21197  smadiadetlem0  21198  smadiadetlem1a  21200  smadiadetlem3lem2  21204  smadiadetlem3  21205  smadiadetlem4  21206  smadiadet  21207  smadiadetglem1  21208  smadiadetglem2  21209  smadiadetg  21210  matinv  21214  matunit  21215  slesolinv  21217  slesolinvbi  21218  slesolex  21219  cramerimplem1  21220  cramerimplem2  21221  cramerimplem3  21222  cramerimp  21223  cramer  21228  mat2pmatmul  21267  mat2pmatmhm  21269  mat2pmatrhm  21270  mat2pmatlin  21271  m2cpmmhm  21281  m2cpmrhm  21282  m2pmfzgsumcl  21284  m2cpmrngiso  21294  monmatcollpw  21315  pmatcollpwlem  21316  pmatcollpw  21317  pmatcollpwfi  21318  pmatcollpw3fi1lem2  21323  pmatcollpwscmat  21327  monmat2matmon  21360  pm2mp  21361  chpmatply1  21368  chpmat1d  21372  chpdmat  21377  chpscmat  21378  chpscmatgsumbin  21380  chpscmatgsummon  21381  chp0mat  21382  chpidmat  21383  chmaidscmat  21384  chfacfscmulcl  21393  chfacfscmul0  21394  chfacfscmulgsum  21396  chfacfpmmulcl  21397  chfacfpmmul0  21398  chfacfpmmulgsum  21400  chfacfpmmulgsum2  21401  cayhamlem1  21402  cpmadurid  21403  cpmidgsumm2pm  21405  cpmidpmatlem2  21407  cpmidpmatlem3  21408  cpmadugsumlemB  21410  cpmadugsumlemC  21411  cpmadugsumlemF  21412  cpmadugsumfi  21413  cpmidgsum2  21415  cpmadumatpolylem1  21417  cpmadumatpolylem2  21418  cpmadumatpoly  21419  cayhamlem2  21420  chcoeffeqlem  21421  cayhamlem4  21424  cayleyhamilton0  21425  cayleyhamiltonALT  21427  cayleyhamilton1  21428  recvs  23677  fta1glem1  24686  fta1g  24688  fta1blem  24689  dchrelbas3  25741  dchrelbasd  25742  dchrzrh1  25747  dchrzrhmul  25749  dchrmulcl  25752  dchrn0  25753  dchrfi  25758  dchrghm  25759  dchrabs  25763  dchrinv  25764  dchrptlem1  25767  dchrptlem2  25768  dchrptlem3  25769  dchrsum2  25771  dchrhash  25774  sum2dchr  25777  lgsqrlem1  25849  lgsqrlem2  25850  lgsqrlem3  25851  lgsqrlem4  25852  lgsdchr  25858  lgseisenlem3  25880  lgseisenlem4  25881  dchrisum0flblem1  26011  dchrisum0re  26016  freshmansdream  30786  rdivmuldivd  30789  subofld  30816  isprmidlc  30881  qsidomlem1  30882  qsidomlem2  30883  mdetpmtr1  30987  mdetpmtr12  30989  madjusmdetlem1  30991  madjusmdetlem4  30994  mdetlap  30996  selvval2lem4  39014  selvval2lem5  39015  frlmpwfi  39576  isnumbasgrplem3  39583  mendlmod  39671  idomrootle  39673  idomodle  39674  2zrng0  44137  cznabel  44153  cznrng  44154  crhmsubc  44277  fldcat  44281  fldhmsubc  44283  crhmsubcALTV  44295  fldcatALTV  44299  fldhmsubcALTV  44301  mgpsumz  44338  mgpsumn  44339  evl1at0  44373  evl1at1  44374
  Copyright terms: Public domain W3C validator