Theorem grpcl 18903

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

Syntax hints:   → wi 4   ∧ w3a 1084   = wceq 1533   ∈ wcel 2098  ‘cfv 6547  (class class class)co 7417  Basecbs 17180  +_gcplusg 17233  Mndcmnd 18694  Grpcgrp 18895

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2696  ax-nul 5306

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-sb 2060  df-clab 2703  df-cleq 2717  df-clel 2802  df-ne 2931  df-ral 3052  df-rex 3061  df-rab 3420  df-v 3465  df-sbc 3775  df-dif 3948  df-un 3950  df-ss 3962  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4909  df-br 5149  df-iota 6499  df-fv 6555  df-ov 7420  df-mgm 18600  df-sgrp 18679  df-mnd 18695  df-grp 18898

This theorem is referenced by:  grpcld  18909  grprcan  18935  grprinv  18952  grplmulf1o  18974  grpinvadd  18979  grpsubf  18980  grpsubadd  18989  grpaddsubass  18991  grpnpcan  18993  grpsubsub4  18994  grppnpcan2  18995  grplactcnv  19004  imasgrp  19017  mulgcl  19051  mulgaddcomlem  19057  mulgdir  19066  subgcl  19096  nsgacs  19122  nmzsubg  19125  nsgid  19130  eqgcpbl  19142  qusgrp  19146  qusadd  19148  ecqusaddcl  19153  qus0subgadd  19159  ghmrn  19188  idghm  19190  ghmpreima  19197  ghmnsgima  19199  ghmnsgpreima  19200  ghmf1o  19207  conjghm  19208  qusghm  19214  gaid  19255  subgga  19256  gass  19257  gaorber  19264  gastacl  19265  gastacos  19266  cntzsubg  19295  galactghm  19364  lactghmga  19365  symgsssg  19427  symgfisg  19428  symggen  19430  sylow1lem2  19559  sylow2blem1  19580  sylow2blem2  19581  sylow2blem3  19582  sylow3lem1  19587  sylow3lem2  19588  subgdisj1  19651  ablsub4  19770  abladdsub4  19771  mulgdi  19786  mulgghm  19788  invghm  19793  ghmplusg  19806  odadd1  19808  odadd2  19809  odadd  19810  gex2abl  19811  gexexlem  19812  torsubg  19814  oddvdssubg  19815  frgpnabllem2  19834  rngacl  20107  rngpropd  20119  ringacl  20219  ringpropd  20229  dvrdir  20356  drngmcl  20646  abvtrivd  20725  idsrngd  20747  lmodacl  20760  lmodvacl  20763  lmodprop2d  20812  rmodislmod  20818  rmodislmodOLD  20819  prdslmodd  20858  pwssplit2  20950  evpmodpmf1o  21533  frlmplusgvalb  21708  asclghm  21821  psraddclOLD  21889  mplind  22022  evlslem1  22036  mhpaddcl  22084  evl1addd  22270  scmataddcl  22449  mdetralt  22541  mdetunilem6  22550  opnsubg  24043  ghmcnp  24050  qustgpopn  24055  ngprcan  24550  ngpocelbl  24652  nmotri  24687  ncvspi  25115  cphipval2  25200  4cphipval2  25201  cphipval  25202  efsubm  26516  abvcxp  27579  ttgcontlem1  28752  abliso  32822  ogrpaddltbi  32864  ogrpaddltrbid  32866  ogrpinvlt  32869  cyc3co2  32929  cyc3genpmlem  32940  cycpmconjs  32945  cyc3conja  32946  archiabllem2a  32970  archiabllem2c  32971  archiabllem2b  32972  imaslmod  33136  quslmod  33141  qusxpid  33146  nsgmgclem  33195  drgextlsp  33380  matunitlindflem1  37176  fldhmf1  41647  primrootsunit1  41653  aks6d1c1p2  41666  aks6d1c1p3  41667  nelsubgcld  41822  evlsaddval  41883  fsuppssind  41908  gicabl  42605  isnumbasgrplem2  42610  mendlmod  42699