Theorem grpsubcl 19074

Description: Closure of group subtraction. (Contributed by NM, 31-Mar-2014.)

Hypotheses

Ref	Expression
grpsubcl.b	⊢ 𝐵 = (Base‘𝐺)
grpsubcl.m	⊢ − = (-g‘𝐺)

Assertion

Ref	Expression
grpsubcl	⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 − 𝑌) ∈ 𝐵)

Proof of Theorem grpsubcl

Step	Hyp	Ref	Expression
1		grpsubcl.b	. . 3 ⊢ 𝐵 = (Base‘𝐺)
2		grpsubcl.m	. . 3 ⊢ − = (-g‘𝐺)
3	1, 2	grpsubf 19073	. 2 ⊢ (𝐺 ∈ Grp → − :(𝐵 × 𝐵)⟶𝐵)
4		fovcdm 7570	. 2 ⊢ (( − :(𝐵 × 𝐵)⟶𝐵 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 − 𝑌) ∈ 𝐵)
5	3, 4	syl3an1 1179	1 ⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 − 𝑌) ∈ 𝐵)

Syntax hints:   → wi 4   ∧ w3a 1101   = wceq 1563   ∈ wcel 2145   × cxp 5649  ⟶wf 6521  ‘cfv 6525  (class class class)co 7400  Basecbs 17257  Grpcgrp 18988  -_gcsg 18990

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2737  ax-sep 5250  ax-nul 5260  ax-pow 5326  ax-pr 5394  ax-un 7722

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-nf 1807  df-sb 2094  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-ral 3080  df-rex 3090  df-rmo 3370  df-reu 3371  df-rab 3418  df-v 3459  df-sbc 3748  df-csb 3856  df-dif 3910  df-un 3912  df-in 3914  df-ss 3924  df-nul 4289  df-if 4484  df-pw 4560  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-iun 4953  df-br 5105  df-opab 5167  df-mpt 5186  df-id 5546  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-iota 6481  df-fun 6527  df-fn 6528  df-f 6529  df-fv 6533  df-riota 7357  df-ov 7403  df-oprab 7404  df-mpo 7405  df-1st 7974  df-2nd 7975  df-0g 17482  df-mgm 18686  df-sgrp 18765  df-mnd 18781  df-grp 18991  df-minusg 18992  df-sbg 18993

This theorem is referenced by:  grpsubsub  19083  grpsubsub4  19087  grpnpncan  19089  grpnnncan2  19091  dfgrp3  19093  xpsgrpsub  19115  nsgconj  19213  nsgacs  19216  nsgid  19224  ghmnsgpreima  19299  ghmeqker  19301  ghmf1  19304  conjghm  19307  conjnmz  19310  conjnmzb  19311  sylow3lem2  19686  abladdsub4  19869  abladdsub  19870  ablsubaddsub  19872  ablpncan3  19874  ablsubsub4  19876  ablpnpcan  19877  ablnnncan  19880  ablnnncan1  19881  telgsumfzslem  20046  telgsumfzs  20047  telgsums  20051  ogrpsublt  20200  isdomn4  20788  ornglmulle  20936  orngrmulle  20937  lmodvsubcl  20994  lvecvscan2  21202  rngqiprngimfolem  21389  rngqiprngimfo  21400  rngqiprngfulem3  21412  rngqiprngfulem4  21413  rngqiprngfulem5  21414  ipsubdir  21749  ipsubdi  21750  ip2subdi  21751  coe1subfv  22384  evl1subd  22459  dmatsubcl  22612  scmatsubcl  22631  mdetunilem9  22734  mdetuni0  22735  chmatcl  22942  chpmat1d  22950  chpdmatlem1  22952  chpscmat  22956  chpidmat  22961  chfacfisf  22968  cpmadugsumlemF  22990  cpmidgsum2  22993  tgpconncomp  24227  ghmcnp  24229  nrmmetd  24688  ngpds2  24720  ngpds3  24722  isngp4  24726  nmsub  24737  nm2dif  24739  nmtri2  24741  subgngp  24749  ngptgp  24750  nrgdsdi  24779  nrgdsdir  24780  nlmdsdi  24795  nlmdsdir  24796  nrginvrcnlem  24805  nmods  24858  tcphcphlem1  25351  tcphcph  25353  cphipval2  25357  4cphipval2  25358  cphipval  25359  ipcnlem2  25360  deg1sublt  26224  ply1divmo  26250  ply1divex  26251  r1pcl  26273  r1pid  26275  ply1remlem  26279  idomrootle  26287  ig1peu  26289  dchr2sum  27391  lgsqrlem2  27465  lgsqrlem3  27466  lgsqrlem4  27467  ttgcontlem1  29139  grpsubcld  33269  archiabllem1a  33419  archiabllem2a  33422  archiabllem2c  33423  erler  33493  rlocf1  33502  fracerl  33537  evls1subd  33774  q1pvsca  33806  irngss  33989  2sqr3minply  34082  lclkrlem2m  42150  aks6d1c2lem4  42751  aks6d1c6lem2  42795  aks6d1c6lem3  42796  aks5lem2  42811  lidldomn1  48852  linply1  49025