Theorem mndcl 18718

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

Syntax hints:   → wi 4   ∧ w3a 1086   = wceq 1540   ∈ wcel 2108  ‘cfv 6530  (class class class)co 7403  Basecbs 17226  +_gcplusg 17269  Mgmcmgm 18614  Mndcmnd 18710

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 2007  ax-8 2110  ax-9 2118  ax-ext 2707  ax-nul 5276

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 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-ne 2933  df-ral 3052  df-rex 3061  df-rab 3416  df-v 3461  df-sbc 3766  df-dif 3929  df-un 3931  df-ss 3943  df-nul 4309  df-if 4501  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-br 5120  df-iota 6483  df-fv 6538  df-ov 7406  df-mgm 18616  df-sgrp 18695  df-mnd 18711

This theorem is referenced by:  mnd4g  18724  mndpropd  18735  issubmnd  18737  prdsplusgcl  18744  imasmnd  18751  xpsmnd0  18754  idmhm  18771  mhmf1o  18772  mndvcl  18773  mhmvlin  18777  issubmd  18782  0mhm  18795  mhmco  18799  mhmeql  18802  submacs  18803  mndind  18804  prdspjmhm  18805  pwsdiagmhm  18807  pwsco1mhm  18808  pwsco2mhm  18809  gsumwmhm  18821  grpcl  18922  mhmmnd  19045  mulgnn0cl  19071  cntzsubm  19319  oppgmnd  19335  lsmssv  19622  frgp0  19739  frgpadd  19742  mulgnn0di  19804  mulgmhm  19806  gsumval3eu  19883  gsumval3  19886  gsumzcl2  19889  gsumzaddlem  19900  gsumzmhm  19916  gsummptfzcl  19948  srgcl  20151  srgacl  20163  srgbinomlem  20188  srgbinom  20189  ringcl  20208  ringpropd  20246  c0mhm  20418  mat2pmatghm  22666  pm2mpghm  22752  cpmadugsumlemF  22812  tsmsadd  24083  mndcld  32963  cmn246135  32974  cmn145236  32975  omndadd2d  33022  omndadd2rd  33023  slmdacl  33152  slmdvacl  33155  gsumncl  34518  primrootsunit1  42056  aks6d1c1  42075  aks6d1c5lem0  42094  aks6d1c5lem3  42096  aks6d1c5lem2  42097  aks6d1c5  42098  aks6d1c6lem1  42129  ofaddmndmap  48266  lincsum  48353  mndtccatid  49412