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

Theorem rnggrp 15346
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 2283 . . 3  |-  ( Base `  R )  =  (
Base `  R )
2 eqid 2283 . . 3  |-  (mulGrp `  R )  =  (mulGrp `  R )
3 eqid 2283 . . 3  |-  ( +g  `  R )  =  ( +g  `  R )
4 eqid 2283 . . 3  |-  ( .r
`  R )  =  ( .r `  R
)
51, 2, 3, 4isrng 15345 . 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 1623    e. wcel 1684   A.wral 2543   ` cfv 5255  (class class class)co 5858   Basecbs 13148   +g cplusg 13208   .rcmulr 13209   Mndcmnd 14361   Grpcgrp 14362  mulGrpcmgp 15325   Ringcrg 15337
This theorem is referenced by:  rngmnd  15350  rng0cl  15362  rngacl  15368  rngcom  15369  rngabl  15370  rnglz  15377  rngrz  15378  rngnegl  15380  rngnegr  15381  rngmneg1  15382  rngmneg2  15383  rngm2neg  15384  rngsubdi  15385  rngsubdir  15386  mulgass2  15387  rnglghm  15388  rngrghm  15389  prdsrngd  15395  imasrng  15402  opprrng  15413  dvdsrneg  15436  dvdsr02  15438  unitnegcl  15463  irrednegb  15493  dfrhm2  15498  isrhmd  15507  pwsco1rhm  15510  pwsco2rhm  15511  drnggrp  15520  subrgsubg  15551  cntzsubr  15577  pwsdiagrhm  15578  isabvd  15585  abvneg  15599  abvsubtri  15600  abvtrivd  15605  srng0  15625  lmodfgrp  15636  lmod0vs  15663  lmodvsnegOLD  15668  lmodvsneg  15669  lmodsubvs  15681  lmodsubdi  15682  lmodsubdir  15683  lssvnegcl  15713  lmodvsinv  15793  sralmod  15939  issubrngd2  15943  lidlsubg  15967  2idlcpbl  15986  asclghm  16078  psrlmod  16146  psrdi  16151  psrdir  16152  psrrng  16155  mpllsslem  16180  mplsubrg  16184  mplcoe1  16209  mplind  16243  evlslem2  16249  coe1z  16340  coe1subfv  16343  cnfld0  16398  cnfldneg  16400  cnfldsub  16402  cnsubglem  16420  mulgghm2  16459  mulgrhm  16460  chrdvds  16482  chrcong  16483  zncyg  16502  cygznlem3  16523  ip2subdi  16548  trggrp  17854  tlmtgp  17878  abvmet  18098  nrgdsdi  18176  nrgdsdir  18177  tngnrg  18185  cnngp  18289  cnfldtgp  18373  cphsubrglem  18613  evlslem1  19399  evl1subd  19418  mdegldg  19452  mdeg0  19456  mdegaddle  19460  deg1add  19489  deg1suble  19493  deg1sub  19494  deg1sublt  19496  ply1nzb  19508  ply1divmo  19521  ply1divex  19522  r1pcl  19543  r1pid  19545  dvdsq1p  19546  dvdsr1p  19547  ply1remlem  19548  ply1rem  19549  ig1peu  19557  reefgim  19826  lgsqrlem1  20580  lgsqrlem2  20581  lgsqrlem3  20582  lgsqrlem4  20583  abvcxp  20764  hbtlem5  27332  mendlmod  27501  subrgacs  27508  idomrootle  27511  lfl0  29255  lflsub  29257  lfl0f  29259  lfladdass  29263  lfladd0l  29264  lflnegcl  29265  lflnegl  29266  ldualvsubcl  29346  ldualvsubval  29347  lkrin  29354  erng0g  31183  lclkrlem2m  31709  lcfrlem2  31733  lcdvsubval  31808  mapdpglem30  31892  baerlem3lem1  31897  baerlem5alem1  31898  baerlem5blem1  31899  baerlem5blem2  31902  hdmapinvlem3  32113  hdmapinvlem4  32114  hdmapglem7b  32121
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264  ax-nul 4149
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-eu 2147  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ne 2448  df-ral 2548  df-rex 2549  df-rab 2552  df-v 2790  df-sbc 2992  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3456  df-if 3566  df-sn 3646  df-pr 3647  df-op 3649  df-uni 3828  df-br 4024  df-iota 5219  df-fv 5263  df-ov 5861  df-rng 15340
  Copyright terms: Public domain W3C validator