Theorem ringgrp 19355

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 2759	. . 3 ⊢ (Base‘𝑅) = (Base‘𝑅)
2		eqid 2759	. . 3 ⊢ (mulGrp‘𝑅) = (mulGrp‘𝑅)
3		eqid 2759	. . 3 ⊢ (+g‘𝑅) = (+g‘𝑅)
4		eqid 2759	. . 3 ⊢ (.r‘𝑅) = (.r‘𝑅)
5	1, 2, 3, 4	isring 19354	. 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 400   = wceq 1539   ∈ wcel 2112  ∀wral 3068  ‘cfv 6328  (class class class)co 7143  Basecbs 16526  +_gcplusg 16608  ._rcmulr 16609  Mndcmnd 17962  Grpcgrp 18154  mulGrpcmgp 19292  Ringcrg 19350

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2730  ax-nul 5169

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 846  df-3an 1087  df-tru 1542  df-ex 1783  df-nf 1787  df-sb 2071  df-mo 2558  df-eu 2589  df-clab 2737  df-cleq 2751  df-clel 2831  df-nfc 2899  df-ral 3073  df-rex 3074  df-rab 3077  df-v 3409  df-sbc 3694  df-dif 3857  df-un 3859  df-in 3861  df-ss 3871  df-nul 4222  df-sn 4516  df-pr 4518  df-op 4522  df-uni 4792  df-br 5026  df-iota 6287  df-fv 6336  df-ov 7146  df-ring 19352

This theorem is referenced by:  ringgrpd  19359  ringmnd  19360  ring0cl  19375  ringacl  19384  ringcom  19385  ringabl  19386  ringlz  19393  ringrz  19394  ringnegl  19400  rngnegr  19401  ringmneg1  19402  ringmneg2  19403  ringm2neg  19404  ringsubdi  19405  rngsubdir  19406  mulgass2  19407  ringlghm  19410  ringrghm  19411  prdsringd  19418  imasring  19425  opprring  19437  dvdsrneg  19460  dvdsr02  19462  unitnegcl  19487  irrednegb  19517  dfrhm2  19525  isrhmd  19537  idrhm  19539  pwsco1rhm  19546  pwsco2rhm  19547  drnggrp  19563  subrgsubg  19594  cntzsubr  19621  pwsdiagrhm  19622  subrgacs  19632  isabvd  19644  abvneg  19658  abvsubtri  19659  abvtrivd  19664  srng0  19684  idsrngd  19686  lmodfgrp  19696  lmod0vs  19720  lmodvsneg  19731  lmodsubvs  19743  lmodsubdi  19744  lmodsubdir  19745  rmodislmodlem  19754  rmodislmod  19755  lssvnegcl  19781  lmodvsinv  19861  sralmod  20012  issubrngd2  20014  lidlsubg  20041  2idlcpbl  20060  0ringnnzr  20095  cnfld0  20175  cnfldneg  20177  cnfldsub  20179  cnsubglem  20200  zringgrp  20228  mulgrhm  20252  chrdvds  20281  chrcong  20282  zncyg  20301  cygznlem3  20322  zrhpsgnelbas  20344  ip2subdi  20394  asclghm  20630  psrlmod  20714  psrdi  20719  psrdir  20720  psrring  20724  mpllsslem  20750  mplsubrg  20755  mplcoe1  20782  mplind  20816  evlslem2  20827  mhplss  20883  coe1z  20972  coe1subfv  20975  evl1subd  21046  evl1gsumd  21061  matinvgcell  21120  mat0dim0  21152  mat1ghm  21168  dmatsubcl  21183  dmatsgrp  21184  scmataddcl  21201  scmatsubcl  21202  scmatsgrp  21204  scmatsgrp1  21207  scmatghm  21218  mdetralt  21293  mdetero  21295  mdetunilem6  21302  mdetunilem9  21305  mdetuni0  21306  m2detleiblem6  21311  cpmatinvcl  21402  cpmatsubgpmat  21405  mat2pmatghm  21415  pm2mpghm  21501  chmatcl  21513  chpmat0d  21519  chpmat1d  21521  chpdmatlem1  21523  chpdmatlem2  21524  chpscmat  21527  chpscmatgsumbin  21529  chpscmatgsummon  21530  chp0mat  21531  chpidmat  21532  chfacfisf  21539  chfacfscmulgsum  21545  chfacfpmmulgsum  21549  cayhamlem1  21551  cpmadugsumlemF  21561  cpmidgsum2  21564  trggrp  22857  tlmtgp  22881  abvmet  23262  nrgdsdi  23352  nrgdsdir  23353  tngnrg  23361  cnngp  23466  cnfldtgp  23555  cnncvsaddassdemo  23849  cphsubrglem  23863  mdegldg  24751  mdeg0  24755  mdegaddle  24759  deg1add  24788  deg1suble  24792  deg1sub  24793  deg1sublt  24795  ply1nzb  24807  ply1divmo  24820  ply1divex  24821  r1pcl  24842  r1pid  24844  dvdsq1p  24845  dvdsr1p  24846  ply1remlem  24847  ply1rem  24848  ig1peu  24856  reefgim  25129  lgsqrlem1  26014  lgsqrlem2  26015  lgsqrlem3  26016  lgsqrlem4  26017  abvcxp  26283  dvdschrmulg  30994  freshmansdream  30995  dvrdir  30998  rmfsupp2  31003  orngsqr  31014  ornglmulle  31015  orngrmulle  31016  ornglmullt  31017  orngrmullt  31018  orngmullt  31019  ofldchr  31024  suborng  31025  isarchiofld  31027  rhmopp  31029  reofld  31050  linds2eq  31081  qsidomlem1  31134  qsidomlem2  31135  mxidlprm  31146  fedgmullem1  31216  ccfldsrarelvec  31247  zrhchr  31430  matunitlindflem1  35318  lfl0  36626  lflsub  36628  lfl0f  36630  lfladdass  36634  lfladd0l  36635  lflnegcl  36636  lflnegl  36637  ldualvsubcl  36717  ldualvsubval  36718  lkrin  36725  erng0g  38555  lclkrlem2m  39080  lcfrlem2  39104  lcdvsubval  39179  mapdpglem30  39263  baerlem3lem1  39268  baerlem5alem1  39269  baerlem5blem1  39270  baerlem5blem2  39273  hdmapinvlem3  39481  hdmapinvlem4  39482  hdmapglem7b  39489  hbtlem5  40430  mendlmod  40495  idomrootle  40497  c0rhm  44888  c0rnghm  44889  zrrnghm  44893  lidldomn1  44897  invginvrid  45121  evl1at0  45150  linply1  45152