Theorem grpcld 18870

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2113  ‘cfv 6489  (class class class)co 7355  Basecbs 17130  +_gcplusg 17171  Grpcgrp 18856

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 2115  ax-9 2123  ax-ext 2705  ax-nul 5248

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 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-ne 2931  df-ral 3050  df-rex 3059  df-rab 3398  df-v 3440  df-sbc 3739  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4861  df-br 5096  df-iota 6445  df-fv 6497  df-ov 7358  df-mgm 18558  df-sgrp 18637  df-mnd 18653  df-grp 18859

This theorem is referenced by:  grpraddf1o  18937  dfgrp3  18962  xpsinv  18983  xpsgrpsub  18984  nmzsubg  19087  eqger  19100  conjnmz  19174  ghmqusnsg  19204  ghmquskerlem3  19208  lringuplu  20469  rnglidl1  21179  rngqiprngimfo  21248  rngqiprngfulem3  21260  mhpaddcl  22076  psdmul  22091  evls1addd  22296  evls1maprhm  22301  rhmmpl  22308  cphpyth  25153  conjga  33150  cntrval2  33151  ringdi22  33209  rlocaddval  33246  rloccring  33248  rlocf1  33251  evl1deg1  33550  evl1deg2  33551  evl1deg3  33552  ply1degltlss  33568  q1pdir  33574  r1pcyc  33578  r1padd1  33579  r1plmhm  33581  mplvrpmga  33586  mplvrpmmhm  33587  algextdeglem8  33748  rtelextdg2lem  33750  cos9thpiminplylem6  33811  cos9thpiminply  33812  zrhcntr  34003  aks6d1c1p3  42213  aks5lem3a  42292  aks5lem5a  42294  grpcominv1  42616  rhmpsr  42660  mplmapghm  42664  evlsmaprhm  42678  evladdval  42683  selvadd  42696