Theorem grpsubcl 19149

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

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1103   = wceq 1570   ∈ wcel 2145   × cxp 5657  ⟶wf 6533  ‘cfv 6537  (class class class)co 7417  Basecbs 17307  Grpcgrp 19063  -_gcsg 19065

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 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2734  ax-sep 5255  ax-nul 5267  ax-pow 5334  ax-pr 5402  ax-un 7740

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 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-ral 3079  df-rex 3089  df-rmo 3367  df-reu 3368  df-rab 3415  df-v 3455  df-sbc 3743  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4283  df-if 4486  df-pw 4562  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4871  df-iun 4956  df-br 5108  df-opab 5172  df-mpt 5191  df-id 5554  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-fv 6545  df-riota 7374  df-ov 7420  df-oprab 7421  df-mpo 7422  df-1st 7990  df-2nd 7991  df-0g 17532  df-mgm 18736  df-sgrp 18827  df-mnd 18843  df-grp 19066  df-minusg 19067  df-sbg 19068

This theorem is used by:  grpsubsub  19158  grpsubsub4  19162  grpnpncan  19164  grpnnncan2  19166  dfgrp3  19168  xpsgrpsub  19190  nsgconj  19288  nsgacs  19291  nsgid  19299  ghmnsgpreima  19374  ghmeqker  19376  ghmf1  19379  conjghm  19382  conjnmz  19385  conjnmzb  19386  sylow3lem2  19761  abladdsub4  19944  abladdsub  19945  ablsubaddsub  19947  ablpncan3  19949  ablsubsub4  19951  ablpnpcan  19952  ablnnncan  19955  ablnnncan1  19956  telgsumfzslem  20121  telgsumfzs  20122  telgsums  20126  ogrpsublt  20275  isdomn4  20883  ornglmulle  21039  orngrmulle  21040  lmodvsubcl  21097  lvecvscan2  21305  rngqiprngimfolem  21499  rngqiprngimfo  21510  rngqiprngfulem3  21522  rngqiprngfulem4  21523  rngqiprngfulem5  21524  ipsubdir  21861  ipsubdi  21862  ip2subdi  21863  coe1subfv  22498  evl1subd  22573  dmatsubcl  22726  scmatsubcl  22745  mdetunilem9  22848  mdetuni0  22849  chmatcl  23059  chpmat1d  23067  chpdmatlem1  23069  chpscmat  23073  chpidmat  23078  chfacfisf  23085  cpmadugsumlemF  23107  cpmidgsum2  23110  tgpconncomp  24345  ghmcnp  24347  nrmmetd  24806  ngpds2  24838  ngpds3  24840  isngp4  24844  nmsub  24855  nm2dif  24857  nmtri2  24859  subgngp  24867  ngptgp  24868  nrgdsdi  24897  nrgdsdir  24898  nlmdsdi  24913  nlmdsdir  24914  nrginvrcnlem  24923  nmods  24976  tcphcphlem1  25469  tcphcph  25471  cphipval2  25475  4cphipval2  25476  cphipval  25477  ipcnlem2  25478  deg1sublt  26342  ply1divmo  26368  ply1divex  26369  r1pcl  26391  r1pid  26393  ply1remlem  26397  idomrootle  26405  ig1peu  26407  dchr2sum  27517  lgsqrlem2  27591  lgsqrlem3  27592  lgsqrlem4  27593  ttgcontlem1  29349  grpsubcld  33489  archiabllem1a  33639  archiabllem2a  33642  archiabllem2c  33643  erler  33713  rlocf1  33722  fracerl  33755  evls1subd  33990  q1pvsca  34022  irngss  34205  2sqr3minply  34298  lclkrlem2m  42400  aks6d1c2lem4  43001  aks6d1c6lem2  43045  aks6d1c6lem3  43046  aks5lem2  43061  lidldomn1  49154  idomcanl  49270  linply1  49331