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

Theorem rngmgp 16637
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 2437 . . 3  |-  ( Base `  R )  =  (
Base `  R )
2 rngmgp.g . . 3  |-  G  =  (mulGrp `  R )
3 eqid 2437 . . 3  |-  ( +g  `  R )  =  ( +g  `  R )
4 eqid 2437 . . 3  |-  ( .r
`  R )  =  ( .r `  R
)
51, 2, 3, 4isrng 16635 . 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 1004 1  |-  ( R  e.  Ring  ->  G  e. 
Mnd )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    = wceq 1369    e. wcel 1756   A.wral 2709   ` cfv 5411  (class class class)co 6086   Basecbs 14166   +g cplusg 14230   .rcmulr 14231   Mndcmnd 15401   Grpcgrp 15402  mulGrpcmgp 16577   Ringcrg 16631
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2418  ax-nul 4414
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2256  df-clab 2424  df-cleq 2430  df-clel 2433  df-nfc 2562  df-ne 2602  df-ral 2714  df-rex 2715  df-rab 2718  df-v 2968  df-sbc 3180  df-dif 3324  df-un 3326  df-in 3328  df-ss 3335  df-nul 3631  df-if 3785  df-sn 3871  df-pr 3873  df-op 3877  df-uni 4085  df-br 4286  df-iota 5374  df-fv 5419  df-ov 6089  df-rng 16633
This theorem is referenced by:  mgpf  16642  rngcl  16644  iscrng2  16646  rngass  16647  rngideu  16648  rngidcl  16651  rngidmlem  16653  unitsubm  16748  dfrhm2  16794  isrhm2d  16802  pwsco1rhm  16806  pwsco2rhm  16807  subrgcrng  16845  subrgsubm  16854  issubrg3  16869  cntzsubr  16873  pwsdiagrhm  16874  psrcrng  17459  mplcoe3  17519  mplcoe3OLD  17520  ply1tmcl  17696  coe1pwmul  17703  ply1coe  17716  evls1gsummul  17729  evl1expd  17748  evl1gsummul  17763  evl1scvarpw  17766  evl1scvarpwval  17767  evl1gsummon  17768  cnfldexp  17818  expmhm  17849  nn0srg  17850  rge0srg  17851  rngvcl  18267  mdet1  18377  m2detleiblem2  18403  nrgtrg  20239  deg1pwle  21560  deg1pw  21561  plypf1  21649  amgm  22353  wilthlem2  22376  wilthlem3  22377  dchrelbas3  22546  lgsqrlem2  22650  lgsqrlem3  22651  lgsqrlem4  22652  iistmd  26280  hbtlem4  29425  subrgacs  29500  idomrootle  29503  isdomn3  29515  mon1psubm  29517  invginvrid  30707  assamulgscmlem2  30740  ply1moncl  30745  ply1coefsupp  30753  lply1binomsc  30755  m1detdiag  30793  mdetdiaglem  30794
  Copyright terms: Public domain W3C validator