Theorem grpcld 19075

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2145  ‘cfv 6537  (class class class)co 7416  Basecbs 17305  +_gcplusg 17346  Grpcgrp 19061

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 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734  ax-nul 5267

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 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-ne 2958  df-ral 3079  df-rex 3089  df-rab 3415  df-v 3455  df-sbc 3743  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4283  df-if 4486  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4871  df-br 5108  df-iota 6493  df-fv 6545  df-ov 7419  df-mgm 18734  df-sgrp 18825  df-mnd 18841  df-grp 19064

This theorem is used by:  grpraddf1o  19141  dfgrp3  19166  xpsinv  19187  xpsgrpsub  19188  nmzsubg  19292  eqger  19307  conjnmz  19383  ghmqusnsg  19413  ghmquskerlem3  19417  ringdi22  20409  lringuplu  20710  rnglidl1  21425  rngqiprngimfo  21508  rngqiprngfulem3  21520  evladdval  22323  mplmapghm  22342  evlsmaprhm  22351  selvadd  22363  mhpaddcl  22383  psdmul  22398  evls1addd  22600  evls1maprhm  22605  rhmmpl  22609  cphpyth  25448  conjga  33612  cntrval2  33613  rlocaddval  33711  rloccring  33713  rlocf1  33716  dflringlem2  33907  evl1deg1  33988  evl1deg2  33989  evl1deg3  33990  ply1degltlss  34008  q1pdir  34015  r1pcyc  34019  r1padd1  34020  r1plmhm  34021  0mplrim  34026  selvply1rhmlem4  34035  mplvrpmga  34057  mplvrpmmhm  34058  algextdeglem8  34236  rtelextdg2lem  34238  cos9thpiminplylem6  34299  cos9thpiminply  34300  zrhcntr  34491  aks6d1c1p3  42978  aks5lem3a  43057  aks5lem5a  43059  grpcominv1  43398  rhmpsr  43431