Theorem grpsubcl 18179

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

Syntax hints:   → wi 4   ∧ w3a 1083   = wceq 1537   ∈ wcel 2114   × cxp 5553  ⟶wf 6351  ‘cfv 6355  (class class class)co 7156  Basecbs 16483  Grpcgrp 18103  -_gcsg 18105

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 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-sep 5203  ax-nul 5210  ax-pow 5266  ax-pr 5330  ax-un 7461

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-ral 3143  df-rex 3144  df-reu 3145  df-rmo 3146  df-rab 3147  df-v 3496  df-sbc 3773  df-csb 3884  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-pw 4541  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4839  df-iun 4921  df-br 5067  df-opab 5129  df-mpt 5147  df-id 5460  df-xp 5561  df-rel 5562  df-cnv 5563  df-co 5564  df-dm 5565  df-rn 5566  df-res 5567  df-ima 5568  df-iota 6314  df-fun 6357  df-fn 6358  df-f 6359  df-fv 6363  df-riota 7114  df-ov 7159  df-oprab 7160  df-mpo 7161  df-1st 7689  df-2nd 7690  df-0g 16715  df-mgm 17852  df-sgrp 17901  df-mnd 17912  df-grp 18106  df-minusg 18107  df-sbg 18108

This theorem is referenced by:  grpsubsub  18188  grpsubsub4  18192  grpnpncan  18194  grpnnncan2  18196  dfgrp3  18198  nsgconj  18311  nsgacs  18314  nsgid  18322  ghmnsgpreima  18383  ghmeqker  18385  ghmf1  18387  conjghm  18389  conjnmz  18392  conjnmzb  18393  sylow3lem2  18753  abladdsub4  18934  abladdsub  18935  ablpncan3  18937  ablsubsub4  18939  ablpnpcan  18940  ablnnncan  18943  ablnnncan1  18944  telgsumfzslem  19108  telgsumfzs  19109  telgsums  19113  lmodvsubcl  19679  lvecvscan2  19884  coe1subfv  20434  evl1subd  20505  ipsubdir  20786  ipsubdi  20787  ip2subdi  20788  dmatsubcl  21107  scmatsubcl  21126  mdetunilem9  21229  mdetuni0  21230  chmatcl  21436  chpmat1d  21444  chpdmatlem1  21446  chpscmat  21450  chpidmat  21455  chfacfisf  21462  cpmadugsumlemF  21484  cpmidgsum2  21487  tgpconncomp  22721  ghmcnp  22723  nrmmetd  23184  ngpds2  23215  ngpds3  23217  isngp4  23221  nmsub  23232  nm2dif  23234  nmtri2  23236  subgngp  23244  ngptgp  23245  nrgdsdi  23274  nrgdsdir  23275  nlmdsdi  23290  nlmdsdir  23291  nrginvrcnlem  23300  nmods  23353  tcphcphlem1  23838  tcphcph  23840  cphipval2  23844  4cphipval2  23845  cphipval  23846  ipcnlem2  23847  deg1sublt  24704  ply1divmo  24729  ply1divex  24730  r1pcl  24751  r1pid  24753  ply1remlem  24756  ig1peu  24765  dchr2sum  25849  lgsqrlem2  25923  lgsqrlem3  25924  lgsqrlem4  25925  ttgcontlem1  26671  ogrpsublt  30722  archiabllem1a  30820  archiabllem2a  30823  archiabllem2c  30824  ornglmulle  30878  orngrmulle  30879  lclkrlem2m  38670  idomrootle  39815  lidldomn1  44212  linply1  44467