Theorem grpcl 19114

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

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1103   = wceq 1570   ∈ wcel 2145  ‘cfv 6527  (class class class)co 7408  Basecbs 17349  +_gcplusg 17390  Mndcmnd 18885  Grpcgrp 19106

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 2732  ax-nul 5259

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 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-dif 3901  df-un 3903  df-ss 3915  df-nul 4279  df-if 4482  df-sn 4584  df-pr 4586  df-op 4590  df-uni 4867  df-br 5103  df-iota 6483  df-fv 6535  df-ov 7411  df-mgm 18778  df-sgrp 18870  df-mnd 18886  df-grp 19109

This theorem is used by:  grpcld  19120  grprcan  19146  grprinv  19163  grplmulf1o  19185  grpinvadd  19190  grpsubf  19191  grpsubadd  19200  grpaddsubass  19202  grpnpcan  19204  grpsubsub4  19205  grppnpcan2  19206  grplactcnv  19215  imasgrp  19228  mulgcl  19263  mulgaddcomlem  19269  mulgdir  19278  subgcl  19308  nsgacs  19334  nmzsubg  19337  nsgid  19342  eqgcpbl  19356  qusxpid  19357  qusgrp  19363  qusadd  19365  ecqusaddcl  19370  qus0subgadd  19376  ghmrn  19405  idghm  19407  ghmpreima  19414  ghmnsgima  19416  ghmnsgpreima  19417  ghmf1o  19424  conjghm  19425  qusghm  19431  gaid  19475  subgga  19476  gass  19477  gaorber  19484  gastacl  19485  gastacos  19486  cntzsubg  19515  galactghm  19580  lactghmga  19581  symgsssg  19643  symgfisg  19644  symggen  19646  sylow1lem2  19775  sylow2blem1  19796  sylow2blem2  19797  sylow2blem3  19798  sylow3lem1  19803  sylow3lem2  19804  subgdisj1  19867  ablsub4  19986  abladdsub4  19987  mulgdi  20002  mulgghm  20004  invghm  20009  ghmplusg  20022  odadd1  20024  odadd2  20025  odadd  20026  gex2abl  20027  gexexlem  20028  torsubg  20030  oddvdssubg  20031  frgpnabllem2  20050  ogrpaddltbi  20315  ogrpaddltrbid  20317  ogrpinvlt  20320  rngacl  20346  rngpropd  20358  ringacl  20469  ringpropd  20481  dvrdir  20604  abvtrivd  21051  idsrngd  21075  lmodacl  21109  lmodvacl  21112  lmodprop2d  21161  rmodislmod  21167  prdslmodd  21206  pwssplit2  21297  evpmodpmf1o  21864  frlmplusgvalb  22037  asclghm  22152  mplind  22341  evlslem1  22353  evlsaddval  22400  evl1addd  22621  scmataddcl  22793  mdetralt  22885  mdetunilem6  22894  matunitlindflem1  22956  opnsubg  24389  ghmcnp  24396  qustgpopn  24401  ngprcan  24891  ngpocelbl  24985  nmotri  25020  ncvspi  25439  cphipval2  25524  4cphipval2  25525  cphipval  25526  efsubm  26843  abvcxp  27906  ttgcontlem1  29396  abliso  33530  cyc3co2  33635  cyc3genpmlem  33646  cycpmconjs  33651  cyc3conja  33652  archiabllem2a  33689  archiabllem2c  33690  archiabllem2b  33691  imaslmod  33848  quslmod  33853  nsgmgclem  33896  drgextlsp  34160  fldhmf1  43060  primrootsunit1  43067  aks6d1c1p2  43079  aks6d1c1p3  43080  nelsubgcld  43489  fsuppssind  43543  gicabl  44044  isnumbasgrplem2  44049  mendlmod  44134