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

Theorem rnggrp 16638
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 2438 . . 3  |-  ( Base `  R )  =  (
Base `  R )
2 eqid 2438 . . 3  |-  (mulGrp `  R )  =  (mulGrp `  R )
3 eqid 2438 . . 3  |-  ( +g  `  R )  =  ( +g  `  R )
4 eqid 2438 . . 3  |-  ( .r
`  R )  =  ( .r `  R
)
51, 2, 3, 4isrng 16637 . 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 1369    e. wcel 1756   A.wral 2710   ` cfv 5413  (class class class)co 6086   Basecbs 14166   +g cplusg 14230   .rcmulr 14231   Mndcmnd 15401   Grpcgrp 15402  mulGrpcmgp 16579   Ringcrg 16633
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419  ax-nul 4416
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2256  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-ral 2715  df-rex 2716  df-rab 2719  df-v 2969  df-sbc 3182  df-dif 3326  df-un 3328  df-in 3330  df-ss 3337  df-nul 3633  df-if 3787  df-sn 3873  df-pr 3875  df-op 3879  df-uni 4087  df-br 4288  df-iota 5376  df-fv 5421  df-ov 6089  df-rng 16635
This theorem is referenced by:  rngmnd  16642  rng0cl  16654  rngacl  16660  rngcom  16661  rngabl  16662  rnglz  16669  rngrz  16670  rngnegl  16673  rngnegr  16674  rngmneg1  16675  rngmneg2  16676  rngm2neg  16677  rngsubdi  16678  rngsubdir  16679  mulgass2  16680  rnglghm  16681  rngrghm  16682  prdsrngd  16692  imasrng  16699  opprrng  16711  dvdsrneg  16734  dvdsr02  16736  unitnegcl  16761  irrednegb  16791  dfrhm2  16796  isrhmd  16805  pwsco1rhm  16808  pwsco2rhm  16809  drnggrp  16818  subrgsubg  16849  cntzsubr  16875  pwsdiagrhm  16876  isabvd  16883  abvneg  16897  abvsubtri  16898  abvtrivd  16903  srng0  16923  idsrngd  16925  lmodfgrp  16935  lmod0vs  16959  lmodvsneg  16967  lmodsubvs  16979  lmodsubdi  16980  lmodsubdir  16981  lssvnegcl  17014  lmodvsinv  17094  sralmod  17245  issubrngd2  17247  lidlsubg  17274  2idlcpbl  17293  asclghm  17386  psrlmod  17449  psrdi  17456  psrdir  17457  psrrng  17460  mpllsslem  17488  mpllsslemOLD  17490  mplsubrg  17496  mplcoe1  17521  mplind  17559  evlslem2  17572  evlslem1  17576  coe1z  17692  coe1subfv  17695  evl1subd  17751  evl1gsumd  17766  cnfld0  17815  cnfldneg  17817  cnfldsub  17819  cnsubglem  17837  zringgrp  17863  mulgrhm  17901  mulgghm2OLD  17903  mulgrhmOLD  17904  chrdvds  17934  chrcong  17935  zncyg  17956  cygznlem3  17977  zrhpsgnelbas  17999  ip2subdi  18048  mdetralt  18389  mdetero  18391  mdetunilem6  18398  mdetunilem9  18401  mdetuni0  18402  m2detleiblem6  18407  trggrp  19721  tlmtgp  19745  abvmet  20143  nrgdsdi  20221  nrgdsdir  20222  tngnrg  20230  cnngp  20334  cnfldtgp  20420  cphsubrglem  20671  mdegldg  21512  mdeg0  21516  mdegaddle  21520  deg1add  21550  deg1suble  21554  deg1sub  21555  deg1sublt  21557  ply1nzb  21569  ply1divmo  21582  ply1divex  21583  r1pcl  21604  r1pid  21606  dvdsq1p  21607  dvdsr1p  21608  ply1remlem  21609  ply1rem  21610  ig1peu  21618  reefgim  21890  lgsqrlem1  22655  lgsqrlem2  22656  lgsqrlem3  22657  lgsqrlem4  22658  abvcxp  22839  dvrdir  26209  orngsqr  26223  ornglmulle  26224  orngrmulle  26225  ornglmullt  26226  orngrmullt  26227  orngmullt  26228  ofldchr  26233  suborng  26234  isarchiofld  26236  rhmopp  26238  kerf1hrm  26243  reofld  26260  zrhchr  26357  hbtlem5  29437  mendlmod  29503  subrgacs  29510  idomrootle  29513  invginvrid  30723  0rngnnzr  30729  evl1at0  30772  linply1  30776  mat0dim0  30786  dmatsubcl  30800  dmatsgrp  30801  scmatsubcl  30807  scmatsgrp  30808  scmatsgrp1  30812  lfl0  32550  lflsub  32552  lfl0f  32554  lfladdass  32558  lfladd0l  32559  lflnegcl  32560  lflnegl  32561  ldualvsubcl  32641  ldualvsubval  32642  lkrin  32649  erng0g  34478  lclkrlem2m  35004  lcfrlem2  35028  lcdvsubval  35103  mapdpglem30  35187  baerlem3lem1  35192  baerlem5alem1  35193  baerlem5blem1  35194  baerlem5blem2  35197  hdmapinvlem3  35408  hdmapinvlem4  35409  hdmapglem7b  35416
  Copyright terms: Public domain W3C validator