MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  rnggrp Structured version   Unicode version

Theorem rnggrp 16586
Description: A ring is a group. (Contributed by NM, 15-Sep-2011.)
Assertion
Ref Expression
rnggrp  |-  ( R  e.  Ring  ->  R  e. 
Grp )

Proof of Theorem rnggrp
Dummy variables  x  y  z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eqid 2433 . . 3  |-  ( Base `  R )  =  (
Base `  R )
2 eqid 2433 . . 3  |-  (mulGrp `  R )  =  (mulGrp `  R )
3 eqid 2433 . . 3  |-  ( +g  `  R )  =  ( +g  `  R )
4 eqid 2433 . . 3  |-  ( .r
`  R )  =  ( .r `  R
)
51, 2, 3, 4isrng 16585 . 2  |-  ( R  e.  Ring  <->  ( R  e. 
Grp  /\  (mulGrp `  R
)  e.  Mnd  /\  A. x  e.  ( Base `  R ) A. y  e.  ( Base `  R
) A. z  e.  ( Base `  R
) ( ( x ( .r `  R
) ( y ( +g  `  R ) z ) )  =  ( ( x ( .r `  R ) y ) ( +g  `  R ) ( x ( .r `  R
) z ) )  /\  ( ( x ( +g  `  R
) y ) ( .r `  R ) z )  =  ( ( x ( .r
`  R ) z ) ( +g  `  R
) ( y ( .r `  R ) z ) ) ) ) )
65simp1bi 996 1  |-  ( R  e.  Ring  ->  R  e. 
Grp )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    = wceq 1362    e. wcel 1755   A.wral 2705   ` cfv 5406  (class class class)co 6080   Basecbs 14157   +g cplusg 14221   .rcmulr 14222   Mndcmnd 15392   Grpcgrp 15393  mulGrpcmgp 16565   Ringcrg 16577
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414  ax-nul 4409
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 960  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-eu 2258  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-ne 2598  df-ral 2710  df-rex 2711  df-rab 2714  df-v 2964  df-sbc 3176  df-dif 3319  df-un 3321  df-in 3323  df-ss 3330  df-nul 3626  df-if 3780  df-sn 3866  df-pr 3868  df-op 3872  df-uni 4080  df-br 4281  df-iota 5369  df-fv 5414  df-ov 6083  df-rng 16580
This theorem is referenced by:  rngmnd  16590  rng0cl  16602  rngacl  16608  rngcom  16609  rngabl  16610  rnglz  16617  rngrz  16618  rngnegl  16620  rngnegr  16621  rngmneg1  16622  rngmneg2  16623  rngm2neg  16624  rngsubdi  16625  rngsubdir  16626  mulgass2  16627  rnglghm  16628  rngrghm  16629  prdsrngd  16639  imasrng  16646  opprrng  16657  dvdsrneg  16680  dvdsr02  16682  unitnegcl  16707  irrednegb  16737  dfrhm2  16742  isrhmd  16751  pwsco1rhm  16754  pwsco2rhm  16755  drnggrp  16764  subrgsubg  16795  cntzsubr  16821  pwsdiagrhm  16822  isabvd  16829  abvneg  16843  abvsubtri  16844  abvtrivd  16849  srng0  16869  idsrngd  16871  lmodfgrp  16881  lmod0vs  16905  lmodvsneg  16913  lmodsubvs  16925  lmodsubdi  16926  lmodsubdir  16927  lssvnegcl  16959  lmodvsinv  17039  sralmod  17190  issubrngd2  17192  lidlsubg  17219  2idlcpbl  17238  asclghm  17331  psrlmod  17406  psrdi  17413  psrdir  17414  psrrng  17417  mpllsslem  17445  mpllsslemOLD  17447  mplsubrg  17453  mplcoe1  17478  mplind  17516  evlslem2  17525  coe1z  17615  coe1subfv  17618  cnfld0  17684  cnfldneg  17686  cnfldsub  17688  cnsubglem  17706  zringgrp  17730  mulgrhm  17768  mulgghm2OLD  17770  mulgrhmOLD  17771  chrdvds  17801  chrcong  17802  zncyg  17823  cygznlem3  17844  zrhpsgnelbas  17866  ip2subdi  17915  mdetralt  18256  mdetero  18258  mdetunilem6  18265  mdetunilem9  18268  mdetuni0  18269  m2detleiblem6  18274  trggrp  19588  tlmtgp  19612  abvmet  20010  nrgdsdi  20088  nrgdsdir  20089  tngnrg  20097  cnngp  20201  cnfldtgp  20287  cphsubrglem  20538  evlslem1  21367  evl1subd  21386  mdegldg  21422  mdeg0  21426  mdegaddle  21430  deg1add  21460  deg1suble  21464  deg1sub  21465  deg1sublt  21467  ply1nzb  21479  ply1divmo  21492  ply1divex  21493  r1pcl  21514  r1pid  21516  dvdsq1p  21517  dvdsr1p  21518  ply1remlem  21519  ply1rem  21520  ig1peu  21528  reefgim  21800  lgsqrlem1  22565  lgsqrlem2  22566  lgsqrlem3  22567  lgsqrlem4  22568  abvcxp  22749  dvrdir  26111  orngsqr  26125  ornglmulle  26126  orngrmulle  26127  ornglmullt  26128  orngrmullt  26129  orngmullt  26130  ofldchr  26135  suborng  26136  isarchiofld  26138  rhmopp  26140  kerf1hrm  26145  reofld  26162  zrhchr  26259  hbtlem5  29329  mendlmod  29395  subrgacs  29402  idomrootle  29405  invginvrid  30603  0rngnnzr  30609  evl1at0  30631  linply1  30635  mat0dim0  30643  lfl0  32283  lflsub  32285  lfl0f  32287  lfladdass  32291  lfladd0l  32292  lflnegcl  32293  lflnegl  32294  ldualvsubcl  32374  ldualvsubval  32375  lkrin  32382  erng0g  34211  lclkrlem2m  34737  lcfrlem2  34761  lcdvsubval  34836  mapdpglem30  34920  baerlem3lem1  34925  baerlem5alem1  34926  baerlem5blem1  34927  baerlem5blem2  34930  hdmapinvlem3  35141  hdmapinvlem4  35142  hdmapglem7b  35149
  Copyright terms: Public domain W3C validator