Theorem mndcl 18795

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

Syntax hints:   → wi 4   ∧ w3a 1103   = wceq 1570   ∈ wcel 2143  ‘cfv 6536  (class class class)co 7410  Basecbs 17264  +_gcplusg 17305  Mgmcmgm 18691  Mndcmnd 18787

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-nul 5269

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-ne 2959  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-sbc 3745  df-dif 3908  df-un 3910  df-ss 3922  df-nul 4287  df-if 4488  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4873  df-br 5110  df-iota 6492  df-fv 6544  df-ov 7413  df-mgm 18693  df-sgrp 18772  df-mnd 18788

This theorem is referenced by:  mnd4g  18801  mndpropd  18812  issubmnd  18814  prdsplusgcl  18821  imasmnd  18828  xpsmnd0  18831  idmhm  18848  mhmf1o  18849  mndvcl  18850  mhmvlin  18854  issubmd  18859  0mhm  18873  mhmco  18877  mhmeql  18880  submacs  18881  mndind  18882  prdspjmhm  18883  pwsdiagmhm  18885  pwsco1mhm  18886  pwsco2mhm  18887  gsumwmhm  18899  grpcl  19003  mhmmnd  19125  mulgnn0cl  19151  cntzsubm  19403  oppgmnd  19419  lsmssv  19708  frgp0  19825  frgpadd  19828  mulgnn0di  19890  mulgmhm  19892  gsumval3eu  19969  gsumval3  19972  gsumzcl2  19975  gsumzaddlem  19986  gsumzmhm  20002  gsummptfzcl  20034  omndadd2d  20195  omndadd2rd  20196  srgcl  20270  srgacl  20282  srgbinomlem  20307  srgbinom  20308  ringcl  20327  ringpropd  20367  c0mhm  20538  mat2pmatghm  22887  pm2mpghm  22973  cpmadugsumlemF  23033  tsmsadd  24304  mndcld  33342  cmn246135  33353  cmn145236  33354  slmdacl  33529  slmdvacl  33532  gsumncl  34930  primrootsunit1  42864  aks6d1c1  42883  aks6d1c5lem0  42902  aks6d1c5lem3  42904  aks6d1c5lem2  42905  aks6d1c5  42906  aks6d1c6lem1  42937  ofaddmndmap  49123  lincsum  49209  mndtccatid  50365