Theorem grpcld 19187

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2147  ‘cfv 6558  (class class class)co 7443  Basecbs 17416  +_gcplusg 17457  Grpcgrp 19173

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-nul 5263

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-ne 2960  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-sbc 3743  df-ss 3901  df-dif 4050  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-br 5107  df-iota 6512  df-fv 6566  df-ov 7446  df-mgm 18845  df-sgrp 18937  df-mnd 18953  df-grp 19176

This theorem is used by:  grpraddf1o  19253  dfgrp3  19278  xpsinv  19299  xpsgrpsub  19300  nmzsubg  19404  eqger  19419  conjnmz  19495  ghmqusnsg  19526  ghmquskerlem3  19530  ringdi22  20523  lringuplu  20826  rnglidl1  21542  rngqiprngimfo  21627  rngqiprngfulem3  21639  evladdval  22442  mplmapghm  22461  evlsmaprhm  22470  selvadd  22482  mhpaddcl  22502  psdmul  22517  evls1addd  22719  evls1maprhm  22724  rhmmpl  22728  cphpyth  25567  conjga  33801  cntrval2  33802  rlocaddval  33900  rloccring  33902  rlocf1  33905  dflringlem2  34097  evl1deg1  34178  evl1deg2  34179  evl1deg3  34180  ply1degltlss  34198  q1pdir  34205  r1pcyc  34209  r1padd1  34210  r1plmhm  34211  0mplrim  34216  selvply1rhmlem4  34225  mplvrpmga  34247  mplvrpmmhm  34248  algextdeglem8  34426  rtelextdg2lem  34428  cos9thpiminplylem6  34489  cos9thpiminply  34490  zrhcntr  34681  aks6d1c1p3  43352  aks5lem3a  43431  aks5lem5a  43433  grpcominv1  43768  rhmpsr  43804