Theorem mndcl 18679

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

Syntax hints:   → wi 4   ∧ w3a 1087   = wceq 1542   ∈ wcel 2114  ‘cfv 6500  (class class class)co 7368  Basecbs 17148  +_gcplusg 17189  Mgmcmgm 18575  Mndcmnd 18671

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 5253

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 3402  df-v 3444  df-sbc 3743  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-iota 6456  df-fv 6508  df-ov 7371  df-mgm 18577  df-sgrp 18656  df-mnd 18672

This theorem is referenced by:  mnd4g  18685  mndpropd  18696  issubmnd  18698  prdsplusgcl  18705  imasmnd  18712  xpsmnd0  18715  idmhm  18732  mhmf1o  18733  mndvcl  18734  mhmvlin  18738  issubmd  18743  0mhm  18756  mhmco  18760  mhmeql  18763  submacs  18764  mndind  18765  prdspjmhm  18766  pwsdiagmhm  18768  pwsco1mhm  18769  pwsco2mhm  18770  gsumwmhm  18782  grpcl  18883  mhmmnd  19006  mulgnn0cl  19032  cntzsubm  19279  oppgmnd  19295  lsmssv  19584  frgp0  19701  frgpadd  19704  mulgnn0di  19766  mulgmhm  19768  gsumval3eu  19845  gsumval3  19848  gsumzcl2  19851  gsumzaddlem  19862  gsumzmhm  19878  gsummptfzcl  19910  omndadd2d  20071  omndadd2rd  20072  srgcl  20140  srgacl  20152  srgbinomlem  20177  srgbinom  20178  ringcl  20197  ringpropd  20235  c0mhm  20408  mat2pmatghm  22686  pm2mpghm  22772  cpmadugsumlemF  22832  tsmsadd  24103  mndcld  33115  cmn246135  33126  cmn145236  33127  slmdacl  33303  slmdvacl  33306  gsumncl  34718  primrootsunit1  42467  aks6d1c1  42486  aks6d1c5lem0  42505  aks6d1c5lem3  42507  aks6d1c5lem2  42508  aks6d1c5  42509  aks6d1c6lem1  42540  ofaddmndmap  48703  lincsum  48789  mndtccatid  49946