Theorem grpcl 18883

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

Syntax hints:   → wi 4   ∧ w3a 1087   = wceq 1542   ∈ wcel 2114  ‘cfv 6500  (class class class)co 7368  Basecbs 17148  +_gcplusg 17189  Mndcmnd 18671  Grpcgrp 18875

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 5253

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 3402  df-v 3444  df-sbc 3743  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-iota 6456  df-fv 6508  df-ov 7371  df-mgm 18577  df-sgrp 18656  df-mnd 18672  df-grp 18878

This theorem is referenced by:  grpcld  18889  grprcan  18915  grprinv  18932  grplmulf1o  18955  grpinvadd  18960  grpsubf  18961  grpsubadd  18970  grpaddsubass  18972  grpnpcan  18974  grpsubsub4  18975  grppnpcan2  18976  grplactcnv  18985  imasgrp  18998  mulgcl  19033  mulgaddcomlem  19039  mulgdir  19048  subgcl  19078  nsgacs  19103  nmzsubg  19106  nsgid  19111  eqgcpbl  19123  qusgrp  19127  qusadd  19129  ecqusaddcl  19134  qus0subgadd  19140  ghmrn  19170  idghm  19172  ghmpreima  19179  ghmnsgima  19181  ghmnsgpreima  19182  ghmf1o  19189  conjghm  19190  qusghm  19196  gaid  19240  subgga  19241  gass  19242  gaorber  19249  gastacl  19250  gastacos  19251  cntzsubg  19280  galactghm  19345  lactghmga  19346  symgsssg  19408  symgfisg  19409  symggen  19411  sylow1lem2  19540  sylow2blem1  19561  sylow2blem2  19562  sylow2blem3  19563  sylow3lem1  19568  sylow3lem2  19569  subgdisj1  19632  ablsub4  19751  abladdsub4  19752  mulgdi  19767  mulgghm  19769  invghm  19774  ghmplusg  19787  odadd1  19789  odadd2  19790  odadd  19791  gex2abl  19792  gexexlem  19793  torsubg  19795  oddvdssubg  19796  frgpnabllem2  19815  ogrpaddltbi  20080  ogrpaddltrbid  20082  ogrpinvlt  20085  rngacl  20109  rngpropd  20121  ringacl  20225  ringpropd  20235  dvrdir  20360  drngmclOLD  20696  abvtrivd  20777  idsrngd  20801  lmodacl  20835  lmodvacl  20838  lmodprop2d  20887  rmodislmod  20893  prdslmodd  20932  pwssplit2  21024  evpmodpmf1o  21563  frlmplusgvalb  21736  asclghm  21850  psraddclOLD  21907  mplind  22037  evlslem1  22049  evl1addd  22297  scmataddcl  22472  mdetralt  22564  mdetunilem6  22573  opnsubg  24064  ghmcnp  24071  qustgpopn  24076  ngprcan  24566  ngpocelbl  24660  nmotri  24695  ncvspi  25124  cphipval2  25209  4cphipval2  25210  cphipval  25211  efsubm  26528  abvcxp  27594  ttgcontlem1  28969  abliso  33128  cyc3co2  33233  cyc3genpmlem  33244  cycpmconjs  33249  cyc3conja  33250  archiabllem2a  33287  archiabllem2c  33288  archiabllem2b  33289  imaslmod  33445  quslmod  33450  qusxpid  33455  nsgmgclem  33503  drgextlsp  33770  matunitlindflem1  37856  fldhmf1  42449  primrootsunit1  42456  aks6d1c1p2  42468  aks6d1c1p3  42469  nelsubgcld  42856  evlsaddval  42918  fsuppssind  42940  gicabl  43445  isnumbasgrplem2  43450  mendlmod  43535