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

Theorem grpcl 17411
Description: Closure of the operation of a group. (Contributed by NM, 14-Aug-2011.)
Hypotheses
Ref Expression
grpcl.b 𝐵 = (Base‘𝐺)
grpcl.p + = (+g𝐺)
Assertion
Ref Expression
grpcl ((𝐺 ∈ Grp ∧ 𝑋𝐵𝑌𝐵) → (𝑋 + 𝑌) ∈ 𝐵)

Proof of Theorem grpcl
StepHypRef Expression
1 grpmnd 17410 . 2 (𝐺 ∈ Grp → 𝐺 ∈ Mnd)
2 grpcl.b . . 3 𝐵 = (Base‘𝐺)
3 grpcl.p . . 3 + = (+g𝐺)
42, 3mndcl 17282 . 2 ((𝐺 ∈ Mnd ∧ 𝑋𝐵𝑌𝐵) → (𝑋 + 𝑌) ∈ 𝐵)
51, 4syl3an1 1357 1 ((𝐺 ∈ Grp ∧ 𝑋𝐵𝑌𝐵) → (𝑋 + 𝑌) ∈ 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1036   = wceq 1481  wcel 1988  cfv 5876  (class class class)co 6635  Basecbs 15838  +gcplusg 15922  Mndcmnd 17275  Grpcgrp 17403
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600  ax-nul 4780
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-eu 2472  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-ral 2914  df-rex 2915  df-rab 2918  df-v 3197  df-sbc 3430  df-dif 3570  df-un 3572  df-in 3574  df-ss 3581  df-nul 3908  df-if 4078  df-sn 4169  df-pr 4171  df-op 4175  df-uni 4428  df-br 4645  df-iota 5839  df-fv 5884  df-ov 6638  df-mgm 17223  df-sgrp 17265  df-mnd 17276  df-grp 17406
This theorem is referenced by:  grprcan  17436  grprinv  17450  grplmulf1o  17470  grpinvadd  17474  grpsubf  17475  grpsubadd  17484  grpaddsubass  17486  grpnpcan  17488  grpsubsub4  17489  grppnpcan2  17490  dfgrp3  17495  grplactcnv  17499  imasgrp  17512  mulgcl  17540  mulgaddcomlem  17544  mulgdir  17554  subgcl  17585  grpissubg  17595  nsgacs  17611  nmzsubg  17616  nsgid  17621  eqger  17625  eqgcpbl  17629  qusgrp  17630  qusadd  17632  ghmrn  17654  idghm  17656  ghmpreima  17663  ghmnsgima  17665  ghmnsgpreima  17666  ghmf1o  17671  conjghm  17672  conjnmz  17675  qusghm  17678  gaid  17713  subgga  17714  gass  17715  gaorber  17722  gastacl  17723  gastacos  17724  cntzsubg  17750  galactghm  17804  lactghmga  17805  symgsssg  17868  symgfisg  17869  symggen  17871  sylow1lem2  17995  sylow2blem1  18016  sylow2blem2  18017  sylow2blem3  18018  sylow3lem1  18023  sylow3lem2  18024  subgdisj1  18085  ablsub4  18199  abladdsub4  18200  mulgdi  18213  mulgghm  18215  invghm  18220  ghmplusg  18230  odadd1  18232  odadd2  18233  odadd  18234  gex2abl  18235  gexexlem  18236  torsubg  18238  oddvdssubg  18239  frgpnabllem2  18258  ringacl  18559  ringpropd  18563  drngmcl  18741  abvtrivd  18821  idsrngd  18843  lmodacl  18855  lmodvacl  18858  lmodprop2d  18906  rmodislmod  18912  prdslmodd  18950  pwssplit2  19041  asclghm  19319  psraddcl  19364  mplind  19483  evlslem1  19496  evl1addd  19686  evpmodpmf1o  19923  scmataddcl  20303  mdetralt  20395  mdetunilem6  20404  opnsubg  21892  ghmcnp  21899  qustgpopn  21904  ngprcan  22395  ngpocelbl  22489  nmotri  22524  ncvspi  22937  cphipval2  23021  4cphipval2  23022  cphipval  23023  efsubm  24278  abvcxp  25285  ttgcontlem1  25746  abliso  29670  ogrpaddltbi  29693  ogrpaddltrbid  29695  ogrpinvlt  29698  archiabllem2a  29722  archiabllem2c  29723  archiabllem2b  29724  dvrdir  29764  matunitlindflem1  33376  gicabl  37488  isnumbasgrplem2  37493  mendlmod  37582
  Copyright terms: Public domain W3C validator