Theorem grpcl 19181

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

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1103   = wceq 1570   ∈ wcel 2147  ‘cfv 6558  (class class class)co 7443  Basecbs 17416  +_gcplusg 17457  Mndcmnd 18952  Grpcgrp 19173

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-nul 5263

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-ne 2960  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-sbc 3743  df-ss 3901  df-dif 4050  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-br 5107  df-iota 6512  df-fv 6566  df-ov 7446  df-mgm 18845  df-sgrp 18937  df-mnd 18953  df-grp 19176

This theorem is used by:  grpcld  19187  grprcan  19213  grprinv  19230  grplmulf1o  19252  grpinvadd  19257  grpsubf  19258  grpsubadd  19267  grpaddsubass  19269  grpnpcan  19271  grpsubsub4  19272  grppnpcan2  19273  grplactcnv  19282  imasgrp  19295  mulgcl  19330  mulgaddcomlem  19336  mulgdir  19345  subgcl  19375  nsgacs  19401  nmzsubg  19404  nsgid  19409  eqgcpbl  19423  qusxpid  19424  qusgrp  19430  qusadd  19432  ecqusaddcl  19437  qus0subgadd  19443  ghmrn  19472  idghm  19474  ghmpreima  19481  ghmnsgima  19483  ghmnsgpreima  19484  ghmf1o  19491  conjghm  19492  qusghm  19498  gaid  19543  subgga  19544  gass  19545  gaorber  19552  gastacl  19553  gastacos  19554  cntzsubg  19583  galactghm  19648  lactghmga  19649  symgsssg  19711  symgfisg  19712  symggen  19714  sylow1lem2  19843  sylow2blem1  19864  sylow2blem2  19865  sylow2blem3  19866  sylow3lem1  19871  sylow3lem2  19872  subgdisj1  19935  ablsub4  20054  abladdsub4  20055  mulgdi  20070  mulgghm  20072  invghm  20077  ghmplusg  20090  odadd1  20092  odadd2  20093  odadd  20094  gex2abl  20095  gexexlem  20096  torsubg  20098  oddvdssubg  20099  frgpnabllem2  20118  ogrpaddltbi  20383  ogrpaddltrbid  20385  ogrpinvlt  20388  rngacl  20414  rngpropd  20426  ringacl  20537  ringpropd  20549  dvrdir  20672  abvtrivd  21119  idsrngd  21143  lmodacl  21177  lmodvacl  21180  lmodprop2d  21229  rmodislmod  21235  prdslmodd  21274  pwssplit2  21365  evpmodpmf1o  21932  frlmplusgvalb  22105  asclghm  22220  mplind  22409  evlslem1  22421  evlsaddval  22468  evl1addd  22689  scmataddcl  22861  mdetralt  22953  mdetunilem6  22962  matunitlindflem1  23024  opnsubg  24457  ghmcnp  24464  qustgpopn  24469  ngprcan  24959  ngpocelbl  25053  nmotri  25088  ncvspi  25507  cphipval2  25592  4cphipval2  25593  cphipval  25594  efsubm  26909  abvcxp  27972  ttgcontlem1  29492  abliso  33666  cyc3co2  33771  cyc3genpmlem  33782  cycpmconjs  33787  cyc3conja  33788  archiabllem2a  33825  archiabllem2c  33826  archiabllem2b  33827  imaslmod  33984  quslmod  33989  nsgmgclem  34032  drgextlsp  34296  fldhmf1  43332  primrootsunit1  43339  aks6d1c1p2  43351  aks6d1c1p3  43352  nelsubgcld  43754  fsuppssind  43814  gicabl  44294  isnumbasgrplem2  44298  mendlmod  44383