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

Theorem ringmgp 19232
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 2818 . . 3 (Base‘𝑅) = (Base‘𝑅)
2 ringmgp.g . . 3 𝐺 = (mulGrp‘𝑅)
3 eqid 2818 . . 3 (+g𝑅) = (+g𝑅)
4 eqid 2818 . . 3 (.r𝑅) = (.r𝑅)
51, 2, 3, 4isring 19230 . 2 (𝑅 ∈ Ring ↔ (𝑅 ∈ Grp ∧ 𝐺 ∈ Mnd ∧ ∀𝑥 ∈ (Base‘𝑅)∀𝑦 ∈ (Base‘𝑅)∀𝑧 ∈ (Base‘𝑅)((𝑥(.r𝑅)(𝑦(+g𝑅)𝑧)) = ((𝑥(.r𝑅)𝑦)(+g𝑅)(𝑥(.r𝑅)𝑧)) ∧ ((𝑥(+g𝑅)𝑦)(.r𝑅)𝑧) = ((𝑥(.r𝑅)𝑧)(+g𝑅)(𝑦(.r𝑅)𝑧)))))
65simp2bi 1138 1 (𝑅 ∈ Ring → 𝐺 ∈ Mnd)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396   = wceq 1528  wcel 2105  wral 3135  cfv 6348  (class class class)co 7145  Basecbs 16471  +gcplusg 16553  .rcmulr 16554  Mndcmnd 17899  Grpcgrp 18041  mulGrpcmgp 19168  Ringcrg 19226
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790  ax-nul 5201
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-mo 2615  df-eu 2647  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-ral 3140  df-rex 3141  df-rab 3144  df-v 3494  df-sbc 3770  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-nul 4289  df-if 4464  df-sn 4558  df-pr 4560  df-op 4564  df-uni 4831  df-br 5058  df-iota 6307  df-fv 6356  df-ov 7148  df-ring 19228
This theorem is referenced by:  mgpf  19238  ringcl  19240  iscrng2  19242  ringass  19243  ringideu  19244  ringidcl  19247  ringidmlem  19249  ringsrg  19268  unitsubm  19349  dfrhm2  19398  isrhm2d  19409  idrhm  19412  pwsco1rhm  19419  pwsco2rhm  19420  subrgcrng  19468  subrgsubm  19477  issubrg3  19492  cntzsubr  19497  pwsdiagrhm  19498  subrgacs  19508  assamulgscmlem2  20057  psrcrng  20121  mplcoe3  20175  mplcoe5lem  20176  mplcoe5  20177  evlsgsummul  20233  ply1moncl  20367  coe1pwmul  20375  ply1coefsupp  20391  ply1coe  20392  gsummoncoe1  20400  lply1binomsc  20403  evls1gsummul  20416  evl1expd  20436  evl1gsummul  20451  evl1scvarpw  20454  evl1scvarpwval  20455  evl1gsummon  20456  cnfldexp  20506  expmhm  20542  nn0srg  20543  rge0srg  20544  ringvcl  20937  mat1mhm  21021  scmatmhm  21071  m1detdiag  21134  mdetdiaglem  21135  m2detleiblem2  21165  mat2pmatmhm  21269  pmatcollpwscmatlem1  21325  mply1topmatcllem  21339  mply1topmatcl  21341  pm2mpghm  21352  pm2mpmhm  21356  monmat2matmon  21360  pm2mp  21361  chpscmatgsumbin  21380  chpscmatgsummon  21381  chfacfscmulcl  21393  chfacfscmul0  21394  chfacfpmmulcl  21397  chfacfpmmul0  21398  chfacfpmmulgsum2  21401  cayhamlem1  21402  cpmadugsumlemB  21410  cpmadugsumlemC  21411  cpmadugsumlemF  21412  cayhamlem2  21420  cayhamlem4  21424  nrgtrg  23226  deg1pw  24641  plypf1  24729  efsubm  25062  amgm  25495  wilthlem2  25573  wilthlem3  25574  dchrelbas3  25741  lgsqrlem2  25850  lgsqrlem3  25851  lgsqrlem4  25852  cntrcrng  30624  psgnid  30666  cnmsgn0g  30715  altgnsg  30718  freshmansdream  30786  iistmd  31044  hbtlem4  39604  idomrootle  39673  isdomn3  39682  mon1psubm  39684  amgm2d  40429  amgm3d  40430  amgm4d  40431  c0rhm  44111  c0rnghm  44112  lidlmsgrp  44125  invginvrid  44343  ply1mulgsumlem4  44371  ply1mulgsum  44372  amgmw2d  44833
  Copyright terms: Public domain W3C validator