Theorem mndcl 18633

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

Syntax hints:   → wi 4   ∧ w3a 1088   = wceq 1542   ∈ wcel 2107  ‘cfv 6544  (class class class)co 7409  Basecbs 17144  +_gcplusg 17197  Mgmcmgm 18559  Mndcmnd 18625

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704  ax-nul 5307

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-ne 2942  df-ral 3063  df-rex 3072  df-rab 3434  df-v 3477  df-sbc 3779  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-br 5150  df-iota 6496  df-fv 6552  df-ov 7412  df-mgm 18561  df-sgrp 18610  df-mnd 18626

This theorem is referenced by:  mnd4g  18639  mndpropd  18650  issubmnd  18652  prdsplusgcl  18656  imasmnd  18663  xpsmnd0  18666  idmhm  18681  mhmf1o  18682  issubmd  18687  0mhm  18700  mhmco  18704  mhmeql  18707  submacs  18708  mndind  18709  prdspjmhm  18710  pwsdiagmhm  18712  pwsco1mhm  18713  pwsco2mhm  18714  gsumwmhm  18726  grpcl  18827  mhmmnd  18947  mulgnn0cl  18970  cntzsubm  19202  oppgmnd  19221  lsmssv  19511  frgp0  19628  frgpadd  19631  mulgnn0di  19693  mulgmhm  19695  gsumval3eu  19772  gsumval3  19775  gsumzcl2  19778  gsumzaddlem  19789  gsumzmhm  19805  gsummptfzcl  19837  srgcl  20016  srgacl  20028  srgbinomlem  20053  srgbinom  20054  ringcl  20073  ringpropd  20102  mndvcl  21893  mhmvlin  21899  mat2pmatghm  22232  pm2mpghm  22318  cpmadugsumlemF  22378  tsmsadd  23651  omndadd2d  32226  omndadd2rd  32227  slmdacl  32354  slmdvacl  32357  gsumncl  33551  c0mhm  46709  ofaddmndmap  47019  lincsum  47110  mndtccatid  47713