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

Theorem grpcl 14810
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 14809 . 2  |-  ( G  e.  Grp  ->  G  e.  Mnd )
2 grpcl.b . . 3  |-  B  =  ( Base `  G
)
3 grpcl.p . . 3  |-  .+  =  ( +g  `  G )
42, 3mndcl 14687 . 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 1652    e. wcel 1725   ` cfv 5446  (class class class)co 6073   Basecbs 13461   +g cplusg 13521   Mndcmnd 14676   Grpcgrp 14677
This theorem is referenced by:  grprcan  14830  grprinv  14844  grplmulf1o  14857  grpinvadd  14859  grpsubf  14860  grpsubadd  14868  grpaddsubass  14870  grpnpcan  14872  grpsubsub4  14873  grppnpcan2  14874  grplactcnv  14879  mulgcl  14899  mulgdir  14907  imasgrp  14926  subgcl  14946  nsgacs  14968  nmzsubg  14973  nsgid  14978  eqger  14982  eqgcpbl  14986  divsgrp  14987  divsadd  14989  ghmrn  15011  idghm  15013  ghmpreima  15019  ghmnsgima  15021  ghmnsgpreima  15022  ghmf1o  15027  conjghm  15028  conjnmz  15031  divsghm  15034  gaid  15068  subgga  15069  gass  15070  gaorber  15077  gastacl  15078  gastacos  15079  galactghm  15098  lactghmga  15099  cntzsubg  15127  sylow1lem2  15225  sylow2blem1  15246  sylow2blem2  15247  sylow2blem3  15248  sylow3lem1  15253  sylow3lem2  15254  subgdisj1  15315  ablsub4  15429  abladdsub4  15430  mulgdi  15441  mulgghm  15443  invghm  15445  ghmplusg  15453  odadd1  15455  odadd2  15456  odadd  15457  gex2abl  15458  gexexlem  15459  torsubg  15461  oddvdssubg  15462  frgpnabllem2  15477  rngacl  15683  rngpropd  15687  drngmcl  15840  abvtrivd  15920  lmodacl  15953  lmodvacl  15956  lmodprop2d  15998  prdslmodd  16037  asclghm  16389  psraddcl  16439  mplind  16554  opnsubg  18129  ghmcnp  18136  divstgpopn  18141  ngprcan  18648  nmotri  18765  evlslem1  19928  evl1addd  19946  abvcxp  21301  dvrdir  24218  pwssplit2  27157  gicabl  27231  isnumbasgrplem2  27237  symgsssg  27376  symgfisg  27377  symggen  27379  mendlmod  27469
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-13 1727  ax-14 1729  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416  ax-nul 4330  ax-pow 4369
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-eu 2284  df-mo 2285  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-ne 2600  df-ral 2702  df-rex 2703  df-rab 2706  df-v 2950  df-sbc 3154  df-dif 3315  df-un 3317  df-in 3319  df-ss 3326  df-nul 3621  df-if 3732  df-sn 3812  df-pr 3813  df-op 3815  df-uni 4008  df-br 4205  df-iota 5410  df-fv 5454  df-ov 6076  df-mnd 14682  df-grp 14804
  Copyright terms: Public domain W3C validator