Theorem grpcl 18824

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

Syntax hints:   → wi 4   ∧ w3a 1088   = wceq 1542   ∈ wcel 2107  ‘cfv 6541  (class class class)co 7406  Basecbs 17141  +_gcplusg 17194  Mndcmnd 18622  Grpcgrp 18816

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704  ax-nul 5306

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-ne 2942  df-ral 3063  df-rex 3072  df-rab 3434  df-v 3477  df-sbc 3778  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-br 5149  df-iota 6493  df-fv 6549  df-ov 7409  df-mgm 18558  df-sgrp 18607  df-mnd 18623  df-grp 18819

This theorem is referenced by:  grpcld  18830  grprcan  18855  grprinv  18872  grplmulf1o  18894  grpinvadd  18898  grpsubf  18899  grpsubadd  18908  grpaddsubass  18910  grpnpcan  18912  grpsubsub4  18913  grppnpcan2  18914  grplactcnv  18923  imasgrp  18936  mulgcl  18966  mulgaddcomlem  18972  mulgdir  18981  subgcl  19011  nsgacs  19037  nmzsubg  19040  nsgid  19045  eqgcpbl  19057  qusgrp  19060  qusadd  19062  qus0subgadd  19071  ghmrn  19100  idghm  19102  ghmpreima  19109  ghmnsgima  19111  ghmnsgpreima  19112  ghmf1o  19117  conjghm  19118  conjnmz  19121  qusghm  19124  gaid  19158  subgga  19159  gass  19160  gaorber  19167  gastacl  19168  gastacos  19169  cntzsubg  19198  galactghm  19267  lactghmga  19268  symgsssg  19330  symgfisg  19331  symggen  19333  sylow1lem2  19462  sylow2blem1  19483  sylow2blem2  19484  sylow2blem3  19485  sylow3lem1  19490  sylow3lem2  19491  subgdisj1  19554  ablsub4  19673  abladdsub4  19674  mulgdi  19689  mulgghm  19691  invghm  19696  ghmplusg  19709  odadd1  19711  odadd2  19712  odadd  19713  gex2abl  19714  gexexlem  19715  torsubg  19717  oddvdssubg  19718  frgpnabllem2  19737  ringacl  20089  ringpropd  20096  dvrdir  20219  drngmcl  20325  abvtrivd  20441  idsrngd  20463  lmodacl  20476  lmodvacl  20479  lmodprop2d  20527  rmodislmod  20533  rmodislmodOLD  20534  prdslmodd  20573  pwssplit2  20664  evpmodpmf1o  21141  frlmplusgvalb  21316  asclghm  21429  psraddcl  21494  mplind  21623  evlslem1  21637  mhpaddcl  21686  evl1addd  21852  scmataddcl  22010  mdetralt  22102  mdetunilem6  22111  opnsubg  23604  ghmcnp  23611  qustgpopn  23616  ngprcan  24111  ngpocelbl  24213  nmotri  24248  ncvspi  24665  cphipval2  24750  4cphipval2  24751  cphipval  24752  efsubm  26052  abvcxp  27108  ttgcontlem1  28132  abliso  32185  ogrpaddltbi  32224  ogrpaddltrbid  32226  ogrpinvlt  32229  cyc3co2  32287  cyc3genpmlem  32298  cycpmconjs  32303  cyc3conja  32304  archiabllem2a  32328  archiabllem2c  32329  archiabllem2b  32330  imaslmod  32457  quslmod  32458  qusxpid  32464  nsgmgclem  32511  drgextlsp  32670  matunitlindflem1  36473  fldhmf1  40944  nelsubgcld  41069  evlsaddval  41138  fsuppssind  41163  gicabl  41827  isnumbasgrplem2  41832  mendlmod  41921  rngacl  46648  rngpropd  46660  ecqusaddcl  46751