Theorem grpcl 17869

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 17868	. 2 ⊢ (𝐺 ∈ Grp → 𝐺 ∈ Mnd)
2		grpcl.b	. . 3 ⊢ 𝐵 = (Base‘𝐺)
3		grpcl.p	. . 3 ⊢ + = (+g‘𝐺)
4	2, 3	mndcl 17740	. 2 ⊢ ((𝐺 ∈ Mnd ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 + 𝑌) ∈ 𝐵)
5	1, 4	syl3an1 1156	1 ⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 + 𝑌) ∈ 𝐵)

Syntax hints:   → wi 4   ∧ w3a 1080   = wceq 1522   ∈ wcel 2081  ‘cfv 6225  (class class class)co 7016  Basecbs 16312  +_gcplusg 16394  Mndcmnd 17733  Grpcgrp 17861

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083  ax-9 2091  ax-10 2112  ax-11 2126  ax-12 2141  ax-ext 2769  ax-nul 5101

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3an 1082  df-tru 1525  df-ex 1762  df-nf 1766  df-sb 2043  df-mo 2576  df-eu 2612  df-clab 2776  df-cleq 2788  df-clel 2863  df-nfc 2935  df-ral 3110  df-rex 3111  df-rab 3114  df-v 3439  df-sbc 3707  df-dif 3862  df-un 3864  df-in 3866  df-ss 3874  df-nul 4212  df-if 4382  df-sn 4473  df-pr 4475  df-op 4479  df-uni 4746  df-br 4963  df-iota 6189  df-fv 6233  df-ov 7019  df-mgm 17681  df-sgrp 17723  df-mnd 17734  df-grp 17864

This theorem is referenced by:  grprcan  17894  grprinv  17910  grplmulf1o  17930  grpinvadd  17934  grpsubf  17935  grpsubadd  17944  grpaddsubass  17946  grpnpcan  17948  grpsubsub4  17949  grppnpcan2  17950  dfgrp3  17955  grplactcnv  17959  imasgrp  17972  mulgcl  18000  mulgaddcomlem  18004  mulgdir  18013  subgcl  18043  grpissubg  18053  nsgacs  18069  nmzsubg  18074  nsgid  18079  eqger  18083  eqgcpbl  18087  qusgrp  18088  qusadd  18090  ghmrn  18112  idghm  18114  ghmpreima  18121  ghmnsgima  18123  ghmnsgpreima  18124  ghmf1o  18129  conjghm  18130  conjnmz  18133  qusghm  18136  gaid  18170  subgga  18171  gass  18172  gaorber  18179  gastacl  18180  gastacos  18181  cntzsubg  18208  galactghm  18262  lactghmga  18263  symgsssg  18326  symgfisg  18327  symggen  18329  sylow1lem2  18454  sylow2blem1  18475  sylow2blem2  18476  sylow2blem3  18477  sylow3lem1  18482  sylow3lem2  18483  subgdisj1  18544  ablsub4  18658  abladdsub4  18659  mulgdi  18672  mulgghm  18674  invghm  18679  ghmplusg  18689  odadd1  18691  odadd2  18692  odadd  18693  gex2abl  18694  gexexlem  18695  torsubg  18697  oddvdssubg  18698  frgpnabllem2  18717  ringacl  19018  ringpropd  19022  drngmcl  19205  abvtrivd  19301  idsrngd  19323  lmodacl  19335  lmodvacl  19338  lmodprop2d  19386  rmodislmod  19392  prdslmodd  19431  pwssplit2  19522  asclghm  19800  psraddcl  19851  mplind  19969  evlslem1  19982  mhpaddcl  20021  evl1addd  20186  evpmodpmf1o  20422  frlmplusgvalb  20595  scmataddcl  20809  mdetralt  20901  mdetunilem6  20910  opnsubg  22399  ghmcnp  22406  qustgpopn  22411  ngprcan  22902  ngpocelbl  22996  nmotri  23031  ncvspi  23443  cphipval2  23527  4cphipval2  23528  cphipval  23529  efsubm  24816  abvcxp  25873  ttgcontlem1  26354  abliso  30357  ogrpaddltbi  30379  ogrpaddltrbid  30381  ogrpinvlt  30384  cyc3co2  30419  cyc3genpmlem  30431  cycpmconjs  30436  cyc3conja  30437  archiabllem2a  30461  archiabllem2c  30462  archiabllem2b  30463  dvrdir  30515  imaslmod  30576  quslmod  30577  drgextlsp  30600  matunitlindflem1  34438  nelsubgcld  38678  gicabl  39203  isnumbasgrplem2  39208  mendlmod  39297