Theorem ringgrp 20141

Description: A ring is a group. (Contributed by NM, 15-Sep-2011.)

Assertion

Ref	Expression
ringgrp	⊢ (𝑅 ∈ Ring → 𝑅 ∈ Grp)

Proof of Theorem ringgrp

Dummy variables 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		eqid 2729	. . 3 ⊢ (Base‘𝑅) = (Base‘𝑅)
2		eqid 2729	. . 3 ⊢ (mulGrp‘𝑅) = (mulGrp‘𝑅)
3		eqid 2729	. . 3 ⊢ (+g‘𝑅) = (+g‘𝑅)
4		eqid 2729	. . 3 ⊢ (.r‘𝑅) = (.r‘𝑅)
5	1, 2, 3, 4	isring 20140	. 2 ⊢ (𝑅 ∈ Ring ↔ (𝑅 ∈ Grp ∧ (mulGrp‘𝑅) ∈ Mnd ∧ ∀𝑥 ∈ (Base‘𝑅)∀𝑦 ∈ (Base‘𝑅)∀𝑧 ∈ (Base‘𝑅)((𝑥(.r‘𝑅)(𝑦(+g‘𝑅)𝑧)) = ((𝑥(.r‘𝑅)𝑦)(+g‘𝑅)(𝑥(.r‘𝑅)𝑧)) ∧ ((𝑥(+g‘𝑅)𝑦)(.r‘𝑅)𝑧) = ((𝑥(.r‘𝑅)𝑧)(+g‘𝑅)(𝑦(.r‘𝑅)𝑧)))))
6	5	simp1bi 1145	1 ⊢ (𝑅 ∈ Ring → 𝑅 ∈ Grp)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2109  ∀wral 3044  ‘cfv 6486  (class class class)co 7353  Basecbs 17138  +_gcplusg 17179  ._rcmulr 17180  Mndcmnd 18626  Grpcgrp 18830  mulGrpcmgp 20043  Ringcrg 20136

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-nul 5248

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ne 2926  df-ral 3045  df-rab 3397  df-v 3440  df-sbc 3745  df-dif 3908  df-un 3910  df-ss 3922  df-nul 4287  df-if 4479  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4862  df-br 5096  df-iota 6442  df-fv 6494  df-ov 7356  df-ring 20138

This theorem is referenced by:  ringgrpd  20145  ringmnd  20146  ring0cl  20170  ringacl  20181  ringabl  20184  ringnegl  20205  ringnegr  20206  ringmneg1  20207  ringmneg2  20208  mulgass2  20212  ringlghm  20215  ringrghm  20216  prdsringd  20224  imasring  20233  dvdsrneg  20273  dvdsr02  20275  unitnegcl  20300  dvrdir  20315  irrednegb  20334  dfrhm2  20377  isrhmd  20391  idrhm  20393  pwsco1rhm  20405  pwsco2rhm  20406  rhmopp  20412  0ringnnzr  20428  c0rhm  20437  c0rnghm  20438  zrrnghm  20439  subrgsubg  20480  cntzsubr  20509  pwsdiagrhm  20510  subrgacs  20703  isabvd  20715  abvneg  20729  abvsubtri  20730  abvtrivd  20735  srng0  20757  idsrngd  20759  orngsqr  20769  ornglmulle  20770  orngrmulle  20771  ornglmullt  20772  orngrmullt  20773  orngmullt  20774  suborng  20779  lmodfgrp  20790  lmod0vs  20816  lmodvsneg  20827  lmodsubvs  20839  lmodsubdi  20840  lmodsubdir  20841  rmodislmodlem  20850  rmodislmod  20851  lmodvsinv  20958  sralmod  21109  issubrgd  21111  lidlsubg  21148  cnfld0  21317  cnfldneg  21320  cnfldsub  21322  cnsubglem  21340  zringgrp  21377  mulgrhm  21402  chrdvds  21451  chrcong  21452  dvdschrmulg  21453  zncyg  21473  cygznlem3  21494  freshmansdream  21499  zrhpsgnelbas  21519  ip2subdi  21569  asclghm  21808  psrlmod  21885  psrring  21895  mpllsslem  21925  mplsubrg  21930  mplcoe1  21960  mplind  21993  evlslem2  22002  coe1z  22165  coe1subfv  22168  evl1subd  22245  evl1gsumd  22260  matinvgcell  22338  mat0dim0  22370  mat1ghm  22386  dmatsubcl  22401  dmatsgrp  22402  scmataddcl  22419  scmatsubcl  22420  scmatsgrp  22422  scmatsgrp1  22425  scmatghm  22436  mdetralt  22511  mdetero  22513  mdetunilem6  22520  mdetunilem9  22523  mdetuni0  22524  m2detleiblem6  22529  cpmatinvcl  22620  cpmatsubgpmat  22623  mat2pmatghm  22633  pm2mpghm  22719  chmatcl  22731  chpmat0d  22737  chpmat1d  22739  chpdmatlem1  22741  chpdmatlem2  22742  chpscmat  22745  chpscmatgsumbin  22747  chpscmatgsummon  22748  chp0mat  22749  chpidmat  22750  chfacfisf  22757  chfacfscmulgsum  22763  chfacfpmmulgsum  22767  cayhamlem1  22769  cpmadugsumlemF  22779  cpmidgsum2  22782  trggrp  24075  tlmtgp  24099  abvmet  24479  nrgdsdi  24569  nrgdsdir  24570  tngnrg  24578  cnngp  24683  cnfldtgp  24776  cnncvsaddassdemo  25079  cphsubrglem  25093  mdegldg  25987  mdeg0  25991  mdegaddle  25995  deg1add  26024  deg1suble  26028  deg1sub  26029  deg1sublt  26031  ply1nzb  26044  ply1divmo  26057  ply1divex  26058  r1pcl  26080  r1pid  26082  dvdsq1p  26084  dvdsr1p  26085  ply1remlem  26086  ply1rem  26087  idomrootle  26094  ig1peu  26096  reefgim  26376  lgsqrlem1  27273  lgsqrlem2  27274  lgsqrlem3  27275  lgsqrlem4  27276  abvcxp  27542  isarchiofld  33151  rmfsupp2  33188  reofld  33291  linds2eq  33328  qsidomlem1  33399  qsidomlem2  33400  qsnzr  33402  mxidlprm  33417  zringfrac  33501  fedgmullem1  33601  ccfldsrarelvec  33642  zrhchr  33940  matunitlindflem1  37595  lfl0  39043  lflsub  39045  lfl0f  39047  lfladdass  39051  lfladd0l  39052  lflnegcl  39053  lflnegl  39054  ldualvsubcl  39134  ldualvsubval  39135  lkrin  39142  erng0g  40973  lclkrlem2m  41498  lcfrlem2  41522  lcdvsubval  41597  mapdpglem30  41681  baerlem3lem1  41686  baerlem5alem1  41687  baerlem5blem1  41688  baerlem5blem2  41691  hdmapinvlem3  41899  hdmapinvlem4  41900  hdmapglem7b  41907  aks6d1c6lem2  42144  aks6d1c6lem3  42145  aks6d1c6isolem2  42148  aks5lem3a  42162  aks5lem7  42173  hbtlem5  43101  mendlmod  43162  lidldomn1  48216  invginvrid  48352  evl1at0  48377  linply1  48379