Theorem mndcl 18755

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

Syntax hints:   → wi 4   ∧ w3a 1087   = wceq 1540   ∈ wcel 2108  ‘cfv 6561  (class class class)co 7431  Basecbs 17247  +_gcplusg 17297  Mgmcmgm 18651  Mndcmnd 18747

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708  ax-nul 5306

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-sbc 3789  df-dif 3954  df-un 3956  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-iota 6514  df-fv 6569  df-ov 7434  df-mgm 18653  df-sgrp 18732  df-mnd 18748

This theorem is referenced by:  mnd4g  18761  mndpropd  18772  issubmnd  18774  prdsplusgcl  18781  imasmnd  18788  xpsmnd0  18791  idmhm  18808  mhmf1o  18809  mndvcl  18810  mhmvlin  18814  issubmd  18819  0mhm  18832  mhmco  18836  mhmeql  18839  submacs  18840  mndind  18841  prdspjmhm  18842  pwsdiagmhm  18844  pwsco1mhm  18845  pwsco2mhm  18846  gsumwmhm  18858  grpcl  18959  mhmmnd  19082  mulgnn0cl  19108  cntzsubm  19356  oppgmnd  19373  lsmssv  19661  frgp0  19778  frgpadd  19781  mulgnn0di  19843  mulgmhm  19845  gsumval3eu  19922  gsumval3  19925  gsumzcl2  19928  gsumzaddlem  19939  gsumzmhm  19955  gsummptfzcl  19987  srgcl  20190  srgacl  20202  srgbinomlem  20227  srgbinom  20228  ringcl  20247  ringpropd  20285  c0mhm  20460  mat2pmatghm  22736  pm2mpghm  22822  cpmadugsumlemF  22882  tsmsadd  24155  mndcld  33027  cmn246135  33038  cmn145236  33039  omndadd2d  33085  omndadd2rd  33086  slmdacl  33215  slmdvacl  33218  gsumncl  34555  primrootsunit1  42098  aks6d1c1  42117  aks6d1c5lem0  42136  aks6d1c5lem3  42138  aks6d1c5lem2  42139  aks6d1c5  42140  aks6d1c6lem1  42171  ofaddmndmap  48259  lincsum  48346  mndtccatid  49184