Theorem ringgrp 20470

Description: A ring is a group. (Contributed by Steve Rodriguez, 9-Sep-2007.) (Revised 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 2760	. . 3 ⊢ (Base‘𝑅) = (Base‘𝑅)
2		eqid 2760	. . 3 ⊢ (mulGrp‘𝑅) = (mulGrp‘𝑅)
3		eqid 2760	. . 3 ⊢ (+g‘𝑅) = (+g‘𝑅)
4		eqid 2760	. . 3 ⊢ (.r‘𝑅) = (.r‘𝑅)
5	1, 2, 3, 4	isring 20469	. 2 ⊢ (𝑅 ∈ Ring ↔ (𝑅 ∈ Grp ∧ (mulGrp‘𝑅) ∈ Mnd ∧ ∀𝑥 ∈ (Base‘𝑅)∀𝑦 ∈ (Base‘𝑅)∀𝑧 ∈ (Base‘𝑅)((𝑥(.r‘𝑅)(𝑦(+g‘𝑅)𝑧)) = ((𝑥(.r‘𝑅)𝑦)(+g‘𝑅)(𝑥(.r‘𝑅)𝑧)) ∧ ((𝑥(+g‘𝑅)𝑦)(.r‘𝑅)𝑧) = ((𝑥(.r‘𝑅)𝑧)(+g‘𝑅)(𝑦(.r‘𝑅)𝑧)))))
6	5	simp1bi 1163	1 ⊢ (𝑅 ∈ Ring → 𝑅 ∈ Grp)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1569   ∈ wcel 2144  ∀wral 3076  ‘cfv 6539  (class class class)co 7421  Basecbs 17393  +_gcplusg 17434  ._rcmulr 17435  Mndcmnd 18929  Grpcgrp 19150  mulGrpcmgp 20366  Ringcrg 20465

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-nul 5259

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ne 2956  df-ral 3077  df-rab 3413  df-v 3452  df-sbc 3739  df-ss 3896  df-dif 4047  df-un 4151  df-nul 4279  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-br 5103  df-iota 6494  df-fv 6547  df-ov 7424  df-ring 20467

This theorem is used by:  ringbn0  20474  ringgrpd  20475  ringmnd  20476  ring0cl  20502  ringacl  20513  ringabl  20516  ringnegl  20539  ringnegr  20540  ringmneg1  20541  ringmneg2  20542  mulgass2  20546  ringlghm  20549  ringrghm  20550  prdsringd  20556  imasring  20566  dvdsrneg  20606  dvdsr02  20608  unitnegcl  20633  dvrdir  20648  irrednegb  20667  dfrhm2  20710  isrhmd  20728  idrhm  20731  pwsco1rhm  20747  pwsco2rhm  20748  rhmopp  20765  0ringnnzr  20782  c0rhm  20792  c0rnghm  20793  zrrnghm  20794  subrgsubg  20835  cntzsubr  20864  pwsdiagrhm  20865  subrgacs  21063  isabvd  21075  abvneg  21089  abvsubtri  21090  abvtrivd  21095  srng0  21117  idsrngd  21119  orngsqr  21129  ornglmulle  21130  orngrmulle  21131  ornglmullt  21132  orngrmullt  21133  orngmullt  21134  suborng  21139  lmodfgrp  21150  lmod0vs  21176  lmodvsneg  21187  lmodsubvs  21199  lmodsubdi  21200  lmodsubdir  21201  rmodislmodlem  21210  rmodislmod  21211  lmodvsinv  21317  sralmod  21468  issubrgd  21470  lidlsubg  21508  qsidomlem1  21642  qsidomlem2  21643  qsnzr  21645  cnfld0  21708  cnfldneg  21710  cnfldsub  21712  cnsubglem  21728  zringgrp  21764  mulgrhm  21789  chrdvds  21838  chrcong  21839  dvdschrmulg  21840  zncyg  21860  cygznlem3  21881  freshmansdream  21886  zrhpsgnelbas  21906  ip2subdi  21956  asclghm  22196  psrlmod  22273  mpllsslem  22313  mplsubrg  22318  mplcoe1  22352  mplind  22385  evlslem2  22394  coe1z  22588  coe1subfv  22591  evl1subd  22666  evl1gsumd  22681  matinvgcell  22756  mat0dim0  22788  mat1ghm  22804  dmatsubcl  22819  dmatsgrp  22820  scmataddcl  22837  scmatsubcl  22838  scmatsgrp  22840  scmatsgrp1  22843  scmatghm  22854  mdetralt  22929  mdetero  22931  mdetunilem6  22938  mdetunilem9  22941  mdetuni0  22942  m2detleiblem6  22947  matunitlindflem1  23000  cpmatinvcl  23041  cpmatsubgpmat  23044  mat2pmatghm  23054  pm2mpghm  23140  chmatcl  23152  chpmat0d  23158  chpmat1d  23160  chpdmatlem1  23162  chpdmatlem2  23163  chpscmat  23166  chpscmatgsumbin  23168  chpscmatgsummon  23169  chp0mat  23170  chpidmat  23171  chfacfisf  23178  chfacfscmulgsum  23184  chfacfpmmulgsum  23188  cayhamlem1  23190  cpmadugsumlemF  23200  cpmidgsum2  23203  trggrp  24497  tlmtgp  24521  abvmet  24900  nrgdsdi  24990  nrgdsdir  24991  tngnrg  24999  cnngp  25104  cnfldtgp  25196  cnncvsaddassdemo  25490  cphsubrglem  25504  mdegldg  26390  mdeg0  26394  mdegaddle  26398  deg1add  26427  deg1suble  26431  deg1sub  26432  deg1sublt  26434  ply1nzb  26447  ply1divmo  26460  ply1divex  26461  r1pcl  26483  r1pid  26485  dvdsq1p  26487  dvdsr1p  26488  ply1remlem  26489  ply1rem  26490  idomrootle  26497  ig1peu  26499  reefgim  26783  lgsqrlem1  27679  lgsqrlem2  27680  lgsqrlem3  27681  lgsqrlem4  27682  abvcxp  27948  isarchiofld  33807  rmfsupp2  33845  reofld  33951  linds2eq  33983  mxidlprm  34042  zringfrac  34133  esplyind  34254  vietadeg1  34257  fedgmullem1  34308  ccfldsrarelvec  34350  zrhchr  34653  lfl0  40216  lflsub  40218  lfl0f  40220  lfladdass  40224  lfladd0l  40225  lflnegcl  40226  lflnegl  40227  ldualvsubcl  40307  ldualvsubval  40308  lkrin  40315  erng0g  42145  lclkrlem2m  42670  lcfrlem2  42694  lcdvsubval  42769  mapdpglem30  42853  baerlem3lem1  42858  baerlem5alem1  42859  baerlem5blem1  42860  baerlem5blem2  42863  hdmapinvlem3  43071  hdmapinvlem4  43072  hdmapglem7b  43079  aks6d1c6lem2  43315  aks6d1c6lem3  43316  aks6d1c6isolem2  43319  aks5lem3a  43333  aks5lem7  43344  hbtlem5  44224  mendlmod  44285  lidldomn1  49422  invginvrid  49573  evl1at0  49597  linply1  49599