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

Theorem grpcl 16262
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 16261 . 2  |-  ( G  e.  Grp  ->  G  e.  Mnd )
2 grpcl.b . . 3  |-  B  =  ( Base `  G
)
3 grpcl.p . . 3  |-  .+  =  ( +g  `  G )
42, 3mndcl 16128 . 2  |-  ( ( G  e.  Mnd  /\  X  e.  B  /\  Y  e.  B )  ->  ( X  .+  Y
)  e.  B )
51, 4syl3an1 1259 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 971    = wceq 1398    e. wcel 1823   ` cfv 5570  (class class class)co 6270   Basecbs 14716   +g cplusg 14784   Mndcmnd 16118   Grpcgrp 16252
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432  ax-nul 4568
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 973  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-eu 2288  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2651  df-ral 2809  df-rex 2810  df-rab 2813  df-v 3108  df-sbc 3325  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3784  df-if 3930  df-sn 4017  df-pr 4019  df-op 4023  df-uni 4236  df-br 4440  df-iota 5534  df-fv 5578  df-ov 6273  df-mgm 16071  df-sgrp 16110  df-mnd 16120  df-grp 16256
This theorem is referenced by:  grprcan  16282  grprinv  16296  grplmulf1o  16311  grpinvadd  16315  grpsubf  16316  grpsubadd  16325  grpaddsubass  16327  grpnpcan  16329  grpsubsub4  16330  grppnpcan2  16331  grplactcnv  16337  mulgcl  16358  mulgdir  16366  imasgrp  16385  subgcl  16410  grpissubg  16420  nsgacs  16436  nmzsubg  16441  nsgid  16446  eqger  16450  eqgcpbl  16454  qusgrp  16455  qusadd  16457  ghmrn  16479  idghm  16481  ghmpreima  16487  ghmnsgima  16489  ghmnsgpreima  16490  ghmf1o  16495  conjghm  16496  conjnmz  16499  qusghm  16502  gaid  16536  subgga  16537  gass  16538  gaorber  16545  gastacl  16546  gastacos  16547  cntzsubg  16573  galactghm  16627  lactghmga  16628  symgsssg  16691  symgfisg  16692  symggen  16694  sylow1lem2  16818  sylow2blem1  16839  sylow2blem2  16840  sylow2blem3  16841  sylow3lem1  16846  sylow3lem2  16847  subgdisj1  16908  ablsub4  17022  abladdsub4  17023  mulgdi  17034  mulgghm  17036  invghm  17041  ghmplusg  17051  odadd1  17053  odadd2  17054  odadd  17055  gex2abl  17056  gexexlem  17057  torsubg  17059  oddvdssubg  17060  frgpnabllem2  17077  ringacl  17421  ringpropd  17425  drngmcl  17604  abvtrivd  17684  idsrngd  17706  lmodacl  17718  lmodvacl  17721  lmodprop2d  17767  prdslmodd  17810  pwssplit2  17901  asclghm  18182  psraddcl  18231  mplind  18362  evlslem1  18379  evl1addd  18572  evpmodpmf1o  18805  scmataddcl  19185  mdetralt  19277  mdetunilem6  19286  opnsubg  20772  ghmcnp  20779  qustgpopn  20784  ngprcan  21295  nmotri  21412  efsubm  23104  abvcxp  23998  ttgcontlem1  24390  abliso  27920  ogrpaddltbi  27943  ogrpaddltrbid  27945  ogrpinvlt  27948  archiabllem2a  27972  archiabllem2c  27973  archiabllem2b  27974  dvrdir  28015  gicabl  31288  isnumbasgrplem2  31294  mendlmod  31383
  Copyright terms: Public domain W3C validator