Theorem grpcl 18239

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

Syntax hints:   → wi 4   ∧ w3a 1088   = wceq 1542   ∈ wcel 2114  ‘cfv 6349  (class class class)co 7182  Basecbs 16598  +_gcplusg 16680  Mndcmnd 18039  Grpcgrp 18231

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2020  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2162  ax-12 2179  ax-ext 2711  ax-nul 5184

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1787  df-nf 1791  df-sb 2075  df-mo 2541  df-eu 2571  df-clab 2718  df-cleq 2731  df-clel 2812  df-ral 3059  df-rex 3060  df-rab 3063  df-v 3402  df-sbc 3686  df-dif 3856  df-un 3858  df-in 3860  df-ss 3870  df-nul 4222  df-sn 4527  df-pr 4529  df-op 4533  df-uni 4807  df-br 5041  df-iota 6307  df-fv 6357  df-ov 7185  df-mgm 17980  df-sgrp 18029  df-mnd 18040  df-grp 18234

This theorem is referenced by:  grpcld  18244  grprcan  18267  grprinv  18283  grplmulf1o  18303  grpinvadd  18307  grpsubf  18308  grpsubadd  18317  grpaddsubass  18319  grpnpcan  18321  grpsubsub4  18322  grppnpcan2  18323  dfgrp3  18328  grplactcnv  18332  imasgrp  18345  mulgcl  18375  mulgaddcomlem  18380  mulgdir  18389  subgcl  18419  nsgacs  18444  nmzsubg  18447  nsgid  18452  eqger  18460  eqgcpbl  18464  qusgrp  18465  qusadd  18467  ghmrn  18501  idghm  18503  ghmpreima  18510  ghmnsgima  18512  ghmnsgpreima  18513  ghmf1o  18518  conjghm  18519  conjnmz  18522  qusghm  18525  gaid  18559  subgga  18560  gass  18561  gaorber  18568  gastacl  18569  gastacos  18570  cntzsubg  18597  galactghm  18662  lactghmga  18663  symgsssg  18725  symgfisg  18726  symggen  18728  sylow1lem2  18854  sylow2blem1  18875  sylow2blem2  18876  sylow2blem3  18877  sylow3lem1  18882  sylow3lem2  18883  subgdisj1  18947  ablsub4  19064  abladdsub4  19065  mulgdi  19078  mulgghm  19080  invghm  19085  ghmplusg  19097  odadd1  19099  odadd2  19100  odadd  19101  gex2abl  19102  gexexlem  19103  torsubg  19105  oddvdssubg  19106  frgpnabllem2  19125  ringacl  19462  ringpropd  19466  drngmcl  19646  abvtrivd  19742  idsrngd  19764  lmodacl  19776  lmodvacl  19779  lmodprop2d  19827  rmodislmod  19833  prdslmodd  19872  pwssplit2  19963  evpmodpmf1o  20424  frlmplusgvalb  20597  asclghm  20708  psraddcl  20774  mplind  20894  evlslem1  20908  mhpaddcl  20957  evl1addd  21123  scmataddcl  21279  mdetralt  21371  mdetunilem6  21380  opnsubg  22871  ghmcnp  22878  qustgpopn  22883  ngprcan  23375  ngpocelbl  23469  nmotri  23504  ncvspi  23920  cphipval2  24005  4cphipval2  24006  cphipval  24007  efsubm  25307  abvcxp  26363  ttgcontlem1  26843  abliso  30894  ogrpaddltbi  30933  ogrpaddltrbid  30935  ogrpinvlt  30938  cyc3co2  30996  cyc3genpmlem  31007  cycpmconjs  31012  cyc3conja  31013  archiabllem2a  31037  archiabllem2c  31038  archiabllem2b  31039  dvrdir  31076  imaslmod  31137  quslmod  31138  qusxpid  31143  nsgmgclem  31180  drgextlsp  31265  matunitlindflem1  35428  nelsubgcld  39843  evlsaddval  39896  fsuppssind  39901  gicabl  40536  isnumbasgrplem2  40541  mendlmod  40630