Theorem ringmgp 20256

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1536   ∈ wcel 2105  ∀wral 3058  ‘cfv 6562  (class class class)co 7430  Basecbs 17244  +_gcplusg 17297  ._rcmulr 17298  Mndcmnd 18759  Grpcgrp 18963  mulGrpcmgp 20151  Ringcrg 20250

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705  ax-nul 5311

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-ne 2938  df-ral 3059  df-rab 3433  df-v 3479  df-sbc 3791  df-dif 3965  df-un 3967  df-ss 3979  df-nul 4339  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-br 5148  df-iota 6515  df-fv 6570  df-ov 7433  df-ring 20252

This theorem is referenced by:  mgpf  20265  ringcl  20267  iscrng2  20269  ringass  20270  ringideu  20271  ringidcl  20279  ringidmlem  20281  ringsrg  20310  pwspjmhmmgpd  20341  pwsexpg  20342  unitsubm  20402  dfrhm2  20490  isrhm2d  20503  idrhm  20506  pwsco1rhm  20518  pwsco2rhm  20519  c0rhm  20550  c0rnghm  20551  subrgcrng  20591  subrgsubm  20601  issubrg3  20616  cntzsubr  20622  pwsdiagrhm  20623  isdomn3  20731  subrgacs  20817  cnfldexp  21434  expmhm  21471  nn0srg  21472  rge0srg  21473  fermltlchr  21561  freshmansdream  21610  frobrhm  21611  assamulgscmlem2  21937  psrcrng  22009  mplcoe3  22073  mplcoe5lem  22074  mplcoe5  22075  evlsgsummul  22133  mhppwdeg  22171  ply1moncl  22289  coe1pwmul  22297  ply1coefsupp  22316  ply1coe  22317  gsummoncoe1  22327  lply1binomsc  22330  evls1gsummul  22344  evl1expd  22364  evl1gsummul  22379  evl1scvarpw  22382  evl1scvarpwval  22383  evl1gsummon  22384  evls1fpws  22388  rhmply1mon  22408  ringvcl  22419  mat1mhm  22505  scmatmhm  22555  m1detdiag  22618  mdetdiaglem  22619  m2detleiblem2  22649  mat2pmatmhm  22754  pmatcollpwscmatlem1  22810  mply1topmatcllem  22824  mply1topmatcl  22826  pm2mpghm  22837  pm2mpmhm  22841  monmat2matmon  22845  pm2mp  22846  chpscmatgsumbin  22865  chpscmatgsummon  22866  chfacfscmulcl  22878  chfacfscmul0  22879  chfacfpmmulcl  22882  chfacfpmmul0  22883  chfacfpmmulgsum2  22886  cayhamlem1  22887  cpmadugsumlemB  22895  cpmadugsumlemC  22896  cpmadugsumlemF  22897  cayhamlem2  22905  cayhamlem4  22909  nrgtrg  24726  deg1pw  26174  idomrootle  26226  plypf1  26265  efsubm  26607  amgm  27048  wilthlem2  27126  wilthlem3  27127  dchrelbas3  27296  lgsqrlem2  27405  lgsqrlem3  27406  lgsqrlem4  27407  cntrcrng  33055  psgnid  33099  cnmsgn0g  33148  altgnsg  33151  isunit3  33230  elrgspnlem1  33231  elrgspnlem2  33232  elrgspnlem3  33233  elrgspnlem4  33234  0ringcring  33238  domnprodn0  33261  rrgsubm  33267  znfermltl  33373  unitprodclb  33396  ringlsmss  33402  rprmdvdspow  33540  1arithidomlem1  33542  1arithidom  33544  1arithufdlem2  33552  1arithufdlem3  33553  1arithufdlem4  33554  zringfrac  33561  evl1deg1  33580  evl1deg2  33581  evl1deg3  33582  gsummoncoe1fzo  33597  ply1degltdimlem  33649  ply1degltdim  33650  assarrginv  33663  evls1fldgencl  33694  rtelextdg2lem  33731  2sqr3minply  33752  iistmd  33862  aks6d1c1p2  42090  aks6d1c1p3  42091  aks6d1c1p6  42095  evl1gprodd  42098  aks6d1c2lem3  42107  idomnnzpownz  42113  aks6d1c5lem3  42118  aks6d1c5lem2  42119  deg1pow  42122  aks6d1c6lem1  42151  aks6d1c6lem2  42152  aks5lem2  42168  aks5lem3a  42170  domnexpgn0cl  42509  abvexp  42518  fidomncyc  42521  evlsvvvallem  42547  evlsvvval  42549  evlsexpval  42553  evlselv  42573  mhphf  42583  hbtlem4  43114  mon1psubm  43187  amgm2d  44187  amgm3d  44188  amgm4d  44189  invginvrid  48211  ply1mulgsumlem4  48234  ply1mulgsum  48235  amgmw2d  49034