Theorem grpsubcl 18962

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

Syntax hints:   → wi 4   ∧ w3a 1087   = wceq 1542   ∈ wcel 2114   × cxp 5630  ⟶wf 6496  ‘cfv 6500  (class class class)co 7368  Basecbs 17148  Grpcgrp 18875  -_gcsg 18877

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5243  ax-nul 5253  ax-pow 5312  ax-pr 5379  ax-un 7690

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-rmo 3352  df-reu 3353  df-rab 3402  df-v 3444  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-pw 4558  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-iun 4950  df-br 5101  df-opab 5163  df-mpt 5182  df-id 5527  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-res 5644  df-ima 5645  df-iota 6456  df-fun 6502  df-fn 6503  df-f 6504  df-fv 6508  df-riota 7325  df-ov 7371  df-oprab 7372  df-mpo 7373  df-1st 7943  df-2nd 7944  df-0g 17373  df-mgm 18577  df-sgrp 18656  df-mnd 18672  df-grp 18878  df-minusg 18879  df-sbg 18880

This theorem is referenced by:  grpsubsub  18971  grpsubsub4  18975  grpnpncan  18977  grpnnncan2  18979  dfgrp3  18981  xpsgrpsub  19003  nsgconj  19100  nsgacs  19103  nsgid  19111  ghmnsgpreima  19182  ghmeqker  19184  ghmf1  19187  conjghm  19190  conjnmz  19193  conjnmzb  19194  sylow3lem2  19569  abladdsub4  19752  abladdsub  19753  ablsubaddsub  19755  ablpncan3  19757  ablsubsub4  19759  ablpnpcan  19760  ablnnncan  19763  ablnnncan1  19764  telgsumfzslem  19929  telgsumfzs  19930  telgsums  19934  ogrpsublt  20083  isdomn4  20661  ornglmulle  20812  orngrmulle  20813  lmodvsubcl  20870  lvecvscan2  21079  rngqiprngimfolem  21257  rngqiprngimfo  21268  rngqiprngfulem3  21280  rngqiprngfulem4  21281  rngqiprngfulem5  21282  ipsubdir  21609  ipsubdi  21610  ip2subdi  21611  coe1subfv  22220  evl1subd  22298  dmatsubcl  22454  scmatsubcl  22473  mdetunilem9  22576  mdetuni0  22577  chmatcl  22784  chpmat1d  22792  chpdmatlem1  22794  chpscmat  22798  chpidmat  22803  chfacfisf  22810  cpmadugsumlemF  22832  cpmidgsum2  22835  tgpconncomp  24069  ghmcnp  24071  nrmmetd  24530  ngpds2  24562  ngpds3  24564  isngp4  24568  nmsub  24579  nm2dif  24581  nmtri2  24583  subgngp  24591  ngptgp  24592  nrgdsdi  24621  nrgdsdir  24622  nlmdsdi  24637  nlmdsdir  24638  nrginvrcnlem  24647  nmods  24700  tcphcphlem1  25203  tcphcph  25205  cphipval2  25209  4cphipval2  25210  cphipval  25211  ipcnlem2  25212  deg1sublt  26083  ply1divmo  26109  ply1divex  26110  r1pcl  26132  r1pid  26134  ply1remlem  26138  idomrootle  26146  ig1peu  26148  dchr2sum  27252  lgsqrlem2  27326  lgsqrlem3  27327  lgsqrlem4  27328  ttgcontlem1  28969  grpsubcld  33133  archiabllem1a  33284  archiabllem2a  33287  archiabllem2c  33288  erler  33358  rlocf1  33366  fracerl  33399  evls1subd  33664  q1pvsca  33696  irngss  33864  2sqr3minply  33957  lclkrlem2m  41889  aks6d1c2lem4  42491  aks6d1c6lem2  42535  aks6d1c6lem3  42536  aks5lem2  42551  lidldomn1  48585  linply1  48747