Theorem ringmgp 18376

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.

Step	Hyp	Ref	Expression
1		eqid 2610	. . 3 ⊢ (Base‘𝑅) = (Base‘𝑅)
2		ringmgp.g	. . 3 ⊢ 𝐺 = (mulGrp‘𝑅)
3		eqid 2610	. . 3 ⊢ (+g‘𝑅) = (+g‘𝑅)
4		eqid 2610	. . 3 ⊢ (.r‘𝑅) = (.r‘𝑅)
5	1, 2, 3, 4	isring 18374	. 2 ⊢ (𝑅 ∈ Ring ↔ (𝑅 ∈ Grp ∧ 𝐺 ∈ Mnd ∧ ∀𝑥 ∈ (Base‘𝑅)∀𝑦 ∈ (Base‘𝑅)∀𝑧 ∈ (Base‘𝑅)((𝑥(.r‘𝑅)(𝑦(+g‘𝑅)𝑧)) = ((𝑥(.r‘𝑅)𝑦)(+g‘𝑅)(𝑥(.r‘𝑅)𝑧)) ∧ ((𝑥(+g‘𝑅)𝑦)(.r‘𝑅)𝑧) = ((𝑥(.r‘𝑅)𝑧)(+g‘𝑅)(𝑦(.r‘𝑅)𝑧)))))
6	5	simp2bi 1070	1 ⊢ (𝑅 ∈ Ring → 𝐺 ∈ Mnd)

Syntax hints:   → wi 4   ∧ wa 383   = wceq 1475   ∈ wcel 1977  ∀wral 2896  ‘cfv 5804  (class class class)co 6549  Basecbs 15695  +_gcplusg 15768  ._rcmulr 15769  Mndcmnd 17117  Grpcgrp 17245  mulGrpcmgp 18312  Ringcrg 18370

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-nul 4717

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ral 2901  df-rex 2902  df-rab 2905  df-v 3175  df-sbc 3403  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-br 4584  df-iota 5768  df-fv 5812  df-ov 6552  df-ring 18372

This theorem is referenced by:  mgpf  18382  ringcl  18384  iscrng2  18386  ringass  18387  ringideu  18388  ringidcl  18391  ringidmlem  18393  ringsrg  18412  unitsubm  18493  dfrhm2  18540  isrhm2d  18551  idrhm  18554  pwsco1rhm  18561  pwsco2rhm  18562  subrgcrng  18607  subrgsubm  18616  issubrg3  18631  cntzsubr  18635  pwsdiagrhm  18636  assamulgscmlem2  19170  psrcrng  19234  mplcoe3  19287  mplcoe5lem  19288  mplcoe5  19289  ply1moncl  19462  coe1pwmul  19470  ply1coefsupp  19486  ply1coe  19487  gsummoncoe1  19495  lply1binomsc  19498  evls1gsummul  19511  evl1expd  19530  evl1gsummul  19545  evl1scvarpw  19548  evl1scvarpwval  19549  evl1gsummon  19550  cnfldexp  19598  expmhm  19634  nn0srg  19635  rge0srg  19636  ringvcl  20023  mat1mhm  20109  scmatmhm  20159  m1detdiag  20222  mdetdiaglem  20223  m2detleiblem2  20253  mat2pmatmhm  20357  pmatcollpwscmatlem1  20413  mply1topmatcllem  20427  mply1topmatcl  20429  pm2mpghm  20440  pm2mpmhm  20444  monmat2matmon  20448  pm2mp  20449  chpscmatgsumbin  20468  chpscmatgsummon  20469  chfacfscmulcl  20481  chfacfscmul0  20482  chfacfpmmulcl  20485  chfacfpmmul0  20486  chfacfpmmulgsum2  20489  cayhamlem1  20490  cpmadugsumlemB  20498  cpmadugsumlemC  20499  cpmadugsumlemF  20500  cayhamlem2  20508  cayhamlem4  20512  nrgtrg  22304  deg1pw  23684  plypf1  23772  efsubm  24101  amgm  24517  wilthlem2  24595  wilthlem3  24596  dchrelbas3  24763  lgsqrlem2  24872  lgsqrlem3  24873  lgsqrlem4  24874  psgnid  29178  iistmd  29276  hbtlem4  36715  subrgacs  36789  idomrootle  36792  isdomn3  36801  mon1psubm  36803  amgm2d  37523  amgm3d  37524  amgm4d  37525  c0rhm  41702  c0rnghm  41703  lidlmsgrp  41716  invginvrid  41942  ply1mulgsumlem4  41971  ply1mulgsum  41972  amgmw2d  42359