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

Theorem grpcl 14773
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 14772 . 2  |-  ( G  e.  Grp  ->  G  e.  Mnd )
2 grpcl.b . . 3  |-  B  =  ( Base `  G
)
3 grpcl.p . . 3  |-  .+  =  ( +g  `  G )
42, 3mndcl 14650 . 2  |-  ( ( G  e.  Mnd  /\  X  e.  B  /\  Y  e.  B )  ->  ( X  .+  Y
)  e.  B )
51, 4syl3an1 1217 1  |-  ( ( G  e.  Grp  /\  X  e.  B  /\  Y  e.  B )  ->  ( X  .+  Y
)  e.  B )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 936    = wceq 1649    e. wcel 1721   ` cfv 5413  (class class class)co 6040   Basecbs 13424   +g cplusg 13484   Mndcmnd 14639   Grpcgrp 14640
This theorem is referenced by:  grprcan  14793  grprinv  14807  grplmulf1o  14820  grpinvadd  14822  grpsubf  14823  grpsubadd  14831  grpaddsubass  14833  grpnpcan  14835  grpsubsub4  14836  grppnpcan2  14837  grplactcnv  14842  mulgcl  14862  mulgdir  14870  imasgrp  14889  subgcl  14909  nsgacs  14931  nmzsubg  14936  nsgid  14941  eqger  14945  eqgcpbl  14949  divsgrp  14950  divsadd  14952  ghmrn  14974  idghm  14976  ghmpreima  14982  ghmnsgima  14984  ghmnsgpreima  14985  ghmf1o  14990  conjghm  14991  conjnmz  14994  divsghm  14997  gaid  15031  subgga  15032  gass  15033  gaorber  15040  gastacl  15041  gastacos  15042  galactghm  15061  lactghmga  15062  cntzsubg  15090  sylow1lem2  15188  sylow2blem1  15209  sylow2blem2  15210  sylow2blem3  15211  sylow3lem1  15216  sylow3lem2  15217  subgdisj1  15278  ablsub4  15392  abladdsub4  15393  mulgdi  15404  mulgghm  15406  invghm  15408  ghmplusg  15416  odadd1  15418  odadd2  15419  odadd  15420  gex2abl  15421  gexexlem  15422  torsubg  15424  oddvdssubg  15425  frgpnabllem2  15440  rngacl  15646  rngpropd  15650  drngmcl  15803  abvtrivd  15883  lmodacl  15916  lmodvacl  15919  lmodprop2d  15961  prdslmodd  16000  asclghm  16352  psraddcl  16402  mplind  16517  opnsubg  18090  ghmcnp  18097  divstgpopn  18102  ngprcan  18609  nmotri  18726  evlslem1  19889  evl1addd  19907  abvcxp  21262  dvrdir  24179  pwssplit2  27057  gicabl  27131  isnumbasgrplem2  27137  symgsssg  27276  symgfisg  27277  symggen  27279  mendlmod  27369
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-13 1723  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385  ax-nul 4298  ax-pow 4337
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2258  df-mo 2259  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ne 2569  df-ral 2671  df-rex 2672  df-rab 2675  df-v 2918  df-sbc 3122  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-nul 3589  df-if 3700  df-sn 3780  df-pr 3781  df-op 3783  df-uni 3976  df-br 4173  df-iota 5377  df-fv 5421  df-ov 6043  df-mnd 14645  df-grp 14767
  Copyright terms: Public domain W3C validator