Theorem grpcl 18105

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

Syntax hints:   → wi 4   ∧ w3a 1083   = wceq 1533   ∈ wcel 2110  ‘cfv 6349  (class class class)co 7150  Basecbs 16477  +_gcplusg 16559  Mndcmnd 17905  Grpcgrp 18097

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793  ax-nul 5202

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-mo 2618  df-eu 2650  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3496  df-sbc 3772  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-nul 4291  df-if 4467  df-sn 4561  df-pr 4563  df-op 4567  df-uni 4832  df-br 5059  df-iota 6308  df-fv 6357  df-ov 7153  df-mgm 17846  df-sgrp 17895  df-mnd 17906  df-grp 18100

This theorem is referenced by:  grprcan  18131  grprinv  18147  grplmulf1o  18167  grpinvadd  18171  grpsubf  18172  grpsubadd  18181  grpaddsubass  18183  grpnpcan  18185  grpsubsub4  18186  grppnpcan2  18187  dfgrp3  18192  grplactcnv  18196  imasgrp  18209  mulgcl  18239  mulgaddcomlem  18244  mulgdir  18253  subgcl  18283  nsgacs  18308  nmzsubg  18311  nsgid  18316  eqger  18324  eqgcpbl  18328  qusgrp  18329  qusadd  18331  ghmrn  18365  idghm  18367  ghmpreima  18374  ghmnsgima  18376  ghmnsgpreima  18377  ghmf1o  18382  conjghm  18383  conjnmz  18386  qusghm  18389  gaid  18423  subgga  18424  gass  18425  gaorber  18432  gastacl  18433  gastacos  18434  cntzsubg  18461  galactghm  18526  lactghmga  18527  symgsssg  18589  symgfisg  18590  symggen  18592  sylow1lem2  18718  sylow2blem1  18739  sylow2blem2  18740  sylow2blem3  18741  sylow3lem1  18746  sylow3lem2  18747  subgdisj1  18811  ablsub4  18927  abladdsub4  18928  mulgdi  18941  mulgghm  18943  invghm  18948  ghmplusg  18960  odadd1  18962  odadd2  18963  odadd  18964  gex2abl  18965  gexexlem  18966  torsubg  18968  oddvdssubg  18969  frgpnabllem2  18988  ringacl  19322  ringpropd  19326  drngmcl  19509  abvtrivd  19605  idsrngd  19627  lmodacl  19639  lmodvacl  19642  lmodprop2d  19690  rmodislmod  19696  prdslmodd  19735  pwssplit2  19826  asclghm  20106  psraddcl  20157  mplind  20276  evlslem1  20289  mhpaddcl  20332  evl1addd  20498  evpmodpmf1o  20734  frlmplusgvalb  20907  scmataddcl  21119  mdetralt  21211  mdetunilem6  21220  opnsubg  22710  ghmcnp  22717  qustgpopn  22722  ngprcan  23213  ngpocelbl  23307  nmotri  23342  ncvspi  23754  cphipval2  23838  4cphipval2  23839  cphipval  23840  efsubm  25129  abvcxp  26185  ttgcontlem1  26665  abliso  30678  ogrpaddltbi  30714  ogrpaddltrbid  30716  ogrpinvlt  30719  cyc3co2  30777  cyc3genpmlem  30788  cycpmconjs  30793  cyc3conja  30794  archiabllem2a  30818  archiabllem2c  30819  archiabllem2b  30820  dvrdir  30856  imaslmod  30917  quslmod  30918  qusxpid  30923  drgextlsp  30991  matunitlindflem1  34882  nelsubgcld  39122  gicabl  39692  isnumbasgrplem2  39697  mendlmod  39786