Theorem grpsubcl 18930

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 18929	. 2 ⊢ (𝐺 ∈ Grp → − :(𝐵 × 𝐵)⟶𝐵)
4		fovcdm 7516	. 2 ⊢ (( − :(𝐵 × 𝐵)⟶𝐵 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 − 𝑌) ∈ 𝐵)
5	3, 4	syl3an1 1163	1 ⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 − 𝑌) ∈ 𝐵)

Syntax hints:   → wi 4   ∧ w3a 1086   = wceq 1541   ∈ wcel 2111   × cxp 5614  ⟶wf 6477  ‘cfv 6481  (class class class)co 7346  Basecbs 17117  Grpcgrp 18843  -_gcsg 18845

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703  ax-sep 5234  ax-nul 5244  ax-pow 5303  ax-pr 5370  ax-un 7668

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2535  df-eu 2564  df-clab 2710  df-cleq 2723  df-clel 2806  df-nfc 2881  df-ne 2929  df-ral 3048  df-rex 3057  df-rmo 3346  df-reu 3347  df-rab 3396  df-v 3438  df-sbc 3742  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4284  df-if 4476  df-pw 4552  df-sn 4577  df-pr 4579  df-op 4583  df-uni 4860  df-iun 4943  df-br 5092  df-opab 5154  df-mpt 5173  df-id 5511  df-xp 5622  df-rel 5623  df-cnv 5624  df-co 5625  df-dm 5626  df-rn 5627  df-res 5628  df-ima 5629  df-iota 6437  df-fun 6483  df-fn 6484  df-f 6485  df-fv 6489  df-riota 7303  df-ov 7349  df-oprab 7350  df-mpo 7351  df-1st 7921  df-2nd 7922  df-0g 17342  df-mgm 18545  df-sgrp 18624  df-mnd 18640  df-grp 18846  df-minusg 18847  df-sbg 18848

This theorem is referenced by:  grpsubsub  18939  grpsubsub4  18943  grpnpncan  18945  grpnnncan2  18947  dfgrp3  18949  xpsgrpsub  18971  nsgconj  19069  nsgacs  19072  nsgid  19080  ghmnsgpreima  19151  ghmeqker  19153  ghmf1  19156  conjghm  19159  conjnmz  19162  conjnmzb  19163  sylow3lem2  19538  abladdsub4  19721  abladdsub  19722  ablsubaddsub  19724  ablpncan3  19726  ablsubsub4  19728  ablpnpcan  19729  ablnnncan  19732  ablnnncan1  19733  telgsumfzslem  19898  telgsumfzs  19899  telgsums  19903  ogrpsublt  20052  isdomn4  20629  ornglmulle  20780  orngrmulle  20781  lmodvsubcl  20838  lvecvscan2  21047  rngqiprngimfolem  21225  rngqiprngimfo  21236  rngqiprngfulem3  21248  rngqiprngfulem4  21249  rngqiprngfulem5  21250  ipsubdir  21577  ipsubdi  21578  ip2subdi  21579  coe1subfv  22178  evl1subd  22255  dmatsubcl  22411  scmatsubcl  22430  mdetunilem9  22533  mdetuni0  22534  chmatcl  22741  chpmat1d  22749  chpdmatlem1  22751  chpscmat  22755  chpidmat  22760  chfacfisf  22767  cpmadugsumlemF  22789  cpmidgsum2  22792  tgpconncomp  24026  ghmcnp  24028  nrmmetd  24487  ngpds2  24519  ngpds3  24521  isngp4  24525  nmsub  24536  nm2dif  24538  nmtri2  24540  subgngp  24548  ngptgp  24549  nrgdsdi  24578  nrgdsdir  24579  nlmdsdi  24594  nlmdsdir  24595  nrginvrcnlem  24604  nmods  24657  tcphcphlem1  25160  tcphcph  25162  cphipval2  25166  4cphipval2  25167  cphipval  25168  ipcnlem2  25169  deg1sublt  26040  ply1divmo  26066  ply1divex  26067  r1pcl  26089  r1pid  26091  ply1remlem  26095  idomrootle  26103  ig1peu  26105  dchr2sum  27209  lgsqrlem2  27283  lgsqrlem3  27284  lgsqrlem4  27285  ttgcontlem1  28861  grpsubcld  33016  archiabllem1a  33155  archiabllem2a  33158  archiabllem2c  33159  erler  33227  rlocf1  33235  fracerl  33267  evls1subd  33530  q1pvsca  33559  irngss  33695  2sqr3minply  33788  lclkrlem2m  41557  aks6d1c2lem4  42159  aks6d1c6lem2  42203  aks6d1c6lem3  42204  aks5lem2  42219  lidldomn1  48261  linply1  48424