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

Theorem grpcl 15669
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 15668 . 2  |-  ( G  e.  Grp  ->  G  e.  Mnd )
2 grpcl.b . . 3  |-  B  =  ( Base `  G
)
3 grpcl.p . . 3  |-  .+  =  ( +g  `  G )
42, 3mndcl 15538 . 2  |-  ( ( G  e.  Mnd  /\  X  e.  B  /\  Y  e.  B )  ->  ( X  .+  Y
)  e.  B )
51, 4syl3an1 1252 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 1370    e. wcel 1758   ` cfv 5525  (class class class)co 6199   Basecbs 14291   +g cplusg 14356   Mndcmnd 15527   Grpcgrp 15528
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-8 1760  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432  ax-nul 4528  ax-pow 4577
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-eu 2266  df-mo 2267  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2649  df-ral 2803  df-rex 2804  df-rab 2807  df-v 3078  df-sbc 3293  df-dif 3438  df-un 3440  df-in 3442  df-ss 3449  df-nul 3745  df-if 3899  df-sn 3985  df-pr 3987  df-op 3991  df-uni 4199  df-br 4400  df-iota 5488  df-fv 5533  df-ov 6202  df-mnd 15533  df-grp 15663
This theorem is referenced by:  grprcan  15689  grprinv  15703  grplmulf1o  15718  grpinvadd  15722  grpsubf  15723  grpsubadd  15731  grpaddsubass  15733  grpnpcan  15735  grpsubsub4  15736  grppnpcan2  15737  grplactcnv  15742  mulgcl  15762  mulgdir  15770  imasgrp  15789  subgcl  15809  grpissubg  15819  nsgacs  15835  nmzsubg  15840  nsgid  15845  eqger  15849  eqgcpbl  15853  divsgrp  15854  divsadd  15856  ghmrn  15878  idghm  15880  ghmpreima  15886  ghmnsgima  15888  ghmnsgpreima  15889  ghmf1o  15894  conjghm  15895  conjnmz  15898  divsghm  15901  gaid  15935  subgga  15936  gass  15937  gaorber  15944  gastacl  15945  gastacos  15946  cntzsubg  15972  galactghm  16026  lactghmga  16027  symgsssg  16091  symgfisg  16092  symggen  16094  sylow1lem2  16218  sylow2blem1  16239  sylow2blem2  16240  sylow2blem3  16241  sylow3lem1  16246  sylow3lem2  16247  subgdisj1  16308  ablsub4  16422  abladdsub4  16423  mulgdi  16434  mulgghm  16436  invghm  16438  ghmplusg  16448  odadd1  16450  odadd2  16451  odadd  16452  gex2abl  16453  gexexlem  16454  torsubg  16456  oddvdssubg  16457  frgpnabllem2  16472  rngacl  16794  rngpropd  16798  drngmcl  16967  abvtrivd  17047  idsrngd  17069  lmodacl  17081  lmodvacl  17084  lmodprop2d  17129  prdslmodd  17172  pwssplit2  17263  asclghm  17531  psraddcl  17576  mplind  17707  evlslem1  17724  evl1addd  17899  evpmodpmf1o  18150  mdetralt  18545  mdetunilem6  18554  opnsubg  19809  ghmcnp  19816  divstgpopn  19821  ngprcan  20332  nmotri  20449  abvcxp  22996  ttgcontlem1  23282  abliso  26303  ogrpaddltbi  26326  ogrpaddltrbid  26328  ogrpinvlt  26331  archiabllem2a  26355  archiabllem2c  26356  archiabllem2b  26357  dvrdir  26402  gicabl  29601  isnumbasgrplem2  29607  mendlmod  29697
  Copyright terms: Public domain W3C validator