Theorem grpcl 19069

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

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1103   = wceq 1570   ∈ wcel 2145  ‘cfv 6537  (class class class)co 7416  Basecbs 17305  +_gcplusg 17346  Mndcmnd 18840  Grpcgrp 19061

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 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734  ax-nul 5267

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 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-ne 2958  df-ral 3079  df-rex 3089  df-rab 3415  df-v 3455  df-sbc 3743  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4283  df-if 4486  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4871  df-br 5108  df-iota 6493  df-fv 6545  df-ov 7419  df-mgm 18734  df-sgrp 18825  df-mnd 18841  df-grp 19064

This theorem is used by:  grpcld  19075  grprcan  19101  grprinv  19118  grplmulf1o  19140  grpinvadd  19145  grpsubf  19146  grpsubadd  19155  grpaddsubass  19157  grpnpcan  19159  grpsubsub4  19160  grppnpcan2  19161  grplactcnv  19170  imasgrp  19183  mulgcl  19218  mulgaddcomlem  19224  mulgdir  19233  subgcl  19263  nsgacs  19289  nmzsubg  19292  nsgid  19297  eqgcpbl  19311  qusxpid  19312  qusgrp  19318  qusadd  19320  ecqusaddcl  19325  qus0subgadd  19331  ghmrn  19360  idghm  19362  ghmpreima  19369  ghmnsgima  19371  ghmnsgpreima  19372  ghmf1o  19379  conjghm  19380  qusghm  19386  gaid  19430  subgga  19431  gass  19432  gaorber  19439  gastacl  19440  gastacos  19441  cntzsubg  19470  galactghm  19535  lactghmga  19536  symgsssg  19598  symgfisg  19599  symggen  19601  sylow1lem2  19730  sylow2blem1  19751  sylow2blem2  19752  sylow2blem3  19753  sylow3lem1  19758  sylow3lem2  19759  subgdisj1  19822  ablsub4  19941  abladdsub4  19942  mulgdi  19957  mulgghm  19959  invghm  19964  ghmplusg  19977  odadd1  19979  odadd2  19980  odadd  19981  gex2abl  19982  gexexlem  19983  torsubg  19985  oddvdssubg  19986  frgpnabllem2  20005  ogrpaddltbi  20270  ogrpaddltrbid  20272  ogrpinvlt  20275  rngacl  20301  rngpropd  20313  ringacl  20423  ringpropd  20434  dvrdir  20557  abvtrivd  21002  idsrngd  21026  lmodacl  21060  lmodvacl  21063  lmodprop2d  21112  rmodislmod  21118  prdslmodd  21157  pwssplit2  21248  evpmodpmf1o  21813  frlmplusgvalb  21986  asclghm  22101  mplind  22290  evlslem1  22302  evlsaddval  22349  evl1addd  22570  scmataddcl  22742  mdetralt  22834  mdetunilem6  22843  matunitlindflem1  22905  opnsubg  24338  ghmcnp  24345  qustgpopn  24350  ngprcan  24840  ngpocelbl  24934  nmotri  24969  ncvspi  25388  cphipval2  25473  4cphipval2  25474  cphipval  25475  efsubm  26789  abvcxp  27852  ttgcontlem1  29342  abliso  33477  cyc3co2  33582  cyc3genpmlem  33593  cycpmconjs  33598  cyc3conja  33599  archiabllem2a  33636  archiabllem2c  33637  archiabllem2b  33638  imaslmod  33795  quslmod  33800  nsgmgclem  33842  drgextlsp  34106  fldhmf1  42958  primrootsunit1  42965  aks6d1c1p2  42977  aks6d1c1p3  42978  nelsubgcld  43387  fsuppssind  43441  gicabl  43942  isnumbasgrplem2  43947  mendlmod  44032