Theorem grpcl 18972

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 18971	. 2 ⊢ (𝐺 ∈ Grp → 𝐺 ∈ Mnd)
2		grpcl.b	. . 3 ⊢ 𝐵 = (Base‘𝐺)
3		grpcl.p	. . 3 ⊢ + = (+g‘𝐺)
4	2, 3	mndcl 18768	. 2 ⊢ ((𝐺 ∈ Mnd ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 + 𝑌) ∈ 𝐵)
5	1, 4	syl3an1 1162	1 ⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 + 𝑌) ∈ 𝐵)

Syntax hints:   → wi 4   ∧ w3a 1086   = wceq 1537   ∈ wcel 2106  ‘cfv 6563  (class class class)co 7431  Basecbs 17245  +_gcplusg 17298  Mndcmnd 18760  Grpcgrp 18964

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706  ax-nul 5312

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-ne 2939  df-ral 3060  df-rex 3069  df-rab 3434  df-v 3480  df-sbc 3792  df-dif 3966  df-un 3968  df-ss 3980  df-nul 4340  df-if 4532  df-sn 4632  df-pr 4634  df-op 4638  df-uni 4913  df-br 5149  df-iota 6516  df-fv 6571  df-ov 7434  df-mgm 18666  df-sgrp 18745  df-mnd 18761  df-grp 18967

This theorem is referenced by:  grpcld  18978  grprcan  19004  grprinv  19021  grplmulf1o  19044  grpinvadd  19049  grpsubf  19050  grpsubadd  19059  grpaddsubass  19061  grpnpcan  19063  grpsubsub4  19064  grppnpcan2  19065  grplactcnv  19074  imasgrp  19087  mulgcl  19122  mulgaddcomlem  19128  mulgdir  19137  subgcl  19167  nsgacs  19193  nmzsubg  19196  nsgid  19201  eqgcpbl  19213  qusgrp  19217  qusadd  19219  ecqusaddcl  19224  qus0subgadd  19230  ghmrn  19260  idghm  19262  ghmpreima  19269  ghmnsgima  19271  ghmnsgpreima  19272  ghmf1o  19279  conjghm  19280  qusghm  19286  gaid  19330  subgga  19331  gass  19332  gaorber  19339  gastacl  19340  gastacos  19341  cntzsubg  19370  galactghm  19437  lactghmga  19438  symgsssg  19500  symgfisg  19501  symggen  19503  sylow1lem2  19632  sylow2blem1  19653  sylow2blem2  19654  sylow2blem3  19655  sylow3lem1  19660  sylow3lem2  19661  subgdisj1  19724  ablsub4  19843  abladdsub4  19844  mulgdi  19859  mulgghm  19861  invghm  19866  ghmplusg  19879  odadd1  19881  odadd2  19882  odadd  19883  gex2abl  19884  gexexlem  19885  torsubg  19887  oddvdssubg  19888  frgpnabllem2  19907  rngacl  20180  rngpropd  20192  ringacl  20292  ringpropd  20302  dvrdir  20429  drngmclOLD  20768  abvtrivd  20850  idsrngd  20874  lmodacl  20887  lmodvacl  20890  lmodprop2d  20939  rmodislmod  20945  rmodislmodOLD  20946  prdslmodd  20985  pwssplit2  21077  evpmodpmf1o  21632  frlmplusgvalb  21807  asclghm  21921  psraddclOLD  21977  mplind  22112  evlslem1  22124  evl1addd  22361  scmataddcl  22538  mdetralt  22630  mdetunilem6  22639  opnsubg  24132  ghmcnp  24139  qustgpopn  24144  ngprcan  24639  ngpocelbl  24741  nmotri  24776  ncvspi  25204  cphipval2  25289  4cphipval2  25290  cphipval  25291  efsubm  26608  abvcxp  27674  ttgcontlem1  28914  abliso  33024  ogrpaddltbi  33078  ogrpaddltrbid  33080  ogrpinvlt  33083  cyc3co2  33143  cyc3genpmlem  33154  cycpmconjs  33159  cyc3conja  33160  archiabllem2a  33184  archiabllem2c  33185  archiabllem2b  33186  imaslmod  33361  quslmod  33366  qusxpid  33371  nsgmgclem  33419  drgextlsp  33623  matunitlindflem1  37603  fldhmf1  42072  primrootsunit1  42079  aks6d1c1p2  42091  aks6d1c1p3  42092  nelsubgcld  42484  evlsaddval  42555  fsuppssind  42580  gicabl  43088  isnumbasgrplem2  43093  mendlmod  43178