Theorem ringgrp 20147

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 20146	. 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 6511  (class class class)co 7387  Basecbs 17179  +_gcplusg 17220  ._rcmulr 17221  Mndcmnd 18661  Grpcgrp 18865  mulGrpcmgp 20049  Ringcrg 20142

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 5261

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 3406  df-v 3449  df-sbc 3754  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-iota 6464  df-fv 6519  df-ov 7390  df-ring 20144

This theorem is referenced by:  ringgrpd  20151  ringmnd  20152  ring0cl  20176  ringacl  20187  ringabl  20190  ringnegl  20211  ringnegr  20212  ringmneg1  20213  ringmneg2  20214  mulgass2  20218  ringlghm  20221  ringrghm  20222  prdsringd  20230  imasring  20239  dvdsrneg  20279  dvdsr02  20281  unitnegcl  20306  dvrdir  20321  irrednegb  20340  dfrhm2  20383  isrhmd  20397  idrhm  20399  pwsco1rhm  20411  pwsco2rhm  20412  rhmopp  20418  0ringnnzr  20434  c0rhm  20443  c0rnghm  20444  zrrnghm  20445  subrgsubg  20486  cntzsubr  20515  pwsdiagrhm  20516  subrgacs  20709  isabvd  20721  abvneg  20735  abvsubtri  20736  abvtrivd  20741  srng0  20763  idsrngd  20765  lmodfgrp  20775  lmod0vs  20801  lmodvsneg  20812  lmodsubvs  20824  lmodsubdi  20825  lmodsubdir  20826  rmodislmodlem  20835  rmodislmod  20836  lmodvsinv  20943  sralmod  21094  issubrgd  21096  lidlsubg  21133  cnfld0  21304  cnfldneg  21307  cnfldsub  21309  cnsubglem  21332  zringgrp  21362  mulgrhm  21387  chrdvds  21436  chrcong  21437  dvdschrmulg  21438  zncyg  21458  cygznlem3  21479  freshmansdream  21484  zrhpsgnelbas  21503  ip2subdi  21553  asclghm  21792  psrlmod  21869  psrring  21879  mpllsslem  21909  mplsubrg  21914  mplcoe1  21944  mplind  21977  evlslem2  21986  coe1z  22149  coe1subfv  22152  evl1subd  22229  evl1gsumd  22244  matinvgcell  22322  mat0dim0  22354  mat1ghm  22370  dmatsubcl  22385  dmatsgrp  22386  scmataddcl  22403  scmatsubcl  22404  scmatsgrp  22406  scmatsgrp1  22409  scmatghm  22420  mdetralt  22495  mdetero  22497  mdetunilem6  22504  mdetunilem9  22507  mdetuni0  22508  m2detleiblem6  22513  cpmatinvcl  22604  cpmatsubgpmat  22607  mat2pmatghm  22617  pm2mpghm  22703  chmatcl  22715  chpmat0d  22721  chpmat1d  22723  chpdmatlem1  22725  chpdmatlem2  22726  chpscmat  22729  chpscmatgsumbin  22731  chpscmatgsummon  22732  chp0mat  22733  chpidmat  22734  chfacfisf  22741  chfacfscmulgsum  22747  chfacfpmmulgsum  22751  cayhamlem1  22753  cpmadugsumlemF  22763  cpmidgsum2  22766  trggrp  24059  tlmtgp  24083  abvmet  24463  nrgdsdi  24553  nrgdsdir  24554  tngnrg  24562  cnngp  24667  cnfldtgp  24760  cnncvsaddassdemo  25063  cphsubrglem  25077  mdegldg  25971  mdeg0  25975  mdegaddle  25979  deg1add  26008  deg1suble  26012  deg1sub  26013  deg1sublt  26015  ply1nzb  26028  ply1divmo  26041  ply1divex  26042  r1pcl  26064  r1pid  26066  dvdsq1p  26068  dvdsr1p  26069  ply1remlem  26070  ply1rem  26071  idomrootle  26078  ig1peu  26080  reefgim  26360  lgsqrlem1  27257  lgsqrlem2  27258  lgsqrlem3  27259  lgsqrlem4  27260  abvcxp  27526  rmfsupp2  33189  orngsqr  33282  ornglmulle  33283  orngrmulle  33284  ornglmullt  33285  orngrmullt  33286  orngmullt  33287  suborng  33293  isarchiofld  33295  reofld  33315  linds2eq  33352  qsidomlem1  33423  qsidomlem2  33424  qsnzr  33426  mxidlprm  33441  zringfrac  33525  fedgmullem1  33625  ccfldsrarelvec  33666  zrhchr  33964  matunitlindflem1  37610  lfl0  39058  lflsub  39060  lfl0f  39062  lfladdass  39066  lfladd0l  39067  lflnegcl  39068  lflnegl  39069  ldualvsubcl  39149  ldualvsubval  39150  lkrin  39157  erng0g  40988  lclkrlem2m  41513  lcfrlem2  41537  lcdvsubval  41612  mapdpglem30  41696  baerlem3lem1  41701  baerlem5alem1  41702  baerlem5blem1  41703  baerlem5blem2  41706  hdmapinvlem3  41914  hdmapinvlem4  41915  hdmapglem7b  41922  aks6d1c6lem2  42159  aks6d1c6lem3  42160  aks6d1c6isolem2  42163  aks5lem3a  42177  aks5lem7  42188  hbtlem5  43117  mendlmod  43178  lidldomn1  48219  invginvrid  48355  evl1at0  48380  linply1  48382