Theorem ringmgp 20204

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 2736	. . 3 ⊢ (Base‘𝑅) = (Base‘𝑅)
2		ringmgp.g	. . 3 ⊢ 𝐺 = (mulGrp‘𝑅)
3		eqid 2736	. . 3 ⊢ (+g‘𝑅) = (+g‘𝑅)
4		eqid 2736	. . 3 ⊢ (.r‘𝑅) = (.r‘𝑅)
5	1, 2, 3, 4	isring 20202	. 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 1540   ∈ wcel 2109  ∀wral 3052  ‘cfv 6536  (class class class)co 7410  Basecbs 17233  +_gcplusg 17276  ._rcmulr 17277  Mndcmnd 18717  Grpcgrp 18921  mulGrpcmgp 20105  Ringcrg 20198

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2708  ax-nul 5281

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2715  df-cleq 2728  df-clel 2810  df-ne 2934  df-ral 3053  df-rab 3421  df-v 3466  df-sbc 3771  df-dif 3934  df-un 3936  df-ss 3948  df-nul 4314  df-if 4506  df-sn 4607  df-pr 4609  df-op 4613  df-uni 4889  df-br 5125  df-iota 6489  df-fv 6544  df-ov 7413  df-ring 20200

This theorem is referenced by:  mgpf  20213  ringcl  20215  iscrng2  20217  ringass  20218  ringideu  20219  ringidcl  20230  ringidmlem  20233  ringsrg  20262  pwspjmhmmgpd  20293  pwsexpg  20294  unitsubm  20351  dfrhm2  20439  isrhm2d  20452  idrhm  20455  pwsco1rhm  20467  pwsco2rhm  20468  c0rhm  20499  c0rnghm  20500  subrgcrng  20540  subrgsubm  20550  issubrg3  20565  cntzsubr  20571  pwsdiagrhm  20572  isdomn3  20680  subrgacs  20765  cnfldexp  21372  expmhm  21409  nn0srg  21410  rge0srg  21411  fermltlchr  21495  freshmansdream  21540  frobrhm  21541  assamulgscmlem2  21865  psrcrng  21937  mplcoe3  22001  mplcoe5lem  22002  mplcoe5  22003  evlsgsummul  22055  mhppwdeg  22093  psdpw  22113  ply1moncl  22213  coe1pwmul  22221  ply1coefsupp  22240  ply1coe  22241  gsummoncoe1  22251  lply1binomsc  22254  evls1gsummul  22268  evl1expd  22288  evl1gsummul  22303  evl1scvarpw  22306  evl1scvarpwval  22307  evl1gsummon  22308  evls1fpws  22312  rhmply1mon  22332  ringvcl  22343  mat1mhm  22427  scmatmhm  22477  m1detdiag  22540  mdetdiaglem  22541  m2detleiblem2  22571  mat2pmatmhm  22676  pmatcollpwscmatlem1  22732  mply1topmatcllem  22746  mply1topmatcl  22748  pm2mpghm  22759  pm2mpmhm  22763  monmat2matmon  22767  pm2mp  22768  chpscmatgsumbin  22787  chpscmatgsummon  22788  chfacfscmulcl  22800  chfacfscmul0  22801  chfacfpmmulcl  22804  chfacfpmmul0  22805  chfacfpmmulgsum2  22808  cayhamlem1  22809  cpmadugsumlemB  22817  cpmadugsumlemC  22818  cpmadugsumlemF  22819  cayhamlem2  22827  cayhamlem4  22831  nrgtrg  24634  deg1pw  26083  idomrootle  26135  plypf1  26174  efsubm  26517  amgm  26958  wilthlem2  27036  wilthlem3  27037  dchrelbas3  27206  lgsqrlem2  27315  lgsqrlem3  27316  lgsqrlem4  27317  cntrcrng  33069  psgnid  33113  cnmsgn0g  33162  altgnsg  33165  isunit3  33241  elrgspnlem1  33242  elrgspnlem2  33243  elrgspnlem3  33244  elrgspnlem4  33245  elrgspn  33246  0ringcring  33252  domnprodn0  33275  rrgsubm  33283  znfermltl  33386  unitprodclb  33409  ringlsmss  33415  rprmdvdspow  33553  1arithidomlem1  33555  1arithidom  33557  1arithufdlem2  33565  1arithufdlem3  33566  1arithufdlem4  33567  zringfrac  33574  ressply1evls1  33583  evl1deg1  33594  evl1deg2  33595  evl1deg3  33596  gsummoncoe1fzo  33612  ply1degltdimlem  33667  ply1degltdim  33668  assarrginv  33681  evls1fldgencl  33716  rtelextdg2lem  33765  2sqr3minply  33819  cos9thpiminplylem6  33826  cos9thpiminply  33827  iistmd  33938  aks6d1c1p2  42127  aks6d1c1p3  42128  aks6d1c1p6  42132  evl1gprodd  42135  aks6d1c2lem3  42144  idomnnzpownz  42150  aks6d1c5lem3  42155  aks6d1c5lem2  42156  deg1pow  42159  aks6d1c6lem1  42188  aks6d1c6lem2  42189  aks5lem2  42205  aks5lem3a  42207  domnexpgn0cl  42521  abvexp  42530  fidomncyc  42533  evlsvvvallem  42559  evlsvvval  42561  evlsexpval  42565  evlselv  42585  mhphf  42595  hbtlem4  43125  mon1psubm  43198  amgm2d  44197  amgm3d  44198  amgm4d  44199  invginvrid  48322  ply1mulgsumlem4  48345  ply1mulgsum  48346  amgmw2d  49648