MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  grpsubcl Structured version   Unicode version

Theorem grpsubcl 16317
Description: Closure of group subtraction. (Contributed by NM, 31-Mar-2014.)
Hypotheses
Ref Expression
grpsubcl.b  |-  B  =  ( Base `  G
)
grpsubcl.m  |-  .-  =  ( -g `  G )
Assertion
Ref Expression
grpsubcl  |-  ( ( G  e.  Grp  /\  X  e.  B  /\  Y  e.  B )  ->  ( X  .-  Y
)  e.  B )

Proof of Theorem grpsubcl
StepHypRef Expression
1 grpsubcl.b . . 3  |-  B  =  ( Base `  G
)
2 grpsubcl.m . . 3  |-  .-  =  ( -g `  G )
31, 2grpsubf 16316 . 2  |-  ( G  e.  Grp  ->  .-  :
( B  X.  B
) --> B )
4 fovrn 6418 . 2  |-  ( ( 
.-  : ( B  X.  B ) --> B  /\  X  e.  B  /\  Y  e.  B
)  ->  ( X  .-  Y )  e.  B
)
53, 4syl3an1 1259 1  |-  ( ( G  e.  Grp  /\  X  e.  B  /\  Y  e.  B )  ->  ( X  .-  Y
)  e.  B )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ w3a 971    = wceq 1398    e. wcel 1823    X. cxp 4986   -->wf 5566   ` cfv 5570  (class class class)co 6270   Basecbs 14716   Grpcgrp 16252   -gcsg 16254
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-8 1825  ax-9 1827  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432  ax-rep 4550  ax-sep 4560  ax-nul 4568  ax-pow 4615  ax-pr 4676  ax-un 6565
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 973  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-eu 2288  df-mo 2289  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2651  df-ral 2809  df-rex 2810  df-reu 2811  df-rmo 2812  df-rab 2813  df-v 3108  df-sbc 3325  df-csb 3421  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3784  df-if 3930  df-pw 4001  df-sn 4017  df-pr 4019  df-op 4023  df-uni 4236  df-iun 4317  df-br 4440  df-opab 4498  df-mpt 4499  df-id 4784  df-xp 4994  df-rel 4995  df-cnv 4996  df-co 4997  df-dm 4998  df-rn 4999  df-res 5000  df-ima 5001  df-iota 5534  df-fun 5572  df-fn 5573  df-f 5574  df-f1 5575  df-fo 5576  df-f1o 5577  df-fv 5578  df-riota 6232  df-ov 6273  df-oprab 6274  df-mpt2 6275  df-1st 6773  df-2nd 6774  df-0g 14931  df-mgm 16071  df-sgrp 16110  df-mnd 16120  df-grp 16256  df-minusg 16257  df-sbg 16258
This theorem is referenced by:  grpsubsub  16326  grpsubsub4  16330  grpnpncan  16332  grpnnncan2  16334  nsgconj  16433  nsgacs  16436  nsgid  16446  ghmnsgpreima  16490  ghmeqker  16492  ghmf1  16494  conjghm  16496  conjnmz  16499  conjnmzb  16500  sylow3lem2  16847  abladdsub4  17023  abladdsub  17024  ablpncan3  17026  ablsubsub4  17028  ablpnpcan  17029  ablnnncan1  17032  telgsumfzslem  17212  telgsumfzs  17213  telgsums  17217  lmodvsubcl  17750  lvecvscan2  17953  coe1subfv  18502  evl1subd  18573  ipsubdir  18850  ipsubdi  18851  ip2subdi  18852  dmatsubcl  19167  scmatsubcl  19186  mdetunilem9  19289  mdetuni0  19290  chmatcl  19496  chpmat1d  19504  chpdmatlem1  19506  chpscmat  19510  chpidmat  19515  chfacfisf  19522  cpmadugsumlemF  19544  cpmidgsum2  19547  tgpconcomp  20777  ghmcnp  20779  nrmmetd  21261  ngpds2  21291  ngpds3  21293  isngp4  21297  nmsub  21308  nm2dif  21310  subgngp  21315  ngptgp  21316  nrgdsdi  21340  nrgdsdir  21341  nlmdsdi  21356  nlmdsdir  21357  nrginvrcnlem  21365  nmods  21417  tchcphlem1  21844  tchcph  21846  ipcnlem2  21850  deg1sublt  22677  ply1divmo  22702  ply1divex  22703  r1pcl  22724  r1pid  22726  ply1remlem  22729  ig1peu  22738  dchr2sum  23746  lgsqrlem2  23815  lgsqrlem3  23816  lgsqrlem4  23817  ttgcontlem1  24390  ogrpsublt  27946  archiabllem1a  27969  archiabllem2a  27972  archiabllem2c  27973  ornglmulle  28030  orngrmulle  28031  idomrootle  31393  lidldomn1  32981  linply1  33247  lclkrlem2m  37643
  Copyright terms: Public domain W3C validator