Theorem grpcld 18886

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109  ‘cfv 6514  (class class class)co 7390  Basecbs 17186  +_gcplusg 17227  Grpcgrp 18872

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702  ax-nul 5264

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-ne 2927  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-sbc 3757  df-dif 3920  df-un 3922  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-iota 6467  df-fv 6522  df-ov 7393  df-mgm 18574  df-sgrp 18653  df-mnd 18669  df-grp 18875

This theorem is referenced by:  grpraddf1o  18953  dfgrp3  18978  xpsinv  18999  xpsgrpsub  19000  nmzsubg  19104  eqger  19117  conjnmz  19191  ghmqusnsg  19221  ghmquskerlem3  19225  lringuplu  20460  rnglidl1  21149  rngqiprngimfo  21218  rngqiprngfulem3  21230  mhpaddcl  22045  psdmul  22060  evls1addd  22265  evls1maprhm  22270  rhmmpl  22277  cphpyth  25123  conjga  33134  cntrval2  33135  ringdi22  33189  rlocaddval  33226  rloccring  33228  rlocf1  33231  evl1deg1  33552  evl1deg2  33553  evl1deg3  33554  ply1degltlss  33569  q1pdir  33575  r1pcyc  33579  r1padd1  33580  r1plmhm  33582  algextdeglem8  33721  rtelextdg2lem  33723  cos9thpiminplylem6  33784  cos9thpiminply  33785  zrhcntr  33976  aks6d1c1p3  42105  aks5lem3a  42184  aks5lem5a  42186  grpcominv1  42503  rhmpsr  42547  mplmapghm  42551  evlsmaprhm  42565  evladdval  42570  selvadd  42583