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

Theorem grpcl 14746
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 14745 . 2  |-  ( G  e.  Grp  ->  G  e.  Mnd )
2 grpcl.b . . 3  |-  B  =  ( Base `  G
)
3 grpcl.p . . 3  |-  .+  =  ( +g  `  G )
42, 3mndcl 14623 . 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 1717   ` cfv 5395  (class class class)co 6021   Basecbs 13397   +g cplusg 13457   Mndcmnd 14612   Grpcgrp 14613
This theorem is referenced by:  grprcan  14766  grprinv  14780  grplmulf1o  14793  grpinvadd  14795  grpsubf  14796  grpsubadd  14804  grpaddsubass  14806  grpnpcan  14808  grpsubsub4  14809  grppnpcan2  14810  grplactcnv  14815  mulgcl  14835  mulgdir  14843  imasgrp  14862  subgcl  14882  nsgacs  14904  nmzsubg  14909  nsgid  14914  eqger  14918  eqgcpbl  14922  divsgrp  14923  divsadd  14925  ghmrn  14947  idghm  14949  ghmpreima  14955  ghmnsgima  14957  ghmnsgpreima  14958  ghmf1o  14963  conjghm  14964  conjnmz  14967  divsghm  14970  gaid  15004  subgga  15005  gass  15006  gaorber  15013  gastacl  15014  gastacos  15015  galactghm  15034  lactghmga  15035  cntzsubg  15063  sylow1lem2  15161  sylow2blem1  15182  sylow2blem2  15183  sylow2blem3  15184  sylow3lem1  15189  sylow3lem2  15190  subgdisj1  15251  ablsub4  15365  abladdsub4  15366  mulgdi  15377  mulgghm  15379  invghm  15381  ghmplusg  15389  odadd1  15391  odadd2  15392  odadd  15393  gex2abl  15394  gexexlem  15395  torsubg  15397  oddvdssubg  15398  frgpnabllem2  15413  rngacl  15619  rngpropd  15623  drngmcl  15776  abvtrivd  15856  lmodacl  15889  lmodvacl  15892  lmodprop2d  15934  prdslmodd  15973  asclghm  16325  psraddcl  16375  mplind  16490  opnsubg  18059  ghmcnp  18066  divstgpopn  18071  ngprcan  18528  nmotri  18645  evlslem1  19804  evl1addd  19822  abvcxp  21177  dvrdir  24056  pwssplit2  26859  gicabl  26933  isnumbasgrplem2  26939  symgsssg  27078  symgfisg  27079  symggen  27081  mendlmod  27171
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 1661  ax-8 1682  ax-13 1719  ax-14 1721  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2369  ax-nul 4280  ax-pow 4319
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 2243  df-mo 2244  df-clab 2375  df-cleq 2381  df-clel 2384  df-nfc 2513  df-ne 2553  df-ral 2655  df-rex 2656  df-rab 2659  df-v 2902  df-sbc 3106  df-dif 3267  df-un 3269  df-in 3271  df-ss 3278  df-nul 3573  df-if 3684  df-sn 3764  df-pr 3765  df-op 3767  df-uni 3959  df-br 4155  df-iota 5359  df-fv 5403  df-ov 6024  df-mnd 14618  df-grp 14740
  Copyright terms: Public domain W3C validator