Theorem mndcl 18832

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

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1103   = wceq 1570   ∈ wcel 2146  ‘cfv 6540  (class class class)co 7419  Basecbs 17291  +_gcplusg 17332  Mgmcmgm 18718  Mndcmnd 18824

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 2148  ax-9 2156  ax-ext 2737  ax-nul 5271

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 2744  df-cleq 2757  df-clel 2840  df-ne 2961  df-ral 3082  df-rex 3092  df-rab 3419  df-v 3459  df-sbc 3747  df-dif 3909  df-un 3911  df-ss 3923  df-nul 4287  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-br 5112  df-iota 6496  df-fv 6548  df-ov 7422  df-mgm 18720  df-sgrp 18809  df-mnd 18825

This theorem is used by:  mnd4g  18839  mndpropd  18852  issubmnd  18854  prdsplusgcl  18863  imasmnd  18870  xpsmnd0  18873  idmhm  18890  mhmf1o  18891  mndvcl  18892  mhmvlin  18896  issubmd  18901  0mhm  18915  mhmco  18919  mhmeql  18922  submacs  18923  mndind  18924  prdspjmhm  18925  pwsdiagmhm  18927  pwsco1mhm  18928  pwsco2mhm  18929  gsumwmhm  18941  grpcl  19052  mhmmnd  19174  mulgnn0cl  19200  cntzsubm  19452  oppgmnd  19468  lsmssv  19757  frgp0  19874  frgpadd  19877  mulgnn0di  19939  mulgmhm  19941  gsumval3eu  20018  gsumval3  20021  gsumzcl2  20024  gsumzaddlem  20035  gsumzmhm  20051  gsummptfzcl  20083  omndadd2d  20244  omndadd2rd  20245  srgcl  20319  srgacl  20331  srgbinomlem  20356  srgbinom  20357  ringcl  20376  ringpropd  20417  c0mhm  20588  mat2pmatghm  22937  pm2mpghm  23023  cpmadugsumlemF  23083  tsmsadd  24355  mndcld  33406  cmn246135  33417  cmn145236  33418  slmdacl  33593  slmdvacl  33596  gsumncl  34995  primrootsunit1  42922  aks6d1c1  42941  aks6d1c5lem0  42960  aks6d1c5lem3  42962  aks6d1c5lem2  42963  aks6d1c5  42964  aks6d1c6lem1  42995  ofaddmndmap  49180  lincsum  49266  mndtccatid  50422