Theorem ringgrp 19302

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

Syntax hints:   → wi 4   ∧ wa 398   = wceq 1537   ∈ wcel 2114  ∀wral 3138  ‘cfv 6355  (class class class)co 7156  Basecbs 16483  +_gcplusg 16565  ._rcmulr 16566  Mndcmnd 17911  Grpcgrp 18103  mulGrpcmgp 19239  Ringcrg 19297

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-nul 5210

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3496  df-sbc 3773  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4839  df-br 5067  df-iota 6314  df-fv 6363  df-ov 7159  df-ring 19299

This theorem is referenced by:  ringmnd  19306  ring0cl  19319  ringacl  19328  ringcom  19329  ringabl  19330  ringlz  19337  ringrz  19338  ringnegl  19344  rngnegr  19345  ringmneg1  19346  ringmneg2  19347  ringm2neg  19348  ringsubdi  19349  rngsubdir  19350  mulgass2  19351  ringlghm  19354  ringrghm  19355  prdsringd  19362  imasring  19369  opprring  19381  dvdsrneg  19404  dvdsr02  19406  unitnegcl  19431  irrednegb  19461  dfrhm2  19469  isrhmd  19481  idrhm  19483  pwsco1rhm  19490  pwsco2rhm  19491  kerf1hrmOLD  19498  drnggrp  19510  subrgsubg  19541  cntzsubr  19568  pwsdiagrhm  19569  subrgacs  19579  isabvd  19591  abvneg  19605  abvsubtri  19606  abvtrivd  19611  srng0  19631  idsrngd  19633  lmodfgrp  19643  lmod0vs  19667  lmodvsneg  19678  lmodsubvs  19690  lmodsubdi  19691  lmodsubdir  19692  rmodislmodlem  19701  rmodislmod  19702  lssvnegcl  19728  lmodvsinv  19808  sralmod  19959  issubrngd2  19961  lidlsubg  19988  2idlcpbl  20007  0ringnnzr  20042  asclghm  20112  psrlmod  20181  psrdi  20186  psrdir  20187  psrring  20191  mpllsslem  20215  mplsubrg  20220  mplcoe1  20246  mplind  20282  evlslem2  20292  evlslem1  20295  mhplss  20342  coe1z  20431  coe1subfv  20434  evl1subd  20505  evl1gsumd  20520  cnfld0  20569  cnfldneg  20571  cnfldsub  20573  cnsubglem  20594  zringgrp  20622  mulgrhm  20645  chrdvds  20675  chrcong  20676  zncyg  20695  cygznlem3  20716  zrhpsgnelbas  20738  ip2subdi  20788  matinvgcell  21044  mat0dim0  21076  mat1ghm  21092  dmatsubcl  21107  dmatsgrp  21108  scmataddcl  21125  scmatsubcl  21126  scmatsgrp  21128  scmatsgrp1  21131  scmatghm  21142  mdetralt  21217  mdetero  21219  mdetunilem6  21226  mdetunilem9  21229  mdetuni0  21230  m2detleiblem6  21235  cpmatinvcl  21325  cpmatsubgpmat  21328  mat2pmatghm  21338  pm2mpghm  21424  chmatcl  21436  chpmat0d  21442  chpmat1d  21444  chpdmatlem1  21446  chpdmatlem2  21447  chpscmat  21450  chpscmatgsumbin  21452  chpscmatgsummon  21453  chp0mat  21454  chpidmat  21455  chfacfisf  21462  chfacfscmulgsum  21468  chfacfpmmulgsum  21472  cayhamlem1  21474  cpmadugsumlemF  21484  cpmidgsum2  21487  trggrp  22780  tlmtgp  22804  abvmet  23185  nrgdsdi  23274  nrgdsdir  23275  tngnrg  23283  cnngp  23388  cnfldtgp  23477  cnncvsaddassdemo  23767  cphsubrglem  23781  mdegldg  24660  mdeg0  24664  mdegaddle  24668  deg1add  24697  deg1suble  24701  deg1sub  24702  deg1sublt  24704  ply1nzb  24716  ply1divmo  24729  ply1divex  24730  r1pcl  24751  r1pid  24753  dvdsq1p  24754  dvdsr1p  24755  ply1remlem  24756  ply1rem  24757  ig1peu  24765  reefgim  25038  lgsqrlem1  25922  lgsqrlem2  25923  lgsqrlem3  25924  lgsqrlem4  25925  abvcxp  26191  dvdschrmulg  30858  freshmansdream  30859  dvrdir  30861  rmfsupp2  30866  orngsqr  30877  ornglmulle  30878  orngrmulle  30879  ornglmullt  30880  orngrmullt  30881  orngmullt  30882  ofldchr  30887  suborng  30888  isarchiofld  30890  rhmopp  30892  reofld  30913  linds2eq  30941  qsidomlem1  30965  qsidomlem2  30966  mxidlprm  30977  fedgmullem1  31025  ccfldsrarelvec  31056  zrhchr  31217  matunitlindflem1  34903  lfl0  36216  lflsub  36218  lfl0f  36220  lfladdass  36224  lfladd0l  36225  lflnegcl  36226  lflnegl  36227  ldualvsubcl  36307  ldualvsubval  36308  lkrin  36315  erng0g  38145  lclkrlem2m  38670  lcfrlem2  38694  lcdvsubval  38769  mapdpglem30  38853  baerlem3lem1  38858  baerlem5alem1  38859  baerlem5blem1  38860  baerlem5blem2  38863  hdmapinvlem3  39071  hdmapinvlem4  39072  hdmapglem7b  39079  hbtlem5  39748  mendlmod  39813  idomrootle  39815  c0rhm  44203  c0rnghm  44204  zrrnghm  44208  lidldomn1  44212  invginvrid  44435  evl1at0  44465  linply1  44467