Theorem mndcl 18844

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

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1103   = wceq 1570   ∈ wcel 2145  ‘cfv 6533  (class class class)co 7413  Basecbs 17301  +_gcplusg 17342  Mgmcmgm 18728  Mndcmnd 18836

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732  ax-nul 5263

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-ne 2956  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-sbc 3740  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-iota 6489  df-fv 6541  df-ov 7416  df-mgm 18730  df-sgrp 18821  df-mnd 18837

This theorem is used by:  mnd4g  18851  mndpropd  18864  issubmnd  18866  prdsplusgcl  18875  imasmnd  18882  xpsmnd0  18885  idmhm  18903  mhmf1o  18904  mndvcl  18905  mhmvlin  18909  issubmd  18914  0mhm  18928  mhmco  18932  mhmeql  18935  submacs  18936  mndind  18937  prdspjmhm  18938  pwsdiagmhm  18940  pwsco1mhm  18941  pwsco2mhm  18942  gsumwmhm  18954  grpcl  19065  mhmmnd  19187  mulgnn0cl  19213  cntzsubm  19465  oppgmnd  19481  lsmssv  19770  frgp0  19887  frgpadd  19890  mulgnn0di  19952  mulgmhm  19954  gsumval3eu  20031  gsumval3  20034  gsumzcl2  20037  gsumzaddlem  20048  gsumzmhm  20064  gsummptfzcl  20096  omndadd2d  20257  omndadd2rd  20258  srgcl  20332  srgacl  20344  srgbinomlem  20369  srgbinom  20370  ringcl  20389  ringpropd  20430  c0mhm  20601  mat2pmatghm  22955  pm2mpghm  23041  cpmadugsumlemF  23101  tsmsadd  24373  mndcld  33462  cmn246135  33473  cmn145236  33474  slmdacl  33649  slmdvacl  33652  gsumncl  35051  primrootsunit1  42963  aks6d1c1  42982  aks6d1c5lem0  43001  aks6d1c5lem3  43003  aks6d1c5lem2  43004  aks6d1c5  43005  aks6d1c6lem1  43036  ofaddmndmap  49273  lincsum  49359  mndtccatid  50513