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

Theorem mndcl 15420
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 967 . . . 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 15419 . . . 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 1183 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 965    = wceq 1369    e. wcel 1756   ` cfv 5418  (class class class)co 6091   Basecbs 14174   +g cplusg 14238   Mndcmnd 15409
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-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-nul 4421  ax-pow 4470
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-mo 2258  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2568  df-ne 2608  df-ral 2720  df-rex 2721  df-rab 2724  df-v 2974  df-sbc 3187  df-dif 3331  df-un 3333  df-in 3335  df-ss 3342  df-nul 3638  df-if 3792  df-sn 3878  df-pr 3880  df-op 3884  df-uni 4092  df-br 4293  df-iota 5381  df-fv 5426  df-ov 6094  df-mnd 15415
This theorem is referenced by:  mnd4g  15426  mndplusf  15431  mndfo  15445  mndpropd  15446  issubmnd  15449  prdsplusgcl  15452  imasmnd  15459  mhmf1o  15473  issubmd  15477  0mhm  15486  mhmco  15490  mhmeql  15492  submacs  15493  mrcmndind  15494  prdspjmhm  15495  pwsdiagmhm  15497  pwsco1mhm  15498  pwsco2mhm  15499  gsumccat  15519  gsumwmhm  15523  grpcl  15551  mulgnncl  15642  mulgnn0cl  15643  mulgnndir  15649  cntzsubm  15853  oppgmnd  15869  lsmssv  16142  frgp0  16257  frgpadd  16260  mulgnn0di  16313  mulgmhm  16315  gsumval3eu  16381  gsumval3OLD  16382  gsumval3  16385  gsumzcl2  16389  gsumzclOLD  16393  gsumzaddlem  16408  gsumzaddlemOLD  16410  gsumzmhm  16430  gsumzmhmOLD  16431  gsummptfzcl  16460  srgcl  16614  srgacl  16625  srglmhm  16634  srgrmhm  16635  srgbinomlem  16642  srgbinom  16643  rngcl  16658  rngpropd  16676  gsumply1subr  17688  mndvcl  18291  mhmvlin  18297  tsmsadd  19721  omndadd2d  26171  omndadd2rd  26172  slmdacl  26225  slmdvacl  26228  gsumncl  26936  ofaddmndmap  30734  pmattomply1ghm  30925  lincsum  30963
  Copyright terms: Public domain W3C validator