Theorem grpsubcl 18905

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

Syntax hints:   → wi 4   ∧ w3a 1087   = wceq 1541   ∈ wcel 2106   × cxp 5674  ⟶wf 6539  ‘cfv 6543  (class class class)co 7411  Basecbs 17146  Grpcgrp 18821  -_gcsg 18823

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7727

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-ral 3062  df-rex 3071  df-rmo 3376  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-iun 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5574  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-fv 6551  df-riota 7367  df-ov 7414  df-oprab 7415  df-mpo 7416  df-1st 7977  df-2nd 7978  df-0g 17389  df-mgm 18563  df-sgrp 18612  df-mnd 18628  df-grp 18824  df-minusg 18825  df-sbg 18826

This theorem is referenced by:  grpsubsub  18914  grpsubsub4  18918  grpnpncan  18920  grpnnncan2  18922  dfgrp3  18924  xpsgrpsub  18946  nsgconj  19041  nsgacs  19044  nsgid  19052  ghmnsgpreima  19119  ghmeqker  19121  ghmf1  19123  conjghm  19125  conjnmz  19128  conjnmzb  19129  sylow3lem2  19498  abladdsub4  19681  abladdsub  19682  ablsubaddsub  19684  ablpncan3  19686  ablsubsub4  19688  ablpnpcan  19689  ablnnncan  19692  ablnnncan1  19693  telgsumfzslem  19858  telgsumfzs  19859  telgsums  19863  lmodvsubcl  20522  lvecvscan2  20731  isdomn4  20924  ipsubdir  21201  ipsubdi  21202  ip2subdi  21203  coe1subfv  21795  evl1subd  21868  dmatsubcl  22007  scmatsubcl  22026  mdetunilem9  22129  mdetuni0  22130  chmatcl  22337  chpmat1d  22345  chpdmatlem1  22347  chpscmat  22351  chpidmat  22356  chfacfisf  22363  cpmadugsumlemF  22385  cpmidgsum2  22388  tgpconncomp  23624  ghmcnp  23626  nrmmetd  24090  ngpds2  24122  ngpds3  24124  isngp4  24128  nmsub  24139  nm2dif  24141  nmtri2  24143  subgngp  24151  ngptgp  24152  nrgdsdi  24189  nrgdsdir  24190  nlmdsdi  24205  nlmdsdir  24206  nrginvrcnlem  24215  nmods  24268  tcphcphlem1  24759  tcphcph  24761  cphipval2  24765  4cphipval2  24766  cphipval  24767  ipcnlem2  24768  deg1sublt  25635  ply1divmo  25660  ply1divex  25661  r1pcl  25682  r1pid  25684  ply1remlem  25687  ig1peu  25696  dchr2sum  26783  lgsqrlem2  26857  lgsqrlem3  26858  lgsqrlem4  26859  ttgcontlem1  28180  ogrpsublt  32280  archiabllem1a  32378  archiabllem2a  32381  archiabllem2c  32382  ornglmulle  32464  orngrmulle  32465  q1pvsca  32720  irngss  32811  lclkrlem2m  40476  idomrootle  42019  rngqiprngimfolem  46854  rngqiprngimfo  46865  rngqiprngfulem3  46877  rngqiprngfulem4  46878  rngqiprngfulem5  46879  lidldomn1  46902  linply1  47152