Theorem ringmgp 20218

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

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1547   ∈ wcel 2119  ∀wral 3054  ‘cfv 6492  (class class class)co 7363  Basecbs 17177  +_gcplusg 17218  ._rcmulr 17219  Mndcmnd 18700  Grpcgrp 18907  mulGrpcmgp 20119  Ringcrg 20212

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712  ax-nul 5235

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-ne 2936  df-ral 3055  df-rab 3393  df-v 3434  df-sbc 3731  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4269  df-if 4462  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4846  df-br 5080  df-iota 6448  df-fv 6500  df-ov 7366  df-ring 20214

This theorem is referenced by:  mgpf  20227  ringcl  20229  iscrng2  20231  ringass  20232  ringideu  20233  ringidcl  20244  ringidmlem  20247  ringsrg  20276  pwspjmhmmgpd  20305  pwsexpg  20306  unitsubm  20364  dfrhm2  20452  isrhm2d  20465  idrhm  20468  pwsco1rhm  20480  pwsco2rhm  20481  c0rhm  20513  c0rnghm  20514  subrgcrng  20554  subrgsubm  20564  issubrg3  20579  cntzsubr  20585  pwsdiagrhm  20586  isdomn3  20694  subrgacs  20779  cnfldexp  21387  expmhm  21418  nn0srg  21419  rge0srg  21420  fermltlchr  21511  freshmansdream  21556  frobrhm  21557  assamulgscmlem2  21882  psrcrng  21953  mplcoe3  22021  mplcoe5lem  22022  mplcoe5  22023  evlsvvvallem  22074  evlsvvval  22076  evlsgsummul  22080  evlsexpval  22111  mhppwdeg  22145  psdpw  22165  ply1moncl  22264  coe1pwmul  22272  ply1coefsupp  22290  ply1coe  22291  gsummoncoe1  22301  lply1binomsc  22304  evls1gsummul  22318  evl1expd  22338  evl1gsummul  22353  evl1scvarpw  22356  evl1scvarpwval  22357  evl1gsummon  22358  evls1fpws  22362  rhmply1mon  22379  ringvcl  22390  mat1mhm  22474  scmatmhm  22524  m1detdiag  22587  mdetdiaglem  22588  m2detleiblem2  22618  mat2pmatmhm  22723  pmatcollpwscmatlem1  22779  mply1topmatcllem  22793  mply1topmatcl  22795  pm2mpghm  22806  pm2mpmhm  22810  monmat2matmon  22814  pm2mp  22815  chpscmatgsumbin  22834  chpscmatgsummon  22835  chfacfscmulcl  22847  chfacfscmul0  22848  chfacfpmmulcl  22851  chfacfpmmul0  22852  chfacfpmmulgsum2  22855  cayhamlem1  22856  cpmadugsumlemB  22864  cpmadugsumlemC  22865  cpmadugsumlemF  22866  cayhamlem2  22874  cayhamlem4  22878  nrgtrg  24680  deg1pw  26111  idomrootle  26163  plypf1  26202  efsubm  26540  amgm  26979  wilthlem2  27057  wilthlem3  27058  dchrelbas3  27226  lgsqrlem2  27335  lgsqrlem3  27336  lgsqrlem4  27337  cntrcrng  33169  psgnid  33185  cnmsgn0g  33234  altgnsg  33237  ringm1expp1  33322  isunit3  33329  elrgspnlem1  33330  elrgspnlem2  33331  elrgspnlem3  33332  elrgspnlem4  33333  elrgspn  33334  0ringcring  33340  domnprodn0  33363  rrgsubm  33372  znfermltl  33456  unitprodclb  33479  ringlsmss  33485  rprmdvdspow  33623  1arithidomlem1  33625  1arithidom  33627  1arithufdlem2  33635  1arithufdlem3  33636  1arithufdlem4  33637  zringfrac  33644  ressply1evls1  33655  evl1deg1  33666  evl1deg2  33667  evl1deg3  33668  evls1monply1  33669  ply1coedeg  33679  gsummoncoe1fzo  33687  vietalem  33770  ply1degltdimlem  33813  ply1degltdim  33814  assarrginv  33827  evls1fldgencl  33861  extdgfialglem1  33883  extdgfialglem2  33884  rtelextdg2lem  33917  2sqr3minply  33971  cos9thpiminplylem6  33978  cos9thpiminply  33979  iistmd  34093  aks6d1c1p2  42601  aks6d1c1p3  42602  aks6d1c1p6  42606  evl1gprodd  42609  aks6d1c2lem3  42618  idomnnzpownz  42624  aks6d1c5lem3  42629  aks6d1c5lem2  42630  deg1pow  42633  aks6d1c6lem1  42662  aks6d1c6lem2  42663  aks5lem2  42679  aks5lem3a  42681  domnexpgn0cl  43016  abvexp  43025  fidomncyc  43028  evlselv  43046  mhphf  43054  hbtlem4  43578  mon1psubm  43651  amgm2d  44649  amgm3d  44650  amgm4d  44651  invginvrid  48865  ply1mulgsumlem4  48887  ply1mulgsum  48888  amgmw2d  50301