Theorem grpcld 18921

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

Syntax hints:   → wi 4   = wceq 1547   ∈ wcel 2119  ‘cfv 6492  (class class class)co 7363  Basecbs 17177  +_gcplusg 17218  Grpcgrp 18907

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712  ax-nul 5235

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-ne 2936  df-ral 3055  df-rex 3065  df-rab 3393  df-v 3434  df-sbc 3731  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4269  df-if 4462  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4846  df-br 5080  df-iota 6448  df-fv 6500  df-ov 7366  df-mgm 18606  df-sgrp 18685  df-mnd 18701  df-grp 18910

This theorem is referenced by:  grpraddf1o  18988  dfgrp3  19013  xpsinv  19034  xpsgrpsub  19035  nmzsubg  19138  eqger  19151  conjnmz  19225  ghmqusnsg  19255  ghmquskerlem3  19259  lringuplu  20523  rnglidl1  21232  rngqiprngimfo  21301  rngqiprngfulem3  21313  evladdval  22086  mplmapghm  22105  evlsmaprhm  22114  selvadd  22126  mhpaddcl  22146  psdmul  22161  evls1addd  22364  evls1maprhm  22369  rhmmpl  22373  cphpyth  25208  conjga  33258  cntrval2  33259  ringdi22  33318  rlocaddval  33356  rloccring  33358  rlocf1  33361  evl1deg1  33666  evl1deg2  33667  evl1deg3  33668  ply1degltlss  33686  q1pdir  33693  r1pcyc  33697  r1padd1  33698  r1plmhm  33700  0mplrim  33705  selvply1rhmlem4  33714  mplvrpmga  33736  mplvrpmmhm  33737  algextdeglem8  33915  rtelextdg2lem  33917  cos9thpiminplylem6  33978  cos9thpiminply  33979  zrhcntr  34170  aks6d1c1p3  42596  aks5lem3a  42675  aks5lem5a  42677  grpcominv1  42999  rhmpsr  43034