Theorem ringmgp 20470

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 20468	. 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 17392  +_gcplusg 17433  ._rcmulr 17434  Mndcmnd 18928  Grpcgrp 19149  mulGrpcmgp 20365  Ringcrg 20464

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 4585  df-pr 4587  df-op 4835  df-uni 4867  df-br 5103  df-iota 6494  df-fv 6546  df-ov 7423  df-ring 20466

This theorem is used by:  mgpf  20480  ringcl  20482  iscrng2  20484  ringass  20485  ringideu  20486  ringidcl  20499  ringidmlem  20502  dfring2  20522  ringsrg  20533  pwspjmhmmgpd  20562  pwsexpg  20563  unitsubm  20621  dfrhm2  20709  isrhm2d  20726  idrhm  20730  pwsco1rhm  20746  pwsco2rhm  20747  c0rhm  20791  c0rnghm  20792  subrgcrng  20832  subrgsubm  20842  issubrg3  20857  cntzsubr  20863  pwsdiagrhm  20864  isdomn3  20971  isdrng3lem1  21010  subrgacs  21062  prmidlsubm  21648  cnfldexp  21716  expmhm  21747  nn0srg  21748  rge0srg  21749  fermltlchr  21840  freshmansdream  21885  frobrhm  21886  assamulgscmlem2  22213  psrcrng  22284  mplcoe3  22352  mplcoe5lem  22353  mplcoe5  22354  evlsvvvallem  22405  evlsvvval  22407  evlsgsummul  22411  evlsexpval  22442  mhppwdeg  22476  psdpw  22496  ply1moncl  22595  coe1pwmul  22603  ply1coefsupp  22620  ply1coe  22621  gsummoncoe1  22631  lply1binomsc  22634  evls1gsummul  22648  evl1expd  22668  evl1gsummul  22683  evl1scvarpw  22686  evl1scvarpwval  22687  evl1gsummon  22688  evls1fpws  22692  rhmply1mon  22709  ringvcl  22720  mat1mhm  22804  scmatmhm  22854  m1detdiag  22917  mdetdiaglem  22918  m2detleiblem2  22948  mat2pmatmhm  23056  pmatcollpwscmatlem1  23112  mply1topmatcllem  23126  mply1topmatcl  23128  pm2mpghm  23139  pm2mpmhm  23143  monmat2matmon  23147  pm2mp  23148  chpscmatgsumbin  23167  chpscmatgsummon  23168  chfacfscmulcl  23180  chfacfscmul0  23181  chfacfpmmulcl  23184  chfacfpmmul0  23185  chfacfpmmulgsum2  23188  cayhamlem1  23189  cpmadugsumlemB  23197  cpmadugsumlemC  23198  cpmadugsumlemF  23199  cayhamlem2  23207  cayhamlem4  23211  nrgtrg  25014  deg1pw  26444  idomrootle  26496  plypf1  26536  efsubm  26884  amgm  27323  wilthlem2  27401  wilthlem3  27402  dchrelbas3  27570  lgsqrlem2  27679  lgsqrlem3  27680  lgsqrlem4  27681  cntrcrng  33688  psgnid  33704  cnmsgn0g  33753  altgnsg  33756  ringm1expp1  33840  isunit3  33847  elrgspnlem1  33849  elrgspnlem2  33850  elrgspnlem3  33851  elrgspnlem4  33852  elrgspn  33853  0ringcring  33859  domnprodn0  33885  rrgsubm  33891  znfermltl  33968  unitprodclb  33990  ringlsmss  33994  rprmdvdspow  34111  1arithidomlem1  34113  1arithidom  34115  1arithufdlem2  34123  1arithufdlem3  34124  1arithufdlem4  34125  zringfrac  34132  ressply1evls1  34143  evl1deg1  34154  evl1deg2  34155  evl1deg3  34156  evls1monply1  34157  ply1coedeg  34167  gsummoncoe1fzo  34175  vietalem  34257  ply1degltdimlem  34300  ply1degltdim  34301  assarrginv  34314  evls1fldgencl  34348  extdgfialglem1  34370  extdgfialglem2  34371  rtelextdg2lem  34404  2sqr3minply  34458  cos9thpiminplylem6  34465  cos9thpiminply  34466  iistmd  34580  aks6d1c1p2  43252  aks6d1c1p3  43253  aks6d1c1p6  43257  evl1gprodd  43260  aks6d1c2lem3  43269  idomnnzpownz  43275  aks6d1c5lem3  43280  aks6d1c5lem2  43281  deg1pow  43284  aks6d1c6lem1  43313  aks6d1c6lem2  43314  aks5lem2  43330  aks5lem3a  43332  domnexpgn0cl  43677  abvexp  43689  fidomncyc  43692  evlselv  43710  mhphf  43718  hbtlem4  44221  mon1psubm  44294  amgm2d  45291  amgm3d  45292  amgm4d  45293  invginvrid  49572  ply1mulgsumlem4  49594  ply1mulgsum  49595  amgmw2d  51157