Theorem ringgrp 20196

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 2735	. . 3 ⊢ (Base‘𝑅) = (Base‘𝑅)
2		eqid 2735	. . 3 ⊢ (mulGrp‘𝑅) = (mulGrp‘𝑅)
3		eqid 2735	. . 3 ⊢ (+g‘𝑅) = (+g‘𝑅)
4		eqid 2735	. . 3 ⊢ (.r‘𝑅) = (.r‘𝑅)
5	1, 2, 3, 4	isring 20195	. 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 2108  ∀wral 3051  ‘cfv 6530  (class class class)co 7403  Basecbs 17226  +_gcplusg 17269  ._rcmulr 17270  Mndcmnd 18710  Grpcgrp 18914  mulGrpcmgp 20098  Ringcrg 20191

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 2007  ax-8 2110  ax-9 2118  ax-ext 2707  ax-nul 5276

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 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-ne 2933  df-ral 3052  df-rab 3416  df-v 3461  df-sbc 3766  df-dif 3929  df-un 3931  df-ss 3943  df-nul 4309  df-if 4501  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-br 5120  df-iota 6483  df-fv 6538  df-ov 7406  df-ring 20193

This theorem is referenced by:  ringgrpd  20200  ringmnd  20201  ring0cl  20225  ringacl  20236  ringabl  20239  ringnegl  20260  ringnegr  20261  ringmneg1  20262  ringmneg2  20263  mulgass2  20267  ringlghm  20270  ringrghm  20271  prdsringd  20279  imasring  20288  dvdsrneg  20328  dvdsr02  20330  unitnegcl  20355  dvrdir  20370  irrednegb  20389  dfrhm2  20432  isrhmd  20446  idrhm  20448  pwsco1rhm  20460  pwsco2rhm  20461  rhmopp  20467  0ringnnzr  20483  c0rhm  20492  c0rnghm  20493  zrrnghm  20494  subrgsubg  20535  cntzsubr  20564  pwsdiagrhm  20565  subrgacs  20758  isabvd  20770  abvneg  20784  abvsubtri  20785  abvtrivd  20790  srng0  20812  idsrngd  20814  lmodfgrp  20824  lmod0vs  20850  lmodvsneg  20861  lmodsubvs  20873  lmodsubdi  20874  lmodsubdir  20875  rmodislmodlem  20884  rmodislmod  20885  lmodvsinv  20992  sralmod  21143  issubrgd  21145  lidlsubg  21182  cnfld0  21353  cnfldneg  21356  cnfldsub  21358  cnsubglem  21381  zringgrp  21411  mulgrhm  21436  chrdvds  21485  chrcong  21486  dvdschrmulg  21487  zncyg  21507  cygznlem3  21528  freshmansdream  21533  zrhpsgnelbas  21552  ip2subdi  21602  asclghm  21841  psrlmod  21918  psrring  21928  mpllsslem  21958  mplsubrg  21963  mplcoe1  21993  mplind  22026  evlslem2  22035  coe1z  22198  coe1subfv  22201  evl1subd  22278  evl1gsumd  22293  matinvgcell  22371  mat0dim0  22403  mat1ghm  22419  dmatsubcl  22434  dmatsgrp  22435  scmataddcl  22452  scmatsubcl  22453  scmatsgrp  22455  scmatsgrp1  22458  scmatghm  22469  mdetralt  22544  mdetero  22546  mdetunilem6  22553  mdetunilem9  22556  mdetuni0  22557  m2detleiblem6  22562  cpmatinvcl  22653  cpmatsubgpmat  22656  mat2pmatghm  22666  pm2mpghm  22752  chmatcl  22764  chpmat0d  22770  chpmat1d  22772  chpdmatlem1  22774  chpdmatlem2  22775  chpscmat  22778  chpscmatgsumbin  22780  chpscmatgsummon  22781  chp0mat  22782  chpidmat  22783  chfacfisf  22790  chfacfscmulgsum  22796  chfacfpmmulgsum  22800  cayhamlem1  22802  cpmadugsumlemF  22812  cpmidgsum2  22815  trggrp  24108  tlmtgp  24132  abvmet  24512  nrgdsdi  24602  nrgdsdir  24603  tngnrg  24611  cnngp  24716  cnfldtgp  24809  cnncvsaddassdemo  25113  cphsubrglem  25127  mdegldg  26021  mdeg0  26025  mdegaddle  26029  deg1add  26058  deg1suble  26062  deg1sub  26063  deg1sublt  26065  ply1nzb  26078  ply1divmo  26091  ply1divex  26092  r1pcl  26114  r1pid  26116  dvdsq1p  26118  dvdsr1p  26119  ply1remlem  26120  ply1rem  26121  idomrootle  26128  ig1peu  26130  reefgim  26410  lgsqrlem1  27307  lgsqrlem2  27308  lgsqrlem3  27309  lgsqrlem4  27310  abvcxp  27576  rmfsupp2  33179  orngsqr  33272  ornglmulle  33273  orngrmulle  33274  ornglmullt  33275  orngrmullt  33276  orngmullt  33277  suborng  33283  isarchiofld  33285  reofld  33305  linds2eq  33342  qsidomlem1  33413  qsidomlem2  33414  qsnzr  33416  mxidlprm  33431  zringfrac  33515  fedgmullem1  33615  ccfldsrarelvec  33658  zrhchr  33951  matunitlindflem1  37586  lfl0  39029  lflsub  39031  lfl0f  39033  lfladdass  39037  lfladd0l  39038  lflnegcl  39039  lflnegl  39040  ldualvsubcl  39120  ldualvsubval  39121  lkrin  39128  erng0g  40959  lclkrlem2m  41484  lcfrlem2  41508  lcdvsubval  41583  mapdpglem30  41667  baerlem3lem1  41672  baerlem5alem1  41673  baerlem5blem1  41674  baerlem5blem2  41677  hdmapinvlem3  41885  hdmapinvlem4  41886  hdmapglem7b  41893  aks6d1c6lem2  42130  aks6d1c6lem3  42131  aks6d1c6isolem2  42134  aks5lem3a  42148  aks5lem7  42159  hbtlem5  43099  mendlmod  43160  lidldomn1  48154  invginvrid  48290  evl1at0  48315  linply1  48317