Theorem mndcl 18806

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

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1102   = wceq 1569   ∈ wcel 2142  ‘cfv 6536  (class class class)co 7412  Basecbs 17275  +_gcplusg 17316  Mgmcmgm 18702  Mndcmnd 18798

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-8 2144  ax-9 2152  ax-ext 2734  ax-nul 5268

This proof depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1104  df-tru 1572  df-fal 1582  df-ex 1809  df-sb 2096  df-clab 2741  df-cleq 2754  df-clel 2837  df-ne 2958  df-ral 3079  df-rex 3089  df-rab 3416  df-v 3456  df-sbc 3744  df-dif 3907  df-un 3909  df-ss 3921  df-nul 4286  df-if 4487  df-sn 4589  df-pr 4591  df-op 4595  df-uni 4872  df-br 5109  df-iota 6492  df-fv 6544  df-ov 7415  df-mgm 18704  df-sgrp 18783  df-mnd 18799

This theorem is used by:  mnd4g  18812  mndpropd  18823  issubmnd  18825  prdsplusgcl  18832  imasmnd  18839  xpsmnd0  18842  idmhm  18859  mhmf1o  18860  mndvcl  18861  mhmvlin  18865  issubmd  18870  0mhm  18884  mhmco  18888  mhmeql  18891  submacs  18892  mndind  18893  prdspjmhm  18894  pwsdiagmhm  18896  pwsco1mhm  18897  pwsco2mhm  18898  gsumwmhm  18910  grpcl  19014  mhmmnd  19136  mulgnn0cl  19162  cntzsubm  19414  oppgmnd  19430  lsmssv  19719  frgp0  19836  frgpadd  19839  mulgnn0di  19901  mulgmhm  19903  gsumval3eu  19980  gsumval3  19983  gsumzcl2  19986  gsumzaddlem  19997  gsumzmhm  20013  gsummptfzcl  20045  omndadd2d  20206  omndadd2rd  20207  srgcl  20281  srgacl  20293  srgbinomlem  20318  srgbinom  20319  ringcl  20338  ringpropd  20378  c0mhm  20549  mat2pmatghm  22898  pm2mpghm  22984  cpmadugsumlemF  23044  tsmsadd  24315  mndcld  33351  cmn246135  33362  cmn145236  33363  slmdacl  33538  slmdvacl  33541  gsumncl  34939  primrootsunit1  42892  aks6d1c1  42911  aks6d1c5lem0  42930  aks6d1c5lem3  42932  aks6d1c5lem2  42933  aks6d1c5  42934  aks6d1c6lem1  42965  ofaddmndmap  49151  lincsum  49237  mndtccatid  50393