Theorem ringmgp 18774

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 18772	. 2 ⊢ (𝑅 ∈ Ring ↔ (𝑅 ∈ Grp ∧ 𝐺 ∈ Mnd ∧ ∀𝑥 ∈ (Base‘𝑅)∀𝑦 ∈ (Base‘𝑅)∀𝑧 ∈ (Base‘𝑅)((𝑥(.r‘𝑅)(𝑦(+g‘𝑅)𝑧)) = ((𝑥(.r‘𝑅)𝑦)(+g‘𝑅)(𝑥(.r‘𝑅)𝑧)) ∧ ((𝑥(+g‘𝑅)𝑦)(.r‘𝑅)𝑧) = ((𝑥(.r‘𝑅)𝑧)(+g‘𝑅)(𝑦(.r‘𝑅)𝑧)))))
6	5	simp2bi 1141	1 ⊢ (𝑅 ∈ Ring → 𝐺 ∈ Mnd)

Syntax hints:   → wi 4   ∧ wa 383   = wceq 1632   ∈ wcel 2140  ∀wral 3051  ‘cfv 6050  (class class class)co 6815  Basecbs 16080  +_gcplusg 16164  ._rcmulr 16165  Mndcmnd 17516  Grpcgrp 17644  mulGrpcmgp 18710  Ringcrg 18768

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1989  ax-6 2055  ax-7 2091  ax-9 2149  ax-10 2169  ax-11 2184  ax-12 2197  ax-13 2392  ax-ext 2741  ax-nul 4942

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2048  df-eu 2612  df-clab 2748  df-cleq 2754  df-clel 2757  df-nfc 2892  df-ral 3056  df-rex 3057  df-rab 3060  df-v 3343  df-sbc 3578  df-dif 3719  df-un 3721  df-in 3723  df-ss 3730  df-nul 4060  df-if 4232  df-sn 4323  df-pr 4325  df-op 4329  df-uni 4590  df-br 4806  df-iota 6013  df-fv 6058  df-ov 6818  df-ring 18770

This theorem is referenced by:  mgpf  18780  ringcl  18782  iscrng2  18784  ringass  18785  ringideu  18786  ringidcl  18789  ringidmlem  18791  ringsrg  18810  unitsubm  18891  dfrhm2  18940  isrhm2d  18951  idrhm  18954  pwsco1rhm  18961  pwsco2rhm  18962  subrgcrng  19007  subrgsubm  19016  issubrg3  19031  cntzsubr  19035  pwsdiagrhm  19036  assamulgscmlem2  19572  psrcrng  19636  mplcoe3  19689  mplcoe5lem  19690  mplcoe5  19691  ply1moncl  19864  coe1pwmul  19872  ply1coefsupp  19888  ply1coe  19889  gsummoncoe1  19897  lply1binomsc  19900  evls1gsummul  19913  evl1expd  19932  evl1gsummul  19947  evl1scvarpw  19950  evl1scvarpwval  19951  evl1gsummon  19952  cnfldexp  20002  expmhm  20038  nn0srg  20039  rge0srg  20040  ringvcl  20427  mat1mhm  20513  scmatmhm  20563  m1detdiag  20626  mdetdiaglem  20627  m2detleiblem2  20657  mat2pmatmhm  20761  pmatcollpwscmatlem1  20817  mply1topmatcllem  20831  mply1topmatcl  20833  pm2mpghm  20844  pm2mpmhm  20848  monmat2matmon  20852  pm2mp  20853  chpscmatgsumbin  20872  chpscmatgsummon  20873  chfacfscmulcl  20885  chfacfscmul0  20886  chfacfpmmulcl  20889  chfacfpmmul0  20890  chfacfpmmulgsum2  20893  cayhamlem1  20894  cpmadugsumlemB  20902  cpmadugsumlemC  20903  cpmadugsumlemF  20904  cayhamlem2  20912  cayhamlem4  20916  nrgtrg  22716  deg1pw  24100  plypf1  24188  efsubm  24518  amgm  24938  wilthlem2  25016  wilthlem3  25017  dchrelbas3  25184  lgsqrlem2  25293  lgsqrlem3  25294  lgsqrlem4  25295  psgnid  30178  iistmd  30279  hbtlem4  38217  subrgacs  38291  idomrootle  38294  isdomn3  38303  mon1psubm  38305  amgm2d  39022  amgm3d  39023  amgm4d  39024  c0rhm  42441  c0rnghm  42442  lidlmsgrp  42455  invginvrid  42677  ply1mulgsumlem4  42706  ply1mulgsum  42707  amgmw2d  43082