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

Theorem mndcl 14388
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 936 . . . 4  |-  ( ( X  e.  B  /\  Y  e.  B  /\  X  e.  B )  <->  ( ( X  e.  B  /\  Y  e.  B
)  /\  X  e.  B ) )
2 anabs1 783 . . . 4  |-  ( ( ( X  e.  B  /\  Y  e.  B
)  /\  X  e.  B )  <->  ( X  e.  B  /\  Y  e.  B ) )
31, 2bitri 240 . . 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 14387 . . . 4  |-  ( ( G  e.  Mnd  /\  ( X  e.  B  /\  Y  e.  B  /\  X  e.  B
) )  ->  (
( X  .+  Y
)  e.  B  /\  ( ( X  .+  Y )  .+  X
)  =  ( X 
.+  ( Y  .+  X ) ) ) )
76simpld 445 . . 3  |-  ( ( G  e.  Mnd  /\  ( X  e.  B  /\  Y  e.  B  /\  X  e.  B
) )  ->  ( X  .+  Y )  e.  B )
83, 7sylan2br 462 . 2  |-  ( ( G  e.  Mnd  /\  ( X  e.  B  /\  Y  e.  B
) )  ->  ( X  .+  Y )  e.  B )
983impb 1147 1  |-  ( ( G  e.  Mnd  /\  X  e.  B  /\  Y  e.  B )  ->  ( X  .+  Y
)  e.  B )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    /\ w3a 934    = wceq 1632    e. wcel 1696   ` cfv 5271  (class class class)co 5874   Basecbs 13164   +g cplusg 13224   Mndcmnd 14377
This theorem is referenced by:  mnd4g  14394  mndplusf  14399  mndfo  14413  mndpropd  14414  issubmnd  14417  prdsplusgcl  14419  imasmnd  14426  0mhm  14451  mhmco  14455  mhmeql  14457  submacs  14458  prdspjmhm  14459  pwsdiagmhm  14461  pwsco1mhm  14462  pwsco2mhm  14463  gsumccat  14480  gsumwmhm  14483  grpcl  14511  mulgnncl  14598  mulgnn0cl  14599  mulgnndir  14605  cntzsubm  14827  oppgmnd  14843  lsmssv  14970  frgp0  15085  frgpadd  15088  mulgnn0di  15141  mulgmhm  15143  gsumval3eu  15206  gsumval3  15207  gsumzcl  15211  gsumzaddlem  15219  gsumzmhm  15226  rngcl  15370  rngpropd  15388  tsmsadd  17845  issubmd  27486  mndvcl  27549  mhmvlin  27555
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-13 1698  ax-14 1700  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277  ax-nul 4165  ax-pow 4204
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-eu 2160  df-mo 2161  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-ne 2461  df-ral 2561  df-rex 2562  df-rab 2565  df-v 2803  df-sbc 3005  df-dif 3168  df-un 3170  df-in 3172  df-ss 3179  df-nul 3469  df-if 3579  df-sn 3659  df-pr 3660  df-op 3662  df-uni 3844  df-br 4040  df-iota 5235  df-fv 5279  df-ov 5877  df-mnd 14383
  Copyright terms: Public domain W3C validator