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

Theorem ringmgp 19601
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 2739 . . 3 (Base‘𝑅) = (Base‘𝑅)
2 ringmgp.g . . 3 𝐺 = (mulGrp‘𝑅)
3 eqid 2739 . . 3 (+g𝑅) = (+g𝑅)
4 eqid 2739 . . 3 (.r𝑅) = (.r𝑅)
51, 2, 3, 4isring 19599 . 2 (𝑅 ∈ Ring ↔ (𝑅 ∈ Grp ∧ 𝐺 ∈ Mnd ∧ ∀𝑥 ∈ (Base‘𝑅)∀𝑦 ∈ (Base‘𝑅)∀𝑧 ∈ (Base‘𝑅)((𝑥(.r𝑅)(𝑦(+g𝑅)𝑧)) = ((𝑥(.r𝑅)𝑦)(+g𝑅)(𝑥(.r𝑅)𝑧)) ∧ ((𝑥(+g𝑅)𝑦)(.r𝑅)𝑧) = ((𝑥(.r𝑅)𝑧)(+g𝑅)(𝑦(.r𝑅)𝑧)))))
65simp2bi 1148 1 (𝑅 ∈ Ring → 𝐺 ∈ Mnd)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399   = wceq 1543  wcel 2112  wral 3064  cfv 6401  (class class class)co 7235  Basecbs 16793  +gcplusg 16835  .rcmulr 16836  Mndcmnd 18206  Grpcgrp 18398  mulGrpcmgp 19537  Ringcrg 19595
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2160  ax-12 2177  ax-ext 2710  ax-nul 5216
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2073  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2818  df-ral 3069  df-rex 3070  df-rab 3073  df-v 3425  df-sbc 3712  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4255  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4837  df-br 5071  df-iota 6359  df-fv 6409  df-ov 7238  df-ring 19597
This theorem is referenced by:  mgpf  19610  ringcl  19612  iscrng2  19614  ringass  19615  ringideu  19616  ringidcl  19619  ringidmlem  19621  ringsrg  19640  unitsubm  19721  dfrhm2  19770  isrhm2d  19781  idrhm  19784  pwsco1rhm  19791  pwsco2rhm  19792  subrgcrng  19837  subrgsubm  19846  issubrg3  19861  cntzsubr  19866  pwsdiagrhm  19867  subrgacs  19877  cnfldexp  20429  expmhm  20465  nn0srg  20466  rge0srg  20467  assamulgscmlem2  20892  psrcrng  20970  mplcoe3  21027  mplcoe5lem  21028  mplcoe5  21029  evlsgsummul  21084  mhppwdeg  21122  ply1moncl  21224  coe1pwmul  21232  ply1coefsupp  21248  ply1coe  21249  gsummoncoe1  21257  lply1binomsc  21260  evls1gsummul  21273  evl1expd  21293  evl1gsummul  21308  evl1scvarpw  21311  evl1scvarpwval  21312  evl1gsummon  21313  ringvcl  21329  mat1mhm  21413  scmatmhm  21463  m1detdiag  21526  mdetdiaglem  21527  m2detleiblem2  21557  mat2pmatmhm  21662  pmatcollpwscmatlem1  21718  mply1topmatcllem  21732  mply1topmatcl  21734  pm2mpghm  21745  pm2mpmhm  21749  monmat2matmon  21753  pm2mp  21754  chpscmatgsumbin  21773  chpscmatgsummon  21774  chfacfscmulcl  21786  chfacfscmul0  21787  chfacfpmmulcl  21790  chfacfpmmul0  21791  chfacfpmmulgsum2  21794  cayhamlem1  21795  cpmadugsumlemB  21803  cpmadugsumlemC  21804  cpmadugsumlemF  21805  cayhamlem2  21813  cayhamlem4  21817  nrgtrg  23620  deg1pw  25050  plypf1  25138  efsubm  25472  amgm  25905  wilthlem2  25983  wilthlem3  25984  dchrelbas3  26151  lgsqrlem2  26260  lgsqrlem3  26261  lgsqrlem4  26262  cntrcrng  31073  psgnid  31115  cnmsgn0g  31164  altgnsg  31167  freshmansdream  31235  frobrhm  31236  znfermltl  31308  ringlsmss  31329  iistmd  31598  pwspjmhmmgpd  40028  pwsexpg  40029  evlsbagval  40034  evlsexpval  40035  mhphf  40044  hbtlem4  40702  idomrootle  40771  isdomn3  40780  mon1psubm  40782  amgm2d  41535  amgm3d  41536  amgm4d  41537  c0rhm  45189  c0rnghm  45190  lidlmsgrp  45203  invginvrid  45422  ply1mulgsumlem4  45449  ply1mulgsum  45450  amgmw2d  46225
  Copyright terms: Public domain W3C validator