Theorem ringgrp 20061

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

Syntax hints:   → wi 4   ∧ wa 397   = wceq 1542   ∈ wcel 2107  ∀wral 3062  ‘cfv 6544  (class class class)co 7409  Basecbs 17144  +_gcplusg 17197  ._rcmulr 17198  Mndcmnd 18625  Grpcgrp 18819  mulGrpcmgp 19987  Ringcrg 20056

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 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704  ax-nul 5307

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-ne 2942  df-ral 3063  df-rab 3434  df-v 3477  df-sbc 3779  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-br 5150  df-iota 6496  df-fv 6552  df-ov 7412  df-ring 20058

This theorem is referenced by:  ringgrpd  20065  ringmnd  20066  ring0cl  20084  ringacl  20095  ringabl  20098  ringlz  20107  ringrz  20108  ringnegl  20114  ringnegr  20115  ringmneg1  20116  ringmneg2  20117  ringm2neg  20118  ringsubdi  20119  ringsubdir  20120  mulgass2  20121  ringlghm  20124  ringrghm  20125  prdsringd  20134  imasring  20143  opprring  20161  dvdsrneg  20184  dvdsr02  20186  unitnegcl  20211  dvrdir  20226  irrednegb  20245  dfrhm2  20253  isrhmd  20266  idrhm  20268  pwsco1rhm  20277  pwsco2rhm  20278  rhmopp  20288  0ringnnzr  20302  subrgsubg  20325  cntzsubr  20353  pwsdiagrhm  20354  subrgacs  20416  isabvd  20428  abvneg  20442  abvsubtri  20443  abvtrivd  20448  srng0  20468  idsrngd  20470  lmodfgrp  20480  lmod0vs  20505  lmodvsneg  20516  lmodsubvs  20528  lmodsubdi  20529  lmodsubdir  20530  rmodislmodlem  20539  rmodislmod  20540  rmodislmodOLD  20541  lssvnegcl  20567  lmodvsinv  20647  sralmod  20809  issubrgd  20811  lidlsubg  20838  2idlcpbl  20871  cnfld0  20969  cnfldneg  20971  cnfldsub  20973  cnsubglem  20994  zringgrp  21022  mulgrhm  21047  chrdvds  21080  chrcong  21081  zncyg  21104  cygznlem3  21125  zrhpsgnelbas  21147  ip2subdi  21197  asclghm  21437  psrlmod  21521  psrdi  21526  psrdir  21527  psrring  21531  mpllsslem  21559  mplsubrg  21564  mplcoe1  21592  mplind  21631  evlslem2  21642  mhplss  21698  coe1z  21785  coe1subfv  21788  evl1subd  21861  evl1gsumd  21876  matinvgcell  21937  mat0dim0  21969  mat1ghm  21985  dmatsubcl  22000  dmatsgrp  22001  scmataddcl  22018  scmatsubcl  22019  scmatsgrp  22021  scmatsgrp1  22024  scmatghm  22035  mdetralt  22110  mdetero  22112  mdetunilem6  22119  mdetunilem9  22122  mdetuni0  22123  m2detleiblem6  22128  cpmatinvcl  22219  cpmatsubgpmat  22222  mat2pmatghm  22232  pm2mpghm  22318  chmatcl  22330  chpmat0d  22336  chpmat1d  22338  chpdmatlem1  22340  chpdmatlem2  22341  chpscmat  22344  chpscmatgsumbin  22346  chpscmatgsummon  22347  chp0mat  22348  chpidmat  22349  chfacfisf  22356  chfacfscmulgsum  22362  chfacfpmmulgsum  22366  cayhamlem1  22368  cpmadugsumlemF  22378  cpmidgsum2  22381  trggrp  23676  tlmtgp  23700  abvmet  24084  nrgdsdi  24182  nrgdsdir  24183  tngnrg  24191  cnngp  24296  cnfldtgp  24385  cnncvsaddassdemo  24680  cphsubrglem  24694  mdegldg  25584  mdeg0  25588  mdegaddle  25592  deg1add  25621  deg1suble  25625  deg1sub  25626  deg1sublt  25628  ply1nzb  25640  ply1divmo  25653  ply1divex  25654  r1pcl  25675  r1pid  25677  dvdsq1p  25678  dvdsr1p  25679  ply1remlem  25680  ply1rem  25681  ig1peu  25689  reefgim  25962  lgsqrlem1  26849  lgsqrlem2  26850  lgsqrlem3  26851  lgsqrlem4  26852  abvcxp  27118  dvdschrmulg  32411  freshmansdream  32412  rmfsupp2  32418  orngsqr  32453  ornglmulle  32454  orngrmulle  32455  ornglmullt  32456  orngrmullt  32457  orngmullt  32458  ofldchr  32463  suborng  32464  isarchiofld  32466  reofld  32490  linds2eq  32528  qsidomlem1  32602  qsidomlem2  32603  qsnzr  32605  mxidlprm  32617  fedgmullem1  32745  ccfldsrarelvec  32776  zrhchr  32987  matunitlindflem1  36532  lfl0  37983  lflsub  37985  lfl0f  37987  lfladdass  37991  lfladd0l  37992  lflnegcl  37993  lflnegl  37994  ldualvsubcl  38074  ldualvsubval  38075  lkrin  38082  erng0g  39913  lclkrlem2m  40438  lcfrlem2  40462  lcdvsubval  40537  mapdpglem30  40621  baerlem3lem1  40626  baerlem5alem1  40627  baerlem5blem1  40628  baerlem5blem2  40631  hdmapinvlem3  40839  hdmapinvlem4  40840  hdmapglem7b  40847  hbtlem5  41918  mendlmod  41983  idomrootle  41985  c0rhm  46759  c0rnghm  46760  zrrnghm  46764  lidldomn1  46871  invginvrid  47091  evl1at0  47120  linply1  47122