Theorem ringgrp 20235

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 2737	. . 3 ⊢ (Base‘𝑅) = (Base‘𝑅)
2		eqid 2737	. . 3 ⊢ (mulGrp‘𝑅) = (mulGrp‘𝑅)
3		eqid 2737	. . 3 ⊢ (+g‘𝑅) = (+g‘𝑅)
4		eqid 2737	. . 3 ⊢ (.r‘𝑅) = (.r‘𝑅)
5	1, 2, 3, 4	isring 20234	. 2 ⊢ (𝑅 ∈ Ring ↔ (𝑅 ∈ Grp ∧ (mulGrp‘𝑅) ∈ Mnd ∧ ∀𝑥 ∈ (Base‘𝑅)∀𝑦 ∈ (Base‘𝑅)∀𝑧 ∈ (Base‘𝑅)((𝑥(.r‘𝑅)(𝑦(+g‘𝑅)𝑧)) = ((𝑥(.r‘𝑅)𝑦)(+g‘𝑅)(𝑥(.r‘𝑅)𝑧)) ∧ ((𝑥(+g‘𝑅)𝑦)(.r‘𝑅)𝑧) = ((𝑥(.r‘𝑅)𝑧)(+g‘𝑅)(𝑦(.r‘𝑅)𝑧)))))
6	5	simp1bi 1146	1 ⊢ (𝑅 ∈ Ring → 𝑅 ∈ Grp)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2108  ∀wral 3061  ‘cfv 6561  (class class class)co 7431  Basecbs 17247  +_gcplusg 17297  ._rcmulr 17298  Mndcmnd 18747  Grpcgrp 18951  mulGrpcmgp 20137  Ringcrg 20230

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 2708  ax-nul 5306

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ne 2941  df-ral 3062  df-rab 3437  df-v 3482  df-sbc 3789  df-dif 3954  df-un 3956  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-iota 6514  df-fv 6569  df-ov 7434  df-ring 20232

This theorem is referenced by:  ringgrpd  20239  ringmnd  20240  ring0cl  20264  ringacl  20275  ringabl  20278  ringnegl  20299  ringnegr  20300  ringmneg1  20301  ringmneg2  20302  mulgass2  20306  ringlghm  20309  ringrghm  20310  prdsringd  20318  imasring  20327  dvdsrneg  20370  dvdsr02  20372  unitnegcl  20397  dvrdir  20412  irrednegb  20431  dfrhm2  20474  isrhmd  20488  idrhm  20490  pwsco1rhm  20502  pwsco2rhm  20503  rhmopp  20509  0ringnnzr  20525  c0rhm  20534  c0rnghm  20535  zrrnghm  20536  subrgsubg  20577  cntzsubr  20606  pwsdiagrhm  20607  subrgacs  20801  isabvd  20813  abvneg  20827  abvsubtri  20828  abvtrivd  20833  srng0  20855  idsrngd  20857  lmodfgrp  20867  lmod0vs  20893  lmodvsneg  20904  lmodsubvs  20916  lmodsubdi  20917  lmodsubdir  20918  rmodislmodlem  20927  rmodislmod  20928  lmodvsinv  21035  sralmod  21194  issubrgd  21196  lidlsubg  21233  cnfld0  21405  cnfldneg  21408  cnfldsub  21410  cnsubglem  21433  zringgrp  21463  mulgrhm  21488  chrdvds  21541  chrcong  21542  dvdschrmulg  21543  zncyg  21567  cygznlem3  21588  freshmansdream  21593  zrhpsgnelbas  21612  ip2subdi  21662  asclghm  21903  psrlmod  21980  psrring  21990  mpllsslem  22020  mplsubrg  22025  mplcoe1  22055  mplind  22094  evlslem2  22103  coe1z  22266  coe1subfv  22269  evl1subd  22346  evl1gsumd  22361  matinvgcell  22441  mat0dim0  22473  mat1ghm  22489  dmatsubcl  22504  dmatsgrp  22505  scmataddcl  22522  scmatsubcl  22523  scmatsgrp  22525  scmatsgrp1  22528  scmatghm  22539  mdetralt  22614  mdetero  22616  mdetunilem6  22623  mdetunilem9  22626  mdetuni0  22627  m2detleiblem6  22632  cpmatinvcl  22723  cpmatsubgpmat  22726  mat2pmatghm  22736  pm2mpghm  22822  chmatcl  22834  chpmat0d  22840  chpmat1d  22842  chpdmatlem1  22844  chpdmatlem2  22845  chpscmat  22848  chpscmatgsumbin  22850  chpscmatgsummon  22851  chp0mat  22852  chpidmat  22853  chfacfisf  22860  chfacfscmulgsum  22866  chfacfpmmulgsum  22870  cayhamlem1  22872  cpmadugsumlemF  22882  cpmidgsum2  22885  trggrp  24180  tlmtgp  24204  abvmet  24588  nrgdsdi  24686  nrgdsdir  24687  tngnrg  24695  cnngp  24800  cnfldtgp  24893  cnncvsaddassdemo  25197  cphsubrglem  25211  mdegldg  26105  mdeg0  26109  mdegaddle  26113  deg1add  26142  deg1suble  26146  deg1sub  26147  deg1sublt  26149  ply1nzb  26162  ply1divmo  26175  ply1divex  26176  r1pcl  26198  r1pid  26200  dvdsq1p  26202  dvdsr1p  26203  ply1remlem  26204  ply1rem  26205  idomrootle  26212  ig1peu  26214  reefgim  26494  lgsqrlem1  27390  lgsqrlem2  27391  lgsqrlem3  27392  lgsqrlem4  27393  abvcxp  27659  rmfsupp2  33242  orngsqr  33334  ornglmulle  33335  orngrmulle  33336  ornglmullt  33337  orngrmullt  33338  orngmullt  33339  suborng  33345  isarchiofld  33347  reofld  33372  linds2eq  33409  qsidomlem1  33480  qsidomlem2  33481  qsnzr  33483  mxidlprm  33498  zringfrac  33582  fedgmullem1  33680  ccfldsrarelvec  33721  zrhchr  33975  matunitlindflem1  37623  lfl0  39066  lflsub  39068  lfl0f  39070  lfladdass  39074  lfladd0l  39075  lflnegcl  39076  lflnegl  39077  ldualvsubcl  39157  ldualvsubval  39158  lkrin  39165  erng0g  40996  lclkrlem2m  41521  lcfrlem2  41545  lcdvsubval  41620  mapdpglem30  41704  baerlem3lem1  41709  baerlem5alem1  41710  baerlem5blem1  41711  baerlem5blem2  41714  hdmapinvlem3  41922  hdmapinvlem4  41923  hdmapglem7b  41930  aks6d1c6lem2  42172  aks6d1c6lem3  42173  aks6d1c6isolem2  42176  aks5lem3a  42190  aks5lem7  42201  hbtlem5  43140  mendlmod  43201  lidldomn1  48147  invginvrid  48283  evl1at0  48308  linply1  48310