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

Theorem grpcl 15542
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 15541 . 2  |-  ( G  e.  Grp  ->  G  e.  Mnd )
2 grpcl.b . . 3  |-  B  =  ( Base `  G
)
3 grpcl.p . . 3  |-  .+  =  ( +g  `  G )
42, 3mndcl 15412 . 2  |-  ( ( G  e.  Mnd  /\  X  e.  B  /\  Y  e.  B )  ->  ( X  .+  Y
)  e.  B )
51, 4syl3an1 1251 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 965    = wceq 1369    e. wcel 1756   ` cfv 5413  (class class class)co 6086   Basecbs 14166   +g cplusg 14230   Mndcmnd 15401   Grpcgrp 15402
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419  ax-nul 4416  ax-pow 4465
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2256  df-mo 2257  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-ral 2715  df-rex 2716  df-rab 2719  df-v 2969  df-sbc 3182  df-dif 3326  df-un 3328  df-in 3330  df-ss 3337  df-nul 3633  df-if 3787  df-sn 3873  df-pr 3875  df-op 3879  df-uni 4087  df-br 4288  df-iota 5376  df-fv 5421  df-ov 6089  df-mnd 15407  df-grp 15536
This theorem is referenced by:  grprcan  15562  grprinv  15576  grplmulf1o  15591  grpinvadd  15595  grpsubf  15596  grpsubadd  15604  grpaddsubass  15606  grpnpcan  15608  grpsubsub4  15609  grppnpcan2  15610  grplactcnv  15615  mulgcl  15635  mulgdir  15643  imasgrp  15662  subgcl  15682  grpissubg  15692  nsgacs  15708  nmzsubg  15713  nsgid  15718  eqger  15722  eqgcpbl  15726  divsgrp  15727  divsadd  15729  ghmrn  15751  idghm  15753  ghmpreima  15759  ghmnsgima  15761  ghmnsgpreima  15762  ghmf1o  15767  conjghm  15768  conjnmz  15771  divsghm  15774  gaid  15808  subgga  15809  gass  15810  gaorber  15817  gastacl  15818  gastacos  15819  cntzsubg  15845  galactghm  15899  lactghmga  15900  symgsssg  15964  symgfisg  15965  symggen  15967  sylow1lem2  16089  sylow2blem1  16110  sylow2blem2  16111  sylow2blem3  16112  sylow3lem1  16117  sylow3lem2  16118  subgdisj1  16179  ablsub4  16293  abladdsub4  16294  mulgdi  16305  mulgghm  16307  invghm  16309  ghmplusg  16319  odadd1  16321  odadd2  16322  odadd  16323  gex2abl  16324  gexexlem  16325  torsubg  16327  oddvdssubg  16328  frgpnabllem2  16343  rngacl  16660  rngpropd  16664  drngmcl  16823  abvtrivd  16903  idsrngd  16925  lmodacl  16937  lmodvacl  16940  lmodprop2d  16985  prdslmodd  17027  pwssplit2  17118  asclghm  17386  psraddcl  17431  mplind  17559  evlslem1  17576  evl1addd  17750  evpmodpmf1o  18001  mdetralt  18389  mdetunilem6  18398  opnsubg  19653  ghmcnp  19660  divstgpopn  19665  ngprcan  20176  nmotri  20293  abvcxp  22839  ttgcontlem1  23082  abliso  26110  ogrpaddltbi  26133  ogrpaddltrbid  26135  ogrpinvlt  26138  archiabllem2a  26162  archiabllem2c  26163  archiabllem2b  26164  dvrdir  26209  gicabl  29407  isnumbasgrplem2  29413  mendlmod  29503
  Copyright terms: Public domain W3C validator