Theorem mndcl 18651

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

Syntax hints:   → wi 4   ∧ w3a 1086   = wceq 1540   ∈ wcel 2109  ‘cfv 6499  (class class class)co 7369  Basecbs 17155  +_gcplusg 17196  Mgmcmgm 18547  Mndcmnd 18643

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-nul 5256

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ne 2926  df-ral 3045  df-rex 3054  df-rab 3403  df-v 3446  df-sbc 3751  df-dif 3914  df-un 3916  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-br 5103  df-iota 6452  df-fv 6507  df-ov 7372  df-mgm 18549  df-sgrp 18628  df-mnd 18644

This theorem is referenced by:  mnd4g  18657  mndpropd  18668  issubmnd  18670  prdsplusgcl  18677  imasmnd  18684  xpsmnd0  18687  idmhm  18704  mhmf1o  18705  mndvcl  18706  mhmvlin  18710  issubmd  18715  0mhm  18728  mhmco  18732  mhmeql  18735  submacs  18736  mndind  18737  prdspjmhm  18738  pwsdiagmhm  18740  pwsco1mhm  18741  pwsco2mhm  18742  gsumwmhm  18754  grpcl  18855  mhmmnd  18978  mulgnn0cl  19004  cntzsubm  19252  oppgmnd  19268  lsmssv  19557  frgp0  19674  frgpadd  19677  mulgnn0di  19739  mulgmhm  19741  gsumval3eu  19818  gsumval3  19821  gsumzcl2  19824  gsumzaddlem  19835  gsumzmhm  19851  gsummptfzcl  19883  omndadd2d  20044  omndadd2rd  20045  srgcl  20113  srgacl  20125  srgbinomlem  20150  srgbinom  20151  ringcl  20170  ringpropd  20208  c0mhm  20380  mat2pmatghm  22650  pm2mpghm  22736  cpmadugsumlemF  22796  tsmsadd  24067  mndcld  33006  cmn246135  33017  cmn145236  33018  slmdacl  33178  slmdvacl  33181  gsumncl  34524  primrootsunit1  42078  aks6d1c1  42097  aks6d1c5lem0  42116  aks6d1c5lem3  42118  aks6d1c5lem2  42119  aks6d1c5  42120  aks6d1c6lem1  42151  ofaddmndmap  48324  lincsum  48411  mndtccatid  49569