Theorem grpcld 19158

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

This proof depends on syntax axioms:   → wi 4   = wceq 1569   ∈ wcel 2144  ‘cfv 6538  (class class class)co 7420  Basecbs 17387  +_gcplusg 17428  Grpcgrp 19144

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-nul 5259

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ne 2956  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-sbc 3739  df-ss 3896  df-dif 4047  df-un 4151  df-nul 4279  df-if 4482  df-sn 4584  df-pr 4586  df-op 4590  df-uni 4867  df-br 5103  df-iota 6494  df-fv 6546  df-ov 7423  df-mgm 18816  df-sgrp 18908  df-mnd 18924  df-grp 19147

This theorem is used by:  grpraddf1o  19224  dfgrp3  19249  xpsinv  19270  xpsgrpsub  19271  nmzsubg  19375  eqger  19390  conjnmz  19466  ghmqusnsg  19496  ghmquskerlem3  19500  ringdi22  20493  lringuplu  20796  rnglidl1  21512  rngqiprngimfo  21597  rngqiprngfulem3  21609  evladdval  22412  mplmapghm  22431  evlsmaprhm  22440  selvadd  22452  mhpaddcl  22472  psdmul  22487  evls1addd  22689  evls1maprhm  22694  rhmmpl  22698  cphpyth  25537  conjga  33731  cntrval2  33732  rlocaddval  33830  rloccring  33832  rlocf1  33835  dflringlem2  34027  evl1deg1  34108  evl1deg2  34109  evl1deg3  34110  ply1degltlss  34128  q1pdir  34135  r1pcyc  34139  r1padd1  34140  r1plmhm  34141  0mplrim  34146  selvply1rhmlem4  34155  mplvrpmga  34177  mplvrpmmhm  34178  algextdeglem8  34356  rtelextdg2lem  34358  cos9thpiminplylem6  34419  cos9thpiminply  34420  zrhcntr  34611  aks6d1c1p3  43161  aks5lem3a  43240  aks5lem5a  43242  grpcominv1  43576  rhmpsr  43612