Theorem grpcl 18889

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

Syntax hints:   → wi 4   ∧ w3a 1085   = wceq 1534   ∈ wcel 2099  ‘cfv 6542  (class class class)co 7414  Basecbs 17171  +_gcplusg 17224  Mndcmnd 18685  Grpcgrp 18881

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2698  ax-nul 5300

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-sb 2061  df-clab 2705  df-cleq 2719  df-clel 2805  df-ne 2936  df-ral 3057  df-rex 3066  df-rab 3428  df-v 3471  df-sbc 3775  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-nul 4319  df-if 4525  df-sn 4625  df-pr 4627  df-op 4631  df-uni 4904  df-br 5143  df-iota 6494  df-fv 6550  df-ov 7417  df-mgm 18591  df-sgrp 18670  df-mnd 18686  df-grp 18884

This theorem is referenced by:  grpcld  18895  grprcan  18921  grprinv  18938  grplmulf1o  18960  grpinvadd  18965  grpsubf  18966  grpsubadd  18975  grpaddsubass  18977  grpnpcan  18979  grpsubsub4  18980  grppnpcan2  18981  grplactcnv  18990  imasgrp  19003  mulgcl  19037  mulgaddcomlem  19043  mulgdir  19052  subgcl  19082  nsgacs  19108  nmzsubg  19111  nsgid  19116  eqgcpbl  19128  qusgrp  19132  qusadd  19134  ecqusaddcl  19139  qus0subgadd  19145  ghmrn  19174  idghm  19176  ghmpreima  19183  ghmnsgima  19185  ghmnsgpreima  19186  ghmf1o  19193  conjghm  19194  conjnmz  19197  qusghm  19200  gaid  19241  subgga  19242  gass  19243  gaorber  19250  gastacl  19251  gastacos  19252  cntzsubg  19281  galactghm  19350  lactghmga  19351  symgsssg  19413  symgfisg  19414  symggen  19416  sylow1lem2  19545  sylow2blem1  19566  sylow2blem2  19567  sylow2blem3  19568  sylow3lem1  19573  sylow3lem2  19574  subgdisj1  19637  ablsub4  19756  abladdsub4  19757  mulgdi  19772  mulgghm  19774  invghm  19779  ghmplusg  19792  odadd1  19794  odadd2  19795  odadd  19796  gex2abl  19797  gexexlem  19798  torsubg  19800  oddvdssubg  19801  frgpnabllem2  19820  rngacl  20093  rngpropd  20105  ringacl  20203  ringpropd  20213  dvrdir  20340  drngmcl  20630  abvtrivd  20709  idsrngd  20731  lmodacl  20744  lmodvacl  20747  lmodprop2d  20796  rmodislmod  20802  rmodislmodOLD  20803  prdslmodd  20842  pwssplit2  20934  evpmodpmf1o  21515  frlmplusgvalb  21690  asclghm  21803  psraddclOLD  21871  mplind  22001  evlslem1  22015  mhpaddcl  22062  evl1addd  22247  scmataddcl  22405  mdetralt  22497  mdetunilem6  22506  opnsubg  23999  ghmcnp  24006  qustgpopn  24011  ngprcan  24506  ngpocelbl  24608  nmotri  24643  ncvspi  25071  cphipval2  25156  4cphipval2  25157  cphipval  25158  efsubm  26472  abvcxp  27535  ttgcontlem1  28682  abliso  32734  ogrpaddltbi  32776  ogrpaddltrbid  32778  ogrpinvlt  32781  cyc3co2  32839  cyc3genpmlem  32850  cycpmconjs  32855  cyc3conja  32856  archiabllem2a  32880  archiabllem2c  32881  archiabllem2b  32882  imaslmod  33005  quslmod  33010  qusxpid  33015  nsgmgclem  33061  drgextlsp  33225  matunitlindflem1  37024  fldhmf1  41498  primrootsunit1  41504  aks6d1c1p2  41513  aks6d1c1p3  41514  nelsubgcld  41657  evlsaddval  41723  fsuppssind  41748  gicabl  42445  isnumbasgrplem2  42450  mendlmod  42539