Theorem ringmgp 20268

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

Syntax hints:   → wi 4   ∧ wa 399   = wceq 1559   ∈ wcel 2141  ∀wral 3075  ‘cfv 6517  (class class class)co 7392  Basecbs 17228  +_gcplusg 17269  ._rcmulr 17270  Mndcmnd 18751  Grpcgrp 18958  mulGrpcmgp 20169  Ringcrg 20262

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733  ax-nul 5255

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-ne 2957  df-ral 3076  df-rab 3414  df-v 3455  df-sbc 3745  df-dif 3907  df-un 3909  df-ss 3921  df-nul 4286  df-if 4480  df-sn 4582  df-pr 4584  df-op 4588  df-uni 4865  df-br 5100  df-iota 6473  df-fv 6525  df-ov 7395  df-ring 20264

This theorem is referenced by:  mgpf  20277  ringcl  20279  iscrng2  20281  ringass  20282  ringideu  20283  ringidcl  20294  ringidmlem  20297  ringsrg  20326  pwspjmhmmgpd  20355  pwsexpg  20356  unitsubm  20414  dfrhm2  20502  isrhm2d  20515  idrhm  20518  pwsco1rhm  20530  pwsco2rhm  20531  c0rhm  20563  c0rnghm  20564  subrgcrng  20604  subrgsubm  20614  issubrg3  20629  cntzsubr  20635  pwsdiagrhm  20636  isdomn3  20744  subrgacs  20829  cnfldexp  21437  expmhm  21468  nn0srg  21469  rge0srg  21470  fermltlchr  21561  freshmansdream  21606  frobrhm  21607  assamulgscmlem2  21932  psrcrng  22003  mplcoe3  22071  mplcoe5lem  22072  mplcoe5  22073  evlsvvvallem  22124  evlsvvval  22126  evlsgsummul  22130  evlsexpval  22161  mhppwdeg  22195  psdpw  22215  ply1moncl  22314  coe1pwmul  22322  ply1coefsupp  22340  ply1coe  22341  gsummoncoe1  22351  lply1binomsc  22354  evls1gsummul  22368  evl1expd  22388  evl1gsummul  22403  evl1scvarpw  22406  evl1scvarpwval  22407  evl1gsummon  22408  evls1fpws  22412  rhmply1mon  22429  ringvcl  22440  mat1mhm  22524  scmatmhm  22574  m1detdiag  22637  mdetdiaglem  22638  m2detleiblem2  22668  mat2pmatmhm  22773  pmatcollpwscmatlem1  22829  mply1topmatcllem  22843  mply1topmatcl  22845  pm2mpghm  22856  pm2mpmhm  22860  monmat2matmon  22864  pm2mp  22865  chpscmatgsumbin  22884  chpscmatgsummon  22885  chfacfscmulcl  22897  chfacfscmul0  22898  chfacfpmmulcl  22901  chfacfpmmul0  22902  chfacfpmmulgsum2  22905  cayhamlem1  22906  cpmadugsumlemB  22914  cpmadugsumlemC  22915  cpmadugsumlemF  22916  cayhamlem2  22924  cayhamlem4  22928  nrgtrg  24730  deg1pw  26161  idomrootle  26213  plypf1  26252  efsubm  26593  amgm  27032  wilthlem2  27110  wilthlem3  27111  dchrelbas3  27279  lgsqrlem2  27388  lgsqrlem3  27389  lgsqrlem4  27390  cntrcrng  33222  psgnid  33238  cnmsgn0g  33287  altgnsg  33290  ringm1expp1  33375  isunit3  33382  elrgspnlem1  33384  elrgspnlem2  33385  elrgspnlem3  33386  elrgspnlem4  33387  elrgspn  33388  0ringcring  33394  domnprodn0  33420  rrgsubm  33429  znfermltl  33513  unitprodclb  33536  ringlsmss  33542  prmidlsubm  33607  rprmdvdspow  33690  1arithidomlem1  33692  1arithidom  33694  1arithufdlem2  33702  1arithufdlem3  33703  1arithufdlem4  33704  zringfrac  33711  ressply1evls1  33722  evl1deg1  33733  evl1deg2  33734  evl1deg3  33735  evls1monply1  33736  ply1coedeg  33746  gsummoncoe1fzo  33754  vietalem  33837  ply1degltdimlem  33880  ply1degltdim  33881  assarrginv  33894  evls1fldgencl  33928  extdgfialglem1  33950  extdgfialglem2  33951  rtelextdg2lem  33984  2sqr3minply  34038  cos9thpiminplylem6  34045  cos9thpiminply  34046  iistmd  34160  aks6d1c1p2  42690  aks6d1c1p3  42691  aks6d1c1p6  42695  evl1gprodd  42698  aks6d1c2lem3  42707  idomnnzpownz  42713  aks6d1c5lem3  42718  aks6d1c5lem2  42719  deg1pow  42722  aks6d1c6lem1  42751  aks6d1c6lem2  42752  aks5lem2  42768  aks5lem3a  42770  domnexpgn0cl  43105  abvexp  43114  fidomncyc  43117  evlselv  43135  mhphf  43143  hbtlem4  43667  mon1psubm  43740  amgm2d  44738  amgm3d  44739  amgm4d  44740  invginvrid  48953  ply1mulgsumlem4  48975  ply1mulgsum  48976  amgmw2d  50389