Theorem grpsubcl 18171

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 18170	. 2 ⊢ (𝐺 ∈ Grp → − :(𝐵 × 𝐵)⟶𝐵)
4		fovrn 7298	. 2 ⊢ (( − :(𝐵 × 𝐵)⟶𝐵 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 − 𝑌) ∈ 𝐵)
5	3, 4	syl3an1 1160	1 ⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 − 𝑌) ∈ 𝐵)

Syntax hints:   → wi 4   ∧ w3a 1084   = wceq 1538   ∈ wcel 2111   × cxp 5517  ⟶wf 6320  ‘cfv 6324  (class class class)co 7135  Basecbs 16475  Grpcgrp 18095  -_gcsg 18097

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-sep 5167  ax-nul 5174  ax-pow 5231  ax-pr 5295  ax-un 7441

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-ral 3111  df-rex 3112  df-reu 3113  df-rmo 3114  df-rab 3115  df-v 3443  df-sbc 3721  df-csb 3829  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-nul 4244  df-if 4426  df-pw 4499  df-sn 4526  df-pr 4528  df-op 4532  df-uni 4801  df-iun 4883  df-br 5031  df-opab 5093  df-mpt 5111  df-id 5425  df-xp 5525  df-rel 5526  df-cnv 5527  df-co 5528  df-dm 5529  df-rn 5530  df-res 5531  df-ima 5532  df-iota 6283  df-fun 6326  df-fn 6327  df-f 6328  df-fv 6332  df-riota 7093  df-ov 7138  df-oprab 7139  df-mpo 7140  df-1st 7671  df-2nd 7672  df-0g 16707  df-mgm 17844  df-sgrp 17893  df-mnd 17904  df-grp 18098  df-minusg 18099  df-sbg 18100

This theorem is referenced by:  grpsubsub  18180  grpsubsub4  18184  grpnpncan  18186  grpnnncan2  18188  dfgrp3  18190  nsgconj  18303  nsgacs  18306  nsgid  18314  ghmnsgpreima  18375  ghmeqker  18377  ghmf1  18379  conjghm  18381  conjnmz  18384  conjnmzb  18385  sylow3lem2  18745  abladdsub4  18927  abladdsub  18928  ablpncan3  18930  ablsubsub4  18932  ablpnpcan  18933  ablnnncan  18936  ablnnncan1  18937  telgsumfzslem  19101  telgsumfzs  19102  telgsums  19106  lmodvsubcl  19672  lvecvscan2  19877  ipsubdir  20331  ipsubdi  20332  ip2subdi  20333  coe1subfv  20895  evl1subd  20966  dmatsubcl  21103  scmatsubcl  21122  mdetunilem9  21225  mdetuni0  21226  chmatcl  21433  chpmat1d  21441  chpdmatlem1  21443  chpscmat  21447  chpidmat  21452  chfacfisf  21459  cpmadugsumlemF  21481  cpmidgsum2  21484  tgpconncomp  22718  ghmcnp  22720  nrmmetd  23181  ngpds2  23212  ngpds3  23214  isngp4  23218  nmsub  23229  nm2dif  23231  nmtri2  23233  subgngp  23241  ngptgp  23242  nrgdsdi  23271  nrgdsdir  23272  nlmdsdi  23287  nlmdsdir  23288  nrginvrcnlem  23297  nmods  23350  tcphcphlem1  23839  tcphcph  23841  cphipval2  23845  4cphipval2  23846  cphipval  23847  ipcnlem2  23848  deg1sublt  24711  ply1divmo  24736  ply1divex  24737  r1pcl  24758  r1pid  24760  ply1remlem  24763  ig1peu  24772  dchr2sum  25857  lgsqrlem2  25931  lgsqrlem3  25932  lgsqrlem4  25933  ttgcontlem1  26679  ogrpsublt  30772  archiabllem1a  30870  archiabllem2a  30873  archiabllem2c  30874  ornglmulle  30929  orngrmulle  30930  lclkrlem2m  38815  idomrootle  40139  lidldomn1  44545  linply1  44801