MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  rngmgp Structured version   Unicode version

Theorem rngmgp 16985
Description: A ring is a monoid under multiplication. (Contributed by Mario Carneiro, 6-Jan-2015.)
Hypothesis
Ref Expression
rngmgp.g  |-  G  =  (mulGrp `  R )
Assertion
Ref Expression
rngmgp  |-  ( R  e.  Ring  ->  G  e. 
Mnd )

Proof of Theorem rngmgp
Dummy variables  x  y  z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eqid 2460 . . 3  |-  ( Base `  R )  =  (
Base `  R )
2 rngmgp.g . . 3  |-  G  =  (mulGrp `  R )
3 eqid 2460 . . 3  |-  ( +g  `  R )  =  ( +g  `  R )
4 eqid 2460 . . 3  |-  ( .r
`  R )  =  ( .r `  R
)
51, 2, 3, 4isrng 16983 . 2  |-  ( R  e.  Ring  <->  ( R  e. 
Grp  /\  G  e.  Mnd  /\  A. x  e.  ( Base `  R
) A. y  e.  ( Base `  R
) A. z  e.  ( Base `  R
) ( ( x ( .r `  R
) ( y ( +g  `  R ) z ) )  =  ( ( x ( .r `  R ) y ) ( +g  `  R ) ( x ( .r `  R
) z ) )  /\  ( ( x ( +g  `  R
) y ) ( .r `  R ) z )  =  ( ( x ( .r
`  R ) z ) ( +g  `  R
) ( y ( .r `  R ) z ) ) ) ) )
65simp2bi 1007 1  |-  ( R  e.  Ring  ->  G  e. 
Mnd )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    = wceq 1374    e. wcel 1762   A.wral 2807   ` cfv 5579  (class class class)co 6275   Basecbs 14479   +g cplusg 14544   .rcmulr 14545   Mndcmnd 15715   Grpcgrp 15716  mulGrpcmgp 16924   Ringcrg 16979
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1961  ax-ext 2438  ax-nul 4569
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 970  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-eu 2272  df-clab 2446  df-cleq 2452  df-clel 2455  df-nfc 2610  df-ne 2657  df-ral 2812  df-rex 2813  df-rab 2816  df-v 3108  df-sbc 3325  df-dif 3472  df-un 3474  df-in 3476  df-ss 3483  df-nul 3779  df-if 3933  df-sn 4021  df-pr 4023  df-op 4027  df-uni 4239  df-br 4441  df-iota 5542  df-fv 5587  df-ov 6278  df-rng 16981
This theorem is referenced by:  mgpf  16990  rngcl  16992  iscrng2  16994  rngass  16995  rngideu  16996  rngidcl  16999  rngidmlem  17001  unitsubm  17096  dfrhm2  17143  isrhm2d  17154  pwsco1rhm  17163  pwsco2rhm  17164  subrgcrng  17209  subrgsubm  17218  issubrg3  17233  cntzsubr  17237  pwsdiagrhm  17238  assamulgscmlem2  17762  psrcrng  17832  mplcoe3  17892  mplcoe3OLD  17893  mplcoe5lem  17894  mplcoe5  17895  ply1moncl  18076  coe1pwmul  18084  ply1coefsupp  18100  ply1coe  18101  ply1coeOLD  18102  gsummoncoe1  18110  lply1binomsc  18113  evls1gsummul  18126  evl1expd  18145  evl1gsummul  18160  evl1scvarpw  18163  evl1scvarpwval  18164  evl1gsummon  18165  cnfldexp  18215  expmhm  18246  nn0srg  18247  rge0srg  18248  rngvcl  18660  mat1mhm  18746  scmatmhm  18796  m1detdiag  18859  mdetdiaglem  18860  m2detleiblem2  18890  mat2pmatmhm  18994  pmatcollpwscmatlem1  19050  mply1topmatcllem  19064  mply1topmatcl  19066  pm2mpghm  19077  pm2mpmhm  19081  monmat2matmon  19085  pm2mp  19086  chpscmatgsumbin  19105  chpscmatgsummon  19106  chfacfscmulcl  19118  chfacfscmul0  19119  chfacfpmmulcl  19122  chfacfpmmul0  19123  chfacfpmmulgsum2  19126  cayhamlem1  19127  cpmadugsumlemB  19135  cpmadugsumlemC  19136  cpmadugsumlemF  19137  cayhamlem2  19145  cayhamlem4  19149  nrgtrg  20926  deg1pwle  22248  deg1pw  22249  plypf1  22337  amgm  23041  wilthlem2  23064  wilthlem3  23065  dchrelbas3  23234  lgsqrlem2  23338  lgsqrlem3  23339  lgsqrlem4  23340  iistmd  27506  hbtlem4  30668  subrgacs  30743  idomrootle  30746  isdomn3  30758  mon1psubm  30760  invginvrid  31900  ply1mulgsumlem4  31937  ply1mulgsum  31938
  Copyright terms: Public domain W3C validator