Theorem mndcl 17124

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

Step	Hyp	Ref	Expression
1		mndmgm 17123	. 2 ⊢ (𝐺 ∈ Mnd → 𝐺 ∈ Mgm)
2		mndcl.b	. . 3 ⊢ 𝐵 = (Base‘𝐺)
3		mndcl.p	. . 3 ⊢ + = (+g‘𝐺)
4	2, 3	mgmcl 17068	. 2 ⊢ ((𝐺 ∈ Mgm ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 + 𝑌) ∈ 𝐵)
5	1, 4	syl3an1 1351	1 ⊢ ((𝐺 ∈ Mnd ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 + 𝑌) ∈ 𝐵)

Syntax hints:   → wi 4   ∧ w3a 1031   = wceq 1475   ∈ wcel 1977  ‘cfv 5804  (class class class)co 6549  Basecbs 15695  +_gcplusg 15768  Mgmcmgm 17063  Mndcmnd 17117

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-nul 4717

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ral 2901  df-rex 2902  df-rab 2905  df-v 3175  df-sbc 3403  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-br 4584  df-iota 5768  df-fv 5812  df-ov 6552  df-mgm 17065  df-sgrp 17107  df-mnd 17118

This theorem is referenced by:  mnd4g  17130  mndpropd  17139  issubmnd  17141  prdsplusgcl  17144  imasmnd  17151  idmhm  17167  mhmf1o  17168  issubmd  17172  0mhm  17181  mhmco  17185  mhmeql  17187  submacs  17188  mrcmndind  17189  prdspjmhm  17190  pwsdiagmhm  17192  pwsco1mhm  17193  pwsco2mhm  17194  gsumccat  17201  gsumwmhm  17205  grpcl  17253  mhmmnd  17360  mulgnnclOLD  17380  mulgnn0cl  17381  mulgnndirOLD  17393  cntzsubm  17591  oppgmnd  17607  lsmssv  17881  frgp0  17996  frgpadd  17999  mulgnn0di  18054  mulgmhm  18056  gsumval3eu  18128  gsumval3  18131  gsumzcl2  18134  gsumzaddlem  18144  gsumzmhm  18160  gsummptfzcl  18191  srgcl  18335  srgacl  18347  srgbinomlem  18367  srgbinom  18368  ringcl  18384  ringpropd  18405  mndvcl  20016  mhmvlin  20022  mat2pmatghm  20354  pm2mpghm  20440  cpmadugsumlemF  20500  tsmsadd  21760  omndadd2d  29039  omndadd2rd  29040  slmdacl  29093  slmdvacl  29096  gsumncl  29941  c0mhm  41700  ofaddmndmap  41915  lincsum  42012