Theorem mndcl 18780

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

Syntax hints:   → wi 4   ∧ w3a 1087   = wceq 1537   ∈ wcel 2108  ‘cfv 6573  (class class class)co 7448  Basecbs 17258  +_gcplusg 17311  Mgmcmgm 18676  Mndcmnd 18772

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711  ax-nul 5324

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-ne 2947  df-ral 3068  df-rex 3077  df-rab 3444  df-v 3490  df-sbc 3805  df-dif 3979  df-un 3981  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-br 5167  df-iota 6525  df-fv 6581  df-ov 7451  df-mgm 18678  df-sgrp 18757  df-mnd 18773

This theorem is referenced by:  mnd4g  18786  mndpropd  18797  issubmnd  18799  prdsplusgcl  18803  imasmnd  18810  xpsmnd0  18813  idmhm  18830  mhmf1o  18831  mndvcl  18832  mhmvlin  18836  issubmd  18841  0mhm  18854  mhmco  18858  mhmeql  18861  submacs  18862  mndind  18863  prdspjmhm  18864  pwsdiagmhm  18866  pwsco1mhm  18867  pwsco2mhm  18868  gsumwmhm  18880  grpcl  18981  mhmmnd  19104  mulgnn0cl  19130  cntzsubm  19378  oppgmnd  19397  lsmssv  19685  frgp0  19802  frgpadd  19805  mulgnn0di  19867  mulgmhm  19869  gsumval3eu  19946  gsumval3  19949  gsumzcl2  19952  gsumzaddlem  19963  gsumzmhm  19979  gsummptfzcl  20011  srgcl  20220  srgacl  20232  srgbinomlem  20257  srgbinom  20258  ringcl  20277  ringpropd  20311  c0mhm  20486  mat2pmatghm  22757  pm2mpghm  22843  cpmadugsumlemF  22903  tsmsadd  24176  mndcld  33008  cmn246135  33019  cmn145236  33020  omndadd2d  33058  omndadd2rd  33059  slmdacl  33188  slmdvacl  33191  gsumncl  34517  primrootsunit1  42054  aks6d1c1  42073  aks6d1c5lem0  42092  aks6d1c5lem3  42094  aks6d1c5lem2  42095  aks6d1c5  42096  aks6d1c6lem1  42127  ofaddmndmap  48068  lincsum  48158  mndtccatid  48760