Theorem grpcl 18566

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

Syntax hints:   → wi 4   ∧ w3a 1085   = wceq 1541   ∈ wcel 2109  ‘cfv 6430  (class class class)co 7268  Basecbs 16893  +_gcplusg 16943  Mndcmnd 18366  Grpcgrp 18558

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-8 2111  ax-9 2119  ax-10 2140  ax-11 2157  ax-12 2174  ax-ext 2710  ax-nul 5233

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1544  df-fal 1554  df-ex 1786  df-nf 1790  df-sb 2071  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2817  df-ral 3070  df-rex 3071  df-rab 3074  df-v 3432  df-sbc 3720  df-dif 3894  df-un 3896  df-in 3898  df-ss 3908  df-nul 4262  df-if 4465  df-sn 4567  df-pr 4569  df-op 4573  df-uni 4845  df-br 5079  df-iota 6388  df-fv 6438  df-ov 7271  df-mgm 18307  df-sgrp 18356  df-mnd 18367  df-grp 18561

This theorem is referenced by:  grpcld  18571  grprcan  18594  grprinv  18610  grplmulf1o  18630  grpinvadd  18634  grpsubf  18635  grpsubadd  18644  grpaddsubass  18646  grpnpcan  18648  grpsubsub4  18649  grppnpcan2  18650  dfgrp3  18655  grplactcnv  18659  imasgrp  18672  mulgcl  18702  mulgaddcomlem  18707  mulgdir  18716  subgcl  18746  nsgacs  18771  nmzsubg  18774  nsgid  18779  eqger  18787  eqgcpbl  18791  qusgrp  18792  qusadd  18794  ghmrn  18828  idghm  18830  ghmpreima  18837  ghmnsgima  18839  ghmnsgpreima  18840  ghmf1o  18845  conjghm  18846  conjnmz  18849  qusghm  18852  gaid  18886  subgga  18887  gass  18888  gaorber  18895  gastacl  18896  gastacos  18897  cntzsubg  18924  galactghm  18993  lactghmga  18994  symgsssg  19056  symgfisg  19057  symggen  19059  sylow1lem2  19185  sylow2blem1  19206  sylow2blem2  19207  sylow2blem3  19208  sylow3lem1  19213  sylow3lem2  19214  subgdisj1  19278  ablsub4  19395  abladdsub4  19396  mulgdi  19409  mulgghm  19411  invghm  19416  ghmplusg  19428  odadd1  19430  odadd2  19431  odadd  19432  gex2abl  19433  gexexlem  19434  torsubg  19436  oddvdssubg  19437  frgpnabllem2  19456  ringacl  19798  ringpropd  19802  drngmcl  19985  abvtrivd  20081  idsrngd  20103  lmodacl  20115  lmodvacl  20118  lmodprop2d  20166  rmodislmod  20172  rmodislmodOLD  20173  prdslmodd  20212  pwssplit2  20303  evpmodpmf1o  20782  frlmplusgvalb  20957  asclghm  21068  psraddcl  21133  mplind  21259  evlslem1  21273  mhpaddcl  21322  evl1addd  21488  scmataddcl  21646  mdetralt  21738  mdetunilem6  21747  opnsubg  23240  ghmcnp  23247  qustgpopn  23252  ngprcan  23747  ngpocelbl  23849  nmotri  23884  ncvspi  24301  cphipval2  24386  4cphipval2  24387  cphipval  24388  efsubm  25688  abvcxp  26744  ttgcontlem1  27233  abliso  31284  ogrpaddltbi  31323  ogrpaddltrbid  31325  ogrpinvlt  31328  cyc3co2  31386  cyc3genpmlem  31397  cycpmconjs  31402  cyc3conja  31403  archiabllem2a  31427  archiabllem2c  31428  archiabllem2b  31429  dvrdir  31466  imaslmod  31532  quslmod  31533  qusxpid  31538  nsgmgclem  31575  drgextlsp  31660  matunitlindflem1  35752  nelsubgcld  40201  evlsaddval  40257  fsuppssind  40262  gicabl  40904  isnumbasgrplem2  40909  mendlmod  40998