Theorem grpcl 18880

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

Syntax hints:   → wi 4   ∧ w3a 1086   = wceq 1540   ∈ wcel 2109  ‘cfv 6514  (class class class)co 7390  Basecbs 17186  +_gcplusg 17227  Mndcmnd 18668  Grpcgrp 18872

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 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702  ax-nul 5264

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-ne 2927  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-sbc 3757  df-dif 3920  df-un 3922  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-iota 6467  df-fv 6522  df-ov 7393  df-mgm 18574  df-sgrp 18653  df-mnd 18669  df-grp 18875

This theorem is referenced by:  grpcld  18886  grprcan  18912  grprinv  18929  grplmulf1o  18952  grpinvadd  18957  grpsubf  18958  grpsubadd  18967  grpaddsubass  18969  grpnpcan  18971  grpsubsub4  18972  grppnpcan2  18973  grplactcnv  18982  imasgrp  18995  mulgcl  19030  mulgaddcomlem  19036  mulgdir  19045  subgcl  19075  nsgacs  19101  nmzsubg  19104  nsgid  19109  eqgcpbl  19121  qusgrp  19125  qusadd  19127  ecqusaddcl  19132  qus0subgadd  19138  ghmrn  19168  idghm  19170  ghmpreima  19177  ghmnsgima  19179  ghmnsgpreima  19180  ghmf1o  19187  conjghm  19188  qusghm  19194  gaid  19238  subgga  19239  gass  19240  gaorber  19247  gastacl  19248  gastacos  19249  cntzsubg  19278  galactghm  19341  lactghmga  19342  symgsssg  19404  symgfisg  19405  symggen  19407  sylow1lem2  19536  sylow2blem1  19557  sylow2blem2  19558  sylow2blem3  19559  sylow3lem1  19564  sylow3lem2  19565  subgdisj1  19628  ablsub4  19747  abladdsub4  19748  mulgdi  19763  mulgghm  19765  invghm  19770  ghmplusg  19783  odadd1  19785  odadd2  19786  odadd  19787  gex2abl  19788  gexexlem  19789  torsubg  19791  oddvdssubg  19792  frgpnabllem2  19811  rngacl  20078  rngpropd  20090  ringacl  20194  ringpropd  20204  dvrdir  20328  drngmclOLD  20667  abvtrivd  20748  idsrngd  20772  lmodacl  20785  lmodvacl  20788  lmodprop2d  20837  rmodislmod  20843  prdslmodd  20882  pwssplit2  20974  evpmodpmf1o  21512  frlmplusgvalb  21685  asclghm  21799  psraddclOLD  21855  mplind  21984  evlslem1  21996  evl1addd  22235  scmataddcl  22410  mdetralt  22502  mdetunilem6  22511  opnsubg  24002  ghmcnp  24009  qustgpopn  24014  ngprcan  24505  ngpocelbl  24599  nmotri  24634  ncvspi  25063  cphipval2  25148  4cphipval2  25149  cphipval  25150  efsubm  26467  abvcxp  27533  ttgcontlem1  28819  abliso  32984  ogrpaddltbi  33039  ogrpaddltrbid  33041  ogrpinvlt  33044  cyc3co2  33104  cyc3genpmlem  33115  cycpmconjs  33120  cyc3conja  33121  archiabllem2a  33155  archiabllem2c  33156  archiabllem2b  33157  imaslmod  33331  quslmod  33336  qusxpid  33341  nsgmgclem  33389  drgextlsp  33596  matunitlindflem1  37617  fldhmf1  42085  primrootsunit1  42092  aks6d1c1p2  42104  aks6d1c1p3  42105  nelsubgcld  42492  evlsaddval  42563  fsuppssind  42588  gicabl  43095  isnumbasgrplem2  43100  mendlmod  43185