Theorem grpcl 17602

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

Step	Hyp	Ref	Expression
1		grpmnd 17601	. 2 ⊢ (𝐺 ∈ Grp → 𝐺 ∈ Mnd)
2		grpcl.b	. . 3 ⊢ 𝐵 = (Base‘𝐺)
3		grpcl.p	. . 3 ⊢ + = (+g‘𝐺)
4	2, 3	mndcl 17473	. 2 ⊢ ((𝐺 ∈ Mnd ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 + 𝑌) ∈ 𝐵)
5	1, 4	syl3an1 1496	1 ⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 + 𝑌) ∈ 𝐵)

Syntax hints:   → wi 4   ∧ w3a 1072   = wceq 1620   ∈ wcel 2127  ‘cfv 6037  (class class class)co 6801  Basecbs 16030  +_gcplusg 16114  Mndcmnd 17466  Grpcgrp 17594

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1859  ax-4 1874  ax-5 1976  ax-6 2042  ax-7 2078  ax-9 2136  ax-10 2156  ax-11 2171  ax-12 2184  ax-13 2379  ax-ext 2728  ax-nul 4929

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1623  df-ex 1842  df-nf 1847  df-sb 2035  df-eu 2599  df-clab 2735  df-cleq 2741  df-clel 2744  df-nfc 2879  df-ral 3043  df-rex 3044  df-rab 3047  df-v 3330  df-sbc 3565  df-dif 3706  df-un 3708  df-in 3710  df-ss 3717  df-nul 4047  df-if 4219  df-sn 4310  df-pr 4312  df-op 4316  df-uni 4577  df-br 4793  df-iota 6000  df-fv 6045  df-ov 6804  df-mgm 17414  df-sgrp 17456  df-mnd 17467  df-grp 17597

This theorem is referenced by:  grprcan  17627  grprinv  17641  grplmulf1o  17661  grpinvadd  17665  grpsubf  17666  grpsubadd  17675  grpaddsubass  17677  grpnpcan  17679  grpsubsub4  17680  grppnpcan2  17681  dfgrp3  17686  grplactcnv  17690  imasgrp  17703  mulgcl  17731  mulgaddcomlem  17735  mulgdir  17745  subgcl  17776  grpissubg  17786  nsgacs  17802  nmzsubg  17807  nsgid  17812  eqger  17816  eqgcpbl  17820  qusgrp  17821  qusadd  17823  ghmrn  17845  idghm  17847  ghmpreima  17854  ghmnsgima  17856  ghmnsgpreima  17857  ghmf1o  17862  conjghm  17863  conjnmz  17866  qusghm  17869  gaid  17903  subgga  17904  gass  17905  gaorber  17912  gastacl  17913  gastacos  17914  cntzsubg  17940  galactghm  17994  lactghmga  17995  symgsssg  18058  symgfisg  18059  symggen  18061  sylow1lem2  18185  sylow2blem1  18206  sylow2blem2  18207  sylow2blem3  18208  sylow3lem1  18213  sylow3lem2  18214  subgdisj1  18275  ablsub4  18389  abladdsub4  18390  mulgdi  18403  mulgghm  18405  invghm  18410  ghmplusg  18420  odadd1  18422  odadd2  18423  odadd  18424  gex2abl  18425  gexexlem  18426  torsubg  18428  oddvdssubg  18429  frgpnabllem2  18448  ringacl  18749  ringpropd  18753  drngmcl  18933  abvtrivd  19013  idsrngd  19035  lmodacl  19047  lmodvacl  19050  lmodprop2d  19098  rmodislmod  19104  prdslmodd  19142  pwssplit2  19233  asclghm  19511  psraddcl  19556  mplind  19675  evlslem1  19688  evl1addd  19878  evpmodpmf1o  20115  scmataddcl  20495  mdetralt  20587  mdetunilem6  20596  opnsubg  22083  ghmcnp  22090  qustgpopn  22095  ngprcan  22586  ngpocelbl  22680  nmotri  22715  ncvspi  23127  cphipval2  23211  4cphipval2  23212  cphipval  23213  efsubm  24467  abvcxp  25474  ttgcontlem1  25935  abliso  29976  ogrpaddltbi  29999  ogrpaddltrbid  30001  ogrpinvlt  30004  archiabllem2a  30028  archiabllem2c  30029  archiabllem2b  30030  dvrdir  30070  matunitlindflem1  33687  gicabl  38140  isnumbasgrplem2  38145  mendlmod  38234