Theorem grpcl 18827

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

Syntax hints:   → wi 4   ∧ w3a 1088   = wceq 1542   ∈ wcel 2107  ‘cfv 6544  (class class class)co 7409  Basecbs 17144  +_gcplusg 17197  Mndcmnd 18625  Grpcgrp 18819

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704  ax-nul 5307

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-ne 2942  df-ral 3063  df-rex 3072  df-rab 3434  df-v 3477  df-sbc 3779  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-br 5150  df-iota 6496  df-fv 6552  df-ov 7412  df-mgm 18561  df-sgrp 18610  df-mnd 18626  df-grp 18822

This theorem is referenced by:  grpcld  18833  grprcan  18858  grprinv  18875  grplmulf1o  18897  grpinvadd  18901  grpsubf  18902  grpsubadd  18911  grpaddsubass  18913  grpnpcan  18915  grpsubsub4  18916  grppnpcan2  18917  grplactcnv  18926  imasgrp  18939  mulgcl  18971  mulgaddcomlem  18977  mulgdir  18986  subgcl  19016  nsgacs  19042  nmzsubg  19045  nsgid  19050  eqgcpbl  19062  qusgrp  19065  qusadd  19067  qus0subgadd  19076  ghmrn  19105  idghm  19107  ghmpreima  19114  ghmnsgima  19116  ghmnsgpreima  19117  ghmf1o  19122  conjghm  19123  conjnmz  19126  qusghm  19129  gaid  19163  subgga  19164  gass  19165  gaorber  19172  gastacl  19173  gastacos  19174  cntzsubg  19203  galactghm  19272  lactghmga  19273  symgsssg  19335  symgfisg  19336  symggen  19338  sylow1lem2  19467  sylow2blem1  19488  sylow2blem2  19489  sylow2blem3  19490  sylow3lem1  19495  sylow3lem2  19496  subgdisj1  19559  ablsub4  19678  abladdsub4  19679  mulgdi  19694  mulgghm  19696  invghm  19701  ghmplusg  19714  odadd1  19716  odadd2  19717  odadd  19718  gex2abl  19719  gexexlem  19720  torsubg  19722  oddvdssubg  19723  frgpnabllem2  19742  ringacl  20095  ringpropd  20102  dvrdir  20226  drngmcl  20374  abvtrivd  20448  idsrngd  20470  lmodacl  20483  lmodvacl  20486  lmodprop2d  20534  rmodislmod  20540  rmodislmodOLD  20541  prdslmodd  20580  pwssplit2  20671  evpmodpmf1o  21149  frlmplusgvalb  21324  asclghm  21437  psraddcl  21502  mplind  21631  evlslem1  21645  mhpaddcl  21694  evl1addd  21860  scmataddcl  22018  mdetralt  22110  mdetunilem6  22119  opnsubg  23612  ghmcnp  23619  qustgpopn  23624  ngprcan  24119  ngpocelbl  24221  nmotri  24256  ncvspi  24673  cphipval2  24758  4cphipval2  24759  cphipval  24760  efsubm  26060  abvcxp  27118  ttgcontlem1  28142  abliso  32197  ogrpaddltbi  32236  ogrpaddltrbid  32238  ogrpinvlt  32241  cyc3co2  32299  cyc3genpmlem  32310  cycpmconjs  32315  cyc3conja  32316  archiabllem2a  32340  archiabllem2c  32341  archiabllem2b  32342  imaslmod  32468  quslmod  32469  qusxpid  32475  nsgmgclem  32522  drgextlsp  32681  matunitlindflem1  36484  fldhmf1  40955  nelsubgcld  41071  evlsaddval  41140  fsuppssind  41165  gicabl  41841  isnumbasgrplem2  41846  mendlmod  41935  rngacl  46661  rngpropd  46673  ecqusaddcl  46769