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

Theorem grpcl 15533
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 15532 . 2  |-  ( G  e.  Grp  ->  G  e.  Mnd )
2 grpcl.b . . 3  |-  B  =  ( Base `  G
)
3 grpcl.p . . 3  |-  .+  =  ( +g  `  G )
42, 3mndcl 15405 . 2  |-  ( ( G  e.  Mnd  /\  X  e.  B  /\  Y  e.  B )  ->  ( X  .+  Y
)  e.  B )
51, 4syl3an1 1246 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 960    = wceq 1364    e. wcel 1757   ` cfv 5408  (class class class)co 6082   Basecbs 14159   +g cplusg 14223   Mndcmnd 15394   Grpcgrp 15395
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1671  ax-6 1709  ax-7 1729  ax-8 1759  ax-9 1761  ax-10 1776  ax-11 1781  ax-12 1793  ax-13 1944  ax-ext 2416  ax-nul 4411  ax-pow 4460
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 962  df-tru 1367  df-ex 1592  df-nf 1595  df-sb 1702  df-eu 2260  df-mo 2261  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-ne 2600  df-ral 2712  df-rex 2713  df-rab 2716  df-v 2966  df-sbc 3178  df-dif 3321  df-un 3323  df-in 3325  df-ss 3332  df-nul 3628  df-if 3782  df-sn 3868  df-pr 3870  df-op 3874  df-uni 4082  df-br 4283  df-iota 5371  df-fv 5416  df-ov 6085  df-mnd 15400  df-grp 15527
This theorem is referenced by:  grprcan  15553  grprinv  15567  grplmulf1o  15582  grpinvadd  15586  grpsubf  15587  grpsubadd  15595  grpaddsubass  15597  grpnpcan  15599  grpsubsub4  15600  grppnpcan2  15601  grplactcnv  15606  mulgcl  15626  mulgdir  15634  imasgrp  15653  subgcl  15673  grpissubg  15683  nsgacs  15699  nmzsubg  15704  nsgid  15709  eqger  15713  eqgcpbl  15717  divsgrp  15718  divsadd  15720  ghmrn  15742  idghm  15744  ghmpreima  15750  ghmnsgima  15752  ghmnsgpreima  15753  ghmf1o  15758  conjghm  15759  conjnmz  15762  divsghm  15765  gaid  15799  subgga  15800  gass  15801  gaorber  15808  gastacl  15809  gastacos  15810  cntzsubg  15836  galactghm  15890  lactghmga  15891  symgsssg  15955  symgfisg  15956  symggen  15958  sylow1lem2  16080  sylow2blem1  16101  sylow2blem2  16102  sylow2blem3  16103  sylow3lem1  16108  sylow3lem2  16109  subgdisj1  16170  ablsub4  16284  abladdsub4  16285  mulgdi  16296  mulgghm  16298  invghm  16300  ghmplusg  16310  odadd1  16312  odadd2  16313  odadd  16314  gex2abl  16315  gexexlem  16316  torsubg  16318  oddvdssubg  16319  frgpnabllem2  16334  rngacl  16610  rngpropd  16614  drngmcl  16771  abvtrivd  16851  idsrngd  16873  lmodacl  16885  lmodvacl  16888  lmodprop2d  16933  prdslmodd  16974  pwssplit2  17065  asclghm  17333  psraddcl  17390  mplind  17518  evpmodpmf1o  17870  mdetralt  18258  mdetunilem6  18267  opnsubg  19522  ghmcnp  19529  divstgpopn  19534  ngprcan  20045  nmotri  20162  evlslem1  21369  evl1addd  21387  abvcxp  22751  ttgcontlem1  22956  abliso  25985  ogrpaddltbi  26008  ogrpaddltrbid  26010  ogrpinvlt  26013  archiabllem2a  26037  archiabllem2c  26038  archiabllem2b  26039  dvrdir  26113  gicabl  29301  isnumbasgrplem2  29307  mendlmod  29397
  Copyright terms: Public domain W3C validator