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

Theorem mndcl 17897
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 𝐵 = (Base‘𝐺)
mndcl.p + = (+g𝐺)
Assertion
Ref Expression
mndcl ((𝐺 ∈ Mnd ∧ 𝑋𝐵𝑌𝐵) → (𝑋 + 𝑌) ∈ 𝐵)

Proof of Theorem mndcl
StepHypRef Expression
1 mndmgm 17896 . 2 (𝐺 ∈ Mnd → 𝐺 ∈ Mgm)
2 mndcl.b . . 3 𝐵 = (Base‘𝐺)
3 mndcl.p . . 3 + = (+g𝐺)
42, 3mgmcl 17833 . 2 ((𝐺 ∈ Mgm ∧ 𝑋𝐵𝑌𝐵) → (𝑋 + 𝑌) ∈ 𝐵)
51, 4syl3an1 1160 1 ((𝐺 ∈ Mnd ∧ 𝑋𝐵𝑌𝐵) → (𝑋 + 𝑌) ∈ 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1084   = wceq 1538  wcel 2115  cfv 6328  (class class class)co 7130  Basecbs 16461  +gcplusg 16543  Mgmcmgm 17828  Mndcmnd 17889
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2178  ax-ext 2793  ax-nul 5183
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2071  df-mo 2623  df-eu 2654  df-clab 2800  df-cleq 2814  df-clel 2892  df-nfc 2960  df-ral 3131  df-rex 3132  df-rab 3135  df-v 3473  df-sbc 3750  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-nul 4267  df-if 4441  df-sn 4541  df-pr 4543  df-op 4547  df-uni 4812  df-br 5040  df-iota 6287  df-fv 6336  df-ov 7133  df-mgm 17830  df-sgrp 17879  df-mnd 17890
This theorem is referenced by:  mnd4g  17903  mndpropd  17914  issubmnd  17916  prdsplusgcl  17920  imasmnd  17927  idmhm  17943  mhmf1o  17944  issubmd  17949  0mhm  17962  mhmco  17966  mhmeql  17968  submacs  17969  mndind  17970  prdspjmhm  17971  pwsdiagmhm  17973  pwsco1mhm  17974  pwsco2mhm  17975  gsumccatOLD  17983  gsumwmhm  17988  grpcl  18089  mhmmnd  18199  mulgnn0cl  18222  cntzsubm  18444  oppgmnd  18460  lsmssv  18746  frgp0  18864  frgpadd  18867  mulgnn0di  18924  mulgmhm  18926  gsumval3eu  19002  gsumval3  19005  gsumzcl2  19008  gsumzaddlem  19019  gsumzmhm  19035  gsummptfzcl  19067  srgcl  19240  srgacl  19252  srgbinomlem  19272  srgbinom  19273  ringcl  19289  ringpropd  19310  mndvcl  20977  mhmvlin  20983  mat2pmatghm  21313  pm2mpghm  21399  cpmadugsumlemF  21459  tsmsadd  22730  omndadd2d  30716  omndadd2rd  30717  slmdacl  30844  slmdvacl  30847  gsumncl  31817  c0mhm  44328  ofaddmndmap  44539  lincsum  44631
  Copyright terms: Public domain W3C validator