Theorem grpcl 18917

Description: Closure of the operation of a group. (Contributed by NM, 14-Aug-2011.)

Hypotheses

Ref	Expression
grpcl.b	⊢ 𝐵 = (Base‘𝐺)
grpcl.p	⊢ + = (+g‘𝐺)

Assertion

Ref	Expression
grpcl	⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 + 𝑌) ∈ 𝐵)

Proof of Theorem grpcl

Step	Hyp	Ref	Expression
1		grpmnd 18916	. 2 ⊢ (𝐺 ∈ Grp → 𝐺 ∈ Mnd)
2		grpcl.b	. . 3 ⊢ 𝐵 = (Base‘𝐺)
3		grpcl.p	. . 3 ⊢ + = (+g‘𝐺)
4	2, 3	mndcl 18710	. 2 ⊢ ((𝐺 ∈ Mnd ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 + 𝑌) ∈ 𝐵)
5	1, 4	syl3an1 1164	1 ⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 + 𝑌) ∈ 𝐵)

Syntax hints:   → wi 4   ∧ w3a 1087   = wceq 1542   ∈ wcel 2114  ‘cfv 6499  (class class class)co 7367  Basecbs 17179  +_gcplusg 17220  Mndcmnd 18702  Grpcgrp 18909

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-nul 5242

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ne 2934  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-sbc 3730  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-iota 6455  df-fv 6507  df-ov 7370  df-mgm 18608  df-sgrp 18687  df-mnd 18703  df-grp 18912

This theorem is referenced by:  grpcld  18923  grprcan  18949  grprinv  18966  grplmulf1o  18989  grpinvadd  18994  grpsubf  18995  grpsubadd  19004  grpaddsubass  19006  grpnpcan  19008  grpsubsub4  19009  grppnpcan2  19010  grplactcnv  19019  imasgrp  19032  mulgcl  19067  mulgaddcomlem  19073  mulgdir  19082  subgcl  19112  nsgacs  19137  nmzsubg  19140  nsgid  19145  eqgcpbl  19157  qusgrp  19161  qusadd  19163  ecqusaddcl  19168  qus0subgadd  19174  ghmrn  19204  idghm  19206  ghmpreima  19213  ghmnsgima  19215  ghmnsgpreima  19216  ghmf1o  19223  conjghm  19224  qusghm  19230  gaid  19274  subgga  19275  gass  19276  gaorber  19283  gastacl  19284  gastacos  19285  cntzsubg  19314  galactghm  19379  lactghmga  19380  symgsssg  19442  symgfisg  19443  symggen  19445  sylow1lem2  19574  sylow2blem1  19595  sylow2blem2  19596  sylow2blem3  19597  sylow3lem1  19602  sylow3lem2  19603  subgdisj1  19666  ablsub4  19785  abladdsub4  19786  mulgdi  19801  mulgghm  19803  invghm  19808  ghmplusg  19821  odadd1  19823  odadd2  19824  odadd  19825  gex2abl  19826  gexexlem  19827  torsubg  19829  oddvdssubg  19830  frgpnabllem2  19849  ogrpaddltbi  20114  ogrpaddltrbid  20116  ogrpinvlt  20119  rngacl  20143  rngpropd  20155  ringacl  20259  ringpropd  20269  dvrdir  20392  drngmclOLD  20728  abvtrivd  20809  idsrngd  20833  lmodacl  20867  lmodvacl  20870  lmodprop2d  20919  rmodislmod  20925  prdslmodd  20964  pwssplit2  21055  evpmodpmf1o  21576  frlmplusgvalb  21749  asclghm  21862  mplind  22048  evlslem1  22060  evl1addd  22306  scmataddcl  22481  mdetralt  22573  mdetunilem6  22582  opnsubg  24073  ghmcnp  24080  qustgpopn  24085  ngprcan  24575  ngpocelbl  24669  nmotri  24704  ncvspi  25123  cphipval2  25208  4cphipval2  25209  cphipval  25210  efsubm  26515  abvcxp  27578  ttgcontlem1  28953  abliso  33096  cyc3co2  33201  cyc3genpmlem  33212  cycpmconjs  33217  cyc3conja  33218  archiabllem2a  33255  archiabllem2c  33256  archiabllem2b  33257  imaslmod  33413  quslmod  33418  qusxpid  33423  nsgmgclem  33471  drgextlsp  33738  matunitlindflem1  37937  fldhmf1  42529  primrootsunit1  42536  aks6d1c1p2  42548  aks6d1c1p3  42549  nelsubgcld  42942  evlsaddval  43004  fsuppssind  43026  gicabl  43527  isnumbasgrplem2  43532  mendlmod  43617