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

Theorem mndcl 15737
Description: Closure of the operation of a monoid. (Contributed by NM, 14-Aug-2011.) (Revised by Mario Carneiro, 6-Jan-2015.)
Hypotheses
Ref Expression
mndlem1.b  |-  B  =  ( Base `  G
)
mndlem1.p  |-  .+  =  ( +g  `  G )
Assertion
Ref Expression
mndcl  |-  ( ( G  e.  Mnd  /\  X  e.  B  /\  Y  e.  B )  ->  ( X  .+  Y
)  e.  B )

Proof of Theorem mndcl
StepHypRef Expression
1 df-3an 975 . . . 4  |-  ( ( X  e.  B  /\  Y  e.  B  /\  X  e.  B )  <->  ( ( X  e.  B  /\  Y  e.  B
)  /\  X  e.  B ) )
2 anabs1 806 . . . 4  |-  ( ( ( X  e.  B  /\  Y  e.  B
)  /\  X  e.  B )  <->  ( X  e.  B  /\  Y  e.  B ) )
31, 2bitri 249 . . 3  |-  ( ( X  e.  B  /\  Y  e.  B  /\  X  e.  B )  <->  ( X  e.  B  /\  Y  e.  B )
)
4 mndlem1.b . . . . 5  |-  B  =  ( Base `  G
)
5 mndlem1.p . . . . 5  |-  .+  =  ( +g  `  G )
64, 5mndlem1 15736 . . . 4  |-  ( ( G  e.  Mnd  /\  ( X  e.  B  /\  Y  e.  B  /\  X  e.  B
) )  ->  (
( X  .+  Y
)  e.  B  /\  ( ( X  .+  Y )  .+  X
)  =  ( X 
.+  ( Y  .+  X ) ) ) )
76simpld 459 . . 3  |-  ( ( G  e.  Mnd  /\  ( X  e.  B  /\  Y  e.  B  /\  X  e.  B
) )  ->  ( X  .+  Y )  e.  B )
83, 7sylan2br 476 . 2  |-  ( ( G  e.  Mnd  /\  ( X  e.  B  /\  Y  e.  B
) )  ->  ( X  .+  Y )  e.  B )
983impb 1192 1  |-  ( ( G  e.  Mnd  /\  X  e.  B  /\  Y  e.  B )  ->  ( X  .+  Y
)  e.  B )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 973    = wceq 1379    e. wcel 1767   ` cfv 5588  (class class class)co 6284   Basecbs 14490   +g cplusg 14555   Mndcmnd 15726
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-8 1769  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-nul 4576  ax-pow 4625
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-eu 2279  df-mo 2280  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-ral 2819  df-rex 2820  df-rab 2823  df-v 3115  df-sbc 3332  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-nul 3786  df-if 3940  df-sn 4028  df-pr 4030  df-op 4034  df-uni 4246  df-br 4448  df-iota 5551  df-fv 5596  df-ov 6287  df-mnd 15732
This theorem is referenced by:  mnd4g  15743  mndplusf  15748  mndpropd  15764  issubmnd  15767  prdsplusgcl  15770  imasmnd  15777  mhmf1o  15795  issubmd  15799  0mhm  15808  mhmco  15812  mhmeql  15814  submacs  15815  mrcmndind  15816  prdspjmhm  15817  pwsdiagmhm  15819  pwsco1mhm  15820  pwsco2mhm  15821  gsumccat  15841  gsumwmhm  15845  grpcl  15873  mulgnncl  15967  mulgnn0cl  15968  mulgnndir  15974  cntzsubm  16178  oppgmnd  16194  lsmssv  16469  frgp0  16584  frgpadd  16587  mulgnn0di  16640  mulgmhm  16642  gsumval3eu  16710  gsumval3OLD  16711  gsumval3  16714  gsumzcl2  16718  gsumzclOLD  16722  gsumzaddlem  16737  gsumzaddlemOLD  16739  gsumzmhm  16760  gsumzmhmOLD  16761  gsummptfzcl  16799  srgcl  16966  srgacl  16977  srglmhm  16988  srgrmhm  16989  srgbinomlem  16997  srgbinom  16998  rngcl  17013  rngpropd  17031  gsumply1subr  18074  mndvcl  18688  mhmvlin  18694  mat2pmatghm  19026  pm2mpghm  19112  cpmadugsumlemF  19172  tsmsadd  20412  omndadd2d  27388  omndadd2rd  27389  slmdacl  27442  slmdvacl  27445  gsumncl  28160  ofaddmndmap  32029  lincsum  32129
  Copyright terms: Public domain W3C validator