Theorem grpcl 18959

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

Syntax hints:   → wi 4   ∧ w3a 1095   = wceq 1554   ∈ wcel 2136  ‘cfv 6510  (class class class)co 7385  Basecbs 17221  +_gcplusg 17262  Mndcmnd 18744  Grpcgrp 18951

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1809  ax-4 1823  ax-5 1924  ax-6 1981  ax-7 2022  ax-8 2138  ax-9 2146  ax-ext 2728  ax-nul 5250

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 857  df-3an 1097  df-tru 1557  df-fal 1567  df-ex 1794  df-sb 2085  df-clab 2735  df-cleq 2748  df-clel 2831  df-ne 2952  df-ral 3071  df-rex 3081  df-rab 3409  df-v 3450  df-sbc 3740  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4281  df-if 4475  df-sn 4577  df-pr 4579  df-op 4583  df-uni 4860  df-br 5095  df-iota 6466  df-fv 6518  df-ov 7388  df-mgm 18650  df-sgrp 18729  df-mnd 18745  df-grp 18954

This theorem is referenced by:  grpcld  18965  grprcan  18991  grprinv  19008  grplmulf1o  19031  grpinvadd  19036  grpsubf  19037  grpsubadd  19046  grpaddsubass  19048  grpnpcan  19050  grpsubsub4  19051  grppnpcan2  19052  grplactcnv  19061  imasgrp  19074  mulgcl  19109  mulgaddcomlem  19115  mulgdir  19124  subgcl  19154  nsgacs  19179  nmzsubg  19182  nsgid  19187  eqgcpbl  19199  qusgrp  19203  qusadd  19205  ecqusaddcl  19210  qus0subgadd  19216  ghmrn  19245  idghm  19247  ghmpreima  19254  ghmnsgima  19256  ghmnsgpreima  19257  ghmf1o  19264  conjghm  19265  qusghm  19271  gaid  19315  subgga  19316  gass  19317  gaorber  19324  gastacl  19325  gastacos  19326  cntzsubg  19355  galactghm  19420  lactghmga  19421  symgsssg  19483  symgfisg  19484  symggen  19486  sylow1lem2  19615  sylow2blem1  19636  sylow2blem2  19637  sylow2blem3  19638  sylow3lem1  19643  sylow3lem2  19644  subgdisj1  19707  ablsub4  19826  abladdsub4  19827  mulgdi  19842  mulgghm  19844  invghm  19849  ghmplusg  19862  odadd1  19864  odadd2  19865  odadd  19866  gex2abl  19867  gexexlem  19868  torsubg  19870  oddvdssubg  19871  frgpnabllem2  19890  ogrpaddltbi  20155  ogrpaddltrbid  20157  ogrpinvlt  20160  rngacl  20184  rngpropd  20196  ringacl  20300  ringpropd  20310  dvrdir  20433  drngmclOLD  20773  abvtrivd  20854  idsrngd  20878  lmodacl  20912  lmodvacl  20915  lmodprop2d  20964  rmodislmod  20970  prdslmodd  21009  pwssplit2  21100  evpmodpmf1o  21621  frlmplusgvalb  21794  asclghm  21907  mplind  22096  evlslem1  22108  evlsaddval  22155  evl1addd  22377  scmataddcl  22549  mdetralt  22641  mdetunilem6  22650  opnsubg  24141  ghmcnp  24148  qustgpopn  24153  ngprcan  24643  ngpocelbl  24737  nmotri  24772  ncvspi  25191  cphipval2  25276  4cphipval2  25277  cphipval  25278  efsubm  26586  abvcxp  27649  ttgcontlem1  29024  abliso  33168  cyc3co2  33274  cyc3genpmlem  33285  cycpmconjs  33290  cyc3conja  33291  archiabllem2a  33328  archiabllem2c  33329  archiabllem2b  33330  imaslmod  33493  quslmod  33498  qusxpid  33503  nsgmgclem  33551  drgextlsp  33845  matunitlindflem1  38063  fldhmf1  42655  primrootsunit1  42662  aks6d1c1p2  42674  aks6d1c1p3  42675  nelsubgcld  43067  fsuppssind  43123  gicabl  43624  isnumbasgrplem2  43629  mendlmod  43714