Theorem grpcl 19153

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

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1103   = wceq 1569   ∈ wcel 2144  ‘cfv 6538  (class class class)co 7420  Basecbs 17388  +_gcplusg 17429  Mndcmnd 18924  Grpcgrp 19145

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-nul 5259

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ne 2956  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-sbc 3739  df-ss 3896  df-dif 4047  df-un 4151  df-nul 4279  df-if 4482  df-sn 4584  df-pr 4586  df-op 4590  df-uni 4867  df-br 5103  df-iota 6494  df-fv 6546  df-ov 7423  df-mgm 18817  df-sgrp 18909  df-mnd 18925  df-grp 19148

This theorem is used by:  grpcld  19159  grprcan  19185  grprinv  19202  grplmulf1o  19224  grpinvadd  19229  grpsubf  19230  grpsubadd  19239  grpaddsubass  19241  grpnpcan  19243  grpsubsub4  19244  grppnpcan2  19245  grplactcnv  19254  imasgrp  19267  mulgcl  19302  mulgaddcomlem  19308  mulgdir  19317  subgcl  19347  nsgacs  19373  nmzsubg  19376  nsgid  19381  eqgcpbl  19395  qusxpid  19396  qusgrp  19402  qusadd  19404  ecqusaddcl  19409  qus0subgadd  19415  ghmrn  19444  idghm  19446  ghmpreima  19453  ghmnsgima  19455  ghmnsgpreima  19456  ghmf1o  19463  conjghm  19464  qusghm  19470  gaid  19514  subgga  19515  gass  19516  gaorber  19523  gastacl  19524  gastacos  19525  cntzsubg  19554  galactghm  19619  lactghmga  19620  symgsssg  19682  symgfisg  19683  symggen  19685  sylow1lem2  19814  sylow2blem1  19835  sylow2blem2  19836  sylow2blem3  19837  sylow3lem1  19842  sylow3lem2  19843  subgdisj1  19906  ablsub4  20025  abladdsub4  20026  mulgdi  20041  mulgghm  20043  invghm  20048  ghmplusg  20061  odadd1  20063  odadd2  20064  odadd  20065  gex2abl  20066  gexexlem  20067  torsubg  20069  oddvdssubg  20070  frgpnabllem2  20089  ogrpaddltbi  20354  ogrpaddltrbid  20356  ogrpinvlt  20359  rngacl  20385  rngpropd  20397  ringacl  20508  ringpropd  20520  dvrdir  20643  abvtrivd  21090  idsrngd  21114  lmodacl  21148  lmodvacl  21151  lmodprop2d  21200  rmodislmod  21206  prdslmodd  21245  pwssplit2  21336  evpmodpmf1o  21903  frlmplusgvalb  22076  asclghm  22191  mplind  22380  evlslem1  22392  evlsaddval  22439  evl1addd  22660  scmataddcl  22832  mdetralt  22924  mdetunilem6  22933  matunitlindflem1  22995  opnsubg  24428  ghmcnp  24435  qustgpopn  24440  ngprcan  24930  ngpocelbl  25024  nmotri  25059  ncvspi  25478  cphipval2  25563  4cphipval2  25564  cphipval  25565  efsubm  26880  abvcxp  27943  ttgcontlem1  29463  abliso  33639  cyc3co2  33744  cyc3genpmlem  33755  cycpmconjs  33760  cyc3conja  33761  archiabllem2a  33798  archiabllem2c  33799  archiabllem2b  33800  imaslmod  33957  quslmod  33962  nsgmgclem  34005  drgextlsp  34269  fldhmf1  43216  primrootsunit1  43223  aks6d1c1p2  43235  aks6d1c1p3  43236  nelsubgcld  43637  fsuppssind  43697  gicabl  44177  isnumbasgrplem2  44182  mendlmod  44267