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

Theorem rnggrp 15671
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 15670 . 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 973 1  |-  ( R  e.  Ring  ->  R  e. 
Grp )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 360    = wceq 1653    e. wcel 1726   A.wral 2707   ` cfv 5456  (class class class)co 6083   Basecbs 13471   +g cplusg 13531   .rcmulr 13532   Mndcmnd 14686   Grpcgrp 14687  mulGrpcmgp 15650   Ringcrg 15662
This theorem is referenced by:  rngmnd  15675  rng0cl  15687  rngacl  15693  rngcom  15694  rngabl  15695  rnglz  15702  rngrz  15703  rngnegl  15705  rngnegr  15706  rngmneg1  15707  rngmneg2  15708  rngm2neg  15709  rngsubdi  15710  rngsubdir  15711  mulgass2  15712  rnglghm  15713  rngrghm  15714  prdsrngd  15720  imasrng  15727  opprrng  15738  dvdsrneg  15761  dvdsr02  15763  unitnegcl  15788  irrednegb  15818  dfrhm2  15823  isrhmd  15832  pwsco1rhm  15835  pwsco2rhm  15836  drnggrp  15845  subrgsubg  15876  cntzsubr  15902  pwsdiagrhm  15903  isabvd  15910  abvneg  15924  abvsubtri  15925  abvtrivd  15930  srng0  15950  lmodfgrp  15961  lmod0vs  15985  lmodvsneg  15990  lmodsubvs  16002  lmodsubdi  16003  lmodsubdir  16004  lssvnegcl  16034  lmodvsinv  16114  sralmod  16260  issubrngd2  16264  lidlsubg  16288  2idlcpbl  16307  asclghm  16399  psrlmod  16467  psrdi  16472  psrdir  16473  psrrng  16476  mpllsslem  16501  mplsubrg  16505  mplcoe1  16530  mplind  16564  evlslem2  16570  coe1z  16658  coe1subfv  16661  cnfld0  16727  cnfldneg  16729  cnfldsub  16731  cnsubglem  16749  mulgghm2  16788  mulgrhm  16789  chrdvds  16811  chrcong  16812  zncyg  16831  cygznlem3  16852  ip2subdi  16877  trggrp  18203  tlmtgp  18227  abvmet  18625  nrgdsdi  18703  nrgdsdir  18704  tngnrg  18712  cnngp  18816  cnfldtgp  18901  cphsubrglem  19142  evlslem1  19938  evl1subd  19957  mdegldg  19991  mdeg0  19995  mdegaddle  19999  deg1add  20028  deg1suble  20032  deg1sub  20033  deg1sublt  20035  ply1nzb  20047  ply1divmo  20060  ply1divex  20061  r1pcl  20082  r1pid  20084  dvdsq1p  20085  dvdsr1p  20086  ply1remlem  20087  ply1rem  20088  ig1peu  20096  reefgim  20368  lgsqrlem1  21127  lgsqrlem2  21128  lgsqrlem3  21129  lgsqrlem4  21130  abvcxp  21311  dvrdir  24228  ofldsqr  24242  ofldaddlt  24243  ofldchr  24246  subofld  24247  rhmopp  24259  kerf1hrm  24264  zrhchr  24362  hbtlem5  27311  mendlmod  27480  subrgacs  27487  idomrootle  27490  lfl0  29925  lflsub  29927  lfl0f  29929  lfladdass  29933  lfladd0l  29934  lflnegcl  29935  lflnegl  29936  ldualvsubcl  30016  ldualvsubval  30017  lkrin  30024  erng0g  31853  lclkrlem2m  32379  lcfrlem2  32403  lcdvsubval  32478  mapdpglem30  32562  baerlem3lem1  32567  baerlem5alem1  32568  baerlem5blem1  32569  baerlem5blem2  32572  hdmapinvlem3  32783  hdmapinvlem4  32784  hdmapglem7b  32791
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419  ax-nul 4340
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-eu 2287  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-ral 2712  df-rex 2713  df-rab 2716  df-v 2960  df-sbc 3164  df-dif 3325  df-un 3327  df-in 3329  df-ss 3336  df-nul 3631  df-if 3742  df-sn 3822  df-pr 3823  df-op 3825  df-uni 4018  df-br 4215  df-iota 5420  df-fv 5464  df-ov 6086  df-rng 15665
  Copyright terms: Public domain W3C validator