Theorem mndcl 18695

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

Syntax hints:   → wi 4   ∧ w3a 1085   = wceq 1534   ∈ wcel 2099  ‘cfv 6542  (class class class)co 7414  Basecbs 17173  +_gcplusg 17226  Mgmcmgm 18591  Mndcmnd 18687

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2699  ax-nul 5300

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-sb 2061  df-clab 2706  df-cleq 2720  df-clel 2806  df-ne 2937  df-ral 3058  df-rex 3067  df-rab 3429  df-v 3472  df-sbc 3776  df-dif 3948  df-un 3950  df-in 3952  df-ss 3962  df-nul 4319  df-if 4525  df-sn 4625  df-pr 4627  df-op 4631  df-uni 4904  df-br 5143  df-iota 6494  df-fv 6550  df-ov 7417  df-mgm 18593  df-sgrp 18672  df-mnd 18688

This theorem is referenced by:  mnd4g  18701  mndpropd  18712  issubmnd  18714  prdsplusgcl  18718  imasmnd  18725  xpsmnd0  18728  idmhm  18745  mhmf1o  18746  issubmd  18751  0mhm  18764  mhmco  18768  mhmeql  18771  submacs  18772  mndind  18773  prdspjmhm  18774  pwsdiagmhm  18776  pwsco1mhm  18777  pwsco2mhm  18778  gsumwmhm  18790  grpcl  18891  mhmmnd  19013  mulgnn0cl  19038  cntzsubm  19282  oppgmnd  19301  lsmssv  19591  frgp0  19708  frgpadd  19711  mulgnn0di  19773  mulgmhm  19775  gsumval3eu  19852  gsumval3  19855  gsumzcl2  19858  gsumzaddlem  19869  gsumzmhm  19885  gsummptfzcl  19917  srgcl  20126  srgacl  20138  srgbinomlem  20163  srgbinom  20164  ringcl  20183  ringpropd  20217  c0mhm  20392  mndvcl  22286  mhmvlin  22292  mat2pmatghm  22625  pm2mpghm  22711  cpmadugsumlemF  22771  tsmsadd  24044  cmn246135  32747  cmn145236  32748  omndadd2d  32782  omndadd2rd  32783  slmdacl  32910  slmdvacl  32913  gsumncl  34166  primrootsunit1  41561  aks6d1c1  41581  aks6d1c5lem0  41600  aks6d1c5lem3  41602  aks6d1c5lem2  41603  aks6d1c5  41604  aks6d1c6lem1  41636  ofaddmndmap  47401  lincsum  47491  mndtccatid  48093

Otomatik - 173.255.232.114 CloudFlare DNS Türk Telekom DNS Google DNS Open DNS

OSZAR »