Theorem grpsubcl 19262

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

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1103   = wceq 1570   ∈ wcel 2147   × cxp 5654  ⟶wf 6557  ‘cfv 6561  (class class class)co 7446  Basecbs 17419  Grpcgrp 19176  -_gcsg 19178

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-sep 5253  ax-nul 5264  ax-pow 5332  ax-pr 5396  ax-un 7778

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 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-ral 3081  df-rex 3091  df-rmo 3369  df-reu 3370  df-rab 3417  df-v 3456  df-sbc 3743  df-csb 3852  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-iun 4956  df-br 5107  df-opab 5172  df-mpt 5191  df-id 5551  df-xp 5662  df-rel 5663  df-cnv 5664  df-co 5665  df-dm 5666  df-rn 5667  df-res 5668  df-ima 5669  df-iota 6515  df-fun 6563  df-fn 6564  df-f 6565  df-fv 6569  df-riota 7403  df-ov 7449  df-oprab 7450  df-mpo 7451  df-1st 8028  df-2nd 8029  df-0g 17644  df-mgm 18848  df-sgrp 18940  df-mnd 18956  df-grp 19179  df-minusg 19180  df-sbg 19181

This theorem is used by:  grpsubsub  19271  grpsubsub4  19275  grpnpncan  19277  grpnnncan2  19279  dfgrp3  19281  xpsgrpsub  19303  nsgconj  19401  nsgacs  19404  nsgid  19412  ghmnsgpreima  19487  ghmeqker  19489  ghmf1  19492  conjghm  19495  conjnmz  19498  conjnmzb  19499  sylow3lem2  19875  abladdsub4  20058  abladdsub  20059  ablsubaddsub  20061  ablpncan3  20063  ablsubsub4  20065  ablpnpcan  20066  ablnnncan  20069  ablnnncan1  20070  telgsumfzslem  20235  telgsumfzs  20236  telgsums  20240  ogrpsublt  20389  isdomn4  21000  ornglmulle  21157  orngrmulle  21158  lmodvsubcl  21215  lvecvscan2  21423  rngqiprngimfolem  21619  rngqiprngimfo  21630  rngqiprngfulem3  21642  rngqiprngfulem4  21643  rngqiprngfulem5  21644  ipsubdir  21981  ipsubdi  21982  ip2subdi  21983  coe1subfv  22618  evl1subd  22693  dmatsubcl  22846  scmatsubcl  22865  mdetunilem9  22968  mdetuni0  22969  chmatcl  23179  chpmat1d  23187  chpdmatlem1  23189  chpscmat  23193  chpidmat  23198  chfacfisf  23205  cpmadugsumlemF  23227  cpmidgsum2  23230  tgpconncomp  24465  ghmcnp  24467  nrmmetd  24926  ngpds2  24958  ngpds3  24960  isngp4  24964  nmsub  24975  nm2dif  24977  nmtri2  24979  subgngp  24987  ngptgp  24988  nrgdsdi  25017  nrgdsdir  25018  nlmdsdi  25033  nlmdsdir  25034  nrginvrcnlem  25043  nmods  25096  tcphcphlem1  25589  tcphcph  25591  cphipval2  25595  4cphipval2  25596  cphipval  25597  ipcnlem2  25598  deg1sublt  26461  ply1divmo  26487  ply1divex  26488  r1pcl  26510  r1pid  26512  ply1remlem  26516  idomrootle  26524  ig1peu  26526  dchr2sum  27633  lgsqrlem2  27707  lgsqrlem3  27708  lgsqrlem4  27709  ttgcontlem1  29495  grpsubcld  33678  archiabllem1a  33828  archiabllem2a  33831  archiabllem2c  33832  erler  33902  rlocf1  33911  fracerl  33952  evls1subd  34187  q1pvsca  34219  irngss  34402  2sqr3minply  34495  lclkrlem2m  42779  aks6d1c2lem4  43380  aks6d1c6lem2  43424  aks6d1c6lem3  43425  aks5lem2  43440  lidldomn1  49543  idomcanl  49659  linply1  49720