Theorem mndcl 18767

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

Syntax hints:   → wi 4   ∧ w3a 1086   = wceq 1536   ∈ wcel 2105  ‘cfv 6562  (class class class)co 7430  Basecbs 17244  +_gcplusg 17297  Mgmcmgm 18663  Mndcmnd 18759

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705  ax-nul 5311

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-ne 2938  df-ral 3059  df-rex 3068  df-rab 3433  df-v 3479  df-sbc 3791  df-dif 3965  df-un 3967  df-ss 3979  df-nul 4339  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-br 5148  df-iota 6515  df-fv 6570  df-ov 7433  df-mgm 18665  df-sgrp 18744  df-mnd 18760

This theorem is referenced by:  mnd4g  18773  mndpropd  18784  issubmnd  18786  prdsplusgcl  18793  imasmnd  18800  xpsmnd0  18803  idmhm  18820  mhmf1o  18821  mndvcl  18822  mhmvlin  18826  issubmd  18831  0mhm  18844  mhmco  18848  mhmeql  18851  submacs  18852  mndind  18853  prdspjmhm  18854  pwsdiagmhm  18856  pwsco1mhm  18857  pwsco2mhm  18858  gsumwmhm  18870  grpcl  18971  mhmmnd  19094  mulgnn0cl  19120  cntzsubm  19368  oppgmnd  19387  lsmssv  19675  frgp0  19792  frgpadd  19795  mulgnn0di  19857  mulgmhm  19859  gsumval3eu  19936  gsumval3  19939  gsumzcl2  19942  gsumzaddlem  19953  gsumzmhm  19969  gsummptfzcl  20001  srgcl  20210  srgacl  20222  srgbinomlem  20247  srgbinom  20248  ringcl  20267  ringpropd  20301  c0mhm  20476  mat2pmatghm  22751  pm2mpghm  22837  cpmadugsumlemF  22897  tsmsadd  24170  mndcld  33009  cmn246135  33020  cmn145236  33021  omndadd2d  33067  omndadd2rd  33068  slmdacl  33197  slmdvacl  33200  gsumncl  34533  primrootsunit1  42078  aks6d1c1  42097  aks6d1c5lem0  42116  aks6d1c5lem3  42118  aks6d1c5lem2  42119  aks6d1c5  42120  aks6d1c6lem1  42151  ofaddmndmap  48187  lincsum  48274  mndtccatid  48895