Theorem grpsubcl 18987

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

Syntax hints:   → wi 4   ∧ w3a 1087   = wceq 1542   ∈ wcel 2114   × cxp 5622  ⟶wf 6488  ‘cfv 6492  (class class class)co 7360  Basecbs 17170  Grpcgrp 18900  -_gcsg 18902

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 5231  ax-nul 5241  ax-pow 5302  ax-pr 5370  ax-un 7682

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 3343  df-reu 3344  df-rab 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-iun 4936  df-br 5087  df-opab 5149  df-mpt 5168  df-id 5519  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-fv 6500  df-riota 7317  df-ov 7363  df-oprab 7364  df-mpo 7365  df-1st 7935  df-2nd 7936  df-0g 17395  df-mgm 18599  df-sgrp 18678  df-mnd 18694  df-grp 18903  df-minusg 18904  df-sbg 18905

This theorem is referenced by:  grpsubsub  18996  grpsubsub4  19000  grpnpncan  19002  grpnnncan2  19004  dfgrp3  19006  xpsgrpsub  19028  nsgconj  19125  nsgacs  19128  nsgid  19136  ghmnsgpreima  19207  ghmeqker  19209  ghmf1  19212  conjghm  19215  conjnmz  19218  conjnmzb  19219  sylow3lem2  19594  abladdsub4  19777  abladdsub  19778  ablsubaddsub  19780  ablpncan3  19782  ablsubsub4  19784  ablpnpcan  19785  ablnnncan  19788  ablnnncan1  19789  telgsumfzslem  19954  telgsumfzs  19955  telgsums  19959  ogrpsublt  20108  isdomn4  20684  ornglmulle  20835  orngrmulle  20836  lmodvsubcl  20893  lvecvscan2  21102  rngqiprngimfolem  21280  rngqiprngimfo  21291  rngqiprngfulem3  21303  rngqiprngfulem4  21304  rngqiprngfulem5  21305  ipsubdir  21632  ipsubdi  21633  ip2subdi  21634  coe1subfv  22241  evl1subd  22317  dmatsubcl  22473  scmatsubcl  22492  mdetunilem9  22595  mdetuni0  22596  chmatcl  22803  chpmat1d  22811  chpdmatlem1  22813  chpscmat  22817  chpidmat  22822  chfacfisf  22829  cpmadugsumlemF  22851  cpmidgsum2  22854  tgpconncomp  24088  ghmcnp  24090  nrmmetd  24549  ngpds2  24581  ngpds3  24583  isngp4  24587  nmsub  24598  nm2dif  24600  nmtri2  24602  subgngp  24610  ngptgp  24611  nrgdsdi  24640  nrgdsdir  24641  nlmdsdi  24656  nlmdsdir  24657  nrginvrcnlem  24666  nmods  24719  tcphcphlem1  25212  tcphcph  25214  cphipval2  25218  4cphipval2  25219  cphipval  25220  ipcnlem2  25221  deg1sublt  26085  ply1divmo  26111  ply1divex  26112  r1pcl  26134  r1pid  26136  ply1remlem  26140  idomrootle  26148  ig1peu  26150  dchr2sum  27250  lgsqrlem2  27324  lgsqrlem3  27325  lgsqrlem4  27326  ttgcontlem1  28967  grpsubcld  33116  archiabllem1a  33267  archiabllem2a  33270  archiabllem2c  33271  erler  33341  rlocf1  33349  fracerl  33382  evls1subd  33647  q1pvsca  33679  irngss  33847  2sqr3minply  33940  lclkrlem2m  41979  aks6d1c2lem4  42580  aks6d1c6lem2  42624  aks6d1c6lem3  42625  aks5lem2  42640  lidldomn1  48719  linply1  48881