Theorem grpcl 18929

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

Syntax hints:   → wi 4   ∧ w3a 1086   = wceq 1540   ∈ wcel 2109  ‘cfv 6536  (class class class)co 7410  Basecbs 17233  +_gcplusg 17276  Mndcmnd 18717  Grpcgrp 18921

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 2008  ax-8 2111  ax-9 2119  ax-ext 2708  ax-nul 5281

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 2066  df-clab 2715  df-cleq 2728  df-clel 2810  df-ne 2934  df-ral 3053  df-rex 3062  df-rab 3421  df-v 3466  df-sbc 3771  df-dif 3934  df-un 3936  df-ss 3948  df-nul 4314  df-if 4506  df-sn 4607  df-pr 4609  df-op 4613  df-uni 4889  df-br 5125  df-iota 6489  df-fv 6544  df-ov 7413  df-mgm 18623  df-sgrp 18702  df-mnd 18718  df-grp 18924

This theorem is referenced by:  grpcld  18935  grprcan  18961  grprinv  18978  grplmulf1o  19001  grpinvadd  19006  grpsubf  19007  grpsubadd  19016  grpaddsubass  19018  grpnpcan  19020  grpsubsub4  19021  grppnpcan2  19022  grplactcnv  19031  imasgrp  19044  mulgcl  19079  mulgaddcomlem  19085  mulgdir  19094  subgcl  19124  nsgacs  19150  nmzsubg  19153  nsgid  19158  eqgcpbl  19170  qusgrp  19174  qusadd  19176  ecqusaddcl  19181  qus0subgadd  19187  ghmrn  19217  idghm  19219  ghmpreima  19226  ghmnsgima  19228  ghmnsgpreima  19229  ghmf1o  19236  conjghm  19237  qusghm  19243  gaid  19287  subgga  19288  gass  19289  gaorber  19296  gastacl  19297  gastacos  19298  cntzsubg  19327  galactghm  19390  lactghmga  19391  symgsssg  19453  symgfisg  19454  symggen  19456  sylow1lem2  19585  sylow2blem1  19606  sylow2blem2  19607  sylow2blem3  19608  sylow3lem1  19613  sylow3lem2  19614  subgdisj1  19677  ablsub4  19796  abladdsub4  19797  mulgdi  19812  mulgghm  19814  invghm  19819  ghmplusg  19832  odadd1  19834  odadd2  19835  odadd  19836  gex2abl  19837  gexexlem  19838  torsubg  19840  oddvdssubg  19841  frgpnabllem2  19860  rngacl  20127  rngpropd  20139  ringacl  20243  ringpropd  20253  dvrdir  20377  drngmclOLD  20716  abvtrivd  20797  idsrngd  20821  lmodacl  20834  lmodvacl  20837  lmodprop2d  20886  rmodislmod  20892  prdslmodd  20931  pwssplit2  21023  evpmodpmf1o  21561  frlmplusgvalb  21734  asclghm  21848  psraddclOLD  21904  mplind  22033  evlslem1  22045  evl1addd  22284  scmataddcl  22459  mdetralt  22551  mdetunilem6  22560  opnsubg  24051  ghmcnp  24058  qustgpopn  24063  ngprcan  24554  ngpocelbl  24648  nmotri  24683  ncvspi  25113  cphipval2  25198  4cphipval2  25199  cphipval  25200  efsubm  26517  abvcxp  27583  ttgcontlem1  28869  abliso  33036  ogrpaddltbi  33091  ogrpaddltrbid  33093  ogrpinvlt  33096  cyc3co2  33156  cyc3genpmlem  33167  cycpmconjs  33172  cyc3conja  33173  archiabllem2a  33197  archiabllem2c  33198  archiabllem2b  33199  imaslmod  33373  quslmod  33378  qusxpid  33383  nsgmgclem  33431  drgextlsp  33638  matunitlindflem1  37645  fldhmf1  42108  primrootsunit1  42115  aks6d1c1p2  42127  aks6d1c1p3  42128  nelsubgcld  42495  evlsaddval  42566  fsuppssind  42591  gicabl  43098  isnumbasgrplem2  43103  mendlmod  43188