Theorem ringmgp 19302

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

Syntax hints:   → wi 4   ∧ wa 398   = wceq 1533   ∈ wcel 2110  ∀wral 3138  ‘cfv 6354  (class class class)co 7155  Basecbs 16482  +_gcplusg 16564  ._rcmulr 16565  Mndcmnd 17910  Grpcgrp 18102  mulGrpcmgp 19238  Ringcrg 19296

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793  ax-nul 5209

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-mo 2618  df-eu 2650  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3496  df-sbc 3772  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-nul 4291  df-if 4467  df-sn 4567  df-pr 4569  df-op 4573  df-uni 4838  df-br 5066  df-iota 6313  df-fv 6362  df-ov 7158  df-ring 19298

This theorem is referenced by:  mgpf  19308  ringcl  19310  iscrng2  19312  ringass  19313  ringideu  19314  ringidcl  19317  ringidmlem  19319  ringsrg  19338  unitsubm  19419  dfrhm2  19468  isrhm2d  19479  idrhm  19482  pwsco1rhm  19489  pwsco2rhm  19490  subrgcrng  19538  subrgsubm  19547  issubrg3  19562  cntzsubr  19567  pwsdiagrhm  19568  subrgacs  19578  assamulgscmlem2  20128  psrcrng  20192  mplcoe3  20246  mplcoe5lem  20247  mplcoe5  20248  evlsgsummul  20304  ply1moncl  20438  coe1pwmul  20446  ply1coefsupp  20462  ply1coe  20463  gsummoncoe1  20471  lply1binomsc  20474  evls1gsummul  20487  evl1expd  20507  evl1gsummul  20522  evl1scvarpw  20525  evl1scvarpwval  20526  evl1gsummon  20527  cnfldexp  20577  expmhm  20613  nn0srg  20614  rge0srg  20615  ringvcl  21008  mat1mhm  21092  scmatmhm  21142  m1detdiag  21205  mdetdiaglem  21206  m2detleiblem2  21236  mat2pmatmhm  21340  pmatcollpwscmatlem1  21396  mply1topmatcllem  21410  mply1topmatcl  21412  pm2mpghm  21423  pm2mpmhm  21427  monmat2matmon  21431  pm2mp  21432  chpscmatgsumbin  21451  chpscmatgsummon  21452  chfacfscmulcl  21464  chfacfscmul0  21465  chfacfpmmulcl  21468  chfacfpmmul0  21469  chfacfpmmulgsum2  21472  cayhamlem1  21473  cpmadugsumlemB  21481  cpmadugsumlemC  21482  cpmadugsumlemF  21483  cayhamlem2  21491  cayhamlem4  21495  nrgtrg  23298  deg1pw  24713  plypf1  24801  efsubm  25134  amgm  25567  wilthlem2  25645  wilthlem3  25646  dchrelbas3  25813  lgsqrlem2  25922  lgsqrlem3  25923  lgsqrlem4  25924  cntrcrng  30697  psgnid  30739  cnmsgn0g  30788  altgnsg  30791  freshmansdream  30859  ringlsmss  30947  iistmd  31145  hbtlem4  39724  idomrootle  39793  isdomn3  39802  mon1psubm  39804  amgm2d  40549  amgm3d  40550  amgm4d  40551  c0rhm  44182  c0rnghm  44183  lidlmsgrp  44196  invginvrid  44414  ply1mulgsumlem4  44442  ply1mulgsum  44443  amgmw2d  44904