Theorem mndcl 18704

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

Syntax hints:   → wi 4   ∧ w3a 1087   = wceq 1542   ∈ wcel 2114  ‘cfv 6493  (class class class)co 7361  Basecbs 17173  +_gcplusg 17214  Mgmcmgm 18600  Mndcmnd 18696

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-nul 5242

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ne 2934  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-sbc 3730  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-iota 6449  df-fv 6501  df-ov 7364  df-mgm 18602  df-sgrp 18681  df-mnd 18697

This theorem is referenced by:  mnd4g  18710  mndpropd  18721  issubmnd  18723  prdsplusgcl  18730  imasmnd  18737  xpsmnd0  18740  idmhm  18757  mhmf1o  18758  mndvcl  18759  mhmvlin  18763  issubmd  18768  0mhm  18781  mhmco  18785  mhmeql  18788  submacs  18789  mndind  18790  prdspjmhm  18791  pwsdiagmhm  18793  pwsco1mhm  18794  pwsco2mhm  18795  gsumwmhm  18807  grpcl  18911  mhmmnd  19034  mulgnn0cl  19060  cntzsubm  19307  oppgmnd  19323  lsmssv  19612  frgp0  19729  frgpadd  19732  mulgnn0di  19794  mulgmhm  19796  gsumval3eu  19873  gsumval3  19876  gsumzcl2  19879  gsumzaddlem  19890  gsumzmhm  19906  gsummptfzcl  19938  omndadd2d  20099  omndadd2rd  20100  srgcl  20168  srgacl  20180  srgbinomlem  20205  srgbinom  20206  ringcl  20225  ringpropd  20263  c0mhm  20434  mat2pmatghm  22708  pm2mpghm  22794  cpmadugsumlemF  22854  tsmsadd  24125  mndcld  33100  cmn246135  33111  cmn145236  33112  slmdacl  33288  slmdvacl  33291  gsumncl  34703  primrootsunit1  42553  aks6d1c1  42572  aks6d1c5lem0  42591  aks6d1c5lem3  42593  aks6d1c5lem2  42594  aks6d1c5  42595  aks6d1c6lem1  42626  ofaddmndmap  48834  lincsum  48920  mndtccatid  50077