Theorem ringgrp 19703

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1539   ∈ wcel 2108  ∀wral 3063  ‘cfv 6418  (class class class)co 7255  Basecbs 16840  +_gcplusg 16888  ._rcmulr 16889  Mndcmnd 18300  Grpcgrp 18492  mulGrpcmgp 19635  Ringcrg 19698

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-nul 5225

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-ral 3068  df-rex 3069  df-rab 3072  df-v 3424  df-sbc 3712  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4837  df-br 5071  df-iota 6376  df-fv 6426  df-ov 7258  df-ring 19700

This theorem is referenced by:  ringgrpd  19707  ringmnd  19708  ring0cl  19723  ringacl  19732  ringcom  19733  ringabl  19734  ringlz  19741  ringrz  19742  ringnegl  19748  rngnegr  19749  ringmneg1  19750  ringmneg2  19751  ringm2neg  19752  ringsubdi  19753  rngsubdir  19754  mulgass2  19755  ringlghm  19758  ringrghm  19759  prdsringd  19766  imasring  19773  opprring  19788  dvdsrneg  19811  dvdsr02  19813  unitnegcl  19838  irrednegb  19868  dfrhm2  19876  isrhmd  19888  idrhm  19890  pwsco1rhm  19897  pwsco2rhm  19898  drnggrp  19914  subrgsubg  19945  cntzsubr  19972  pwsdiagrhm  19973  subrgacs  19983  isabvd  19995  abvneg  20009  abvsubtri  20010  abvtrivd  20015  srng0  20035  idsrngd  20037  lmodfgrp  20047  lmod0vs  20071  lmodvsneg  20082  lmodsubvs  20094  lmodsubdi  20095  lmodsubdir  20096  rmodislmodlem  20105  rmodislmod  20106  rmodislmodOLD  20107  lssvnegcl  20133  lmodvsinv  20213  sralmod  20370  issubrngd2  20372  lidlsubg  20399  2idlcpbl  20418  0ringnnzr  20453  cnfld0  20534  cnfldneg  20536  cnfldsub  20538  cnsubglem  20559  zringgrp  20587  mulgrhm  20611  chrdvds  20644  chrcong  20645  zncyg  20668  cygznlem3  20689  zrhpsgnelbas  20711  ip2subdi  20761  asclghm  20997  psrlmod  21080  psrdi  21085  psrdir  21086  psrring  21090  mpllsslem  21116  mplsubrg  21121  mplcoe1  21148  mplind  21188  evlslem2  21199  mhplss  21255  coe1z  21344  coe1subfv  21347  evl1subd  21418  evl1gsumd  21433  matinvgcell  21492  mat0dim0  21524  mat1ghm  21540  dmatsubcl  21555  dmatsgrp  21556  scmataddcl  21573  scmatsubcl  21574  scmatsgrp  21576  scmatsgrp1  21579  scmatghm  21590  mdetralt  21665  mdetero  21667  mdetunilem6  21674  mdetunilem9  21677  mdetuni0  21678  m2detleiblem6  21683  cpmatinvcl  21774  cpmatsubgpmat  21777  mat2pmatghm  21787  pm2mpghm  21873  chmatcl  21885  chpmat0d  21891  chpmat1d  21893  chpdmatlem1  21895  chpdmatlem2  21896  chpscmat  21899  chpscmatgsumbin  21901  chpscmatgsummon  21902  chp0mat  21903  chpidmat  21904  chfacfisf  21911  chfacfscmulgsum  21917  chfacfpmmulgsum  21921  cayhamlem1  21923  cpmadugsumlemF  21933  cpmidgsum2  21936  trggrp  23231  tlmtgp  23255  abvmet  23637  nrgdsdi  23735  nrgdsdir  23736  tngnrg  23744  cnngp  23849  cnfldtgp  23938  cnncvsaddassdemo  24232  cphsubrglem  24246  mdegldg  25136  mdeg0  25140  mdegaddle  25144  deg1add  25173  deg1suble  25177  deg1sub  25178  deg1sublt  25180  ply1nzb  25192  ply1divmo  25205  ply1divex  25206  r1pcl  25227  r1pid  25229  dvdsq1p  25230  dvdsr1p  25231  ply1remlem  25232  ply1rem  25233  ig1peu  25241  reefgim  25514  lgsqrlem1  26399  lgsqrlem2  26400  lgsqrlem3  26401  lgsqrlem4  26402  abvcxp  26668  dvdschrmulg  31385  freshmansdream  31386  dvrdir  31389  rmfsupp2  31394  orngsqr  31405  ornglmulle  31406  orngrmulle  31407  ornglmullt  31408  orngrmullt  31409  orngmullt  31410  ofldchr  31415  suborng  31416  isarchiofld  31418  rhmopp  31420  reofld  31446  linds2eq  31477  qsidomlem1  31530  qsidomlem2  31531  mxidlprm  31542  fedgmullem1  31612  ccfldsrarelvec  31643  zrhchr  31826  matunitlindflem1  35700  lfl0  37006  lflsub  37008  lfl0f  37010  lfladdass  37014  lfladd0l  37015  lflnegcl  37016  lflnegl  37017  ldualvsubcl  37097  ldualvsubval  37098  lkrin  37105  erng0g  38935  lclkrlem2m  39460  lcfrlem2  39484  lcdvsubval  39559  mapdpglem30  39643  baerlem3lem1  39648  baerlem5alem1  39649  baerlem5blem1  39650  baerlem5blem2  39653  hdmapinvlem3  39861  hdmapinvlem4  39862  hdmapglem7b  39869  hbtlem5  40869  mendlmod  40934  idomrootle  40936  c0rhm  45358  c0rnghm  45359  zrrnghm  45363  lidldomn1  45367  invginvrid  45591  evl1at0  45620  linply1  45622