Theorem ringmgp 20159

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 2733	. . 3 ⊢ (Base‘𝑅) = (Base‘𝑅)
2		ringmgp.g	. . 3 ⊢ 𝐺 = (mulGrp‘𝑅)
3		eqid 2733	. . 3 ⊢ (+g‘𝑅) = (+g‘𝑅)
4		eqid 2733	. . 3 ⊢ (.r‘𝑅) = (.r‘𝑅)
5	1, 2, 3, 4	isring 20157	. 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 395   = wceq 1541   ∈ wcel 2113  ∀wral 3048  ‘cfv 6486  (class class class)co 7352  Basecbs 17122  +_gcplusg 17163  ._rcmulr 17164  Mndcmnd 18644  Grpcgrp 18848  mulGrpcmgp 20060  Ringcrg 20153

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705  ax-nul 5246

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-ne 2930  df-ral 3049  df-rab 3397  df-v 3439  df-sbc 3738  df-dif 3901  df-un 3903  df-ss 3915  df-nul 4283  df-if 4475  df-sn 4576  df-pr 4578  df-op 4582  df-uni 4859  df-br 5094  df-iota 6442  df-fv 6494  df-ov 7355  df-ring 20155

This theorem is referenced by:  mgpf  20168  ringcl  20170  iscrng2  20172  ringass  20173  ringideu  20174  ringidcl  20185  ringidmlem  20188  ringsrg  20217  pwspjmhmmgpd  20248  pwsexpg  20249  unitsubm  20306  dfrhm2  20394  isrhm2d  20406  idrhm  20409  pwsco1rhm  20419  pwsco2rhm  20420  c0rhm  20451  c0rnghm  20452  subrgcrng  20492  subrgsubm  20502  issubrg3  20517  cntzsubr  20523  pwsdiagrhm  20524  isdomn3  20632  subrgacs  20717  cnfldexp  21343  expmhm  21375  nn0srg  21376  rge0srg  21377  fermltlchr  21468  freshmansdream  21513  frobrhm  21514  assamulgscmlem2  21839  psrcrng  21910  mplcoe3  21974  mplcoe5lem  21975  mplcoe5  21976  evlsgsummul  22028  mhppwdeg  22066  psdpw  22086  ply1moncl  22186  coe1pwmul  22194  ply1coefsupp  22213  ply1coe  22214  gsummoncoe1  22224  lply1binomsc  22227  evls1gsummul  22241  evl1expd  22261  evl1gsummul  22276  evl1scvarpw  22279  evl1scvarpwval  22280  evl1gsummon  22281  evls1fpws  22285  rhmply1mon  22305  ringvcl  22316  mat1mhm  22400  scmatmhm  22450  m1detdiag  22513  mdetdiaglem  22514  m2detleiblem2  22544  mat2pmatmhm  22649  pmatcollpwscmatlem1  22705  mply1topmatcllem  22719  mply1topmatcl  22721  pm2mpghm  22732  pm2mpmhm  22736  monmat2matmon  22740  pm2mp  22741  chpscmatgsumbin  22760  chpscmatgsummon  22761  chfacfscmulcl  22773  chfacfscmul0  22774  chfacfpmmulcl  22777  chfacfpmmul0  22778  chfacfpmmulgsum2  22781  cayhamlem1  22782  cpmadugsumlemB  22790  cpmadugsumlemC  22791  cpmadugsumlemF  22792  cayhamlem2  22800  cayhamlem4  22804  nrgtrg  24606  deg1pw  26054  idomrootle  26106  plypf1  26145  efsubm  26488  amgm  26929  wilthlem2  27007  wilthlem3  27008  dchrelbas3  27177  lgsqrlem2  27286  lgsqrlem3  27287  lgsqrlem4  27288  cntrcrng  33057  psgnid  33073  cnmsgn0g  33122  altgnsg  33125  isunit3  33215  elrgspnlem1  33216  elrgspnlem2  33217  elrgspnlem3  33218  elrgspnlem4  33219  elrgspn  33220  0ringcring  33226  domnprodn0  33249  rrgsubm  33257  znfermltl  33338  unitprodclb  33361  ringlsmss  33367  rprmdvdspow  33505  1arithidomlem1  33507  1arithidom  33509  1arithufdlem2  33517  1arithufdlem3  33518  1arithufdlem4  33519  zringfrac  33526  ressply1evls1  33535  evl1deg1  33546  evl1deg2  33547  evl1deg3  33548  evls1monply1  33549  gsummoncoe1fzo  33565  ply1degltdimlem  33656  ply1degltdim  33657  assarrginv  33670  evls1fldgencl  33704  extdgfialglem1  33726  extdgfialglem2  33727  rtelextdg2lem  33760  2sqr3minply  33814  cos9thpiminplylem6  33821  cos9thpiminply  33822  iistmd  33936  aks6d1c1p2  42223  aks6d1c1p3  42224  aks6d1c1p6  42228  evl1gprodd  42231  aks6d1c2lem3  42240  idomnnzpownz  42246  aks6d1c5lem3  42251  aks6d1c5lem2  42252  deg1pow  42255  aks6d1c6lem1  42284  aks6d1c6lem2  42285  aks5lem2  42301  aks5lem3a  42303  domnexpgn0cl  42642  abvexp  42651  fidomncyc  42654  evlsvvvallem  42680  evlsvvval  42682  evlsexpval  42686  evlselv  42706  mhphf  42716  hbtlem4  43244  mon1psubm  43317  amgm2d  44316  amgm3d  44317  amgm4d  44318  invginvrid  48492  ply1mulgsumlem4  48515  ply1mulgsum  48516  amgmw2d  49930