Theorem mndcl 18667

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

Syntax hints:   → wi 4   ∧ w3a 1086   = wceq 1541   ∈ wcel 2113  ‘cfv 6492  (class class class)co 7358  Basecbs 17136  +_gcplusg 17177  Mgmcmgm 18563  Mndcmnd 18659

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708  ax-nul 5251

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-ne 2933  df-ral 3052  df-rex 3061  df-rab 3400  df-v 3442  df-sbc 3741  df-dif 3904  df-un 3906  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-br 5099  df-iota 6448  df-fv 6500  df-ov 7361  df-mgm 18565  df-sgrp 18644  df-mnd 18660

This theorem is referenced by:  mnd4g  18673  mndpropd  18684  issubmnd  18686  prdsplusgcl  18693  imasmnd  18700  xpsmnd0  18703  idmhm  18720  mhmf1o  18721  mndvcl  18722  mhmvlin  18726  issubmd  18731  0mhm  18744  mhmco  18748  mhmeql  18751  submacs  18752  mndind  18753  prdspjmhm  18754  pwsdiagmhm  18756  pwsco1mhm  18757  pwsco2mhm  18758  gsumwmhm  18770  grpcl  18871  mhmmnd  18994  mulgnn0cl  19020  cntzsubm  19267  oppgmnd  19283  lsmssv  19572  frgp0  19689  frgpadd  19692  mulgnn0di  19754  mulgmhm  19756  gsumval3eu  19833  gsumval3  19836  gsumzcl2  19839  gsumzaddlem  19850  gsumzmhm  19866  gsummptfzcl  19898  omndadd2d  20059  omndadd2rd  20060  srgcl  20128  srgacl  20140  srgbinomlem  20165  srgbinom  20166  ringcl  20185  ringpropd  20223  c0mhm  20396  mat2pmatghm  22674  pm2mpghm  22760  cpmadugsumlemF  22820  tsmsadd  24091  mndcld  33104  cmn246135  33115  cmn145236  33116  slmdacl  33291  slmdvacl  33294  gsumncl  34697  primrootsunit1  42351  aks6d1c1  42370  aks6d1c5lem0  42389  aks6d1c5lem3  42391  aks6d1c5lem2  42392  aks6d1c5  42393  aks6d1c6lem1  42424  ofaddmndmap  48589  lincsum  48675  mndtccatid  49832