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

Theorem grpcl 15932
Description: Closure of the operation of a group. (Contributed by NM, 14-Aug-2011.)
Hypotheses
Ref Expression
grpcl.b  |-  B  =  ( Base `  G
)
grpcl.p  |-  .+  =  ( +g  `  G )
Assertion
Ref Expression
grpcl  |-  ( ( G  e.  Grp  /\  X  e.  B  /\  Y  e.  B )  ->  ( X  .+  Y
)  e.  B )

Proof of Theorem grpcl
StepHypRef Expression
1 grpmnd 15931 . 2  |-  ( G  e.  Grp  ->  G  e.  Mnd )
2 grpcl.b . . 3  |-  B  =  ( Base `  G
)
3 grpcl.p . . 3  |-  .+  =  ( +g  `  G )
42, 3mndcl 15798 . 2  |-  ( ( G  e.  Mnd  /\  X  e.  B  /\  Y  e.  B )  ->  ( X  .+  Y
)  e.  B )
51, 4syl3an1 1260 1  |-  ( ( G  e.  Grp  /\  X  e.  B  /\  Y  e.  B )  ->  ( X  .+  Y
)  e.  B )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ w3a 972    = wceq 1381    e. wcel 1802   ` cfv 5574  (class class class)co 6277   Basecbs 14504   +g cplusg 14569   Mndcmnd 15788   Grpcgrp 15922
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774  ax-10 1821  ax-11 1826  ax-12 1838  ax-13 1983  ax-ext 2419  ax-nul 4562
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 974  df-tru 1384  df-ex 1598  df-nf 1602  df-sb 1725  df-eu 2270  df-clab 2427  df-cleq 2433  df-clel 2436  df-nfc 2591  df-ne 2638  df-ral 2796  df-rex 2797  df-rab 2800  df-v 3095  df-sbc 3312  df-dif 3461  df-un 3463  df-in 3465  df-ss 3472  df-nul 3768  df-if 3923  df-sn 4011  df-pr 4013  df-op 4017  df-uni 4231  df-br 4434  df-iota 5537  df-fv 5582  df-ov 6280  df-mgm 15741  df-sgrp 15780  df-mnd 15790  df-grp 15926
This theorem is referenced by:  grprcan  15952  grprinv  15966  grplmulf1o  15981  grpinvadd  15985  grpsubf  15986  grpsubadd  15995  grpaddsubass  15997  grpnpcan  15999  grpsubsub4  16000  grppnpcan2  16001  grplactcnv  16007  mulgcl  16028  mulgdir  16036  imasgrp  16055  subgcl  16080  grpissubg  16090  nsgacs  16106  nmzsubg  16111  nsgid  16116  eqger  16120  eqgcpbl  16124  qusgrp  16125  qusadd  16127  ghmrn  16149  idghm  16151  ghmpreima  16157  ghmnsgima  16159  ghmnsgpreima  16160  ghmf1o  16165  conjghm  16166  conjnmz  16169  qusghm  16172  gaid  16206  subgga  16207  gass  16208  gaorber  16215  gastacl  16216  gastacos  16217  cntzsubg  16243  galactghm  16297  lactghmga  16298  symgsssg  16361  symgfisg  16362  symggen  16364  sylow1lem2  16488  sylow2blem1  16509  sylow2blem2  16510  sylow2blem3  16511  sylow3lem1  16516  sylow3lem2  16517  subgdisj1  16578  ablsub4  16692  abladdsub4  16693  mulgdi  16704  mulgghm  16706  invghm  16711  ghmplusg  16721  odadd1  16723  odadd2  16724  odadd  16725  gex2abl  16726  gexexlem  16727  torsubg  16729  oddvdssubg  16730  frgpnabllem2  16747  ringacl  17094  ringpropd  17098  drngmcl  17277  abvtrivd  17357  idsrngd  17379  lmodacl  17391  lmodvacl  17394  lmodprop2d  17440  prdslmodd  17483  pwssplit2  17574  asclghm  17855  psraddcl  17904  mplind  18035  evlslem1  18052  evl1addd  18245  evpmodpmf1o  18499  scmataddcl  18885  mdetralt  18977  mdetunilem6  18986  opnsubg  20472  ghmcnp  20479  qustgpopn  20484  ngprcan  20995  nmotri  21112  efsubm  22803  abvcxp  23665  ttgcontlem1  24053  abliso  27552  ogrpaddltbi  27575  ogrpaddltrbid  27577  ogrpinvlt  27580  archiabllem2a  27604  archiabllem2c  27605  archiabllem2b  27606  dvrdir  27646  gicabl  31015  isnumbasgrplem2  31021  mendlmod  31111
  Copyright terms: Public domain W3C validator