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

Theorem grpsubcl 17762
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
StepHypRef Expression
1 grpsubcl.b . . 3 𝐵 = (Base‘𝐺)
2 grpsubcl.m . . 3 = (-g𝐺)
31, 2grpsubf 17761 . 2 (𝐺 ∈ Grp → :(𝐵 × 𝐵)⟶𝐵)
4 fovrn 7002 . 2 (( :(𝐵 × 𝐵)⟶𝐵𝑋𝐵𝑌𝐵) → (𝑋 𝑌) ∈ 𝐵)
53, 4syl3an1 1202 1 ((𝐺 ∈ Grp ∧ 𝑋𝐵𝑌𝐵) → (𝑋 𝑌) ∈ 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1107   = wceq 1652  wcel 2155   × cxp 5275  wf 6064  cfv 6068  (class class class)co 6842  Basecbs 16130  Grpcgrp 17689  -gcsg 17691
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-8 2157  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743  ax-rep 4930  ax-sep 4941  ax-nul 4949  ax-pow 5001  ax-pr 5062  ax-un 7147
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3an 1109  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-mo 2565  df-eu 2582  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-ne 2938  df-ral 3060  df-rex 3061  df-reu 3062  df-rmo 3063  df-rab 3064  df-v 3352  df-sbc 3597  df-csb 3692  df-dif 3735  df-un 3737  df-in 3739  df-ss 3746  df-nul 4080  df-if 4244  df-pw 4317  df-sn 4335  df-pr 4337  df-op 4341  df-uni 4595  df-iun 4678  df-br 4810  df-opab 4872  df-mpt 4889  df-id 5185  df-xp 5283  df-rel 5284  df-cnv 5285  df-co 5286  df-dm 5287  df-rn 5288  df-res 5289  df-ima 5290  df-iota 6031  df-fun 6070  df-fn 6071  df-f 6072  df-f1 6073  df-fo 6074  df-f1o 6075  df-fv 6076  df-riota 6803  df-ov 6845  df-oprab 6846  df-mpt2 6847  df-1st 7366  df-2nd 7367  df-0g 16368  df-mgm 17508  df-sgrp 17550  df-mnd 17561  df-grp 17692  df-minusg 17693  df-sbg 17694
This theorem is referenced by:  grpsubsub  17771  grpsubsub4  17775  grpnpncan  17777  grpnnncan2  17779  dfgrp3  17781  nsgconj  17891  nsgacs  17894  nsgid  17904  ghmnsgpreima  17949  ghmeqker  17951  ghmf1  17953  conjghm  17955  conjnmz  17958  conjnmzb  17959  sylow3lem2  18307  abladdsub4  18485  abladdsub  18486  ablpncan3  18488  ablsubsub4  18490  ablpnpcan  18491  ablnnncan  18494  ablnnncan1  18495  telgsumfzslem  18652  telgsumfzs  18653  telgsums  18657  lmodvsubcl  19177  lvecvscan2  19384  coe1subfv  19909  evl1subd  19979  ipsubdir  20262  ipsubdi  20263  ip2subdi  20264  dmatsubcl  20581  scmatsubcl  20600  mdetunilem9  20703  mdetuni0  20704  chmatcl  20912  chpmat1d  20920  chpdmatlem1  20922  chpscmat  20926  chpidmat  20931  chfacfisf  20938  cpmadugsumlemF  20960  cpmidgsum2  20963  tgpconncomp  22195  ghmcnp  22197  nrmmetd  22658  ngpds2  22689  ngpds3  22691  isngp4  22695  nmsub  22706  nm2dif  22708  nmtri2  22710  subgngp  22718  ngptgp  22719  nrgdsdi  22748  nrgdsdir  22749  nlmdsdi  22764  nlmdsdir  22765  nrginvrcnlem  22774  nmods  22827  tcphcphlem1  23312  tcphcph  23314  cphipval2  23318  4cphipval2  23319  cphipval  23320  ipcnlem2  23321  deg1sublt  24161  ply1divmo  24186  ply1divex  24187  r1pcl  24208  r1pid  24210  ply1remlem  24213  ig1peu  24222  dchr2sum  25289  lgsqrlem2  25363  lgsqrlem3  25364  lgsqrlem4  25365  ttgcontlem1  26056  ogrpsublt  30169  archiabllem1a  30192  archiabllem2a  30195  archiabllem2c  30196  ornglmulle  30252  orngrmulle  30253  lclkrlem2m  37475  idomrootle  38450  lidldomn1  42590  linply1  42850
  Copyright terms: Public domain W3C validator