Theorem grpcld 18852

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 18846	. 2 ⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 + 𝑌) ∈ 𝐵)
7	1, 2, 3, 6	syl3anc 1373	1 ⊢ (𝜑 → (𝑋 + 𝑌) ∈ 𝐵)

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2110  ‘cfv 6477  (class class class)co 7341  Basecbs 17112  +_gcplusg 17153  Grpcgrp 18838

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2112  ax-9 2120  ax-ext 2702  ax-nul 5242

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2067  df-clab 2709  df-cleq 2722  df-clel 2804  df-ne 2927  df-ral 3046  df-rex 3055  df-rab 3394  df-v 3436  df-sbc 3740  df-dif 3903  df-un 3905  df-ss 3917  df-nul 4282  df-if 4474  df-sn 4575  df-pr 4577  df-op 4581  df-uni 4858  df-br 5090  df-iota 6433  df-fv 6485  df-ov 7344  df-mgm 18540  df-sgrp 18619  df-mnd 18635  df-grp 18841

This theorem is referenced by:  grpraddf1o  18919  dfgrp3  18944  xpsinv  18965  xpsgrpsub  18966  nmzsubg  19070  eqger  19083  conjnmz  19157  ghmqusnsg  19187  ghmquskerlem3  19191  lringuplu  20452  rnglidl1  21162  rngqiprngimfo  21231  rngqiprngfulem3  21243  mhpaddcl  22059  psdmul  22074  evls1addd  22279  evls1maprhm  22284  rhmmpl  22291  cphpyth  25136  conjga  33129  cntrval2  33130  ringdi22  33188  rlocaddval  33225  rloccring  33227  rlocf1  33230  evl1deg1  33529  evl1deg2  33530  evl1deg3  33531  ply1degltlss  33547  q1pdir  33553  r1pcyc  33557  r1padd1  33558  r1plmhm  33560  mplvrpmga  33565  mplvrpmmhm  33566  algextdeglem8  33727  rtelextdg2lem  33729  cos9thpiminplylem6  33790  cos9thpiminply  33791  zrhcntr  33982  aks6d1c1p3  42122  aks5lem3a  42201  aks5lem5a  42203  grpcominv1  42520  rhmpsr  42564  mplmapghm  42568  evlsmaprhm  42582  evladdval  42587  selvadd  42600