Theorem mndcl 17615

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

Syntax hints:   → wi 4   ∧ w3a 1108   = wceq 1653   ∈ wcel 2157  ‘cfv 6102  (class class class)co 6879  Basecbs 16183  +_gcplusg 16266  Mgmcmgm 17554  Mndcmnd 17608

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-9 2166  ax-10 2185  ax-11 2200  ax-12 2213  ax-13 2378  ax-ext 2778  ax-nul 4984

This theorem depends on definitions:  df-bi 199  df-an 386  df-or 875  df-3an 1110  df-tru 1657  df-ex 1876  df-nf 1880  df-sb 2065  df-mo 2592  df-eu 2610  df-clab 2787  df-cleq 2793  df-clel 2796  df-nfc 2931  df-ral 3095  df-rex 3096  df-rab 3099  df-v 3388  df-sbc 3635  df-dif 3773  df-un 3775  df-in 3777  df-ss 3784  df-nul 4117  df-if 4279  df-sn 4370  df-pr 4372  df-op 4376  df-uni 4630  df-br 4845  df-iota 6065  df-fv 6110  df-ov 6882  df-mgm 17556  df-sgrp 17598  df-mnd 17609

This theorem is referenced by:  mnd4g  17621  mndpropd  17630  issubmnd  17632  prdsplusgcl  17635  imasmnd  17642  idmhm  17658  mhmf1o  17659  issubmd  17663  0mhm  17672  mhmco  17676  mhmeql  17678  submacs  17679  mrcmndind  17680  prdspjmhm  17681  pwsdiagmhm  17683  pwsco1mhm  17684  pwsco2mhm  17685  gsumccat  17692  gsumwmhm  17697  grpcl  17745  mhmmnd  17852  mulgnn0cl  17872  cntzsubm  18079  oppgmnd  18095  lsmssv  18370  frgp0  18487  frgpadd  18490  mulgnn0di  18545  mulgmhm  18547  gsumval3eu  18619  gsumval3  18622  gsumzcl2  18625  gsumzaddlem  18635  gsumzmhm  18651  gsummptfzcl  18682  srgcl  18827  srgacl  18839  srgbinomlem  18859  srgbinom  18860  ringcl  18876  ringpropd  18897  mndvcl  20521  mhmvlin  20527  mat2pmatghm  20862  pm2mpghm  20948  cpmadugsumlemF  21008  tsmsadd  22277  omndadd2d  30223  omndadd2rd  30224  slmdacl  30277  slmdvacl  30280  gsumncl  31130  c0mhm  42704  ofaddmndmap  42916  lincsum  43012