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

Theorem rnggrp 15362
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 2296 . . 3  |-  ( Base `  R )  =  (
Base `  R )
2 eqid 2296 . . 3  |-  (mulGrp `  R )  =  (mulGrp `  R )
3 eqid 2296 . . 3  |-  ( +g  `  R )  =  ( +g  `  R )
4 eqid 2296 . . 3  |-  ( .r
`  R )  =  ( .r `  R
)
51, 2, 3, 4isrng 15361 . 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 970 1  |-  ( R  e.  Ring  ->  R  e. 
Grp )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    = wceq 1632    e. wcel 1696   A.wral 2556   ` cfv 5271  (class class class)co 5874   Basecbs 13164   +g cplusg 13224   .rcmulr 13225   Mndcmnd 14377   Grpcgrp 14378  mulGrpcmgp 15341   Ringcrg 15353
This theorem is referenced by:  rngmnd  15366  rng0cl  15378  rngacl  15384  rngcom  15385  rngabl  15386  rnglz  15393  rngrz  15394  rngnegl  15396  rngnegr  15397  rngmneg1  15398  rngmneg2  15399  rngm2neg  15400  rngsubdi  15401  rngsubdir  15402  mulgass2  15403  rnglghm  15404  rngrghm  15405  prdsrngd  15411  imasrng  15418  opprrng  15429  dvdsrneg  15452  dvdsr02  15454  unitnegcl  15479  irrednegb  15509  dfrhm2  15514  isrhmd  15523  pwsco1rhm  15526  pwsco2rhm  15527  drnggrp  15536  subrgsubg  15567  cntzsubr  15593  pwsdiagrhm  15594  isabvd  15601  abvneg  15615  abvsubtri  15616  abvtrivd  15621  srng0  15641  lmodfgrp  15652  lmod0vs  15679  lmodvsnegOLD  15684  lmodvsneg  15685  lmodsubvs  15697  lmodsubdi  15698  lmodsubdir  15699  lssvnegcl  15729  lmodvsinv  15809  sralmod  15955  issubrngd2  15959  lidlsubg  15983  2idlcpbl  16002  asclghm  16094  psrlmod  16162  psrdi  16167  psrdir  16168  psrrng  16171  mpllsslem  16196  mplsubrg  16200  mplcoe1  16225  mplind  16259  evlslem2  16265  coe1z  16356  coe1subfv  16359  cnfld0  16414  cnfldneg  16416  cnfldsub  16418  cnsubglem  16436  mulgghm2  16475  mulgrhm  16476  chrdvds  16498  chrcong  16499  zncyg  16518  cygznlem3  16539  ip2subdi  16564  trggrp  17870  tlmtgp  17894  abvmet  18114  nrgdsdi  18192  nrgdsdir  18193  tngnrg  18201  cnngp  18305  cnfldtgp  18389  cphsubrglem  18629  evlslem1  19415  evl1subd  19434  mdegldg  19468  mdeg0  19472  mdegaddle  19476  deg1add  19505  deg1suble  19509  deg1sub  19510  deg1sublt  19512  ply1nzb  19524  ply1divmo  19537  ply1divex  19538  r1pcl  19559  r1pid  19561  dvdsq1p  19562  dvdsr1p  19563  ply1remlem  19564  ply1rem  19565  ig1peu  19573  reefgim  19842  lgsqrlem1  20596  lgsqrlem2  20597  lgsqrlem3  20598  lgsqrlem4  20599  abvcxp  20780  hbtlem5  27435  mendlmod  27604  subrgacs  27611  idomrootle  27614  lfl0  29877  lflsub  29879  lfl0f  29881  lfladdass  29885  lfladd0l  29886  lflnegcl  29887  lflnegl  29888  ldualvsubcl  29968  ldualvsubval  29969  lkrin  29976  erng0g  31805  lclkrlem2m  32331  lcfrlem2  32355  lcdvsubval  32430  mapdpglem30  32514  baerlem3lem1  32519  baerlem5alem1  32520  baerlem5blem1  32521  baerlem5blem2  32524  hdmapinvlem3  32735  hdmapinvlem4  32736  hdmapglem7b  32743
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277  ax-nul 4165
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-eu 2160  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-ne 2461  df-ral 2561  df-rex 2562  df-rab 2565  df-v 2803  df-sbc 3005  df-dif 3168  df-un 3170  df-in 3172  df-ss 3179  df-nul 3469  df-if 3579  df-sn 3659  df-pr 3660  df-op 3662  df-uni 3844  df-br 4040  df-iota 5235  df-fv 5279  df-ov 5877  df-rng 15356
  Copyright terms: Public domain W3C validator