Theorem grpsubcl 19087

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

Syntax hints:   → wi 4   ∧ w3a 1103   = wceq 1570   ∈ wcel 2143   × cxp 5661  ⟶wf 6534  ‘cfv 6538  (class class class)co 7412  Basecbs 17270  Grpcgrp 19001  -_gcsg 19003

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5258  ax-nul 5270  ax-pow 5338  ax-pr 5406  ax-un 7734

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-ral 3080  df-rex 3090  df-rmo 3369  df-reu 3370  df-rab 3417  df-v 3457  df-sbc 3746  df-csb 3855  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4288  df-if 4489  df-pw 4565  df-sn 4591  df-pr 4593  df-op 4597  df-uni 4874  df-iun 4959  df-br 5111  df-opab 5175  df-mpt 5194  df-id 5558  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676  df-iota 6494  df-fun 6540  df-fn 6541  df-f 6542  df-fv 6546  df-riota 7369  df-ov 7415  df-oprab 7416  df-mpo 7417  df-1st 7987  df-2nd 7988  df-0g 17495  df-mgm 18699  df-sgrp 18778  df-mnd 18794  df-grp 19004  df-minusg 19005  df-sbg 19006

This theorem is referenced by:  grpsubsub  19096  grpsubsub4  19100  grpnpncan  19102  grpnnncan2  19104  dfgrp3  19106  xpsgrpsub  19128  nsgconj  19226  nsgacs  19229  nsgid  19237  ghmnsgpreima  19312  ghmeqker  19314  ghmf1  19317  conjghm  19320  conjnmz  19323  conjnmzb  19324  sylow3lem2  19699  abladdsub4  19882  abladdsub  19883  ablsubaddsub  19885  ablpncan3  19887  ablsubsub4  19889  ablpnpcan  19890  ablnnncan  19893  ablnnncan1  19894  telgsumfzslem  20059  telgsumfzs  20060  telgsums  20064  ogrpsublt  20213  isdomn4  20801  ornglmulle  20951  orngrmulle  20952  lmodvsubcl  21009  lvecvscan2  21217  rngqiprngimfolem  21411  rngqiprngimfo  21422  rngqiprngfulem3  21434  rngqiprngfulem4  21435  rngqiprngfulem5  21436  ipsubdir  21773  ipsubdi  21774  ip2subdi  21775  coe1subfv  22408  evl1subd  22483  dmatsubcl  22636  scmatsubcl  22655  mdetunilem9  22758  mdetuni0  22759  chmatcl  22966  chpmat1d  22974  chpdmatlem1  22976  chpscmat  22980  chpidmat  22985  chfacfisf  22992  cpmadugsumlemF  23014  cpmidgsum2  23017  tgpconncomp  24251  ghmcnp  24253  nrmmetd  24712  ngpds2  24744  ngpds3  24746  isngp4  24750  nmsub  24761  nm2dif  24763  nmtri2  24765  subgngp  24773  ngptgp  24774  nrgdsdi  24803  nrgdsdir  24804  nlmdsdi  24819  nlmdsdir  24820  nrginvrcnlem  24829  nmods  24882  tcphcphlem1  25375  tcphcph  25377  cphipval2  25381  4cphipval2  25382  cphipval  25383  ipcnlem2  25384  deg1sublt  26248  ply1divmo  26274  ply1divex  26275  r1pcl  26297  r1pid  26299  ply1remlem  26303  idomrootle  26311  ig1peu  26313  dchr2sum  27418  lgsqrlem2  27492  lgsqrlem3  27493  lgsqrlem4  27494  ttgcontlem1  29215  grpsubcld  33342  archiabllem1a  33492  archiabllem2a  33495  archiabllem2c  33496  erler  33566  rlocf1  33575  fracerl  33608  evls1subd  33843  q1pvsca  33875  irngss  34058  2sqr3minply  34151  lclkrlem2m  42274  aks6d1c2lem4  42875  aks6d1c6lem2  42919  aks6d1c6lem3  42920  aks5lem2  42935  lidldomn1  48979  idomcanl  49095  linply1  49156