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

Theorem rnggrp 16776
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 2454 . . 3  |-  ( Base `  R )  =  (
Base `  R )
2 eqid 2454 . . 3  |-  (mulGrp `  R )  =  (mulGrp `  R )
3 eqid 2454 . . 3  |-  ( +g  `  R )  =  ( +g  `  R )
4 eqid 2454 . . 3  |-  ( .r
`  R )  =  ( .r `  R
)
51, 2, 3, 4isrng 16775 . 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 1003 1  |-  ( R  e.  Ring  ->  R  e. 
Grp )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    = wceq 1370    e. wcel 1758   A.wral 2799   ` cfv 5529  (class class class)co 6203   Basecbs 14295   +g cplusg 14360   .rcmulr 14361   Mndcmnd 15531   Grpcgrp 15532  mulGrpcmgp 16716   Ringcrg 16771
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432  ax-nul 4532
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-eu 2266  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2650  df-ral 2804  df-rex 2805  df-rab 2808  df-v 3080  df-sbc 3295  df-dif 3442  df-un 3444  df-in 3446  df-ss 3453  df-nul 3749  df-if 3903  df-sn 3989  df-pr 3991  df-op 3995  df-uni 4203  df-br 4404  df-iota 5492  df-fv 5537  df-ov 6206  df-rng 16773
This theorem is referenced by:  rngmnd  16780  rng0cl  16792  rngacl  16798  rngcom  16799  rngabl  16800  rnglz  16807  rngrz  16808  rngnegl  16811  rngnegr  16812  rngmneg1  16813  rngmneg2  16814  rngm2neg  16815  rngsubdi  16816  rngsubdir  16817  mulgass2  16818  rnglghm  16819  rngrghm  16820  prdsrngd  16830  imasrng  16837  opprrng  16849  dvdsrneg  16872  dvdsr02  16874  unitnegcl  16899  irrednegb  16929  dfrhm2  16934  isrhmd  16945  pwsco1rhm  16952  pwsco2rhm  16953  kerf1hrm  16957  drnggrp  16966  subrgsubg  16997  cntzsubr  17023  pwsdiagrhm  17024  isabvd  17031  abvneg  17045  abvsubtri  17046  abvtrivd  17051  srng0  17071  idsrngd  17073  lmodfgrp  17083  lmod0vs  17107  lmodvsneg  17115  lmodsubvs  17127  lmodsubdi  17128  lmodsubdir  17129  lssvnegcl  17163  lmodvsinv  17243  sralmod  17394  issubrngd2  17396  lidlsubg  17423  2idlcpbl  17442  asclghm  17535  psrlmod  17598  psrdi  17605  psrdir  17606  psrrng  17610  mpllsslem  17638  mpllsslemOLD  17640  mplsubrg  17646  mplcoe1  17671  mplind  17711  evlslem2  17724  evlslem1  17728  coe1z  17843  coe1subfv  17846  evl1subd  17904  evl1gsumd  17919  cnfld0  17968  cnfldneg  17970  cnfldsub  17972  cnsubglem  17990  zringgrp  18016  mulgrhm  18054  mulgghm2OLD  18056  mulgrhmOLD  18057  chrdvds  18087  chrcong  18088  zncyg  18109  cygznlem3  18130  zrhpsgnelbas  18152  ip2subdi  18201  mdetralt  18549  mdetero  18551  mdetunilem6  18558  mdetunilem9  18561  mdetuni0  18562  m2detleiblem6  18567  trggrp  19881  tlmtgp  19905  abvmet  20303  nrgdsdi  20381  nrgdsdir  20382  tngnrg  20390  cnngp  20494  cnfldtgp  20580  cphsubrglem  20831  mdegldg  21673  mdeg0  21677  mdegaddle  21681  deg1add  21711  deg1suble  21715  deg1sub  21716  deg1sublt  21718  ply1nzb  21730  ply1divmo  21743  ply1divex  21744  r1pcl  21765  r1pid  21767  dvdsq1p  21768  dvdsr1p  21769  ply1remlem  21770  ply1rem  21771  ig1peu  21779  reefgim  22051  lgsqrlem1  22816  lgsqrlem2  22817  lgsqrlem3  22818  lgsqrlem4  22819  abvcxp  23000  dvrdir  26423  orngsqr  26437  ornglmulle  26438  orngrmulle  26439  ornglmullt  26440  orngrmullt  26441  orngmullt  26442  ofldchr  26447  suborng  26448  isarchiofld  26450  rhmopp  26452  reofld  26473  zrhchr  26570  hbtlem5  29652  mendlmod  29718  subrgacs  29725  idomrootle  29728  invginvrid  30940  0rngnnzr  30946  evl1at0  31027  linply1  31031  matinvgcell  31039  mat0dim0  31049  dmatsubcl  31076  dmatsgrp  31077  scmatsubcl  31083  scmatsgrp  31084  scmatsgrp1  31088  cpmatinvcl  31226  cpmatsubgpmat  31229  mat2pmatghm  31239  pm2mpghm  31323  chmacl  31334  cpmat0d  31340  cpmat1d  31342  cpdmatlem1  31344  cpdmatlem2  31345  cpscmat  31348  cpscmatgsumbin  31350  cpscmatgsummon  31351  cp0mat  31352  cpidmat  31353  chfacfisf  31360  chfacfscmulgsum  31366  chfacfpmmulgsum  31370  cayhamlem1  31372  cpmadugsumlemF  31382  cpmidgsum2  31385  lfl0  33068  lflsub  33070  lfl0f  33072  lfladdass  33076  lfladd0l  33077  lflnegcl  33078  lflnegl  33079  ldualvsubcl  33159  ldualvsubval  33160  lkrin  33167  erng0g  34996  lclkrlem2m  35522  lcfrlem2  35546  lcdvsubval  35621  mapdpglem30  35705  baerlem3lem1  35710  baerlem5alem1  35711  baerlem5blem1  35712  baerlem5blem2  35715  hdmapinvlem3  35926  hdmapinvlem4  35927  hdmapglem7b  35934
  Copyright terms: Public domain W3C validator