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

Theorem ringmgp 19282
 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 2820 . . 3 (Base‘𝑅) = (Base‘𝑅)
2 ringmgp.g . . 3 𝐺 = (mulGrp‘𝑅)
3 eqid 2820 . . 3 (+g𝑅) = (+g𝑅)
4 eqid 2820 . . 3 (.r𝑅) = (.r𝑅)
51, 2, 3, 4isring 19280 . 2 (𝑅 ∈ Ring ↔ (𝑅 ∈ Grp ∧ 𝐺 ∈ Mnd ∧ ∀𝑥 ∈ (Base‘𝑅)∀𝑦 ∈ (Base‘𝑅)∀𝑧 ∈ (Base‘𝑅)((𝑥(.r𝑅)(𝑦(+g𝑅)𝑧)) = ((𝑥(.r𝑅)𝑦)(+g𝑅)(𝑥(.r𝑅)𝑧)) ∧ ((𝑥(+g𝑅)𝑦)(.r𝑅)𝑧) = ((𝑥(.r𝑅)𝑧)(+g𝑅)(𝑦(.r𝑅)𝑧)))))
65simp2bi 1142 1 (𝑅 ∈ Ring → 𝐺 ∈ Mnd)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 398   = wceq 1537   ∈ wcel 2114  ∀wral 3125  ‘cfv 6331  (class class class)co 7133  Basecbs 16462  +gcplusg 16544  .rcmulr 16545  Mndcmnd 17890  Grpcgrp 18082  mulGrpcmgp 19218  Ringcrg 19276 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2792  ax-nul 5186 This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2653  df-clab 2799  df-cleq 2813  df-clel 2891  df-nfc 2959  df-ral 3130  df-rex 3131  df-rab 3134  df-v 3475  df-sbc 3753  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4270  df-if 4444  df-sn 4544  df-pr 4546  df-op 4550  df-uni 4815  df-br 5043  df-iota 6290  df-fv 6339  df-ov 7136  df-ring 19278 This theorem is referenced by:  mgpf  19288  ringcl  19290  iscrng2  19292  ringass  19293  ringideu  19294  ringidcl  19297  ringidmlem  19299  ringsrg  19318  unitsubm  19399  dfrhm2  19448  isrhm2d  19459  idrhm  19462  pwsco1rhm  19469  pwsco2rhm  19470  subrgcrng  19515  subrgsubm  19524  issubrg3  19539  cntzsubr  19544  pwsdiagrhm  19545  subrgacs  19555  assamulgscmlem2  20105  psrcrng  20169  mplcoe3  20223  mplcoe5lem  20224  mplcoe5  20225  evlsgsummul  20281  ply1moncl  20415  coe1pwmul  20423  ply1coefsupp  20439  ply1coe  20440  gsummoncoe1  20448  lply1binomsc  20451  evls1gsummul  20464  evl1expd  20484  evl1gsummul  20499  evl1scvarpw  20502  evl1scvarpwval  20503  evl1gsummon  20504  cnfldexp  20554  expmhm  20590  nn0srg  20591  rge0srg  20592  ringvcl  20985  mat1mhm  21069  scmatmhm  21119  m1detdiag  21182  mdetdiaglem  21183  m2detleiblem2  21213  mat2pmatmhm  21317  pmatcollpwscmatlem1  21373  mply1topmatcllem  21387  mply1topmatcl  21389  pm2mpghm  21400  pm2mpmhm  21404  monmat2matmon  21408  pm2mp  21409  chpscmatgsumbin  21428  chpscmatgsummon  21429  chfacfscmulcl  21441  chfacfscmul0  21442  chfacfpmmulcl  21445  chfacfpmmul0  21446  chfacfpmmulgsum2  21449  cayhamlem1  21450  cpmadugsumlemB  21458  cpmadugsumlemC  21459  cpmadugsumlemF  21460  cayhamlem2  21468  cayhamlem4  21472  nrgtrg  23275  deg1pw  24700  plypf1  24788  efsubm  25122  amgm  25555  wilthlem2  25633  wilthlem3  25634  dchrelbas3  25801  lgsqrlem2  25910  lgsqrlem3  25911  lgsqrlem4  25912  cntrcrng  30705  psgnid  30747  cnmsgn0g  30796  altgnsg  30799  freshmansdream  30867  ringlsmss  30957  iistmd  31153  hbtlem4  39863  idomrootle  39932  isdomn3  39941  mon1psubm  39943  amgm2d  40686  amgm3d  40687  amgm4d  40688  c0rhm  44328  c0rnghm  44329  lidlmsgrp  44342  invginvrid  44560  ply1mulgsumlem4  44588  ply1mulgsum  44589  amgmw2d  45092
 Copyright terms: Public domain W3C validator