Theorem grpsubcl 19096

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

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1103   = wceq 1570   ∈ wcel 2146   × cxp 5662  ⟶wf 6536  ‘cfv 6540  (class class class)co 7416  Basecbs 17279  Grpcgrp 19010  -_gcsg 19012

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2738  ax-sep 5260  ax-nul 5272  ax-pow 5339  ax-pr 5407  ax-un 7738

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2570  df-eu 2600  df-clab 2745  df-cleq 2758  df-clel 2841  df-nfc 2915  df-ne 2962  df-ral 3083  df-rex 3093  df-rmo 3372  df-reu 3373  df-rab 3420  df-v 3460  df-sbc 3748  df-csb 3857  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-nul 4290  df-if 4491  df-pw 4567  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4876  df-iun 4961  df-br 5113  df-opab 5177  df-mpt 5196  df-id 5559  df-xp 5670  df-rel 5671  df-cnv 5672  df-co 5673  df-dm 5674  df-rn 5675  df-res 5676  df-ima 5677  df-iota 6496  df-fun 6542  df-fn 6543  df-f 6544  df-fv 6548  df-riota 7373  df-ov 7419  df-oprab 7420  df-mpo 7421  df-1st 7988  df-2nd 7989  df-0g 17504  df-mgm 18708  df-sgrp 18787  df-mnd 18803  df-grp 19013  df-minusg 19014  df-sbg 19015

This theorem is used by:  grpsubsub  19105  grpsubsub4  19109  grpnpncan  19111  grpnnncan2  19113  dfgrp3  19115  xpsgrpsub  19137  nsgconj  19235  nsgacs  19238  nsgid  19246  ghmnsgpreima  19321  ghmeqker  19323  ghmf1  19326  conjghm  19329  conjnmz  19332  conjnmzb  19333  sylow3lem2  19708  abladdsub4  19891  abladdsub  19892  ablsubaddsub  19894  ablpncan3  19896  ablsubsub4  19898  ablpnpcan  19899  ablnnncan  19902  ablnnncan1  19903  telgsumfzslem  20068  telgsumfzs  20069  telgsums  20073  ogrpsublt  20222  isdomn4  20829  ornglmulle  20985  orngrmulle  20986  lmodvsubcl  21043  lvecvscan2  21251  rngqiprngimfolem  21445  rngqiprngimfo  21456  rngqiprngfulem3  21468  rngqiprngfulem4  21469  rngqiprngfulem5  21470  ipsubdir  21807  ipsubdi  21808  ip2subdi  21809  coe1subfv  22442  evl1subd  22517  dmatsubcl  22670  scmatsubcl  22689  mdetunilem9  22792  mdetuni0  22793  chmatcl  23000  chpmat1d  23008  chpdmatlem1  23010  chpscmat  23014  chpidmat  23019  chfacfisf  23026  cpmadugsumlemF  23048  cpmidgsum2  23051  tgpconncomp  24285  ghmcnp  24287  nrmmetd  24746  ngpds2  24778  ngpds3  24780  isngp4  24784  nmsub  24795  nm2dif  24797  nmtri2  24799  subgngp  24807  ngptgp  24808  nrgdsdi  24837  nrgdsdir  24838  nlmdsdi  24853  nlmdsdir  24854  nrginvrcnlem  24863  nmods  24916  tcphcphlem1  25409  tcphcph  25411  cphipval2  25415  4cphipval2  25416  cphipval  25417  ipcnlem2  25418  deg1sublt  26282  ply1divmo  26308  ply1divex  26309  r1pcl  26331  r1pid  26333  ply1remlem  26337  idomrootle  26345  ig1peu  26347  dchr2sum  27452  lgsqrlem2  27526  lgsqrlem3  27527  lgsqrlem4  27528  ttgcontlem1  29249  grpsubcld  33374  archiabllem1a  33524  archiabllem2a  33527  archiabllem2c  33528  erler  33598  rlocf1  33607  fracerl  33640  evls1subd  33875  q1pvsca  33907  irngss  34090  2sqr3minply  34183  lclkrlem2m  42325  aks6d1c2lem4  42926  aks6d1c6lem2  42970  aks6d1c6lem3  42971  aks5lem2  42986  lidldomn1  49028  idomcanl  49144  linply1  49205