MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ringmgp Structured version   Unicode version

Theorem ringmgp 17721
Description: A ring is a monoid under multiplication. (Contributed by Mario Carneiro, 6-Jan-2015.)
Hypothesis
Ref Expression
ringmgp.g  |-  G  =  (mulGrp `  R )
Assertion
Ref Expression
ringmgp  |-  ( R  e.  Ring  ->  G  e. 
Mnd )

Proof of Theorem ringmgp
Dummy variables  x  y  z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eqid 2429 . . 3  |-  ( Base `  R )  =  (
Base `  R )
2 ringmgp.g . . 3  |-  G  =  (mulGrp `  R )
3 eqid 2429 . . 3  |-  ( +g  `  R )  =  ( +g  `  R )
4 eqid 2429 . . 3  |-  ( .r
`  R )  =  ( .r `  R
)
51, 2, 3, 4isring 17719 . 2  |-  ( R  e.  Ring  <->  ( R  e. 
Grp  /\  G  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 ) ) ) ) )
65simp2bi 1021 1  |-  ( R  e.  Ring  ->  G  e. 
Mnd )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 370    = wceq 1437    e. wcel 1870   A.wral 2782   ` cfv 5601  (class class class)co 6305   Basecbs 15084   +g cplusg 15152   .rcmulr 15153   Mndcmnd 16486   Grpcgrp 16620  mulGrpcmgp 17658   Ringcrg 17715
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407  ax-nul 4556
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-eu 2270  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2579  df-ne 2627  df-ral 2787  df-rex 2788  df-rab 2791  df-v 3089  df-sbc 3306  df-dif 3445  df-un 3447  df-in 3449  df-ss 3456  df-nul 3768  df-if 3916  df-sn 4003  df-pr 4005  df-op 4009  df-uni 4223  df-br 4427  df-iota 5565  df-fv 5609  df-ov 6308  df-ring 17717
This theorem is referenced by:  mgpf  17727  ringcl  17729  iscrng2  17731  ringass  17732  ringideu  17733  ringidcl  17736  ringidmlem  17738  ringsrg  17754  unitsubm  17833  dfrhm2  17880  isrhm2d  17891  idrhm  17894  pwsco1rhm  17901  pwsco2rhm  17902  subrgcrng  17947  subrgsubm  17956  issubrg3  17971  cntzsubr  17975  pwsdiagrhm  17976  assamulgscmlem2  18508  psrcrng  18572  mplcoe3  18625  mplcoe5lem  18626  mplcoe5  18627  ply1moncl  18799  coe1pwmul  18807  ply1coefsupp  18823  ply1coe  18824  ply1coeOLD  18825  gsummoncoe1  18833  lply1binomsc  18836  evls1gsummul  18849  evl1expd  18868  evl1gsummul  18883  evl1scvarpw  18886  evl1scvarpwval  18887  evl1gsummon  18888  cnfldexp  18936  expmhm  18970  nn0srg  18971  rge0srg  18972  ringvcl  19354  mat1mhm  19440  scmatmhm  19490  m1detdiag  19553  mdetdiaglem  19554  m2detleiblem2  19584  mat2pmatmhm  19688  pmatcollpwscmatlem1  19744  mply1topmatcllem  19758  mply1topmatcl  19760  pm2mpghm  19771  pm2mpmhm  19775  monmat2matmon  19779  pm2mp  19780  chpscmatgsumbin  19799  chpscmatgsummon  19800  chfacfscmulcl  19812  chfacfscmul0  19813  chfacfpmmulcl  19816  chfacfpmmul0  19817  chfacfpmmulgsum2  19820  cayhamlem1  19821  cpmadugsumlemB  19829  cpmadugsumlemC  19830  cpmadugsumlemF  19831  cayhamlem2  19839  cayhamlem4  19843  nrgtrg  21623  deg1pw  22946  plypf1  23034  efsubm  23365  amgm  23781  wilthlem2  23859  wilthlem3  23860  dchrelbas3  24029  lgsqrlem2  24133  lgsqrlem3  24134  lgsqrlem4  24135  psgnid  28449  iistmd  28547  hbtlem4  35691  subrgacs  35765  idomrootle  35768  isdomn3  35780  mon1psubm  35782  amgm2d  36287  amgm3d  36288  amgm4d  36289  c0rhm  38670  c0rnghm  38671  lidlmsgrp  38684  invginvrid  38912  ply1mulgsumlem4  38941  ply1mulgsum  38942
  Copyright terms: Public domain W3C validator