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

Theorem rngmgp 16654
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 2443 . . 3  |-  ( Base `  R )  =  (
Base `  R )
2 rngmgp.g . . 3  |-  G  =  (mulGrp `  R )
3 eqid 2443 . . 3  |-  ( +g  `  R )  =  ( +g  `  R )
4 eqid 2443 . . 3  |-  ( .r
`  R )  =  ( .r `  R
)
51, 2, 3, 4isrng 16652 . 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 2718   ` cfv 5421  (class class class)co 6094   Basecbs 14177   +g cplusg 14241   .rcmulr 14242   Mndcmnd 15412   Grpcgrp 15413  mulGrpcmgp 16594   Ringcrg 16648
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 2423  ax-nul 4424
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 2257  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2571  df-ne 2611  df-ral 2723  df-rex 2724  df-rab 2727  df-v 2977  df-sbc 3190  df-dif 3334  df-un 3336  df-in 3338  df-ss 3345  df-nul 3641  df-if 3795  df-sn 3881  df-pr 3883  df-op 3887  df-uni 4095  df-br 4296  df-iota 5384  df-fv 5429  df-ov 6097  df-rng 16650
This theorem is referenced by:  mgpf  16659  rngcl  16661  iscrng2  16663  rngass  16664  rngideu  16665  rngidcl  16668  rngidmlem  16670  unitsubm  16765  dfrhm2  16811  isrhm2d  16821  pwsco1rhm  16829  pwsco2rhm  16830  subrgcrng  16872  subrgsubm  16881  issubrg3  16896  cntzsubr  16900  pwsdiagrhm  16901  psrcrng  17488  mplcoe3  17548  mplcoe3OLD  17549  mplcoe5lem  17550  mplcoe5  17551  ply1tmcl  17728  coe1pwmul  17735  ply1coefsupp  17748  ply1coe  17749  ply1coeOLD  17750  evls1gsummul  17763  evl1expd  17782  evl1gsummul  17797  evl1scvarpw  17800  evl1scvarpwval  17801  evl1gsummon  17802  cnfldexp  17852  expmhm  17883  nn0srg  17884  rge0srg  17885  rngvcl  18301  mdet1  18411  m2detleiblem2  18437  nrgtrg  20273  deg1pwle  21594  deg1pw  21595  plypf1  21683  amgm  22387  wilthlem2  22410  wilthlem3  22411  dchrelbas3  22580  lgsqrlem2  22684  lgsqrlem3  22685  lgsqrlem4  22686  iistmd  26335  hbtlem4  29485  subrgacs  29560  idomrootle  29563  isdomn3  29575  mon1psubm  29577  invginvrid  30775  assamulgscmlem2  30824  ply1moncl  30829  mon1ply1  30843  gsummoncoe1  30846  ply1mulgsumlem4  30850  ply1mulgsum  30851  lply1binomsc  30855  mply1topmatcllem  30896  mply1topmatcl  30898  pmatcollpw1id  30902  pmatcollpw1lem4  30905  pmatcollpw1  30907  pmatcollpw2lem  30908  pmatcollpw2  30909  pmattomply1ghmlem1  30910  pmattomply1rn  30915  idpmattoidmply1  30918  mp2pm2mplem2  30920  mp2pm2mplem4  30922  pmattomply1ghm  30928  pmattomply1mhmlem1  30931  pmattomply1mhmlem2  30932  pmattomply1mhm  30933  m1detdiag  30937  mdetdiaglem  30938
  Copyright terms: Public domain W3C validator