Theorem grpcl 19071

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 19070	. 2 ⊢ (𝐺 ∈ Grp → 𝐺 ∈ Mnd)
2		grpcl.b	. . 3 ⊢ 𝐵 = (Base‘𝐺)
3		grpcl.p	. . 3 ⊢ + = (+g‘𝐺)
4	2, 3	mndcl 18850	. 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 7417  Basecbs 17307  +_gcplusg 17348  Mndcmnd 18842  Grpcgrp 19063

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 7420  df-mgm 18736  df-sgrp 18827  df-mnd 18843  df-grp 19066

This theorem is used by:  grpcld  19077  grprcan  19103  grprinv  19120  grplmulf1o  19142  grpinvadd  19147  grpsubf  19148  grpsubadd  19157  grpaddsubass  19159  grpnpcan  19161  grpsubsub4  19162  grppnpcan2  19163  grplactcnv  19172  imasgrp  19185  mulgcl  19220  mulgaddcomlem  19226  mulgdir  19235  subgcl  19265  nsgacs  19291  nmzsubg  19294  nsgid  19299  eqgcpbl  19313  qusxpid  19314  qusgrp  19320  qusadd  19322  ecqusaddcl  19327  qus0subgadd  19333  ghmrn  19362  idghm  19364  ghmpreima  19371  ghmnsgima  19373  ghmnsgpreima  19374  ghmf1o  19381  conjghm  19382  qusghm  19388  gaid  19432  subgga  19433  gass  19434  gaorber  19441  gastacl  19442  gastacos  19443  cntzsubg  19472  galactghm  19537  lactghmga  19538  symgsssg  19600  symgfisg  19601  symggen  19603  sylow1lem2  19732  sylow2blem1  19753  sylow2blem2  19754  sylow2blem3  19755  sylow3lem1  19760  sylow3lem2  19761  subgdisj1  19824  ablsub4  19943  abladdsub4  19944  mulgdi  19959  mulgghm  19961  invghm  19966  ghmplusg  19979  odadd1  19981  odadd2  19982  odadd  19983  gex2abl  19984  gexexlem  19985  torsubg  19987  oddvdssubg  19988  frgpnabllem2  20007  ogrpaddltbi  20272  ogrpaddltrbid  20274  ogrpinvlt  20277  rngacl  20303  rngpropd  20315  ringacl  20425  ringpropd  20436  dvrdir  20559  abvtrivd  21004  idsrngd  21028  lmodacl  21062  lmodvacl  21065  lmodprop2d  21114  rmodislmod  21120  prdslmodd  21159  pwssplit2  21250  evpmodpmf1o  21815  frlmplusgvalb  21988  asclghm  22103  mplind  22292  evlslem1  22304  evlsaddval  22351  evl1addd  22572  scmataddcl  22744  mdetralt  22836  mdetunilem6  22845  matunitlindflem1  22907  opnsubg  24340  ghmcnp  24347  qustgpopn  24352  ngprcan  24842  ngpocelbl  24936  nmotri  24971  ncvspi  25390  cphipval2  25475  4cphipval2  25476  cphipval  25477  efsubm  26796  abvcxp  27859  ttgcontlem1  29349  abliso  33483  cyc3co2  33588  cyc3genpmlem  33599  cycpmconjs  33604  cyc3conja  33605  archiabllem2a  33642  archiabllem2c  33643  archiabllem2b  33644  imaslmod  33801  quslmod  33806  nsgmgclem  33848  drgextlsp  34112  fldhmf1  42964  primrootsunit1  42971  aks6d1c1p2  42983  aks6d1c1p3  42984  nelsubgcld  43393  fsuppssind  43447  gicabl  43948  isnumbasgrplem2  43953  mendlmod  44038