Theorem ringgrp 18552

Description: A ring is a group. (Contributed by NM, 15-Sep-2011.)

Assertion

Ref	Expression
ringgrp	|- ( R e. Ring -> R e. Grp )

Proof of Theorem ringgrp

Dummy variables x y z are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		eqid 2622	. . 3 |- ( Base ` R ) = ( Base ` R )
2		eqid 2622	. . 3 |- (mulGrp ` R ) = (mulGrp ` R )
3		eqid 2622	. . 3 |- ( +g ` R ) = ( +g ` R )
4		eqid 2622	. . 3 |- ( .r ` R ) = ( .r ` R )
5	1, 2, 3, 4	isring 18551	. 2 |- ( R e. Ring <-> ( R e. Grp /\ (mulGrp ` R ) e. Mnd /\ A. x e. ( Base ` R ) A. y e. ( Base ` R ) A. z e. ( Base ` R ) ( ( x ( .r ` R ) ( y ( +g ` R ) z ) ) = ( ( x ( .r ` R ) y ) ( +g ` R ) ( x ( .r ` R ) z ) ) /\ ( ( x ( +g ` R ) y ) ( .r ` R ) z ) = ( ( x ( .r ` R ) z ) ( +g ` R ) ( y ( .r ` R ) z ) ) ) ) )
6	5	simp1bi 1076	1 |- ( R e. Ring -> R e. Grp )

Syntax hints:   -> wi 4   /\ wa 384   = wceq 1483   e. wcel 1990   A.wral 2912   ` cfv 5888  (class class class)co 6650   Basecbs 15857   +g cplusg 15941   .rcmulr 15942   Mndcmnd 17294   Grpcgrp 17422  mulGrpcmgp 18489   Ringcrg 18547

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-nul 4789

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-sbc 3436  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-br 4654  df-iota 5851  df-fv 5896  df-ov 6653  df-ring 18549

This theorem is referenced by:  ringmnd  18556  ring0cl  18569  ringacl  18578  ringcom  18579  ringabl  18580  ringlz  18587  ringrz  18588  ringnegl  18594  rngnegr  18595  ringmneg1  18596  ringmneg2  18597  ringm2neg  18598  ringsubdi  18599  rngsubdir  18600  mulgass2  18601  ringlghm  18604  ringrghm  18605  prdsringd  18612  imasring  18619  opprring  18631  dvdsrneg  18654  dvdsr02  18656  unitnegcl  18681  irrednegb  18711  dfrhm2  18717  isrhmd  18729  idrhm  18731  pwsco1rhm  18738  pwsco2rhm  18739  kerf1hrm  18743  drnggrp  18755  subrgsubg  18786  cntzsubr  18812  pwsdiagrhm  18813  isabvd  18820  abvneg  18834  abvsubtri  18835  abvtrivd  18840  srng0  18860  idsrngd  18862  lmodfgrp  18872  lmod0vs  18896  lmodvsneg  18907  lmodsubvs  18919  lmodsubdi  18920  lmodsubdir  18921  rmodislmodlem  18930  rmodislmod  18931  lssvnegcl  18956  lmodvsinv  19036  sralmod  19187  issubrngd2  19189  lidlsubg  19215  2idlcpbl  19234  0ringnnzr  19269  asclghm  19338  psrlmod  19401  psrdi  19406  psrdir  19407  psrring  19411  mpllsslem  19435  mplsubrg  19440  mplcoe1  19465  mplind  19502  evlslem2  19512  evlslem1  19515  coe1z  19633  coe1subfv  19636  evl1subd  19706  evl1gsumd  19721  cnfld0  19770  cnfldneg  19772  cnfldsub  19774  cnsubglem  19795  zringgrp  19823  mulgrhm  19846  chrdvds  19876  chrcong  19877  zncyg  19897  cygznlem3  19918  zrhpsgnelbas  19940  ip2subdi  19989  matinvgcell  20241  mat0dim0  20273  mat1ghm  20289  dmatsubcl  20304  dmatsgrp  20305  scmataddcl  20322  scmatsubcl  20323  scmatsgrp  20325  scmatsgrp1  20328  scmatghm  20339  mdetralt  20414  mdetero  20416  mdetunilem6  20423  mdetunilem9  20426  mdetuni0  20427  m2detleiblem6  20432  cpmatinvcl  20522  cpmatsubgpmat  20525  mat2pmatghm  20535  pm2mpghm  20621  chmatcl  20633  chpmat0d  20639  chpmat1d  20641  chpdmatlem1  20643  chpdmatlem2  20644  chpscmat  20647  chpscmatgsumbin  20649  chpscmatgsummon  20650  chp0mat  20651  chpidmat  20652  chfacfisf  20659  chfacfscmulgsum  20665  chfacfpmmulgsum  20669  cayhamlem1  20671  cpmadugsumlemF  20681  cpmidgsum2  20684  trggrp  21975  tlmtgp  21999  abvmet  22380  nrgdsdi  22469  nrgdsdir  22470  tngnrg  22478  cnngp  22583  cnfldtgp  22672  cnncvsaddassdemo  22963  cphsubrglem  22977  mdegldg  23826  mdeg0  23830  mdegaddle  23834  deg1add  23863  deg1suble  23867  deg1sub  23868  deg1sublt  23870  ply1nzb  23882  ply1divmo  23895  ply1divex  23896  r1pcl  23917  r1pid  23919  dvdsq1p  23920  dvdsr1p  23921  ply1remlem  23922  ply1rem  23923  ig1peu  23931  reefgim  24204  lgsqrlem1  25071  lgsqrlem2  25072  lgsqrlem3  25073  lgsqrlem4  25074  abvcxp  25304  dvrdir  29790  orngsqr  29804  ornglmulle  29805  orngrmulle  29806  ornglmullt  29807  orngrmullt  29808  orngmullt  29809  ofldchr  29814  suborng  29815  isarchiofld  29817  rhmopp  29819  reofld  29840  zrhchr  30020  matunitlindflem1  33405  lfl0  34352  lflsub  34354  lfl0f  34356  lfladdass  34360  lfladd0l  34361  lflnegcl  34362  lflnegl  34363  ldualvsubcl  34443  ldualvsubval  34444  lkrin  34451  erng0g  36282  lclkrlem2m  36808  lcfrlem2  36832  lcdvsubval  36907  mapdpglem30  36991  baerlem3lem1  36996  baerlem5alem1  36997  baerlem5blem1  36998  baerlem5blem2  37001  hdmapinvlem3  37212  hdmapinvlem4  37213  hdmapglem7b  37220  hbtlem5  37698  mendlmod  37763  subrgacs  37770  idomrootle  37773  c0rhm  41912  c0rnghm  41913  zrrnghm  41917  lidldomn1  41921  invginvrid  42148  evl1at0  42179  linply1  42181