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

Theorem grpsubval 18870
Description: Group subtraction (division) operation. (Contributed by NM, 31-Mar-2014.) (Revised by Mario Carneiro, 13-Dec-2014.)
Hypotheses
Ref Expression
grpsubval.b 𝐵 = (Base‘𝐺)
grpsubval.p + = (+g𝐺)
grpsubval.i 𝐼 = (invg𝐺)
grpsubval.m = (-g𝐺)
Assertion
Ref Expression
grpsubval ((𝑋𝐵𝑌𝐵) → (𝑋 𝑌) = (𝑋 + (𝐼𝑌)))

Proof of Theorem grpsubval
Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 oveq1 7416 . 2 (𝑥 = 𝑋 → (𝑥 + (𝐼𝑦)) = (𝑋 + (𝐼𝑦)))
2 fveq2 6892 . . 3 (𝑦 = 𝑌 → (𝐼𝑦) = (𝐼𝑌))
32oveq2d 7425 . 2 (𝑦 = 𝑌 → (𝑋 + (𝐼𝑦)) = (𝑋 + (𝐼𝑌)))
4 grpsubval.b . . 3 𝐵 = (Base‘𝐺)
5 grpsubval.p . . 3 + = (+g𝐺)
6 grpsubval.i . . 3 𝐼 = (invg𝐺)
7 grpsubval.m . . 3 = (-g𝐺)
84, 5, 6, 7grpsubfval 18868 . 2 = (𝑥𝐵, 𝑦𝐵 ↦ (𝑥 + (𝐼𝑦)))
9 ovex 7442 . 2 (𝑋 + (𝐼𝑌)) ∈ V
101, 3, 8, 9ovmpo 7568 1 ((𝑋𝐵𝑌𝐵) → (𝑋 𝑌) = (𝑋 + (𝐼𝑌)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397   = wceq 1542  wcel 2107  cfv 6544  (class class class)co 7409  Basecbs 17144  +gcplusg 17197  invgcminusg 18820  -gcsg 18821
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-sep 5300  ax-nul 5307  ax-pow 5364  ax-pr 5428  ax-un 7725
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-ral 3063  df-rex 3072  df-rab 3434  df-v 3477  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-iun 5000  df-br 5150  df-opab 5212  df-mpt 5233  df-id 5575  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-fv 6552  df-ov 7412  df-oprab 7413  df-mpo 7414  df-1st 7975  df-2nd 7976  df-sbg 18824
This theorem is referenced by:  grpsubinv  18896  grpsubrcan  18904  grpinvsub  18905  grpinvval2  18906  grpsubid  18907  grpsubid1  18908  grpsubeq0  18909  grpsubadd0sub  18910  grpsubadd  18911  grpsubsub  18912  grpaddsubass  18913  grpnpcan  18915  pwssub  18937  mulgsubdir  18994  subgsubcl  19017  subgsub  19018  issubg4  19025  qussub  19070  ghmsub  19100  sylow2blem1  19488  lsmelvalm  19519  ablsub2inv  19676  ablsub4  19678  ablsubsub4  19686  mulgsubdi  19697  eqgabl  19702  gsumsub  19816  dprdfsub  19891  ringsubdi  20119  ringsubdir  20120  abvsubtri  20443  lmodvsubval2  20527  lmodsubdir  20530  lspsntrim  20709  cnfldsub  20973  m2detleiblem7  22129  chpscmatgsumbin  22346  tgpconncomp  23617  tsmssub  23653  tsmsxplem1  23657  isngp4  24121  ngpsubcan  24123  ngptgp  24145  tngngp3  24173  clmpm1dir  24619  cphipval  24760  deg1suble  25625  deg1sub  25626  dchr2sum  26776  ogrpsub  32234  symgsubg  32248  cycpmconjv  32301  archiabllem2c  32341  linds2eq  32497  ressply1sub  32659  lflsub  37937  ldualvsubval  38027  lcdvsubval  40489  baerlem3lem1  40578  baerlem5alem1  40579  baerlem5amN  40587  baerlem5bmN  40588  baerlem5abmN  40589  hdmapsub  40718  nelsubgsubcld  41072  rngsubdi  46670  rngsubdir  46671
  Copyright terms: Public domain W3C validator