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

Theorem mndcl 16550
Description: Closure of the operation of a monoid. (Contributed by NM, 14-Aug-2011.) (Revised by Mario Carneiro, 6-Jan-2015.) (Proof shortened by AV, 8-Feb-2020.)
Hypotheses
Ref Expression
mndcl.b  |-  B  =  ( Base `  G
)
mndcl.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 mndmgm 16549 . 2  |-  ( G  e.  Mnd  ->  G  e. Mgm )
2 mndcl.b . . 3  |-  B  =  ( Base `  G
)
3 mndcl.p . . 3  |-  .+  =  ( +g  `  G )
42, 3mgmcl 16496 . 2  |-  ( ( G  e. Mgm  /\  X  e.  B  /\  Y  e.  B )  ->  ( X  .+  Y )  e.  B )
51, 4syl3an1 1298 1  |-  ( ( G  e.  Mnd  /\  X  e.  B  /\  Y  e.  B )  ->  ( X  .+  Y
)  e.  B )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ w3a 983    = wceq 1438    e. wcel 1873   ` cfv 5607  (class class class)co 6311   Basecbs 15126   +g cplusg 15195  Mgmcmgm 16491   Mndcmnd 16540
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1664  ax-4 1677  ax-5 1753  ax-6 1799  ax-7 1844  ax-10 1892  ax-11 1897  ax-12 1910  ax-13 2058  ax-ext 2402  ax-nul 4561
This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3an 985  df-tru 1441  df-ex 1659  df-nf 1663  df-sb 1792  df-eu 2274  df-clab 2409  df-cleq 2415  df-clel 2418  df-nfc 2573  df-ne 2621  df-ral 2781  df-rex 2782  df-rab 2785  df-v 3087  df-sbc 3306  df-dif 3445  df-un 3447  df-in 3449  df-ss 3456  df-nul 3768  df-if 3918  df-sn 4005  df-pr 4007  df-op 4011  df-uni 4226  df-br 4430  df-iota 5571  df-fv 5615  df-ov 6314  df-mgm 16493  df-sgrp 16532  df-mnd 16542
This theorem is referenced by:  mnd4g  16558  mndpropd  16567  issubmnd  16569  prdsplusgcl  16572  imasmnd  16579  idmhm  16596  mhmf1o  16597  issubmd  16601  0mhm  16610  mhmco  16614  mhmeql  16616  submacs  16617  mrcmndind  16618  prdspjmhm  16619  pwsdiagmhm  16621  pwsco1mhm  16622  pwsco2mhm  16623  gsumccat  16630  gsumwmhm  16634  grpcl  16684  mulgnncl  16778  mulgnn0cl  16779  mulgnndir  16785  mhmmnd  16813  cntzsubm  16994  oppgmnd  17010  lsmssv  17300  frgp0  17415  frgpadd  17418  mulgnn0di  17471  mulgmhm  17473  gsumval3eu  17543  gsumval3  17546  gsumzcl2  17549  gsumzaddlem  17559  gsumzmhm  17575  gsummptfzcl  17606  srgcl  17751  srgacl  17762  srgbinomlem  17782  srgbinom  17783  ringcl  17799  ringpropd  17817  mndvcl  19420  mhmvlin  19426  mat2pmatghm  19758  pm2mpghm  19844  cpmadugsumlemF  19904  tsmsadd  21165  omndadd2d  28484  omndadd2rd  28485  slmdacl  28538  slmdvacl  28541  gsumncl  29438  c0mhm  39527  ofaddmndmap  39744  lincsum  39841
  Copyright terms: Public domain W3C validator