Theorem mndcl 18799

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 18798	. 2 ⊢ (𝐺 ∈ Mnd → 𝐺 ∈ Mgm)
2		mndcl.b	. . 3 ⊢ 𝐵 = (Base‘𝐺)
3		mndcl.p	. . 3 ⊢ + = (+g‘𝐺)
4	2, 3	mgmcl 18700	. 2 ⊢ ((𝐺 ∈ Mgm ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 + 𝑌) ∈ 𝐵)
5	1, 4	syl3an1 1179	1 ⊢ ((𝐺 ∈ Mnd ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 + 𝑌) ∈ 𝐵)

Syntax hints:   → wi 4   ∧ w3a 1101   = wceq 1567   ∈ wcel 2149  ‘cfv 6537  (class class class)co 7411  Basecbs 17268  +_gcplusg 17309  Mgmcmgm 18695  Mndcmnd 18791

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741  ax-nul 5271

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-ne 2965  df-ral 3086  df-rex 3096  df-rab 3424  df-v 3465  df-sbc 3754  df-dif 3916  df-un 3918  df-ss 3930  df-nul 4295  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4877  df-br 5114  df-iota 6493  df-fv 6545  df-ov 7414  df-mgm 18697  df-sgrp 18776  df-mnd 18792

This theorem is referenced by:  mnd4g  18805  mndpropd  18816  issubmnd  18818  prdsplusgcl  18825  imasmnd  18832  xpsmnd0  18835  idmhm  18852  mhmf1o  18853  mndvcl  18854  mhmvlin  18858  issubmd  18863  0mhm  18877  mhmco  18881  mhmeql  18884  submacs  18885  mndind  18886  prdspjmhm  18887  pwsdiagmhm  18889  pwsco1mhm  18890  pwsco2mhm  18891  gsumwmhm  18903  grpcl  19007  mhmmnd  19129  mulgnn0cl  19155  cntzsubm  19407  oppgmnd  19423  lsmssv  19712  frgp0  19829  frgpadd  19832  mulgnn0di  19894  mulgmhm  19896  gsumval3eu  19973  gsumval3  19976  gsumzcl2  19979  gsumzaddlem  19990  gsumzmhm  20006  gsummptfzcl  20038  omndadd2d  20199  omndadd2rd  20200  srgcl  20274  srgacl  20286  srgbinomlem  20311  srgbinom  20312  ringcl  20331  ringpropd  20370  c0mhm  20541  mat2pmatghm  22855  pm2mpghm  22941  cpmadugsumlemF  23001  tsmsadd  24272  mndcld  33282  cmn246135  33293  cmn145236  33294  slmdacl  33469  slmdvacl  33472  gsumncl  34874  primrootsunit1  42753  aks6d1c1  42772  aks6d1c5lem0  42791  aks6d1c5lem3  42793  aks6d1c5lem2  42794  aks6d1c5  42795  aks6d1c6lem1  42826  ofaddmndmap  49007  lincsum  49093  mndtccatid  50249