Theorem mndcl 18981

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

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1103   = wceq 1570   ∈ wcel 2147  ‘cfv 6566  (class class class)co 7451  Basecbs 17431  +_gcplusg 17472  Mgmcmgm 18864  Mndcmnd 18973

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-nul 5266

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 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-ne 2960  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-sbc 3743  df-ss 3901  df-dif 4050  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4841  df-uni 4873  df-br 5109  df-iota 6520  df-fv 6574  df-ov 7454  df-mgm 18866  df-sgrp 18958  df-mnd 18974

This theorem is used by:  mnd4g  18988  mndpropd  19001  issubmnd  19003  prdsplusgcl  19012  imasmnd  19019  xpsmnd0  19022  idmhm  19040  mhmf1o  19041  mndvcl  19042  mhmvlin  19046  issubmd  19051  0mhm  19065  mhmco  19069  mhmeql  19072  submacs  19073  mndind  19074  prdspjmhm  19075  pwsdiagmhm  19077  pwsco1mhm  19078  pwsco2mhm  19079  gsumwmhm  19091  grpcl  19202  mhmmnd  19324  mulgnn0cl  19350  cntzsubm  19603  oppgmnd  19619  lsmssv  19908  frgp0  20025  frgpadd  20028  mulgnn0di  20090  mulgmhm  20092  gsumval3eu  20169  gsumval3  20172  gsumzcl2  20175  gsumzaddlem  20186  gsumzmhm  20202  gsummptfzcl  20234  omndadd2d  20395  omndadd2rd  20396  srgcl  20470  srgacl  20482  srgbinomlem  20507  srgbinom  20508  ringcl  20528  ringpropd  20570  c0mhm  20741  mat2pmatghm  23103  pm2mpghm  23189  cpmadugsumlemF  23249  tsmsadd  24521  mndcld  33682  cmn246135  33693  cmn145236  33694  slmdacl  33869  slmdvacl  33872  gsumncl  35283  primrootsunit1  43413  aks6d1c1  43432  aks6d1c5lem0  43451  aks6d1c5lem3  43453  aks6d1c5lem2  43454  aks6d1c5  43455  aks6d1c6lem1  43486  ofaddmndmap  49786  lincsum  49872  mndtccatid  51056