Theorem grpcld 19013

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

Step	Hyp	Ref	Expression
1		grpcld.r	. 2 ⊢ (𝜑 → 𝐺 ∈ Grp)
2		grpcld.x	. 2 ⊢ (𝜑 → 𝑋 ∈ 𝐵)
3		grpcld.y	. 2 ⊢ (𝜑 → 𝑌 ∈ 𝐵)
4		grpcld.b	. . 3 ⊢ 𝐵 = (Base‘𝐺)
5		grpcld.p	. . 3 ⊢ + = (+g‘𝐺)
6	4, 5	grpcl 19007	. 2 ⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 + 𝑌) ∈ 𝐵)
7	1, 2, 3, 6	syl3anc 1396	1 ⊢ (𝜑 → (𝑋 + 𝑌) ∈ 𝐵)

Syntax hints:   → wi 4   = wceq 1568   ∈ wcel 2141  ‘cfv 6536  (class class class)co 7410  Basecbs 17268  +_gcplusg 17309  Grpcgrp 18999

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1823  ax-4 1837  ax-5 1938  ax-6 1995  ax-7 2036  ax-8 2143  ax-9 2151  ax-ext 2733  ax-nul 5268

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1571  df-fal 1581  df-ex 1808  df-sb 2095  df-clab 2740  df-cleq 2753  df-clel 2836  df-ne 2957  df-ral 3078  df-rex 3088  df-rab 3415  df-v 3455  df-sbc 3744  df-dif 3907  df-un 3909  df-ss 3921  df-nul 4286  df-if 4487  df-sn 4589  df-pr 4591  df-op 4595  df-uni 4872  df-br 5109  df-iota 6492  df-fv 6544  df-ov 7413  df-mgm 18697  df-sgrp 18776  df-mnd 18792  df-grp 19002

This theorem is referenced by:  grpraddf1o  19079  dfgrp3  19104  xpsinv  19125  xpsgrpsub  19126  nmzsubg  19230  eqger  19245  conjnmz  19321  ghmqusnsg  19351  ghmquskerlem3  19355  ringdi22  20346  lringuplu  20628  rnglidl1  21337  rngqiprngimfo  21420  rngqiprngfulem3  21432  evladdval  22233  mplmapghm  22252  evlsmaprhm  22261  selvadd  22273  mhpaddcl  22293  psdmul  22308  evls1addd  22510  evls1maprhm  22515  rhmmpl  22519  cphpyth  25354  conjga  33456  cntrval2  33457  rlocaddval  33555  rloccring  33557  rlocf1  33560  dflringlem2  33751  evl1deg1  33832  evl1deg2  33833  evl1deg3  33834  ply1degltlss  33852  q1pdir  33859  r1pcyc  33863  r1padd1  33864  r1plmhm  33865  0mplrim  33870  selvply1rhmlem4  33879  mplvrpmga  33901  mplvrpmmhm  33902  algextdeglem8  34080  rtelextdg2lem  34082  cos9thpiminplylem6  34143  cos9thpiminply  34144  zrhcntr  34335  aks6d1c1p3  42845  aks5lem3a  42924  aks5lem5a  42926  grpcominv1  43250  rhmpsr  43285