Theorem grpsubcl 18952

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

Syntax hints:   → wi 4   ∧ w3a 1086   = wceq 1540   ∈ wcel 2109   × cxp 5636  ⟶wf 6507  ‘cfv 6511  (class class class)co 7387  Basecbs 17179  Grpcgrp 18865  -_gcsg 18867

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5251  ax-nul 5261  ax-pow 5320  ax-pr 5387  ax-un 7711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-ral 3045  df-rex 3054  df-rmo 3354  df-reu 3355  df-rab 3406  df-v 3449  df-sbc 3754  df-csb 3863  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4297  df-if 4489  df-pw 4565  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-iun 4957  df-br 5108  df-opab 5170  df-mpt 5189  df-id 5533  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-iota 6464  df-fun 6513  df-fn 6514  df-f 6515  df-fv 6519  df-riota 7344  df-ov 7390  df-oprab 7391  df-mpo 7392  df-1st 7968  df-2nd 7969  df-0g 17404  df-mgm 18567  df-sgrp 18646  df-mnd 18662  df-grp 18868  df-minusg 18869  df-sbg 18870

This theorem is referenced by:  grpsubsub  18961  grpsubsub4  18965  grpnpncan  18967  grpnnncan2  18969  dfgrp3  18971  xpsgrpsub  18993  nsgconj  19091  nsgacs  19094  nsgid  19102  ghmnsgpreima  19173  ghmeqker  19175  ghmf1  19178  conjghm  19181  conjnmz  19184  conjnmzb  19185  sylow3lem2  19558  abladdsub4  19741  abladdsub  19742  ablsubaddsub  19744  ablpncan3  19746  ablsubsub4  19748  ablpnpcan  19749  ablnnncan  19752  ablnnncan1  19753  telgsumfzslem  19918  telgsumfzs  19919  telgsums  19923  isdomn4  20625  lmodvsubcl  20813  lvecvscan2  21022  rngqiprngimfolem  21200  rngqiprngimfo  21211  rngqiprngfulem3  21223  rngqiprngfulem4  21224  rngqiprngfulem5  21225  ipsubdir  21551  ipsubdi  21552  ip2subdi  21553  coe1subfv  22152  evl1subd  22229  dmatsubcl  22385  scmatsubcl  22404  mdetunilem9  22507  mdetuni0  22508  chmatcl  22715  chpmat1d  22723  chpdmatlem1  22725  chpscmat  22729  chpidmat  22734  chfacfisf  22741  cpmadugsumlemF  22763  cpmidgsum2  22766  tgpconncomp  24000  ghmcnp  24002  nrmmetd  24462  ngpds2  24494  ngpds3  24496  isngp4  24500  nmsub  24511  nm2dif  24513  nmtri2  24515  subgngp  24523  ngptgp  24524  nrgdsdi  24553  nrgdsdir  24554  nlmdsdi  24569  nlmdsdir  24570  nrginvrcnlem  24579  nmods  24632  tcphcphlem1  25135  tcphcph  25137  cphipval2  25141  4cphipval2  25142  cphipval  25143  ipcnlem2  25144  deg1sublt  26015  ply1divmo  26041  ply1divex  26042  r1pcl  26064  r1pid  26066  ply1remlem  26070  idomrootle  26078  ig1peu  26080  dchr2sum  27184  lgsqrlem2  27258  lgsqrlem3  27259  lgsqrlem4  27260  ttgcontlem1  28812  grpsubcld  32981  ogrpsublt  33035  archiabllem1a  33145  archiabllem2a  33148  archiabllem2c  33149  erler  33216  rlocf1  33224  fracerl  33256  ornglmulle  33283  orngrmulle  33284  evls1subd  33541  q1pvsca  33569  irngss  33682  2sqr3minply  33770  lclkrlem2m  41513  aks6d1c2lem4  42115  aks6d1c6lem2  42159  aks6d1c6lem3  42160  aks5lem2  42175  lidldomn1  48219  linply1  48382