Theorem mndcl 18710

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

Syntax hints:   → wi 4   ∧ w3a 1087   = wceq 1542   ∈ wcel 2114  ‘cfv 6498  (class class class)co 7367  Basecbs 17179  +_gcplusg 17220  Mgmcmgm 18606  Mndcmnd 18702

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708  ax-nul 5241

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-ne 2933  df-ral 3052  df-rex 3062  df-rab 3390  df-v 3431  df-sbc 3729  df-dif 3892  df-un 3894  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-br 5086  df-iota 6454  df-fv 6506  df-ov 7370  df-mgm 18608  df-sgrp 18687  df-mnd 18703

This theorem is referenced by:  mnd4g  18716  mndpropd  18727  issubmnd  18729  prdsplusgcl  18736  imasmnd  18743  xpsmnd0  18746  idmhm  18763  mhmf1o  18764  mndvcl  18765  mhmvlin  18769  issubmd  18774  0mhm  18787  mhmco  18791  mhmeql  18794  submacs  18795  mndind  18796  prdspjmhm  18797  pwsdiagmhm  18799  pwsco1mhm  18800  pwsco2mhm  18801  gsumwmhm  18813  grpcl  18917  mhmmnd  19040  mulgnn0cl  19066  cntzsubm  19313  oppgmnd  19329  lsmssv  19618  frgp0  19735  frgpadd  19738  mulgnn0di  19800  mulgmhm  19802  gsumval3eu  19879  gsumval3  19882  gsumzcl2  19885  gsumzaddlem  19896  gsumzmhm  19912  gsummptfzcl  19944  omndadd2d  20105  omndadd2rd  20106  srgcl  20174  srgacl  20186  srgbinomlem  20211  srgbinom  20212  ringcl  20231  ringpropd  20269  c0mhm  20440  mat2pmatghm  22695  pm2mpghm  22781  cpmadugsumlemF  22841  tsmsadd  24112  mndcld  33082  cmn246135  33093  cmn145236  33094  slmdacl  33270  slmdvacl  33273  gsumncl  34684  primrootsunit1  42536  aks6d1c1  42555  aks6d1c5lem0  42574  aks6d1c5lem3  42576  aks6d1c5lem2  42577  aks6d1c5  42578  aks6d1c6lem1  42609  ofaddmndmap  48819  lincsum  48905  mndtccatid  50062