Theorem grpcl 19007

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

Syntax hints:   → wi 4   ∧ w3a 1101   = wceq 1568   ∈ wcel 2141  ‘cfv 6536  (class class class)co 7410  Basecbs 17268  +_gcplusg 17309  Mndcmnd 18791  Grpcgrp 18999

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1823  ax-4 1837  ax-5 1938  ax-6 1995  ax-7 2036  ax-8 2143  ax-9 2151  ax-ext 2733  ax-nul 5268

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1571  df-fal 1581  df-ex 1808  df-sb 2095  df-clab 2740  df-cleq 2753  df-clel 2836  df-ne 2957  df-ral 3078  df-rex 3088  df-rab 3415  df-v 3455  df-sbc 3744  df-dif 3907  df-un 3909  df-ss 3921  df-nul 4286  df-if 4487  df-sn 4589  df-pr 4591  df-op 4595  df-uni 4872  df-br 5109  df-iota 6492  df-fv 6544  df-ov 7413  df-mgm 18697  df-sgrp 18776  df-mnd 18792  df-grp 19002

This theorem is referenced by:  grpcld  19013  grprcan  19039  grprinv  19056  grplmulf1o  19078  grpinvadd  19083  grpsubf  19084  grpsubadd  19093  grpaddsubass  19095  grpnpcan  19097  grpsubsub4  19098  grppnpcan2  19099  grplactcnv  19108  imasgrp  19121  mulgcl  19156  mulgaddcomlem  19162  mulgdir  19171  subgcl  19201  nsgacs  19227  nmzsubg  19230  nsgid  19235  eqgcpbl  19249  qusxpid  19250  qusgrp  19256  qusadd  19258  ecqusaddcl  19263  qus0subgadd  19269  ghmrn  19298  idghm  19300  ghmpreima  19307  ghmnsgima  19309  ghmnsgpreima  19310  ghmf1o  19317  conjghm  19318  qusghm  19324  gaid  19368  subgga  19369  gass  19370  gaorber  19377  gastacl  19378  gastacos  19379  cntzsubg  19408  galactghm  19473  lactghmga  19474  symgsssg  19536  symgfisg  19537  symggen  19539  sylow1lem2  19668  sylow2blem1  19689  sylow2blem2  19690  sylow2blem3  19691  sylow3lem1  19696  sylow3lem2  19697  subgdisj1  19760  ablsub4  19879  abladdsub4  19880  mulgdi  19895  mulgghm  19897  invghm  19902  ghmplusg  19915  odadd1  19917  odadd2  19918  odadd  19919  gex2abl  19920  gexexlem  19921  torsubg  19923  oddvdssubg  19924  frgpnabllem2  19943  ogrpaddltbi  20208  ogrpaddltrbid  20210  ogrpinvlt  20213  rngacl  20239  rngpropd  20251  ringacl  20360  ringpropd  20370  dvrdir  20493  abvtrivd  20914  idsrngd  20938  lmodacl  20972  lmodvacl  20975  lmodprop2d  21024  rmodislmod  21030  prdslmodd  21069  pwssplit2  21160  evpmodpmf1o  21725  frlmplusgvalb  21898  asclghm  22011  mplind  22200  evlslem1  22212  evlsaddval  22259  evl1addd  22480  scmataddcl  22652  mdetralt  22744  mdetunilem6  22753  opnsubg  24244  ghmcnp  24251  qustgpopn  24256  ngprcan  24746  ngpocelbl  24840  nmotri  24875  ncvspi  25294  cphipval2  25379  4cphipval2  25380  cphipval  25381  efsubm  26692  abvcxp  27755  ttgcontlem1  29200  abliso  33321  cyc3co2  33426  cyc3genpmlem  33437  cycpmconjs  33442  cyc3conja  33443  archiabllem2a  33480  archiabllem2c  33481  archiabllem2b  33482  imaslmod  33639  quslmod  33644  nsgmgclem  33686  drgextlsp  33950  matunitlindflem1  38233  fldhmf1  42825  primrootsunit1  42832  aks6d1c1p2  42844  aks6d1c1p3  42845  nelsubgcld  43239  fsuppssind  43295  gicabl  43796  isnumbasgrplem2  43801  mendlmod  43886