Theorem grpcl 19014

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

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1102   = wceq 1569   ∈ wcel 2142  ‘cfv 6536  (class class class)co 7412  Basecbs 17275  +_gcplusg 17316  Mndcmnd 18798  Grpcgrp 19006

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-8 2144  ax-9 2152  ax-ext 2734  ax-nul 5268

This proof depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1104  df-tru 1572  df-fal 1582  df-ex 1809  df-sb 2096  df-clab 2741  df-cleq 2754  df-clel 2837  df-ne 2958  df-ral 3079  df-rex 3089  df-rab 3416  df-v 3456  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 7415  df-mgm 18704  df-sgrp 18783  df-mnd 18799  df-grp 19009

This theorem is used by:  grpcld  19020  grprcan  19046  grprinv  19063  grplmulf1o  19085  grpinvadd  19090  grpsubf  19091  grpsubadd  19100  grpaddsubass  19102  grpnpcan  19104  grpsubsub4  19105  grppnpcan2  19106  grplactcnv  19115  imasgrp  19128  mulgcl  19163  mulgaddcomlem  19169  mulgdir  19178  subgcl  19208  nsgacs  19234  nmzsubg  19237  nsgid  19242  eqgcpbl  19256  qusxpid  19257  qusgrp  19263  qusadd  19265  ecqusaddcl  19270  qus0subgadd  19276  ghmrn  19305  idghm  19307  ghmpreima  19314  ghmnsgima  19316  ghmnsgpreima  19317  ghmf1o  19324  conjghm  19325  qusghm  19331  gaid  19375  subgga  19376  gass  19377  gaorber  19384  gastacl  19385  gastacos  19386  cntzsubg  19415  galactghm  19480  lactghmga  19481  symgsssg  19543  symgfisg  19544  symggen  19546  sylow1lem2  19675  sylow2blem1  19696  sylow2blem2  19697  sylow2blem3  19698  sylow3lem1  19703  sylow3lem2  19704  subgdisj1  19767  ablsub4  19886  abladdsub4  19887  mulgdi  19902  mulgghm  19904  invghm  19909  ghmplusg  19922  odadd1  19924  odadd2  19925  odadd  19926  gex2abl  19927  gexexlem  19928  torsubg  19930  oddvdssubg  19931  frgpnabllem2  19950  ogrpaddltbi  20215  ogrpaddltrbid  20217  ogrpinvlt  20220  rngacl  20246  rngpropd  20258  ringacl  20368  ringpropd  20378  dvrdir  20501  abvtrivd  20946  idsrngd  20970  lmodacl  21004  lmodvacl  21007  lmodprop2d  21056  rmodislmod  21062  prdslmodd  21101  pwssplit2  21192  evpmodpmf1o  21757  frlmplusgvalb  21930  asclghm  22043  mplind  22232  evlslem1  22244  evlsaddval  22291  evl1addd  22512  scmataddcl  22684  mdetralt  22776  mdetunilem6  22785  opnsubg  24276  ghmcnp  24283  qustgpopn  24288  ngprcan  24778  ngpocelbl  24872  nmotri  24907  ncvspi  25326  cphipval2  25411  4cphipval2  25412  cphipval  25413  efsubm  26727  abvcxp  27790  ttgcontlem1  29245  abliso  33364  cyc3co2  33469  cyc3genpmlem  33480  cycpmconjs  33485  cyc3conja  33486  archiabllem2a  33523  archiabllem2c  33524  archiabllem2b  33525  imaslmod  33682  quslmod  33687  nsgmgclem  33729  drgextlsp  33993  matunitlindflem1  38295  fldhmf1  42885  primrootsunit1  42892  aks6d1c1p2  42904  aks6d1c1p3  42905  nelsubgcld  43299  fsuppssind  43353  gicabl  43854  isnumbasgrplem2  43859  mendlmod  43944