Theorem grpcl 18871

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

Syntax hints:   → wi 4   ∧ w3a 1086   = wceq 1541   ∈ wcel 2113  ‘cfv 6492  (class class class)co 7358  Basecbs 17136  +_gcplusg 17177  Mndcmnd 18659  Grpcgrp 18863

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708  ax-nul 5251

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-ne 2933  df-ral 3052  df-rex 3061  df-rab 3400  df-v 3442  df-sbc 3741  df-dif 3904  df-un 3906  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-br 5099  df-iota 6448  df-fv 6500  df-ov 7361  df-mgm 18565  df-sgrp 18644  df-mnd 18660  df-grp 18866

This theorem is referenced by:  grpcld  18877  grprcan  18903  grprinv  18920  grplmulf1o  18943  grpinvadd  18948  grpsubf  18949  grpsubadd  18958  grpaddsubass  18960  grpnpcan  18962  grpsubsub4  18963  grppnpcan2  18964  grplactcnv  18973  imasgrp  18986  mulgcl  19021  mulgaddcomlem  19027  mulgdir  19036  subgcl  19066  nsgacs  19091  nmzsubg  19094  nsgid  19099  eqgcpbl  19111  qusgrp  19115  qusadd  19117  ecqusaddcl  19122  qus0subgadd  19128  ghmrn  19158  idghm  19160  ghmpreima  19167  ghmnsgima  19169  ghmnsgpreima  19170  ghmf1o  19177  conjghm  19178  qusghm  19184  gaid  19228  subgga  19229  gass  19230  gaorber  19237  gastacl  19238  gastacos  19239  cntzsubg  19268  galactghm  19333  lactghmga  19334  symgsssg  19396  symgfisg  19397  symggen  19399  sylow1lem2  19528  sylow2blem1  19549  sylow2blem2  19550  sylow2blem3  19551  sylow3lem1  19556  sylow3lem2  19557  subgdisj1  19620  ablsub4  19739  abladdsub4  19740  mulgdi  19755  mulgghm  19757  invghm  19762  ghmplusg  19775  odadd1  19777  odadd2  19778  odadd  19779  gex2abl  19780  gexexlem  19781  torsubg  19783  oddvdssubg  19784  frgpnabllem2  19803  ogrpaddltbi  20068  ogrpaddltrbid  20070  ogrpinvlt  20073  rngacl  20097  rngpropd  20109  ringacl  20213  ringpropd  20223  dvrdir  20348  drngmclOLD  20684  abvtrivd  20765  idsrngd  20789  lmodacl  20823  lmodvacl  20826  lmodprop2d  20875  rmodislmod  20881  prdslmodd  20920  pwssplit2  21012  evpmodpmf1o  21551  frlmplusgvalb  21724  asclghm  21838  psraddclOLD  21895  mplind  22025  evlslem1  22037  evl1addd  22285  scmataddcl  22460  mdetralt  22552  mdetunilem6  22561  opnsubg  24052  ghmcnp  24059  qustgpopn  24064  ngprcan  24554  ngpocelbl  24648  nmotri  24683  ncvspi  25112  cphipval2  25197  4cphipval2  25198  cphipval  25199  efsubm  26516  abvcxp  27582  ttgcontlem1  28957  abliso  33118  cyc3co2  33222  cyc3genpmlem  33233  cycpmconjs  33238  cyc3conja  33239  archiabllem2a  33276  archiabllem2c  33277  archiabllem2b  33278  imaslmod  33434  quslmod  33439  qusxpid  33444  nsgmgclem  33492  drgextlsp  33750  matunitlindflem1  37817  fldhmf1  42344  primrootsunit1  42351  aks6d1c1p2  42363  aks6d1c1p3  42364  nelsubgcld  42752  evlsaddval  42814  fsuppssind  42836  gicabl  43341  isnumbasgrplem2  43346  mendlmod  43431