Theorem ringgrp 20154

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 2730	. . 3 ⊢ (Base‘𝑅) = (Base‘𝑅)
2		eqid 2730	. . 3 ⊢ (mulGrp‘𝑅) = (mulGrp‘𝑅)
3		eqid 2730	. . 3 ⊢ (+g‘𝑅) = (+g‘𝑅)
4		eqid 2730	. . 3 ⊢ (.r‘𝑅) = (.r‘𝑅)
5	1, 2, 3, 4	isring 20153	. 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 3045  ‘cfv 6514  (class class class)co 7390  Basecbs 17186  +_gcplusg 17227  ._rcmulr 17228  Mndcmnd 18668  Grpcgrp 18872  mulGrpcmgp 20056  Ringcrg 20149

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 2702  ax-nul 5264

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 2709  df-cleq 2722  df-clel 2804  df-ne 2927  df-ral 3046  df-rab 3409  df-v 3452  df-sbc 3757  df-dif 3920  df-un 3922  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-iota 6467  df-fv 6522  df-ov 7393  df-ring 20151

This theorem is referenced by:  ringgrpd  20158  ringmnd  20159  ring0cl  20183  ringacl  20194  ringabl  20197  ringnegl  20218  ringnegr  20219  ringmneg1  20220  ringmneg2  20221  mulgass2  20225  ringlghm  20228  ringrghm  20229  prdsringd  20237  imasring  20246  dvdsrneg  20286  dvdsr02  20288  unitnegcl  20313  dvrdir  20328  irrednegb  20347  dfrhm2  20390  isrhmd  20404  idrhm  20406  pwsco1rhm  20418  pwsco2rhm  20419  rhmopp  20425  0ringnnzr  20441  c0rhm  20450  c0rnghm  20451  zrrnghm  20452  subrgsubg  20493  cntzsubr  20522  pwsdiagrhm  20523  subrgacs  20716  isabvd  20728  abvneg  20742  abvsubtri  20743  abvtrivd  20748  srng0  20770  idsrngd  20772  lmodfgrp  20782  lmod0vs  20808  lmodvsneg  20819  lmodsubvs  20831  lmodsubdi  20832  lmodsubdir  20833  rmodislmodlem  20842  rmodislmod  20843  lmodvsinv  20950  sralmod  21101  issubrgd  21103  lidlsubg  21140  cnfld0  21311  cnfldneg  21314  cnfldsub  21316  cnsubglem  21339  zringgrp  21369  mulgrhm  21394  chrdvds  21443  chrcong  21444  dvdschrmulg  21445  zncyg  21465  cygznlem3  21486  freshmansdream  21491  zrhpsgnelbas  21510  ip2subdi  21560  asclghm  21799  psrlmod  21876  psrring  21886  mpllsslem  21916  mplsubrg  21921  mplcoe1  21951  mplind  21984  evlslem2  21993  coe1z  22156  coe1subfv  22159  evl1subd  22236  evl1gsumd  22251  matinvgcell  22329  mat0dim0  22361  mat1ghm  22377  dmatsubcl  22392  dmatsgrp  22393  scmataddcl  22410  scmatsubcl  22411  scmatsgrp  22413  scmatsgrp1  22416  scmatghm  22427  mdetralt  22502  mdetero  22504  mdetunilem6  22511  mdetunilem9  22514  mdetuni0  22515  m2detleiblem6  22520  cpmatinvcl  22611  cpmatsubgpmat  22614  mat2pmatghm  22624  pm2mpghm  22710  chmatcl  22722  chpmat0d  22728  chpmat1d  22730  chpdmatlem1  22732  chpdmatlem2  22733  chpscmat  22736  chpscmatgsumbin  22738  chpscmatgsummon  22739  chp0mat  22740  chpidmat  22741  chfacfisf  22748  chfacfscmulgsum  22754  chfacfpmmulgsum  22758  cayhamlem1  22760  cpmadugsumlemF  22770  cpmidgsum2  22773  trggrp  24066  tlmtgp  24090  abvmet  24470  nrgdsdi  24560  nrgdsdir  24561  tngnrg  24569  cnngp  24674  cnfldtgp  24767  cnncvsaddassdemo  25070  cphsubrglem  25084  mdegldg  25978  mdeg0  25982  mdegaddle  25986  deg1add  26015  deg1suble  26019  deg1sub  26020  deg1sublt  26022  ply1nzb  26035  ply1divmo  26048  ply1divex  26049  r1pcl  26071  r1pid  26073  dvdsq1p  26075  dvdsr1p  26076  ply1remlem  26077  ply1rem  26078  idomrootle  26085  ig1peu  26087  reefgim  26367  lgsqrlem1  27264  lgsqrlem2  27265  lgsqrlem3  27266  lgsqrlem4  27267  abvcxp  27533  rmfsupp2  33196  orngsqr  33289  ornglmulle  33290  orngrmulle  33291  ornglmullt  33292  orngrmullt  33293  orngmullt  33294  suborng  33300  isarchiofld  33302  reofld  33322  linds2eq  33359  qsidomlem1  33430  qsidomlem2  33431  qsnzr  33433  mxidlprm  33448  zringfrac  33532  fedgmullem1  33632  ccfldsrarelvec  33673  zrhchr  33971  matunitlindflem1  37617  lfl0  39065  lflsub  39067  lfl0f  39069  lfladdass  39073  lfladd0l  39074  lflnegcl  39075  lflnegl  39076  ldualvsubcl  39156  ldualvsubval  39157  lkrin  39164  erng0g  40995  lclkrlem2m  41520  lcfrlem2  41544  lcdvsubval  41619  mapdpglem30  41703  baerlem3lem1  41708  baerlem5alem1  41709  baerlem5blem1  41710  baerlem5blem2  41713  hdmapinvlem3  41921  hdmapinvlem4  41922  hdmapglem7b  41929  aks6d1c6lem2  42166  aks6d1c6lem3  42167  aks6d1c6isolem2  42170  aks5lem3a  42184  aks5lem7  42195  hbtlem5  43124  mendlmod  43185  lidldomn1  48223  invginvrid  48359  evl1at0  48384  linply1  48386