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

Theorem rnggrp 15624
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 2404 . . 3  |-  ( Base `  R )  =  (
Base `  R )
2 eqid 2404 . . 3  |-  (mulGrp `  R )  =  (mulGrp `  R )
3 eqid 2404 . . 3  |-  ( +g  `  R )  =  ( +g  `  R )
4 eqid 2404 . . 3  |-  ( .r
`  R )  =  ( .r `  R
)
51, 2, 3, 4isrng 15623 . 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 972 1  |-  ( R  e.  Ring  ->  R  e. 
Grp )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    = wceq 1649    e. wcel 1721   A.wral 2666   ` cfv 5413  (class class class)co 6040   Basecbs 13424   +g cplusg 13484   .rcmulr 13485   Mndcmnd 14639   Grpcgrp 14640  mulGrpcmgp 15603   Ringcrg 15615
This theorem is referenced by:  rngmnd  15628  rng0cl  15640  rngacl  15646  rngcom  15647  rngabl  15648  rnglz  15655  rngrz  15656  rngnegl  15658  rngnegr  15659  rngmneg1  15660  rngmneg2  15661  rngm2neg  15662  rngsubdi  15663  rngsubdir  15664  mulgass2  15665  rnglghm  15666  rngrghm  15667  prdsrngd  15673  imasrng  15680  opprrng  15691  dvdsrneg  15714  dvdsr02  15716  unitnegcl  15741  irrednegb  15771  dfrhm2  15776  isrhmd  15785  pwsco1rhm  15788  pwsco2rhm  15789  drnggrp  15798  subrgsubg  15829  cntzsubr  15855  pwsdiagrhm  15856  isabvd  15863  abvneg  15877  abvsubtri  15878  abvtrivd  15883  srng0  15903  lmodfgrp  15914  lmod0vs  15938  lmodvsneg  15943  lmodsubvs  15955  lmodsubdi  15956  lmodsubdir  15957  lssvnegcl  15987  lmodvsinv  16067  sralmod  16213  issubrngd2  16217  lidlsubg  16241  2idlcpbl  16260  asclghm  16352  psrlmod  16420  psrdi  16425  psrdir  16426  psrrng  16429  mpllsslem  16454  mplsubrg  16458  mplcoe1  16483  mplind  16517  evlslem2  16523  coe1z  16611  coe1subfv  16614  cnfld0  16680  cnfldneg  16682  cnfldsub  16684  cnsubglem  16702  mulgghm2  16741  mulgrhm  16742  chrdvds  16764  chrcong  16765  zncyg  16784  cygznlem3  16805  ip2subdi  16830  trggrp  18154  tlmtgp  18178  abvmet  18576  nrgdsdi  18654  nrgdsdir  18655  tngnrg  18663  cnngp  18767  cnfldtgp  18852  cphsubrglem  19093  evlslem1  19889  evl1subd  19908  mdegldg  19942  mdeg0  19946  mdegaddle  19950  deg1add  19979  deg1suble  19983  deg1sub  19984  deg1sublt  19986  ply1nzb  19998  ply1divmo  20011  ply1divex  20012  r1pcl  20033  r1pid  20035  dvdsq1p  20036  dvdsr1p  20037  ply1remlem  20038  ply1rem  20039  ig1peu  20047  reefgim  20319  lgsqrlem1  21078  lgsqrlem2  21079  lgsqrlem3  21080  lgsqrlem4  21081  abvcxp  21262  dvrdir  24179  ofldsqr  24193  ofldaddlt  24194  ofldchr  24197  subofld  24198  rhmopp  24210  kerf1hrm  24215  zrhchr  24313  hbtlem5  27200  mendlmod  27369  subrgacs  27376  idomrootle  27379  lfl0  29548  lflsub  29550  lfl0f  29552  lfladdass  29556  lfladd0l  29557  lflnegcl  29558  lflnegl  29559  ldualvsubcl  29639  ldualvsubval  29640  lkrin  29647  erng0g  31476  lclkrlem2m  32002  lcfrlem2  32026  lcdvsubval  32101  mapdpglem30  32185  baerlem3lem1  32190  baerlem5alem1  32191  baerlem5blem1  32192  baerlem5blem2  32195  hdmapinvlem3  32406  hdmapinvlem4  32407  hdmapglem7b  32414
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385  ax-nul 4298
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2258  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ne 2569  df-ral 2671  df-rex 2672  df-rab 2675  df-v 2918  df-sbc 3122  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-nul 3589  df-if 3700  df-sn 3780  df-pr 3781  df-op 3783  df-uni 3976  df-br 4173  df-iota 5377  df-fv 5421  df-ov 6043  df-rng 15618
  Copyright terms: Public domain W3C validator