Theorem mndcl 18940

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

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1103   = wceq 1569   ∈ wcel 2144  ‘cfv 6543  (class class class)co 7424  Basecbs 17396  +_gcplusg 17437  Mgmcmgm 18823  Mndcmnd 18932

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-nul 5259

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  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 3739  df-ss 3897  df-dif 4046  df-un 4150  df-nul 4278  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-br 5103  df-iota 6497  df-fv 6551  df-ov 7427  df-mgm 18825  df-sgrp 18917  df-mnd 18933

This theorem is used by:  mnd4g  18947  mndpropd  18960  issubmnd  18962  prdsplusgcl  18971  imasmnd  18978  xpsmnd0  18981  idmhm  18999  mhmf1o  19000  mndvcl  19001  mhmvlin  19005  issubmd  19010  0mhm  19024  mhmco  19028  mhmeql  19031  submacs  19032  mndind  19033  prdspjmhm  19034  pwsdiagmhm  19036  pwsco1mhm  19037  pwsco2mhm  19038  gsumwmhm  19050  grpcl  19161  mhmmnd  19283  mulgnn0cl  19309  cntzsubm  19561  oppgmnd  19577  lsmssv  19866  frgp0  19983  frgpadd  19986  mulgnn0di  20048  mulgmhm  20050  gsumval3eu  20127  gsumval3  20130  gsumzcl2  20133  gsumzaddlem  20144  gsumzmhm  20160  gsummptfzcl  20192  omndadd2d  20353  omndadd2rd  20354  srgcl  20428  srgacl  20440  srgbinomlem  20465  srgbinom  20466  ringcl  20486  ringpropd  20528  c0mhm  20699  mat2pmatghm  23057  pm2mpghm  23143  cpmadugsumlemF  23203  tsmsadd  24475  mndcld  33633  cmn246135  33644  cmn145236  33645  slmdacl  33820  slmdvacl  33823  gsumncl  35222  primrootsunit1  43284  aks6d1c1  43303  aks6d1c5lem0  43322  aks6d1c5lem3  43324  aks6d1c5lem2  43325  aks6d1c5  43326  aks6d1c6lem1  43357  ofaddmndmap  49591  lincsum  49677  mndtccatid  50861