Theorem grpsubcl 18946

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

Syntax hints:   → wi 4   ∧ w3a 1086   = wceq 1540   ∈ wcel 2105   × cxp 5674  ⟶wf 6539  ‘cfv 6543  (class class class)co 7412  Basecbs 17151  Grpcgrp 18861  -_gcsg 18863

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2702  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7729

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ne 2940  df-ral 3061  df-rex 3070  df-rmo 3375  df-reu 3376  df-rab 3432  df-v 3475  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-iun 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5574  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-fv 6551  df-riota 7368  df-ov 7415  df-oprab 7416  df-mpo 7417  df-1st 7979  df-2nd 7980  df-0g 17394  df-mgm 18571  df-sgrp 18650  df-mnd 18666  df-grp 18864  df-minusg 18865  df-sbg 18866

This theorem is referenced by:  grpsubsub  18955  grpsubsub4  18959  grpnpncan  18961  grpnnncan2  18963  dfgrp3  18965  xpsgrpsub  18987  nsgconj  19082  nsgacs  19085  nsgid  19093  ghmnsgpreima  19162  ghmeqker  19164  ghmf1  19167  conjghm  19170  conjnmz  19173  conjnmzb  19174  sylow3lem2  19544  abladdsub4  19727  abladdsub  19728  ablsubaddsub  19730  ablpncan3  19732  ablsubsub4  19734  ablpnpcan  19735  ablnnncan  19738  ablnnncan1  19739  telgsumfzslem  19904  telgsumfzs  19905  telgsums  19909  lmodvsubcl  20749  lvecvscan2  20959  rngqiprngimfolem  21138  rngqiprngimfo  21149  rngqiprngfulem3  21161  rngqiprngfulem4  21162  rngqiprngfulem5  21163  isdomn4  21207  ipsubdir  21505  ipsubdi  21506  ip2subdi  21507  coe1subfv  22108  evl1subd  22181  dmatsubcl  22320  scmatsubcl  22339  mdetunilem9  22442  mdetuni0  22443  chmatcl  22650  chpmat1d  22658  chpdmatlem1  22660  chpscmat  22664  chpidmat  22669  chfacfisf  22676  cpmadugsumlemF  22698  cpmidgsum2  22701  tgpconncomp  23937  ghmcnp  23939  nrmmetd  24403  ngpds2  24435  ngpds3  24437  isngp4  24441  nmsub  24452  nm2dif  24454  nmtri2  24456  subgngp  24464  ngptgp  24465  nrgdsdi  24502  nrgdsdir  24503  nlmdsdi  24518  nlmdsdir  24519  nrginvrcnlem  24528  nmods  24581  tcphcphlem1  25083  tcphcph  25085  cphipval2  25089  4cphipval2  25090  cphipval  25091  ipcnlem2  25092  deg1sublt  25966  ply1divmo  25991  ply1divex  25992  r1pcl  26013  r1pid  26015  ply1remlem  26018  ig1peu  26027  dchr2sum  27119  lgsqrlem2  27193  lgsqrlem3  27194  lgsqrlem4  27195  ttgcontlem1  28575  ogrpsublt  32675  archiabllem1a  32773  archiabllem2a  32776  archiabllem2c  32777  ornglmulle  32859  orngrmulle  32860  q1pvsca  33115  irngss  33206  lclkrlem2m  40854  idomrootle  42400  lidldomn1  47068  linply1  47236