Theorem mndcl 18776

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

Syntax hints:   → wi 4   ∧ w3a 1098   = wceq 1560   ∈ wcel 2142  ‘cfv 6521  (class class class)co 7396  Basecbs 17245  +_gcplusg 17286  Mgmcmgm 18672  Mndcmnd 18768

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734  ax-nul 5256

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1100  df-tru 1563  df-fal 1573  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-ne 2958  df-ral 3077  df-rex 3087  df-rab 3415  df-v 3456  df-sbc 3745  df-dif 3907  df-un 3909  df-ss 3921  df-nul 4286  df-if 4481  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-iota 6477  df-fv 6529  df-ov 7399  df-mgm 18674  df-sgrp 18753  df-mnd 18769

This theorem is referenced by:  mnd4g  18782  mndpropd  18793  issubmnd  18795  prdsplusgcl  18802  imasmnd  18809  xpsmnd0  18812  idmhm  18829  mhmf1o  18830  mndvcl  18831  mhmvlin  18835  issubmd  18840  0mhm  18853  mhmco  18857  mhmeql  18860  submacs  18861  mndind  18862  prdspjmhm  18863  pwsdiagmhm  18865  pwsco1mhm  18866  pwsco2mhm  18867  gsumwmhm  18879  grpcl  18983  mhmmnd  19106  mulgnn0cl  19132  cntzsubm  19378  oppgmnd  19394  lsmssv  19683  frgp0  19800  frgpadd  19803  mulgnn0di  19865  mulgmhm  19867  gsumval3eu  19944  gsumval3  19947  gsumzcl2  19950  gsumzaddlem  19961  gsumzmhm  19977  gsummptfzcl  20009  omndadd2d  20170  omndadd2rd  20171  srgcl  20239  srgacl  20251  srgbinomlem  20276  srgbinom  20277  ringcl  20296  ringpropd  20334  c0mhm  20505  mat2pmatghm  22787  pm2mpghm  22873  cpmadugsumlemF  22933  tsmsadd  24204  mndcld  33197  cmn246135  33208  cmn145236  33209  slmdacl  33386  slmdvacl  33389  gsumncl  34834  primrootsunit1  42711  aks6d1c1  42730  aks6d1c5lem0  42749  aks6d1c5lem3  42751  aks6d1c5lem2  42752  aks6d1c5  42753  aks6d1c6lem1  42784  ofaddmndmap  48962  lincsum  49048  mndtccatid  50205