Theorem ringmgp 18474

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 2621	. . 3 ⊢ (Base‘𝑅) = (Base‘𝑅)
2		ringmgp.g	. . 3 ⊢ 𝐺 = (mulGrp‘𝑅)
3		eqid 2621	. . 3 ⊢ (+g‘𝑅) = (+g‘𝑅)
4		eqid 2621	. . 3 ⊢ (.r‘𝑅) = (.r‘𝑅)
5	1, 2, 3, 4	isring 18472	. 2 ⊢ (𝑅 ∈ Ring ↔ (𝑅 ∈ Grp ∧ 𝐺 ∈ Mnd ∧ ∀𝑥 ∈ (Base‘𝑅)∀𝑦 ∈ (Base‘𝑅)∀𝑧 ∈ (Base‘𝑅)((𝑥(.r‘𝑅)(𝑦(+g‘𝑅)𝑧)) = ((𝑥(.r‘𝑅)𝑦)(+g‘𝑅)(𝑥(.r‘𝑅)𝑧)) ∧ ((𝑥(+g‘𝑅)𝑦)(.r‘𝑅)𝑧) = ((𝑥(.r‘𝑅)𝑧)(+g‘𝑅)(𝑦(.r‘𝑅)𝑧)))))
6	5	simp2bi 1075	1 ⊢ (𝑅 ∈ Ring → 𝐺 ∈ Mnd)

Syntax hints:   → wi 4   ∧ wa 384   = wceq 1480   ∈ wcel 1987  ∀wral 2907  ‘cfv 5847  (class class class)co 6604  Basecbs 15781  +_gcplusg 15862  ._rcmulr 15863  Mndcmnd 17215  Grpcgrp 17343  mulGrpcmgp 18410  Ringcrg 18468

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-nul 4749

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ral 2912  df-rex 2913  df-rab 2916  df-v 3188  df-sbc 3418  df-dif 3558  df-un 3560  df-in 3562  df-ss 3569  df-nul 3892  df-if 4059  df-sn 4149  df-pr 4151  df-op 4155  df-uni 4403  df-br 4614  df-iota 5810  df-fv 5855  df-ov 6607  df-ring 18470

This theorem is referenced by:  mgpf  18480  ringcl  18482  iscrng2  18484  ringass  18485  ringideu  18486  ringidcl  18489  ringidmlem  18491  ringsrg  18510  unitsubm  18591  dfrhm2  18638  isrhm2d  18649  idrhm  18652  pwsco1rhm  18659  pwsco2rhm  18660  subrgcrng  18705  subrgsubm  18714  issubrg3  18729  cntzsubr  18733  pwsdiagrhm  18734  assamulgscmlem2  19268  psrcrng  19332  mplcoe3  19385  mplcoe5lem  19386  mplcoe5  19387  ply1moncl  19560  coe1pwmul  19568  ply1coefsupp  19584  ply1coe  19585  gsummoncoe1  19593  lply1binomsc  19596  evls1gsummul  19609  evl1expd  19628  evl1gsummul  19643  evl1scvarpw  19646  evl1scvarpwval  19647  evl1gsummon  19648  cnfldexp  19698  expmhm  19734  nn0srg  19735  rge0srg  19736  ringvcl  20123  mat1mhm  20209  scmatmhm  20259  m1detdiag  20322  mdetdiaglem  20323  m2detleiblem2  20353  mat2pmatmhm  20457  pmatcollpwscmatlem1  20513  mply1topmatcllem  20527  mply1topmatcl  20529  pm2mpghm  20540  pm2mpmhm  20544  monmat2matmon  20548  pm2mp  20549  chpscmatgsumbin  20568  chpscmatgsummon  20569  chfacfscmulcl  20581  chfacfscmul0  20582  chfacfpmmulcl  20585  chfacfpmmul0  20586  chfacfpmmulgsum2  20589  cayhamlem1  20590  cpmadugsumlemB  20598  cpmadugsumlemC  20599  cpmadugsumlemF  20600  cayhamlem2  20608  cayhamlem4  20612  nrgtrg  22404  deg1pw  23784  plypf1  23872  efsubm  24201  amgm  24617  wilthlem2  24695  wilthlem3  24696  dchrelbas3  24863  lgsqrlem2  24972  lgsqrlem3  24973  lgsqrlem4  24974  psgnid  29629  iistmd  29727  hbtlem4  37174  subrgacs  37248  idomrootle  37251  isdomn3  37260  mon1psubm  37262  amgm2d  37980  amgm3d  37981  amgm4d  37982  c0rhm  41197  c0rnghm  41198  lidlmsgrp  41211  invginvrid  41433  ply1mulgsumlem4  41462  ply1mulgsum  41463  amgmw2d  41850