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

Theorem ringmgp 19234
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 2821 . . 3 (Base‘𝑅) = (Base‘𝑅)
2 ringmgp.g . . 3 𝐺 = (mulGrp‘𝑅)
3 eqid 2821 . . 3 (+g𝑅) = (+g𝑅)
4 eqid 2821 . . 3 (.r𝑅) = (.r𝑅)
51, 2, 3, 4isring 19232 . 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 3138  cfv 6349  (class class class)co 7145  Basecbs 16473  +gcplusg 16555  .rcmulr 16556  Mndcmnd 17901  Grpcgrp 18043  mulGrpcmgp 19170  Ringcrg 19228
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 2793  ax-nul 5202
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 2618  df-eu 2650  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3497  df-sbc 3772  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-nul 4291  df-if 4466  df-sn 4560  df-pr 4562  df-op 4566  df-uni 4833  df-br 5059  df-iota 6308  df-fv 6357  df-ov 7148  df-ring 19230
This theorem is referenced by:  mgpf  19240  ringcl  19242  iscrng2  19244  ringass  19245  ringideu  19246  ringidcl  19249  ringidmlem  19251  ringsrg  19270  unitsubm  19351  dfrhm2  19400  isrhm2d  19411  idrhm  19414  pwsco1rhm  19421  pwsco2rhm  19422  subrgcrng  19470  subrgsubm  19479  issubrg3  19494  cntzsubr  19499  pwsdiagrhm  19500  subrgacs  19510  assamulgscmlem2  20059  psrcrng  20123  mplcoe3  20177  mplcoe5lem  20178  mplcoe5  20179  evlsgsummul  20235  ply1moncl  20369  coe1pwmul  20377  ply1coefsupp  20393  ply1coe  20394  gsummoncoe1  20402  lply1binomsc  20405  evls1gsummul  20418  evl1expd  20438  evl1gsummul  20453  evl1scvarpw  20456  evl1scvarpwval  20457  evl1gsummon  20458  cnfldexp  20508  expmhm  20544  nn0srg  20545  rge0srg  20546  ringvcl  20939  mat1mhm  21023  scmatmhm  21073  m1detdiag  21136  mdetdiaglem  21137  m2detleiblem2  21167  mat2pmatmhm  21271  pmatcollpwscmatlem1  21327  mply1topmatcllem  21341  mply1topmatcl  21343  pm2mpghm  21354  pm2mpmhm  21358  monmat2matmon  21362  pm2mp  21363  chpscmatgsumbin  21382  chpscmatgsummon  21383  chfacfscmulcl  21395  chfacfscmul0  21396  chfacfpmmulcl  21399  chfacfpmmul0  21400  chfacfpmmulgsum2  21403  cayhamlem1  21404  cpmadugsumlemB  21412  cpmadugsumlemC  21413  cpmadugsumlemF  21414  cayhamlem2  21422  cayhamlem4  21426  nrgtrg  23228  deg1pw  24643  plypf1  24731  efsubm  25062  amgm  25496  wilthlem2  25574  wilthlem3  25575  dchrelbas3  25742  lgsqrlem2  25851  lgsqrlem3  25852  lgsqrlem4  25853  cntrcrng  30625  psgnid  30667  cnmsgn0g  30716  altgnsg  30719  freshmansdream  30787  iistmd  31045  hbtlem4  39606  idomrootle  39675  isdomn3  39684  mon1psubm  39686  amgm2d  40432  amgm3d  40433  amgm4d  40434  c0rhm  44081  c0rnghm  44082  lidlmsgrp  44095  invginvrid  44313  ply1mulgsumlem4  44341  ply1mulgsum  44342  amgmw2d  44803
  Copyright terms: Public domain W3C validator