MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  grpcl Structured version   Visualization version   GIF version

Theorem grpcl 17700
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
StepHypRef Expression
1 grpmnd 17699 . 2 (𝐺 ∈ Grp → 𝐺 ∈ Mnd)
2 grpcl.b . . 3 𝐵 = (Base‘𝐺)
3 grpcl.p . . 3 + = (+g𝐺)
42, 3mndcl 17570 . 2 ((𝐺 ∈ Mnd ∧ 𝑋𝐵𝑌𝐵) → (𝑋 + 𝑌) ∈ 𝐵)
51, 4syl3an1 1202 1 ((𝐺 ∈ Grp ∧ 𝑋𝐵𝑌𝐵) → (𝑋 + 𝑌) ∈ 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1107   = wceq 1652  wcel 2155  cfv 6070  (class class class)co 6844  Basecbs 16133  +gcplusg 16217  Mndcmnd 17563  Grpcgrp 17692
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743  ax-nul 4951
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3an 1109  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-mo 2565  df-eu 2582  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-ral 3060  df-rex 3061  df-rab 3064  df-v 3352  df-sbc 3599  df-dif 3737  df-un 3739  df-in 3741  df-ss 3748  df-nul 4082  df-if 4246  df-sn 4337  df-pr 4339  df-op 4343  df-uni 4597  df-br 4812  df-iota 6033  df-fv 6078  df-ov 6847  df-mgm 17511  df-sgrp 17553  df-mnd 17564  df-grp 17695
This theorem is referenced by:  grprcan  17725  grprinv  17739  grplmulf1o  17759  grpinvadd  17763  grpsubf  17764  grpsubadd  17773  grpaddsubass  17775  grpnpcan  17777  grpsubsub4  17778  grppnpcan2  17779  dfgrp3  17784  grplactcnv  17788  imasgrp  17801  mulgcl  17828  mulgaddcomlem  17832  mulgdir  17841  subgcl  17871  grpissubg  17881  nsgacs  17897  nmzsubg  17902  nsgid  17907  eqger  17911  eqgcpbl  17915  qusgrp  17916  qusadd  17918  ghmrn  17940  idghm  17942  ghmpreima  17949  ghmnsgima  17951  ghmnsgpreima  17952  ghmf1o  17957  conjghm  17958  conjnmz  17961  qusghm  17964  gaid  17998  subgga  17999  gass  18000  gaorber  18007  gastacl  18008  gastacos  18009  cntzsubg  18035  galactghm  18089  lactghmga  18090  symgsssg  18153  symgfisg  18154  symggen  18156  sylow1lem2  18281  sylow2blem1  18302  sylow2blem2  18303  sylow2blem3  18304  sylow3lem1  18309  sylow3lem2  18310  subgdisj1  18371  ablsub4  18487  abladdsub4  18488  mulgdi  18501  mulgghm  18503  invghm  18508  ghmplusg  18518  odadd1  18520  odadd2  18521  odadd  18522  gex2abl  18523  gexexlem  18524  torsubg  18526  oddvdssubg  18527  frgpnabllem2  18546  ringacl  18848  ringpropd  18852  drngmcl  19032  abvtrivd  19112  idsrngd  19134  lmodacl  19146  lmodvacl  19149  lmodprop2d  19197  rmodislmod  19203  prdslmodd  19244  pwssplit2  19335  asclghm  19615  psraddcl  19660  mplind  19778  evlslem1  19791  evl1addd  19981  evpmodpmf1o  20218  scmataddcl  20602  mdetralt  20694  mdetunilem6  20703  opnsubg  22193  ghmcnp  22200  qustgpopn  22205  ngprcan  22696  ngpocelbl  22790  nmotri  22825  ncvspi  23237  cphipval2  23321  4cphipval2  23322  cphipval  23323  efsubm  24592  abvcxp  25598  ttgcontlem1  26059  abliso  30146  ogrpaddltbi  30169  ogrpaddltrbid  30171  ogrpinvlt  30174  archiabllem2a  30198  archiabllem2c  30199  archiabllem2b  30200  dvrdir  30240  matunitlindflem1  33832  gicabl  38349  isnumbasgrplem2  38354  mendlmod  38443
  Copyright terms: Public domain W3C validator