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

Theorem grpcld 18875
Description: Closure of the operation of a group. (Contributed by SN, 29-Jul-2024.)
Hypotheses
Ref Expression
grpcld.b 𝐵 = (Base‘𝐺)
grpcld.p + = (+g𝐺)
grpcld.r (𝜑𝐺 ∈ Grp)
grpcld.x (𝜑𝑋𝐵)
grpcld.y (𝜑𝑌𝐵)
Assertion
Ref Expression
grpcld (𝜑 → (𝑋 + 𝑌) ∈ 𝐵)

Proof of Theorem grpcld
StepHypRef Expression
1 grpcld.r . 2 (𝜑𝐺 ∈ Grp)
2 grpcld.x . 2 (𝜑𝑋𝐵)
3 grpcld.y . 2 (𝜑𝑌𝐵)
4 grpcld.b . . 3 𝐵 = (Base‘𝐺)
5 grpcld.p . . 3 + = (+g𝐺)
64, 5grpcl 18869 . 2 ((𝐺 ∈ Grp ∧ 𝑋𝐵𝑌𝐵) → (𝑋 + 𝑌) ∈ 𝐵)
71, 2, 3, 6syl3anc 1368 1 (𝜑 → (𝑋 + 𝑌) ∈ 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1533  wcel 2098  cfv 6536  (class class class)co 7404  Basecbs 17151  +gcplusg 17204  Grpcgrp 18861
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2697  ax-nul 5299
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-sb 2060  df-clab 2704  df-cleq 2718  df-clel 2804  df-ne 2935  df-ral 3056  df-rex 3065  df-rab 3427  df-v 3470  df-sbc 3773  df-dif 3946  df-un 3948  df-in 3950  df-ss 3960  df-nul 4318  df-if 4524  df-sn 4624  df-pr 4626  df-op 4630  df-uni 4903  df-br 5142  df-iota 6488  df-fv 6544  df-ov 7407  df-mgm 18571  df-sgrp 18650  df-mnd 18666  df-grp 18864
This theorem is referenced by:  dfgrp3  18965  xpsinv  18986  xpsgrpsub  18987  nmzsubg  19090  eqger  19103  lringuplu  20442  rnglidl1  21089  rngqiprngimfo  21152  rngqiprngfulem3  21164  cphpyth  25095  ghmquskerlem3  33037  evls1addd  33157  ply1degltlss  33172  q1pdir  33178  r1pcyc  33182  r1padd1  33183  r1plmhm  33185  evls1maprhm  33278  algextdeglem8  33301  aks6d1c1p3  41485  grpcominv1  41624  rhmmpl  41663  mplmapghm  41666  evlsmaprhm  41680  evladdval  41685  selvadd  41698
  Copyright terms: Public domain W3C validator