Theorem grpcl 18630

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

Syntax hints:   → wi 4   ∧ w3a 1087   = wceq 1539   ∈ wcel 2104  ‘cfv 6458  (class class class)co 7307  Basecbs 16957  +_gcplusg 17007  Mndcmnd 18430  Grpcgrp 18622

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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2707  ax-nul 5239

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 846  df-3an 1089  df-tru 1542  df-fal 1552  df-ex 1780  df-sb 2066  df-clab 2714  df-cleq 2728  df-clel 2814  df-ne 2942  df-ral 3063  df-rex 3072  df-rab 3287  df-v 3439  df-sbc 3722  df-dif 3895  df-un 3897  df-in 3899  df-ss 3909  df-nul 4263  df-if 4466  df-sn 4566  df-pr 4568  df-op 4572  df-uni 4845  df-br 5082  df-iota 6410  df-fv 6466  df-ov 7310  df-mgm 18371  df-sgrp 18420  df-mnd 18431  df-grp 18625

This theorem is referenced by:  grpcld  18635  grprcan  18658  grprinv  18674  grplmulf1o  18694  grpinvadd  18698  grpsubf  18699  grpsubadd  18708  grpaddsubass  18710  grpnpcan  18712  grpsubsub4  18713  grppnpcan2  18714  grplactcnv  18723  imasgrp  18736  mulgcl  18766  mulgaddcomlem  18771  mulgdir  18780  subgcl  18810  nsgacs  18835  nmzsubg  18838  nsgid  18843  eqger  18851  eqgcpbl  18855  qusgrp  18856  qusadd  18858  ghmrn  18892  idghm  18894  ghmpreima  18901  ghmnsgima  18903  ghmnsgpreima  18904  ghmf1o  18909  conjghm  18910  conjnmz  18913  qusghm  18916  gaid  18950  subgga  18951  gass  18952  gaorber  18959  gastacl  18960  gastacos  18961  cntzsubg  18988  galactghm  19057  lactghmga  19058  symgsssg  19120  symgfisg  19121  symggen  19123  sylow1lem2  19249  sylow2blem1  19270  sylow2blem2  19271  sylow2blem3  19272  sylow3lem1  19277  sylow3lem2  19278  subgdisj1  19342  ablsub4  19459  abladdsub4  19460  mulgdi  19473  mulgghm  19475  invghm  19480  ghmplusg  19492  odadd1  19494  odadd2  19495  odadd  19496  gex2abl  19497  gexexlem  19498  torsubg  19500  oddvdssubg  19501  frgpnabllem2  19520  ringacl  19862  ringpropd  19866  drngmcl  20049  abvtrivd  20145  idsrngd  20167  lmodacl  20179  lmodvacl  20182  lmodprop2d  20230  rmodislmod  20236  rmodislmodOLD  20237  prdslmodd  20276  pwssplit2  20367  evpmodpmf1o  20846  frlmplusgvalb  21021  asclghm  21132  psraddcl  21197  mplind  21323  evlslem1  21337  mhpaddcl  21386  evl1addd  21552  scmataddcl  21710  mdetralt  21802  mdetunilem6  21811  opnsubg  23304  ghmcnp  23311  qustgpopn  23316  ngprcan  23811  ngpocelbl  23913  nmotri  23948  ncvspi  24365  cphipval2  24450  4cphipval2  24451  cphipval  24452  efsubm  25752  abvcxp  26808  ttgcontlem1  27297  abliso  31350  ogrpaddltbi  31389  ogrpaddltrbid  31391  ogrpinvlt  31394  cyc3co2  31452  cyc3genpmlem  31463  cycpmconjs  31468  cyc3conja  31469  archiabllem2a  31493  archiabllem2c  31494  archiabllem2b  31495  dvrdir  31532  imaslmod  31598  quslmod  31599  qusxpid  31604  nsgmgclem  31641  drgextlsp  31726  matunitlindflem1  35817  nelsubgcld  40258  evlsaddval  40314  fsuppssind  40319  gicabl  40962  isnumbasgrplem2  40967  mendlmod  41056