Theorem mndcl 18931

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

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1103   = wceq 1570   ∈ wcel 2145  ‘cfv 6538  (class class class)co 7420  Basecbs 17387  +_gcplusg 17428  Mgmcmgm 18814  Mndcmnd 18923

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733  ax-nul 5260

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-ne 2957  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-sbc 3740  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-iota 6494  df-fv 6546  df-ov 7423  df-mgm 18816  df-sgrp 18908  df-mnd 18924

This theorem is used by:  mnd4g  18938  mndpropd  18951  issubmnd  18953  prdsplusgcl  18962  imasmnd  18969  xpsmnd0  18972  idmhm  18990  mhmf1o  18991  mndvcl  18992  mhmvlin  18996  issubmd  19001  0mhm  19015  mhmco  19019  mhmeql  19022  submacs  19023  mndind  19024  prdspjmhm  19025  pwsdiagmhm  19027  pwsco1mhm  19028  pwsco2mhm  19029  gsumwmhm  19041  grpcl  19152  mhmmnd  19274  mulgnn0cl  19300  cntzsubm  19552  oppgmnd  19568  lsmssv  19857  frgp0  19974  frgpadd  19977  mulgnn0di  20039  mulgmhm  20041  gsumval3eu  20118  gsumval3  20121  gsumzcl2  20124  gsumzaddlem  20135  gsumzmhm  20151  gsummptfzcl  20183  omndadd2d  20344  omndadd2rd  20345  srgcl  20419  srgacl  20431  srgbinomlem  20456  srgbinom  20457  ringcl  20477  ringpropd  20519  c0mhm  20690  mat2pmatghm  23048  pm2mpghm  23134  cpmadugsumlemF  23194  tsmsadd  24466  mndcld  33583  cmn246135  33594  cmn145236  33595  slmdacl  33770  slmdvacl  33773  gsumncl  35172  primrootsunit1  43147  aks6d1c1  43166  aks6d1c5lem0  43185  aks6d1c5lem3  43187  aks6d1c5lem2  43188  aks6d1c5  43189  aks6d1c6lem1  43220  ofaddmndmap  49454  lincsum  49540  mndtccatid  50694