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

Theorem rngmgp 15347
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 2283 . . 3  |-  ( Base `  R )  =  (
Base `  R )
2 rngmgp.g . . 3  |-  G  =  (mulGrp `  R )
3 eqid 2283 . . 3  |-  ( +g  `  R )  =  ( +g  `  R )
4 eqid 2283 . . 3  |-  ( .r
`  R )  =  ( .r `  R
)
51, 2, 3, 4isrng 15345 . 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 971 1  |-  ( R  e.  Ring  ->  G  e. 
Mnd )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    = wceq 1623    e. wcel 1684   A.wral 2543   ` cfv 5255  (class class class)co 5858   Basecbs 13148   +g cplusg 13208   .rcmulr 13209   Mndcmnd 14361   Grpcgrp 14362  mulGrpcmgp 15325   Ringcrg 15337
This theorem is referenced by:  mgpf  15352  rngcl  15354  iscrng2  15356  rngass  15357  rngideu  15358  rngidcl  15361  rngidmlem  15363  unitsubm  15452  dfrhm2  15498  isrhm2d  15506  pwsco1rhm  15510  pwsco2rhm  15511  subrgcrng  15549  subrgsubm  15558  issubrg3  15573  cntzsubr  15577  pwsdiagrhm  15578  psrcrng  16157  mplcoe3  16210  ply1tmcl  16348  coe1pwmul  16355  ply1coe  16368  cnfldexp  16407  expmhm  16449  nrgtrg  18200  evl1expd  19421  deg1pwle  19505  deg1pw  19506  plypf1  19594  amgm  20285  wilthlem2  20307  wilthlem3  20308  dchrelbas3  20477  lgsqrlem2  20581  lgsqrlem3  20582  lgsqrlem4  20583  iistmd  23286  hbtlem4  27330  rngvcl  27453  subrgacs  27508  idomrootle  27511  isdomn3  27523  mon1psubm  27525
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264  ax-nul 4149
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-eu 2147  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ne 2448  df-ral 2548  df-rex 2549  df-rab 2552  df-v 2790  df-sbc 2992  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3456  df-if 3566  df-sn 3646  df-pr 3647  df-op 3649  df-uni 3828  df-br 4024  df-iota 5219  df-fv 5263  df-ov 5861  df-rng 15340
  Copyright terms: Public domain W3C validator