Theorem grpcl 18906

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

Syntax hints:   → wi 4   ∧ w3a 1087   = wceq 1542   ∈ wcel 2114  ‘cfv 6490  (class class class)co 7358  Basecbs 17168  +_gcplusg 17209  Mndcmnd 18691  Grpcgrp 18898

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-nul 5241

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ne 2934  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-sbc 3730  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-iota 6446  df-fv 6498  df-ov 7361  df-mgm 18597  df-sgrp 18676  df-mnd 18692  df-grp 18901

This theorem is referenced by:  grpcld  18912  grprcan  18938  grprinv  18955  grplmulf1o  18978  grpinvadd  18983  grpsubf  18984  grpsubadd  18993  grpaddsubass  18995  grpnpcan  18997  grpsubsub4  18998  grppnpcan2  18999  grplactcnv  19008  imasgrp  19021  mulgcl  19056  mulgaddcomlem  19062  mulgdir  19071  subgcl  19101  nsgacs  19126  nmzsubg  19129  nsgid  19134  eqgcpbl  19146  qusgrp  19150  qusadd  19152  ecqusaddcl  19157  qus0subgadd  19163  ghmrn  19193  idghm  19195  ghmpreima  19202  ghmnsgima  19204  ghmnsgpreima  19205  ghmf1o  19212  conjghm  19213  qusghm  19219  gaid  19263  subgga  19264  gass  19265  gaorber  19272  gastacl  19273  gastacos  19274  cntzsubg  19303  galactghm  19368  lactghmga  19369  symgsssg  19431  symgfisg  19432  symggen  19434  sylow1lem2  19563  sylow2blem1  19584  sylow2blem2  19585  sylow2blem3  19586  sylow3lem1  19591  sylow3lem2  19592  subgdisj1  19655  ablsub4  19774  abladdsub4  19775  mulgdi  19790  mulgghm  19792  invghm  19797  ghmplusg  19810  odadd1  19812  odadd2  19813  odadd  19814  gex2abl  19815  gexexlem  19816  torsubg  19818  oddvdssubg  19819  frgpnabllem2  19838  ogrpaddltbi  20103  ogrpaddltrbid  20105  ogrpinvlt  20108  rngacl  20132  rngpropd  20144  ringacl  20248  ringpropd  20258  dvrdir  20381  drngmclOLD  20717  abvtrivd  20798  idsrngd  20822  lmodacl  20856  lmodvacl  20859  lmodprop2d  20908  rmodislmod  20914  prdslmodd  20953  pwssplit2  21045  evpmodpmf1o  21584  frlmplusgvalb  21757  asclghm  21870  psraddclOLD  21927  mplind  22057  evlslem1  22069  evl1addd  22315  scmataddcl  22490  mdetralt  22582  mdetunilem6  22591  opnsubg  24082  ghmcnp  24089  qustgpopn  24094  ngprcan  24584  ngpocelbl  24678  nmotri  24713  ncvspi  25132  cphipval2  25217  4cphipval2  25218  cphipval  25219  efsubm  26531  abvcxp  27597  ttgcontlem1  28972  abliso  33116  cyc3co2  33221  cyc3genpmlem  33232  cycpmconjs  33237  cyc3conja  33238  archiabllem2a  33275  archiabllem2c  33276  archiabllem2b  33277  imaslmod  33433  quslmod  33438  qusxpid  33443  nsgmgclem  33491  drgextlsp  33758  matunitlindflem1  37948  fldhmf1  42540  primrootsunit1  42547  aks6d1c1p2  42559  aks6d1c1p3  42560  nelsubgcld  42953  evlsaddval  43015  fsuppssind  43037  gicabl  43542  isnumbasgrplem2  43547  mendlmod  43632