Theorem mndcl 18669

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

Syntax hints:   → wi 4   ∧ w3a 1086   = wceq 1540   ∈ wcel 2109  ‘cfv 6511  (class class class)co 7387  Basecbs 17179  +_gcplusg 17220  Mgmcmgm 18565  Mndcmnd 18661

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 5261

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 3406  df-v 3449  df-sbc 3754  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-iota 6464  df-fv 6519  df-ov 7390  df-mgm 18567  df-sgrp 18646  df-mnd 18662

This theorem is referenced by:  mnd4g  18675  mndpropd  18686  issubmnd  18688  prdsplusgcl  18695  imasmnd  18702  xpsmnd0  18705  idmhm  18722  mhmf1o  18723  mndvcl  18724  mhmvlin  18728  issubmd  18733  0mhm  18746  mhmco  18750  mhmeql  18753  submacs  18754  mndind  18755  prdspjmhm  18756  pwsdiagmhm  18758  pwsco1mhm  18759  pwsco2mhm  18760  gsumwmhm  18772  grpcl  18873  mhmmnd  18996  mulgnn0cl  19022  cntzsubm  19270  oppgmnd  19286  lsmssv  19573  frgp0  19690  frgpadd  19693  mulgnn0di  19755  mulgmhm  19757  gsumval3eu  19834  gsumval3  19837  gsumzcl2  19840  gsumzaddlem  19851  gsumzmhm  19867  gsummptfzcl  19899  srgcl  20102  srgacl  20114  srgbinomlem  20139  srgbinom  20140  ringcl  20159  ringpropd  20197  c0mhm  20369  mat2pmatghm  22617  pm2mpghm  22703  cpmadugsumlemF  22763  tsmsadd  24034  mndcld  32963  cmn246135  32974  cmn145236  32975  omndadd2d  33022  omndadd2rd  33023  slmdacl  33162  slmdvacl  33165  gsumncl  34531  primrootsunit1  42085  aks6d1c1  42104  aks6d1c5lem0  42123  aks6d1c5lem3  42125  aks6d1c5lem2  42126  aks6d1c5  42127  aks6d1c6lem1  42158  ofaddmndmap  48331  lincsum  48418  mndtccatid  49576