Theorem grpsubcl 18994

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

Syntax hints:   → wi 4   ∧ w3a 1092   = wceq 1547   ∈ wcel 2119   × cxp 5623  ⟶wf 6488  ‘cfv 6492  (class class class)co 7363  Basecbs 17177  Grpcgrp 18907  -_gcsg 18909

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2712  ax-sep 5225  ax-nul 5235  ax-pow 5301  ax-pr 5369  ax-un 7685

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2719  df-cleq 2732  df-clel 2815  df-nfc 2889  df-ne 2936  df-ral 3055  df-rex 3065  df-rmo 3345  df-reu 3346  df-rab 3393  df-v 3434  df-sbc 3731  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4269  df-if 4462  df-pw 4538  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4846  df-iun 4930  df-br 5080  df-opab 5142  df-mpt 5161  df-id 5520  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-fv 6500  df-riota 7320  df-ov 7366  df-oprab 7367  df-mpo 7368  df-1st 7938  df-2nd 7939  df-0g 17402  df-mgm 18606  df-sgrp 18685  df-mnd 18701  df-grp 18910  df-minusg 18911  df-sbg 18912

This theorem is referenced by:  grpsubsub  19003  grpsubsub4  19007  grpnpncan  19009  grpnnncan2  19011  dfgrp3  19013  xpsgrpsub  19035  nsgconj  19132  nsgacs  19135  nsgid  19143  ghmnsgpreima  19214  ghmeqker  19216  ghmf1  19219  conjghm  19222  conjnmz  19225  conjnmzb  19226  sylow3lem2  19601  abladdsub4  19784  abladdsub  19785  ablsubaddsub  19787  ablpncan3  19789  ablsubsub4  19791  ablpnpcan  19792  ablnnncan  19795  ablnnncan1  19796  telgsumfzslem  19961  telgsumfzs  19962  telgsums  19966  ogrpsublt  20115  isdomn4  20695  ornglmulle  20846  orngrmulle  20847  lmodvsubcl  20904  lvecvscan2  21112  rngqiprngimfolem  21290  rngqiprngimfo  21301  rngqiprngfulem3  21313  rngqiprngfulem4  21314  rngqiprngfulem5  21315  ipsubdir  21624  ipsubdi  21625  ip2subdi  21626  coe1subfv  22259  evl1subd  22335  dmatsubcl  22488  scmatsubcl  22507  mdetunilem9  22610  mdetuni0  22611  chmatcl  22818  chpmat1d  22826  chpdmatlem1  22828  chpscmat  22832  chpidmat  22837  chfacfisf  22844  cpmadugsumlemF  22866  cpmidgsum2  22869  tgpconncomp  24103  ghmcnp  24105  nrmmetd  24564  ngpds2  24596  ngpds3  24598  isngp4  24602  nmsub  24613  nm2dif  24615  nmtri2  24617  subgngp  24625  ngptgp  24626  nrgdsdi  24655  nrgdsdir  24656  nlmdsdi  24671  nlmdsdir  24672  nrginvrcnlem  24681  nmods  24734  tcphcphlem1  25227  tcphcph  25229  cphipval2  25233  4cphipval2  25234  cphipval  25235  ipcnlem2  25236  deg1sublt  26100  ply1divmo  26126  ply1divex  26127  r1pcl  26149  r1pid  26151  ply1remlem  26155  idomrootle  26163  ig1peu  26165  dchr2sum  27261  lgsqrlem2  27335  lgsqrlem3  27336  lgsqrlem4  27337  ttgcontlem1  28978  grpsubcld  33128  archiabllem1a  33279  archiabllem2a  33282  archiabllem2c  33283  erler  33353  rlocf1  33361  fracerl  33397  evls1subd  33662  q1pvsca  33694  irngss  33878  2sqr3minply  33971  lclkrlem2m  42018  aks6d1c2lem4  42619  aks6d1c6lem2  42663  aks6d1c6lem3  42664  aks5lem2  42679  lidldomn1  48729  linply1  48891