Theorem ringmgp 19984

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

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1541   ∈ wcel 2106  ∀wral 3060  ‘cfv 6501  (class class class)co 7362  Basecbs 17094  +_gcplusg 17147  ._rcmulr 17148  Mndcmnd 18570  Grpcgrp 18762  mulGrpcmgp 19910  Ringcrg 19978

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702  ax-nul 5268

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-ne 2940  df-ral 3061  df-rab 3406  df-v 3448  df-sbc 3743  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4288  df-if 4492  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4871  df-br 5111  df-iota 6453  df-fv 6509  df-ov 7365  df-ring 19980

This theorem is referenced by:  mgpf  19993  ringcl  19995  iscrng2  19997  ringass  19998  ringideu  19999  ringidcl  20003  ringidmlem  20005  ringsrg  20027  pwspjmhmmgpd  20057  pwsexpg  20058  unitsubm  20113  dfrhm2  20164  isrhm2d  20176  idrhm  20179  pwsco1rhm  20188  pwsco2rhm  20189  subrgcrng  20274  subrgsubm  20283  issubrg3  20299  cntzsubr  20305  pwsdiagrhm  20306  subrgacs  20323  cnfldexp  20867  expmhm  20903  nn0srg  20904  rge0srg  20905  assamulgscmlem2  21340  psrcrng  21419  mplcoe3  21476  mplcoe5lem  21477  mplcoe5  21478  evlsgsummul  21539  mhppwdeg  21577  ply1moncl  21679  coe1pwmul  21687  ply1coefsupp  21703  ply1coe  21704  gsummoncoe1  21712  lply1binomsc  21715  evls1gsummul  21728  evl1expd  21748  evl1gsummul  21763  evl1scvarpw  21766  evl1scvarpwval  21767  evl1gsummon  21768  ringvcl  21784  mat1mhm  21870  scmatmhm  21920  m1detdiag  21983  mdetdiaglem  21984  m2detleiblem2  22014  mat2pmatmhm  22119  pmatcollpwscmatlem1  22175  mply1topmatcllem  22189  mply1topmatcl  22191  pm2mpghm  22202  pm2mpmhm  22206  monmat2matmon  22210  pm2mp  22211  chpscmatgsumbin  22230  chpscmatgsummon  22231  chfacfscmulcl  22243  chfacfscmul0  22244  chfacfpmmulcl  22247  chfacfpmmul0  22248  chfacfpmmulgsum2  22251  cayhamlem1  22252  cpmadugsumlemB  22260  cpmadugsumlemC  22261  cpmadugsumlemF  22262  cayhamlem2  22270  cayhamlem4  22274  nrgtrg  24091  deg1pw  25522  plypf1  25610  efsubm  25944  amgm  26377  wilthlem2  26455  wilthlem3  26456  dchrelbas3  26623  lgsqrlem2  26732  lgsqrlem3  26733  lgsqrlem4  26734  cntrcrng  31974  psgnid  32016  cnmsgn0g  32065  altgnsg  32068  freshmansdream  32137  frobrhm  32138  fermltlchr  32226  znfermltl  32227  ringlsmss  32249  evls1fpws  32348  gsummoncoe1fzo  32367  ply1degltdimlem  32404  ply1degltdim  32405  iistmd  32572  evlsbagval  40806  evlsexpval  40807  mhphf  40829  hbtlem4  41511  idomrootle  41580  isdomn3  41589  mon1psubm  41591  amgm2d  42593  amgm3d  42594  amgm4d  42595  c0rhm  46330  c0rnghm  46331  lidlmsgrp  46344  invginvrid  46563  ply1mulgsumlem4  46590  ply1mulgsum  46591  amgmw2d  47371