Theorem grpcl 18838

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

Syntax hints:   → wi 4   ∧ w3a 1086   = wceq 1540   ∈ wcel 2109  ‘cfv 6486  (class class class)co 7353  Basecbs 17138  +_gcplusg 17179  Mndcmnd 18626  Grpcgrp 18830

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-nul 5248

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ne 2926  df-ral 3045  df-rex 3054  df-rab 3397  df-v 3440  df-sbc 3745  df-dif 3908  df-un 3910  df-ss 3922  df-nul 4287  df-if 4479  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4862  df-br 5096  df-iota 6442  df-fv 6494  df-ov 7356  df-mgm 18532  df-sgrp 18611  df-mnd 18627  df-grp 18833

This theorem is referenced by:  grpcld  18844  grprcan  18870  grprinv  18887  grplmulf1o  18910  grpinvadd  18915  grpsubf  18916  grpsubadd  18925  grpaddsubass  18927  grpnpcan  18929  grpsubsub4  18930  grppnpcan2  18931  grplactcnv  18940  imasgrp  18953  mulgcl  18988  mulgaddcomlem  18994  mulgdir  19003  subgcl  19033  nsgacs  19059  nmzsubg  19062  nsgid  19067  eqgcpbl  19079  qusgrp  19083  qusadd  19085  ecqusaddcl  19090  qus0subgadd  19096  ghmrn  19126  idghm  19128  ghmpreima  19135  ghmnsgima  19137  ghmnsgpreima  19138  ghmf1o  19145  conjghm  19146  qusghm  19152  gaid  19196  subgga  19197  gass  19198  gaorber  19205  gastacl  19206  gastacos  19207  cntzsubg  19236  galactghm  19301  lactghmga  19302  symgsssg  19364  symgfisg  19365  symggen  19367  sylow1lem2  19496  sylow2blem1  19517  sylow2blem2  19518  sylow2blem3  19519  sylow3lem1  19524  sylow3lem2  19525  subgdisj1  19588  ablsub4  19707  abladdsub4  19708  mulgdi  19723  mulgghm  19725  invghm  19730  ghmplusg  19743  odadd1  19745  odadd2  19746  odadd  19747  gex2abl  19748  gexexlem  19749  torsubg  19751  oddvdssubg  19752  frgpnabllem2  19771  ogrpaddltbi  20036  ogrpaddltrbid  20038  ogrpinvlt  20041  rngacl  20065  rngpropd  20077  ringacl  20181  ringpropd  20191  dvrdir  20315  drngmclOLD  20654  abvtrivd  20735  idsrngd  20759  lmodacl  20793  lmodvacl  20796  lmodprop2d  20845  rmodislmod  20851  prdslmodd  20890  pwssplit2  20982  evpmodpmf1o  21521  frlmplusgvalb  21694  asclghm  21808  psraddclOLD  21864  mplind  21993  evlslem1  22005  evl1addd  22244  scmataddcl  22419  mdetralt  22511  mdetunilem6  22520  opnsubg  24011  ghmcnp  24018  qustgpopn  24023  ngprcan  24514  ngpocelbl  24608  nmotri  24643  ncvspi  25072  cphipval2  25157  4cphipval2  25158  cphipval  25159  efsubm  26476  abvcxp  27542  ttgcontlem1  28848  abliso  33003  cyc3co2  33095  cyc3genpmlem  33106  cycpmconjs  33111  cyc3conja  33112  archiabllem2a  33146  archiabllem2c  33147  archiabllem2b  33148  imaslmod  33300  quslmod  33305  qusxpid  33310  nsgmgclem  33358  drgextlsp  33565  matunitlindflem1  37595  fldhmf1  42063  primrootsunit1  42070  aks6d1c1p2  42082  aks6d1c1p3  42083  nelsubgcld  42470  evlsaddval  42541  fsuppssind  42566  gicabl  43072  isnumbasgrplem2  43077  mendlmod  43162