Theorem grpcl 18915

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

Syntax hints:   → wi 4   ∧ w3a 1092   = wceq 1547   ∈ wcel 2119  ‘cfv 6492  (class class class)co 7363  Basecbs 17177  +_gcplusg 17218  Mndcmnd 18700  Grpcgrp 18907

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712  ax-nul 5235

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-ne 2936  df-ral 3055  df-rex 3065  df-rab 3393  df-v 3434  df-sbc 3731  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4269  df-if 4462  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4846  df-br 5080  df-iota 6448  df-fv 6500  df-ov 7366  df-mgm 18606  df-sgrp 18685  df-mnd 18701  df-grp 18910

This theorem is referenced by:  grpcld  18921  grprcan  18947  grprinv  18964  grplmulf1o  18987  grpinvadd  18992  grpsubf  18993  grpsubadd  19002  grpaddsubass  19004  grpnpcan  19006  grpsubsub4  19007  grppnpcan2  19008  grplactcnv  19017  imasgrp  19030  mulgcl  19065  mulgaddcomlem  19071  mulgdir  19080  subgcl  19110  nsgacs  19135  nmzsubg  19138  nsgid  19143  eqgcpbl  19155  qusgrp  19159  qusadd  19161  ecqusaddcl  19166  qus0subgadd  19172  ghmrn  19202  idghm  19204  ghmpreima  19211  ghmnsgima  19213  ghmnsgpreima  19214  ghmf1o  19221  conjghm  19222  qusghm  19228  gaid  19272  subgga  19273  gass  19274  gaorber  19281  gastacl  19282  gastacos  19283  cntzsubg  19312  galactghm  19377  lactghmga  19378  symgsssg  19440  symgfisg  19441  symggen  19443  sylow1lem2  19572  sylow2blem1  19593  sylow2blem2  19594  sylow2blem3  19595  sylow3lem1  19600  sylow3lem2  19601  subgdisj1  19664  ablsub4  19783  abladdsub4  19784  mulgdi  19799  mulgghm  19801  invghm  19806  ghmplusg  19819  odadd1  19821  odadd2  19822  odadd  19823  gex2abl  19824  gexexlem  19825  torsubg  19827  oddvdssubg  19828  frgpnabllem2  19847  ogrpaddltbi  20112  ogrpaddltrbid  20114  ogrpinvlt  20117  rngacl  20141  rngpropd  20153  ringacl  20257  ringpropd  20267  dvrdir  20390  drngmclOLD  20730  abvtrivd  20811  idsrngd  20835  lmodacl  20869  lmodvacl  20872  lmodprop2d  20921  rmodislmod  20927  prdslmodd  20966  pwssplit2  21057  evpmodpmf1o  21578  frlmplusgvalb  21751  asclghm  21864  mplind  22053  evlslem1  22065  evlsaddval  22112  evl1addd  22334  scmataddcl  22506  mdetralt  22598  mdetunilem6  22607  opnsubg  24098  ghmcnp  24105  qustgpopn  24110  ngprcan  24600  ngpocelbl  24694  nmotri  24729  ncvspi  25148  cphipval2  25233  4cphipval2  25234  cphipval  25235  efsubm  26540  abvcxp  27603  ttgcontlem1  28978  abliso  33122  cyc3co2  33228  cyc3genpmlem  33239  cycpmconjs  33244  cyc3conja  33245  archiabllem2a  33282  archiabllem2c  33283  archiabllem2b  33284  imaslmod  33443  quslmod  33448  qusxpid  33453  nsgmgclem  33501  drgextlsp  33785  matunitlindflem1  37984  fldhmf1  42576  primrootsunit1  42583  aks6d1c1p2  42595  aks6d1c1p3  42596  nelsubgcld  42988  fsuppssind  43044  gicabl  43545  isnumbasgrplem2  43550  mendlmod  43635