Theorem ringmgp 20465

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1569   ∈ wcel 2144  ∀wral 3076  ‘cfv 6538  (class class class)co 7420  Basecbs 17387  +_gcplusg 17428  ._rcmulr 17429  Mndcmnd 18923  Grpcgrp 19144  mulGrpcmgp 20360  Ringcrg 20459

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-nul 5259

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ne 2956  df-ral 3077  df-rab 3413  df-v 3452  df-sbc 3739  df-ss 3896  df-dif 4047  df-un 4151  df-nul 4279  df-if 4482  df-sn 4584  df-pr 4586  df-op 4590  df-uni 4867  df-br 5103  df-iota 6494  df-fv 6546  df-ov 7423  df-ring 20461

This theorem is used by:  mgpf  20475  ringcl  20477  iscrng2  20479  ringass  20480  ringideu  20481  ringidcl  20494  ringidmlem  20497  dfring2  20517  ringsrg  20528  pwspjmhmmgpd  20557  pwsexpg  20558  unitsubm  20616  dfrhm2  20704  isrhm2d  20721  idrhm  20725  pwsco1rhm  20741  pwsco2rhm  20742  c0rhm  20786  c0rnghm  20787  subrgcrng  20827  subrgsubm  20837  issubrg3  20852  cntzsubr  20858  pwsdiagrhm  20859  isdomn3  20966  isdrng3lem1  21005  subrgacs  21057  prmidlsubm  21643  cnfldexp  21711  expmhm  21742  nn0srg  21743  rge0srg  21744  fermltlchr  21835  freshmansdream  21880  frobrhm  21881  assamulgscmlem2  22208  psrcrng  22279  mplcoe3  22347  mplcoe5lem  22348  mplcoe5  22349  evlsvvvallem  22400  evlsvvval  22402  evlsgsummul  22406  evlsexpval  22437  mhppwdeg  22471  psdpw  22491  ply1moncl  22590  coe1pwmul  22598  ply1coefsupp  22615  ply1coe  22616  gsummoncoe1  22626  lply1binomsc  22629  evls1gsummul  22643  evl1expd  22663  evl1gsummul  22678  evl1scvarpw  22681  evl1scvarpwval  22682  evl1gsummon  22683  evls1fpws  22687  rhmply1mon  22704  ringvcl  22715  mat1mhm  22799  scmatmhm  22849  m1detdiag  22912  mdetdiaglem  22913  m2detleiblem2  22943  mat2pmatmhm  23051  pmatcollpwscmatlem1  23107  mply1topmatcllem  23121  mply1topmatcl  23123  pm2mpghm  23134  pm2mpmhm  23138  monmat2matmon  23142  pm2mp  23143  chpscmatgsumbin  23162  chpscmatgsummon  23163  chfacfscmulcl  23175  chfacfscmul0  23176  chfacfpmmulcl  23179  chfacfpmmul0  23180  chfacfpmmulgsum2  23183  cayhamlem1  23184  cpmadugsumlemB  23192  cpmadugsumlemC  23193  cpmadugsumlemF  23194  cayhamlem2  23202  cayhamlem4  23206  nrgtrg  25009  deg1pw  26439  idomrootle  26491  plypf1  26531  efsubm  26879  amgm  27318  wilthlem2  27396  wilthlem3  27397  dchrelbas3  27565  lgsqrlem2  27674  lgsqrlem3  27675  lgsqrlem4  27676  cntrcrng  33684  psgnid  33700  cnmsgn0g  33749  altgnsg  33752  ringm1expp1  33836  isunit3  33843  elrgspnlem1  33845  elrgspnlem2  33846  elrgspnlem3  33847  elrgspnlem4  33848  elrgspn  33849  0ringcring  33855  domnprodn0  33881  rrgsubm  33887  znfermltl  33964  unitprodclb  33986  ringlsmss  33990  rprmdvdspow  34107  1arithidomlem1  34109  1arithidom  34111  1arithufdlem2  34119  1arithufdlem3  34120  1arithufdlem4  34121  zringfrac  34128  ressply1evls1  34139  evl1deg1  34150  evl1deg2  34151  evl1deg3  34152  evls1monply1  34153  ply1coedeg  34163  gsummoncoe1fzo  34171  vietalem  34253  ply1degltdimlem  34296  ply1degltdim  34297  assarrginv  34310  evls1fldgencl  34344  extdgfialglem1  34366  extdgfialglem2  34367  rtelextdg2lem  34400  2sqr3minply  34454  cos9thpiminplylem6  34461  cos9thpiminply  34462  iistmd  34576  aks6d1c1p2  43202  aks6d1c1p3  43203  aks6d1c1p6  43207  evl1gprodd  43210  aks6d1c2lem3  43219  idomnnzpownz  43225  aks6d1c5lem3  43230  aks6d1c5lem2  43231  deg1pow  43234  aks6d1c6lem1  43263  aks6d1c6lem2  43264  aks5lem2  43280  aks5lem3a  43282  domnexpgn0cl  43627  abvexp  43639  fidomncyc  43642  evlselv  43660  mhphf  43668  hbtlem4  44171  mon1psubm  44244  amgm2d  45241  amgm3d  45242  amgm4d  45243  invginvrid  49522  ply1mulgsumlem4  49544  ply1mulgsum  49545  amgmw2d  51032