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

Theorem ringmgp 19977
Description: A ring is a monoid under multiplication. (Contributed by Mario Carneiro, 6-Jan-2015.)
Hypothesis
Ref Expression
ringmgp.g 𝐺 = (mulGrp‘𝑅)
Assertion
Ref Expression
ringmgp (𝑅 ∈ Ring → 𝐺 ∈ Mnd)

Proof of Theorem ringmgp
Dummy variables 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eqid 2737 . . 3 (Base‘𝑅) = (Base‘𝑅)
2 ringmgp.g . . 3 𝐺 = (mulGrp‘𝑅)
3 eqid 2737 . . 3 (+g𝑅) = (+g𝑅)
4 eqid 2737 . . 3 (.r𝑅) = (.r𝑅)
51, 2, 3, 4isring 19975 . 2 (𝑅 ∈ Ring ↔ (𝑅 ∈ Grp ∧ 𝐺 ∈ Mnd ∧ ∀𝑥 ∈ (Base‘𝑅)∀𝑦 ∈ (Base‘𝑅)∀𝑧 ∈ (Base‘𝑅)((𝑥(.r𝑅)(𝑦(+g𝑅)𝑧)) = ((𝑥(.r𝑅)𝑦)(+g𝑅)(𝑥(.r𝑅)𝑧)) ∧ ((𝑥(+g𝑅)𝑦)(.r𝑅)𝑧) = ((𝑥(.r𝑅)𝑧)(+g𝑅)(𝑦(.r𝑅)𝑧)))))
65simp2bi 1147 1 (𝑅 ∈ Ring → 𝐺 ∈ Mnd)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397   = wceq 1542  wcel 2107  wral 3065  cfv 6501  (class class class)co 7362  Basecbs 17090  +gcplusg 17140  .rcmulr 17141  Mndcmnd 18563  Grpcgrp 18755  mulGrpcmgp 19903  Ringcrg 19971
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 2708  ax-nul 5268
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 2715  df-cleq 2729  df-clel 2815  df-ne 2945  df-ral 3066  df-rab 3411  df-v 3450  df-sbc 3745  df-dif 3918  df-un 3920  df-in 3922  df-ss 3932  df-nul 4288  df-if 4492  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4871  df-br 5111  df-iota 6453  df-fv 6509  df-ov 7365  df-ring 19973
This theorem is referenced by:  mgpf  19986  ringcl  19988  iscrng2  19990  ringass  19991  ringideu  19992  ringidcl  19996  ringidmlem  19998  ringsrg  20020  pwspjmhmmgpd  20050  pwsexpg  20051  unitsubm  20106  dfrhm2  20157  isrhm2d  20169  idrhm  20172  pwsco1rhm  20181  pwsco2rhm  20182  subrgcrng  20242  subrgsubm  20251  issubrg3  20266  cntzsubr  20271  pwsdiagrhm  20272  subrgacs  20283  cnfldexp  20846  expmhm  20882  nn0srg  20883  rge0srg  20884  assamulgscmlem2  21319  psrcrng  21398  mplcoe3  21455  mplcoe5lem  21456  mplcoe5  21457  evlsgsummul  21518  mhppwdeg  21556  ply1moncl  21658  coe1pwmul  21666  ply1coefsupp  21682  ply1coe  21683  gsummoncoe1  21691  lply1binomsc  21694  evls1gsummul  21707  evl1expd  21727  evl1gsummul  21742  evl1scvarpw  21745  evl1scvarpwval  21746  evl1gsummon  21747  ringvcl  21763  mat1mhm  21849  scmatmhm  21899  m1detdiag  21962  mdetdiaglem  21963  m2detleiblem2  21993  mat2pmatmhm  22098  pmatcollpwscmatlem1  22154  mply1topmatcllem  22168  mply1topmatcl  22170  pm2mpghm  22181  pm2mpmhm  22185  monmat2matmon  22189  pm2mp  22190  chpscmatgsumbin  22209  chpscmatgsummon  22210  chfacfscmulcl  22222  chfacfscmul0  22223  chfacfpmmulcl  22226  chfacfpmmul0  22227  chfacfpmmulgsum2  22230  cayhamlem1  22231  cpmadugsumlemB  22239  cpmadugsumlemC  22240  cpmadugsumlemF  22241  cayhamlem2  22249  cayhamlem4  22253  nrgtrg  24070  deg1pw  25501  plypf1  25589  efsubm  25923  amgm  26356  wilthlem2  26434  wilthlem3  26435  dchrelbas3  26602  lgsqrlem2  26711  lgsqrlem3  26712  lgsqrlem4  26713  cntrcrng  31946  psgnid  31988  cnmsgn0g  32037  altgnsg  32040  freshmansdream  32109  frobrhm  32110  fermltlchr  32194  znfermltl  32195  ringlsmss  32216  evls1fpws  32311  iistmd  32523  evlsbagval  40777  evlsexpval  40778  mhphf  40800  hbtlem4  41482  idomrootle  41551  isdomn3  41560  mon1psubm  41562  amgm2d  42545  amgm3d  42546  amgm4d  42547  c0rhm  46284  c0rnghm  46285  lidlmsgrp  46298  invginvrid  46517  ply1mulgsumlem4  46544  ply1mulgsum  46545  amgmw2d  47325
  Copyright terms: Public domain W3C validator