Theorem grpcld 19020

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

This proof depends on syntax axioms:   → wi 4   = wceq 1569   ∈ wcel 2142  ‘cfv 6536  (class class class)co 7412  Basecbs 17275  +_gcplusg 17316  Grpcgrp 19006

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-8 2144  ax-9 2152  ax-ext 2734  ax-nul 5268

This proof depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1104  df-tru 1572  df-fal 1582  df-ex 1809  df-sb 2096  df-clab 2741  df-cleq 2754  df-clel 2837  df-ne 2958  df-ral 3079  df-rex 3089  df-rab 3416  df-v 3456  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 7415  df-mgm 18704  df-sgrp 18783  df-mnd 18799  df-grp 19009

This theorem is used by:  grpraddf1o  19086  dfgrp3  19111  xpsinv  19132  xpsgrpsub  19133  nmzsubg  19237  eqger  19252  conjnmz  19328  ghmqusnsg  19358  ghmquskerlem3  19362  ringdi22  20354  lringuplu  20654  rnglidl1  21369  rngqiprngimfo  21452  rngqiprngfulem3  21464  evladdval  22265  mplmapghm  22284  evlsmaprhm  22293  selvadd  22305  mhpaddcl  22325  psdmul  22340  evls1addd  22542  evls1maprhm  22547  rhmmpl  22551  cphpyth  25386  conjga  33499  cntrval2  33500  rlocaddval  33598  rloccring  33600  rlocf1  33603  dflringlem2  33794  evl1deg1  33875  evl1deg2  33876  evl1deg3  33877  ply1degltlss  33895  q1pdir  33902  r1pcyc  33906  r1padd1  33907  r1plmhm  33908  0mplrim  33913  selvply1rhmlem4  33922  mplvrpmga  33944  mplvrpmmhm  33945  algextdeglem8  34123  rtelextdg2lem  34125  cos9thpiminplylem6  34186  cos9thpiminply  34187  zrhcntr  34378  aks6d1c1p3  42905  aks5lem3a  42984  aks5lem5a  42986  grpcominv1  43310  rhmpsr  43343