Theorem mndcl 18616

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

Syntax hints:   → wi 4   ∧ w3a 1086   = wceq 1540   ∈ wcel 2109  ‘cfv 6482  (class class class)co 7349  Basecbs 17120  +_gcplusg 17161  Mgmcmgm 18512  Mndcmnd 18608

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 5245

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 3395  df-v 3438  df-sbc 3743  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4859  df-br 5093  df-iota 6438  df-fv 6490  df-ov 7352  df-mgm 18514  df-sgrp 18593  df-mnd 18609

This theorem is referenced by:  mnd4g  18622  mndpropd  18633  issubmnd  18635  prdsplusgcl  18642  imasmnd  18649  xpsmnd0  18652  idmhm  18669  mhmf1o  18670  mndvcl  18671  mhmvlin  18675  issubmd  18680  0mhm  18693  mhmco  18697  mhmeql  18700  submacs  18701  mndind  18702  prdspjmhm  18703  pwsdiagmhm  18705  pwsco1mhm  18706  pwsco2mhm  18707  gsumwmhm  18719  grpcl  18820  mhmmnd  18943  mulgnn0cl  18969  cntzsubm  19217  oppgmnd  19233  lsmssv  19522  frgp0  19639  frgpadd  19642  mulgnn0di  19704  mulgmhm  19706  gsumval3eu  19783  gsumval3  19786  gsumzcl2  19789  gsumzaddlem  19800  gsumzmhm  19816  gsummptfzcl  19848  omndadd2d  20009  omndadd2rd  20010  srgcl  20078  srgacl  20090  srgbinomlem  20115  srgbinom  20116  ringcl  20135  ringpropd  20173  c0mhm  20345  mat2pmatghm  22615  pm2mpghm  22701  cpmadugsumlemF  22761  tsmsadd  24032  mndcld  32976  cmn246135  32987  cmn145236  32988  slmdacl  33151  slmdvacl  33154  gsumncl  34508  primrootsunit1  42070  aks6d1c1  42089  aks6d1c5lem0  42108  aks6d1c5lem3  42110  aks6d1c5lem2  42111  aks6d1c5  42112  aks6d1c6lem1  42143  ofaddmndmap  48327  lincsum  48414  mndtccatid  49572