Theorem grpsubcl 19210

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

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1103   = wceq 1570   ∈ wcel 2145   × cxp 5649  ⟶wf 6527  ‘cfv 6531  (class class class)co 7412  Basecbs 17367  Grpcgrp 19124  -_gcsg 19126

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 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733  ax-sep 5249  ax-nul 5260  ax-pow 5327  ax-pr 5391  ax-un 7740

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 2100  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-ral 3078  df-rex 3088  df-rmo 3366  df-reu 3367  df-rab 3414  df-v 3453  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-iun 4953  df-br 5104  df-opab 5168  df-mpt 5187  df-id 5546  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-iota 6487  df-fun 6533  df-fn 6534  df-f 6535  df-fv 6539  df-riota 7369  df-ov 7415  df-oprab 7416  df-mpo 7417  df-1st 7990  df-2nd 7991  df-0g 17592  df-mgm 18796  df-sgrp 18888  df-mnd 18904  df-grp 19127  df-minusg 19128  df-sbg 19129

This theorem is used by:  grpsubsub  19219  grpsubsub4  19223  grpnpncan  19225  grpnnncan2  19227  dfgrp3  19229  xpsgrpsub  19251  nsgconj  19349  nsgacs  19352  nsgid  19360  ghmnsgpreima  19435  ghmeqker  19437  ghmf1  19440  conjghm  19443  conjnmz  19446  conjnmzb  19447  sylow3lem2  19822  abladdsub4  20005  abladdsub  20006  ablsubaddsub  20008  ablpncan3  20010  ablsubsub4  20012  ablpnpcan  20013  ablnnncan  20016  ablnnncan1  20017  telgsumfzslem  20182  telgsumfzs  20183  telgsums  20187  ogrpsublt  20336  isdomn4  20947  ornglmulle  21104  orngrmulle  21105  lmodvsubcl  21162  lvecvscan2  21370  rngqiprngimfolem  21566  rngqiprngimfo  21577  rngqiprngfulem3  21589  rngqiprngfulem4  21590  rngqiprngfulem5  21591  ipsubdir  21928  ipsubdi  21929  ip2subdi  21930  coe1subfv  22565  evl1subd  22640  dmatsubcl  22793  scmatsubcl  22812  mdetunilem9  22915  mdetuni0  22916  chmatcl  23126  chpmat1d  23134  chpdmatlem1  23136  chpscmat  23140  chpidmat  23145  chfacfisf  23152  cpmadugsumlemF  23174  cpmidgsum2  23177  tgpconncomp  24412  ghmcnp  24414  nrmmetd  24873  ngpds2  24905  ngpds3  24907  isngp4  24911  nmsub  24922  nm2dif  24924  nmtri2  24926  subgngp  24934  ngptgp  24935  nrgdsdi  24964  nrgdsdir  24965  nlmdsdi  24980  nlmdsdir  24981  nrginvrcnlem  24990  nmods  25043  tcphcphlem1  25536  tcphcph  25538  cphipval2  25542  4cphipval2  25543  cphipval  25544  ipcnlem2  25545  deg1sublt  26408  ply1divmo  26434  ply1divex  26435  r1pcl  26457  r1pid  26459  ply1remlem  26463  idomrootle  26471  ig1peu  26473  dchr2sum  27582  lgsqrlem2  27656  lgsqrlem3  27657  lgsqrlem4  27658  ttgcontlem1  29444  grpsubcld  33584  archiabllem1a  33734  archiabllem2a  33737  archiabllem2c  33738  erler  33808  rlocf1  33817  fracerl  33850  evls1subd  34086  q1pvsca  34118  irngss  34301  2sqr3minply  34394  lclkrlem2m  42544  aks6d1c2lem4  43145  aks6d1c6lem2  43189  aks6d1c6lem3  43190  aks5lem2  43205  lidldomn1  49272  idomcanl  49388  linply1  49449