Theorem mndcl 18665

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

Syntax hints:   → wi 4   ∧ w3a 1086   = wceq 1541   ∈ wcel 2113  ‘cfv 6490  (class class class)co 7356  Basecbs 17134  +_gcplusg 17175  Mgmcmgm 18561  Mndcmnd 18657

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706  ax-nul 5249

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-ne 2931  df-ral 3050  df-rex 3059  df-rab 3398  df-v 3440  df-sbc 3739  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4284  df-if 4478  df-sn 4579  df-pr 4581  df-op 4585  df-uni 4862  df-br 5097  df-iota 6446  df-fv 6498  df-ov 7359  df-mgm 18563  df-sgrp 18642  df-mnd 18658

This theorem is referenced by:  mnd4g  18671  mndpropd  18682  issubmnd  18684  prdsplusgcl  18691  imasmnd  18698  xpsmnd0  18701  idmhm  18718  mhmf1o  18719  mndvcl  18720  mhmvlin  18724  issubmd  18729  0mhm  18742  mhmco  18746  mhmeql  18749  submacs  18750  mndind  18751  prdspjmhm  18752  pwsdiagmhm  18754  pwsco1mhm  18755  pwsco2mhm  18756  gsumwmhm  18768  grpcl  18869  mhmmnd  18992  mulgnn0cl  19018  cntzsubm  19265  oppgmnd  19281  lsmssv  19570  frgp0  19687  frgpadd  19690  mulgnn0di  19752  mulgmhm  19754  gsumval3eu  19831  gsumval3  19834  gsumzcl2  19837  gsumzaddlem  19848  gsumzmhm  19864  gsummptfzcl  19896  omndadd2d  20057  omndadd2rd  20058  srgcl  20126  srgacl  20138  srgbinomlem  20163  srgbinom  20164  ringcl  20183  ringpropd  20221  c0mhm  20394  mat2pmatghm  22672  pm2mpghm  22758  cpmadugsumlemF  22818  tsmsadd  24089  mndcld  33053  cmn246135  33064  cmn145236  33065  slmdacl  33240  slmdvacl  33243  gsumncl  34646  primrootsunit1  42290  aks6d1c1  42309  aks6d1c5lem0  42328  aks6d1c5lem3  42330  aks6d1c5lem2  42331  aks6d1c5  42332  aks6d1c6lem1  42363  ofaddmndmap  48531  lincsum  48617  mndtccatid  49774