Theorem grpcl 18960

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

Syntax hints:   → wi 4   ∧ w3a 1086   = wceq 1539   ∈ wcel 2107  ‘cfv 6560  (class class class)co 7432  Basecbs 17248  +_gcplusg 17298  Mndcmnd 18748  Grpcgrp 18952

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2707  ax-nul 5305

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-sb 2064  df-clab 2714  df-cleq 2728  df-clel 2815  df-ne 2940  df-ral 3061  df-rex 3070  df-rab 3436  df-v 3481  df-sbc 3788  df-dif 3953  df-un 3955  df-ss 3967  df-nul 4333  df-if 4525  df-sn 4626  df-pr 4628  df-op 4632  df-uni 4907  df-br 5143  df-iota 6513  df-fv 6568  df-ov 7435  df-mgm 18654  df-sgrp 18733  df-mnd 18749  df-grp 18955

This theorem is referenced by:  grpcld  18966  grprcan  18992  grprinv  19009  grplmulf1o  19032  grpinvadd  19037  grpsubf  19038  grpsubadd  19047  grpaddsubass  19049  grpnpcan  19051  grpsubsub4  19052  grppnpcan2  19053  grplactcnv  19062  imasgrp  19075  mulgcl  19110  mulgaddcomlem  19116  mulgdir  19125  subgcl  19155  nsgacs  19181  nmzsubg  19184  nsgid  19189  eqgcpbl  19201  qusgrp  19205  qusadd  19207  ecqusaddcl  19212  qus0subgadd  19218  ghmrn  19248  idghm  19250  ghmpreima  19257  ghmnsgima  19259  ghmnsgpreima  19260  ghmf1o  19267  conjghm  19268  qusghm  19274  gaid  19318  subgga  19319  gass  19320  gaorber  19327  gastacl  19328  gastacos  19329  cntzsubg  19358  galactghm  19423  lactghmga  19424  symgsssg  19486  symgfisg  19487  symggen  19489  sylow1lem2  19618  sylow2blem1  19639  sylow2blem2  19640  sylow2blem3  19641  sylow3lem1  19646  sylow3lem2  19647  subgdisj1  19710  ablsub4  19829  abladdsub4  19830  mulgdi  19845  mulgghm  19847  invghm  19852  ghmplusg  19865  odadd1  19867  odadd2  19868  odadd  19869  gex2abl  19870  gexexlem  19871  torsubg  19873  oddvdssubg  19874  frgpnabllem2  19893  rngacl  20160  rngpropd  20172  ringacl  20276  ringpropd  20286  dvrdir  20413  drngmclOLD  20752  abvtrivd  20834  idsrngd  20858  lmodacl  20871  lmodvacl  20874  lmodprop2d  20923  rmodislmod  20929  prdslmodd  20968  pwssplit2  21060  evpmodpmf1o  21615  frlmplusgvalb  21790  asclghm  21904  psraddclOLD  21960  mplind  22095  evlslem1  22107  evl1addd  22346  scmataddcl  22523  mdetralt  22615  mdetunilem6  22624  opnsubg  24117  ghmcnp  24124  qustgpopn  24129  ngprcan  24624  ngpocelbl  24726  nmotri  24761  ncvspi  25191  cphipval2  25276  4cphipval2  25277  cphipval  25278  efsubm  26594  abvcxp  27660  ttgcontlem1  28900  abliso  33042  ogrpaddltbi  33096  ogrpaddltrbid  33098  ogrpinvlt  33101  cyc3co2  33161  cyc3genpmlem  33172  cycpmconjs  33177  cyc3conja  33178  archiabllem2a  33202  archiabllem2c  33203  archiabllem2b  33204  imaslmod  33382  quslmod  33387  qusxpid  33392  nsgmgclem  33440  drgextlsp  33645  matunitlindflem1  37624  fldhmf1  42092  primrootsunit1  42099  aks6d1c1p2  42111  aks6d1c1p3  42112  nelsubgcld  42512  evlsaddval  42583  fsuppssind  42608  gicabl  43116  isnumbasgrplem2  43121  mendlmod  43206