Theorem grpsubcl 19008

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

Syntax hints:   → wi 4   ∧ w3a 1086   = wceq 1539   ∈ wcel 2107   × cxp 5663  ⟶wf 6537  ‘cfv 6541  (class class class)co 7413  Basecbs 17230  Grpcgrp 18921  -_gcsg 18923

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-10 2140  ax-11 2156  ax-12 2176  ax-ext 2706  ax-sep 5276  ax-nul 5286  ax-pow 5345  ax-pr 5412  ax-un 7737

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-nf 1783  df-sb 2064  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2726  df-clel 2808  df-nfc 2884  df-ne 2932  df-ral 3051  df-rex 3060  df-rmo 3363  df-reu 3364  df-rab 3420  df-v 3465  df-sbc 3771  df-csb 3880  df-dif 3934  df-un 3936  df-in 3938  df-ss 3948  df-nul 4314  df-if 4506  df-pw 4582  df-sn 4607  df-pr 4609  df-op 4613  df-uni 4888  df-iun 4973  df-br 5124  df-opab 5186  df-mpt 5206  df-id 5558  df-xp 5671  df-rel 5672  df-cnv 5673  df-co 5674  df-dm 5675  df-rn 5676  df-res 5677  df-ima 5678  df-iota 6494  df-fun 6543  df-fn 6544  df-f 6545  df-fv 6549  df-riota 7370  df-ov 7416  df-oprab 7417  df-mpo 7418  df-1st 7996  df-2nd 7997  df-0g 17458  df-mgm 18623  df-sgrp 18702  df-mnd 18718  df-grp 18924  df-minusg 18925  df-sbg 18926

This theorem is referenced by:  grpsubsub  19017  grpsubsub4  19021  grpnpncan  19023  grpnnncan2  19025  dfgrp3  19027  xpsgrpsub  19049  nsgconj  19147  nsgacs  19150  nsgid  19158  ghmnsgpreima  19229  ghmeqker  19231  ghmf1  19234  conjghm  19237  conjnmz  19240  conjnmzb  19241  sylow3lem2  19615  abladdsub4  19798  abladdsub  19799  ablsubaddsub  19801  ablpncan3  19803  ablsubsub4  19805  ablpnpcan  19806  ablnnncan  19809  ablnnncan1  19810  telgsumfzslem  19975  telgsumfzs  19976  telgsums  19980  isdomn4  20685  lmodvsubcl  20874  lvecvscan2  21083  rngqiprngimfolem  21263  rngqiprngimfo  21274  rngqiprngfulem3  21286  rngqiprngfulem4  21287  rngqiprngfulem5  21288  ipsubdir  21615  ipsubdi  21616  ip2subdi  21617  coe1subfv  22218  evl1subd  22295  dmatsubcl  22453  scmatsubcl  22472  mdetunilem9  22575  mdetuni0  22576  chmatcl  22783  chpmat1d  22791  chpdmatlem1  22793  chpscmat  22797  chpidmat  22802  chfacfisf  22809  cpmadugsumlemF  22831  cpmidgsum2  22834  tgpconncomp  24068  ghmcnp  24070  nrmmetd  24532  ngpds2  24564  ngpds3  24566  isngp4  24570  nmsub  24581  nm2dif  24583  nmtri2  24585  subgngp  24593  ngptgp  24594  nrgdsdi  24623  nrgdsdir  24624  nlmdsdi  24639  nlmdsdir  24640  nrginvrcnlem  24649  nmods  24702  tcphcphlem1  25206  tcphcph  25208  cphipval2  25212  4cphipval2  25213  cphipval  25214  ipcnlem2  25215  deg1sublt  26086  ply1divmo  26112  ply1divex  26113  r1pcl  26135  r1pid  26137  ply1remlem  26141  idomrootle  26149  ig1peu  26151  dchr2sum  27254  lgsqrlem2  27328  lgsqrlem3  27329  lgsqrlem4  27330  ttgcontlem1  28831  grpsubcld  32989  ogrpsublt  33042  archiabllem1a  33142  archiabllem2a  33145  archiabllem2c  33146  erler  33213  rlocf1  33221  fracerl  33253  ornglmulle  33280  orngrmulle  33281  evls1subd  33537  q1pvsca  33564  irngss  33679  2sqr3minply  33765  lclkrlem2m  41496  aks6d1c2lem4  42103  aks6d1c6lem2  42147  aks6d1c6lem3  42148  aks5lem2  42163  lidldomn1  48120  linply1  48283