Theorem mndcl 18676

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

Syntax hints:   → wi 4   ∧ w3a 1086   = wceq 1540   ∈ wcel 2109  ‘cfv 6514  (class class class)co 7390  Basecbs 17186  +_gcplusg 17227  Mgmcmgm 18572  Mndcmnd 18668

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 2008  ax-8 2111  ax-9 2119  ax-ext 2702  ax-nul 5264

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-ne 2927  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-sbc 3757  df-dif 3920  df-un 3922  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-iota 6467  df-fv 6522  df-ov 7393  df-mgm 18574  df-sgrp 18653  df-mnd 18669

This theorem is referenced by:  mnd4g  18682  mndpropd  18693  issubmnd  18695  prdsplusgcl  18702  imasmnd  18709  xpsmnd0  18712  idmhm  18729  mhmf1o  18730  mndvcl  18731  mhmvlin  18735  issubmd  18740  0mhm  18753  mhmco  18757  mhmeql  18760  submacs  18761  mndind  18762  prdspjmhm  18763  pwsdiagmhm  18765  pwsco1mhm  18766  pwsco2mhm  18767  gsumwmhm  18779  grpcl  18880  mhmmnd  19003  mulgnn0cl  19029  cntzsubm  19277  oppgmnd  19293  lsmssv  19580  frgp0  19697  frgpadd  19700  mulgnn0di  19762  mulgmhm  19764  gsumval3eu  19841  gsumval3  19844  gsumzcl2  19847  gsumzaddlem  19858  gsumzmhm  19874  gsummptfzcl  19906  srgcl  20109  srgacl  20121  srgbinomlem  20146  srgbinom  20147  ringcl  20166  ringpropd  20204  c0mhm  20376  mat2pmatghm  22624  pm2mpghm  22710  cpmadugsumlemF  22770  tsmsadd  24041  mndcld  32970  cmn246135  32981  cmn145236  32982  omndadd2d  33029  omndadd2rd  33030  slmdacl  33169  slmdvacl  33172  gsumncl  34538  primrootsunit1  42092  aks6d1c1  42111  aks6d1c5lem0  42130  aks6d1c5lem3  42132  aks6d1c5lem2  42133  aks6d1c5  42134  aks6d1c6lem1  42165  ofaddmndmap  48335  lincsum  48422  mndtccatid  49580