Theorem ringgrp 20265

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 2740	. . 3 ⊢ (Base‘𝑅) = (Base‘𝑅)
2		eqid 2740	. . 3 ⊢ (mulGrp‘𝑅) = (mulGrp‘𝑅)
3		eqid 2740	. . 3 ⊢ (+g‘𝑅) = (+g‘𝑅)
4		eqid 2740	. . 3 ⊢ (.r‘𝑅) = (.r‘𝑅)
5	1, 2, 3, 4	isring 20264	. 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 1537   ∈ wcel 2108  ∀wral 3067  ‘cfv 6573  (class class class)co 7448  Basecbs 17258  +_gcplusg 17311  ._rcmulr 17312  Mndcmnd 18772  Grpcgrp 18973  mulGrpcmgp 20161  Ringcrg 20260

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711  ax-nul 5324

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-ne 2947  df-ral 3068  df-rab 3444  df-v 3490  df-sbc 3805  df-dif 3979  df-un 3981  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-br 5167  df-iota 6525  df-fv 6581  df-ov 7451  df-ring 20262

This theorem is referenced by:  ringgrpd  20269  ringmnd  20270  ring0cl  20290  ringacl  20301  ringabl  20304  ringnegl  20325  ringnegr  20326  ringmneg1  20327  ringmneg2  20328  mulgass2  20332  ringlghm  20335  ringrghm  20336  prdsringd  20344  imasring  20353  dvdsrneg  20396  dvdsr02  20398  unitnegcl  20423  dvrdir  20438  irrednegb  20457  dfrhm2  20500  isrhmd  20514  idrhm  20516  pwsco1rhm  20528  pwsco2rhm  20529  rhmopp  20535  0ringnnzr  20551  c0rhm  20560  c0rnghm  20561  zrrnghm  20562  subrgsubg  20605  cntzsubr  20634  pwsdiagrhm  20635  subrgacs  20823  isabvd  20835  abvneg  20849  abvsubtri  20850  abvtrivd  20855  srng0  20877  idsrngd  20879  lmodfgrp  20889  lmod0vs  20915  lmodvsneg  20926  lmodsubvs  20938  lmodsubdi  20939  lmodsubdir  20940  rmodislmodlem  20949  rmodislmod  20950  rmodislmodOLD  20951  lmodvsinv  21058  sralmod  21217  issubrgd  21219  lidlsubg  21256  cnfld0  21428  cnfldneg  21431  cnfldsub  21433  cnsubglem  21456  zringgrp  21486  mulgrhm  21511  chrdvds  21564  chrcong  21565  dvdschrmulg  21566  zncyg  21590  cygznlem3  21611  freshmansdream  21616  zrhpsgnelbas  21635  ip2subdi  21685  asclghm  21926  psrlmod  22003  psrring  22013  mpllsslem  22043  mplsubrg  22048  mplcoe1  22078  mplind  22117  evlslem2  22126  coe1z  22287  coe1subfv  22290  evl1subd  22367  evl1gsumd  22382  matinvgcell  22462  mat0dim0  22494  mat1ghm  22510  dmatsubcl  22525  dmatsgrp  22526  scmataddcl  22543  scmatsubcl  22544  scmatsgrp  22546  scmatsgrp1  22549  scmatghm  22560  mdetralt  22635  mdetero  22637  mdetunilem6  22644  mdetunilem9  22647  mdetuni0  22648  m2detleiblem6  22653  cpmatinvcl  22744  cpmatsubgpmat  22747  mat2pmatghm  22757  pm2mpghm  22843  chmatcl  22855  chpmat0d  22861  chpmat1d  22863  chpdmatlem1  22865  chpdmatlem2  22866  chpscmat  22869  chpscmatgsumbin  22871  chpscmatgsummon  22872  chp0mat  22873  chpidmat  22874  chfacfisf  22881  chfacfscmulgsum  22887  chfacfpmmulgsum  22891  cayhamlem1  22893  cpmadugsumlemF  22903  cpmidgsum2  22906  trggrp  24201  tlmtgp  24225  abvmet  24609  nrgdsdi  24707  nrgdsdir  24708  tngnrg  24716  cnngp  24821  cnfldtgp  24912  cnncvsaddassdemo  25216  cphsubrglem  25230  mdegldg  26125  mdeg0  26129  mdegaddle  26133  deg1add  26162  deg1suble  26166  deg1sub  26167  deg1sublt  26169  ply1nzb  26182  ply1divmo  26195  ply1divex  26196  r1pcl  26218  r1pid  26220  dvdsq1p  26222  dvdsr1p  26223  ply1remlem  26224  ply1rem  26225  idomrootle  26232  ig1peu  26234  reefgim  26512  lgsqrlem1  27408  lgsqrlem2  27409  lgsqrlem3  27410  lgsqrlem4  27411  abvcxp  27677  rmfsupp2  33218  orngsqr  33299  ornglmulle  33300  orngrmulle  33301  ornglmullt  33302  orngrmullt  33303  orngmullt  33304  suborng  33310  isarchiofld  33312  reofld  33337  linds2eq  33374  qsidomlem1  33445  qsidomlem2  33446  qsnzr  33448  mxidlprm  33463  zringfrac  33547  fedgmullem1  33642  ccfldsrarelvec  33681  zrhchr  33922  matunitlindflem1  37576  lfl0  39021  lflsub  39023  lfl0f  39025  lfladdass  39029  lfladd0l  39030  lflnegcl  39031  lflnegl  39032  ldualvsubcl  39112  ldualvsubval  39113  lkrin  39120  erng0g  40951  lclkrlem2m  41476  lcfrlem2  41500  lcdvsubval  41575  mapdpglem30  41659  baerlem3lem1  41664  baerlem5alem1  41665  baerlem5blem1  41666  baerlem5blem2  41669  hdmapinvlem3  41877  hdmapinvlem4  41878  hdmapglem7b  41885  aks6d1c6lem2  42128  aks6d1c6lem3  42129  aks6d1c6isolem2  42132  aks5lem3a  42146  aks5lem7  42157  hbtlem5  43085  mendlmod  43150  lidldomn1  47954  invginvrid  48092  evl1at0  48120  linply1  48122