Theorem grpcl 18864

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

Syntax hints:   → wi 4   ∧ w3a 1086   = wceq 1541   ∈ wcel 2113  ‘cfv 6489  (class class class)co 7355  Basecbs 17130  +_gcplusg 17171  Mndcmnd 18652  Grpcgrp 18856

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705  ax-nul 5248

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-ne 2931  df-ral 3050  df-rex 3059  df-rab 3398  df-v 3440  df-sbc 3739  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4861  df-br 5096  df-iota 6445  df-fv 6497  df-ov 7358  df-mgm 18558  df-sgrp 18637  df-mnd 18653  df-grp 18859

This theorem is referenced by:  grpcld  18870  grprcan  18896  grprinv  18913  grplmulf1o  18936  grpinvadd  18941  grpsubf  18942  grpsubadd  18951  grpaddsubass  18953  grpnpcan  18955  grpsubsub4  18956  grppnpcan2  18957  grplactcnv  18966  imasgrp  18979  mulgcl  19014  mulgaddcomlem  19020  mulgdir  19029  subgcl  19059  nsgacs  19084  nmzsubg  19087  nsgid  19092  eqgcpbl  19104  qusgrp  19108  qusadd  19110  ecqusaddcl  19115  qus0subgadd  19121  ghmrn  19151  idghm  19153  ghmpreima  19160  ghmnsgima  19162  ghmnsgpreima  19163  ghmf1o  19170  conjghm  19171  qusghm  19177  gaid  19221  subgga  19222  gass  19223  gaorber  19230  gastacl  19231  gastacos  19232  cntzsubg  19261  galactghm  19326  lactghmga  19327  symgsssg  19389  symgfisg  19390  symggen  19392  sylow1lem2  19521  sylow2blem1  19542  sylow2blem2  19543  sylow2blem3  19544  sylow3lem1  19549  sylow3lem2  19550  subgdisj1  19613  ablsub4  19732  abladdsub4  19733  mulgdi  19748  mulgghm  19750  invghm  19755  ghmplusg  19768  odadd1  19770  odadd2  19771  odadd  19772  gex2abl  19773  gexexlem  19774  torsubg  19776  oddvdssubg  19777  frgpnabllem2  19796  ogrpaddltbi  20061  ogrpaddltrbid  20063  ogrpinvlt  20066  rngacl  20090  rngpropd  20102  ringacl  20206  ringpropd  20216  dvrdir  20340  drngmclOLD  20676  abvtrivd  20757  idsrngd  20781  lmodacl  20815  lmodvacl  20818  lmodprop2d  20867  rmodislmod  20873  prdslmodd  20912  pwssplit2  21004  evpmodpmf1o  21543  frlmplusgvalb  21716  asclghm  21830  psraddclOLD  21886  mplind  22015  evlslem1  22027  evl1addd  22266  scmataddcl  22441  mdetralt  22533  mdetunilem6  22542  opnsubg  24033  ghmcnp  24040  qustgpopn  24045  ngprcan  24535  ngpocelbl  24629  nmotri  24664  ncvspi  25093  cphipval2  25178  4cphipval2  25179  cphipval  25180  efsubm  26497  abvcxp  27563  ttgcontlem1  28873  abliso  33028  cyc3co2  33120  cyc3genpmlem  33131  cycpmconjs  33136  cyc3conja  33137  archiabllem2a  33174  archiabllem2c  33175  archiabllem2b  33176  imaslmod  33329  quslmod  33334  qusxpid  33339  nsgmgclem  33387  drgextlsp  33617  matunitlindflem1  37666  fldhmf1  42193  primrootsunit1  42200  aks6d1c1p2  42212  aks6d1c1p3  42213  nelsubgcld  42605  evlsaddval  42676  fsuppssind  42701  gicabl  43206  isnumbasgrplem2  43211  mendlmod  43296