Theorem grpcld 18965

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

Syntax hints:   → wi 4   = wceq 1554   ∈ wcel 2136  ‘cfv 6510  (class class class)co 7385  Basecbs 17221  +_gcplusg 17262  Grpcgrp 18951

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1809  ax-4 1823  ax-5 1924  ax-6 1981  ax-7 2022  ax-8 2138  ax-9 2146  ax-ext 2728  ax-nul 5250

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 857  df-3an 1097  df-tru 1557  df-fal 1567  df-ex 1794  df-sb 2085  df-clab 2735  df-cleq 2748  df-clel 2831  df-ne 2952  df-ral 3071  df-rex 3081  df-rab 3409  df-v 3450  df-sbc 3740  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4281  df-if 4475  df-sn 4577  df-pr 4579  df-op 4583  df-uni 4860  df-br 5095  df-iota 6466  df-fv 6518  df-ov 7388  df-mgm 18650  df-sgrp 18729  df-mnd 18745  df-grp 18954

This theorem is referenced by:  grpraddf1o  19032  dfgrp3  19057  xpsinv  19078  xpsgrpsub  19079  nmzsubg  19182  eqger  19195  conjnmz  19268  ghmqusnsg  19298  ghmquskerlem3  19302  lringuplu  20566  rnglidl1  21275  rngqiprngimfo  21344  rngqiprngfulem3  21356  evladdval  22129  mplmapghm  22148  evlsmaprhm  22157  selvadd  22169  mhpaddcl  22189  psdmul  22204  evls1addd  22407  evls1maprhm  22412  rhmmpl  22416  cphpyth  25251  conjga  33304  cntrval2  33305  ringdi22  33364  rlocaddval  33404  rloccring  33406  rlocf1  33409  dflringlem2  33645  evl1deg1  33726  evl1deg2  33727  evl1deg3  33728  ply1degltlss  33746  q1pdir  33753  r1pcyc  33757  r1padd1  33758  r1plmhm  33760  0mplrim  33765  selvply1rhmlem4  33774  mplvrpmga  33796  mplvrpmmhm  33797  algextdeglem8  33975  rtelextdg2lem  33977  cos9thpiminplylem6  34038  cos9thpiminply  34039  zrhcntr  34230  aks6d1c1p3  42675  aks5lem3a  42754  aks5lem5a  42756  grpcominv1  43078  rhmpsr  43113