Theorem grpsubcl 19050

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

Syntax hints:   → wi 4   ∧ w3a 1086   = wceq 1536   ∈ wcel 2105   × cxp 5686  ⟶wf 6558  ‘cfv 6562  (class class class)co 7430  Basecbs 17244  Grpcgrp 18963  -_gcsg 18965

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pow 5370  ax-pr 5437  ax-un 7753

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ne 2938  df-ral 3059  df-rex 3068  df-rmo 3377  df-reu 3378  df-rab 3433  df-v 3479  df-sbc 3791  df-csb 3908  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-nul 4339  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-iun 4997  df-br 5148  df-opab 5210  df-mpt 5231  df-id 5582  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-res 5700  df-ima 5701  df-iota 6515  df-fun 6564  df-fn 6565  df-f 6566  df-fv 6570  df-riota 7387  df-ov 7433  df-oprab 7434  df-mpo 7435  df-1st 8012  df-2nd 8013  df-0g 17487  df-mgm 18665  df-sgrp 18744  df-mnd 18760  df-grp 18966  df-minusg 18967  df-sbg 18968

This theorem is referenced by:  grpsubsub  19059  grpsubsub4  19063  grpnpncan  19065  grpnnncan2  19067  dfgrp3  19069  xpsgrpsub  19091  nsgconj  19189  nsgacs  19192  nsgid  19200  ghmnsgpreima  19271  ghmeqker  19273  ghmf1  19276  conjghm  19279  conjnmz  19282  conjnmzb  19283  sylow3lem2  19660  abladdsub4  19843  abladdsub  19844  ablsubaddsub  19846  ablpncan3  19848  ablsubsub4  19850  ablpnpcan  19851  ablnnncan  19854  ablnnncan1  19855  telgsumfzslem  20020  telgsumfzs  20021  telgsums  20025  isdomn4  20732  lmodvsubcl  20921  lvecvscan2  21131  rngqiprngimfolem  21317  rngqiprngimfo  21328  rngqiprngfulem3  21340  rngqiprngfulem4  21341  rngqiprngfulem5  21342  ipsubdir  21677  ipsubdi  21678  ip2subdi  21679  coe1subfv  22284  evl1subd  22361  dmatsubcl  22519  scmatsubcl  22538  mdetunilem9  22641  mdetuni0  22642  chmatcl  22849  chpmat1d  22857  chpdmatlem1  22859  chpscmat  22863  chpidmat  22868  chfacfisf  22875  cpmadugsumlemF  22897  cpmidgsum2  22900  tgpconncomp  24136  ghmcnp  24138  nrmmetd  24602  ngpds2  24634  ngpds3  24636  isngp4  24640  nmsub  24651  nm2dif  24653  nmtri2  24655  subgngp  24663  ngptgp  24664  nrgdsdi  24701  nrgdsdir  24702  nlmdsdi  24717  nlmdsdir  24718  nrginvrcnlem  24727  nmods  24780  tcphcphlem1  25282  tcphcph  25284  cphipval2  25288  4cphipval2  25289  cphipval  25290  ipcnlem2  25291  deg1sublt  26163  ply1divmo  26189  ply1divex  26190  r1pcl  26212  r1pid  26214  ply1remlem  26218  idomrootle  26226  ig1peu  26228  dchr2sum  27331  lgsqrlem2  27405  lgsqrlem3  27406  lgsqrlem4  27407  ttgcontlem1  28913  grpsubcld  33027  ogrpsublt  33080  archiabllem1a  33180  archiabllem2a  33183  archiabllem2c  33184  erler  33251  rlocf1  33259  fracerl  33287  ornglmulle  33314  orngrmulle  33315  evls1subd  33576  q1pvsca  33603  irngss  33701  2sqr3minply  33752  lclkrlem2m  41501  aks6d1c2lem4  42108  aks6d1c6lem2  42152  aks6d1c6lem3  42153  aks5lem2  42168  lidldomn1  48074  linply1  48238